[mc] Get rid of the ugly "value" out parameter in MC_state_get_request()

diff --git a/src/mc/CommunicationDeterminismChecker.cpp b/src/mc/CommunicationDeterminismChecker.cpp
index 174b7e0..86b26cc 100644 (file)
--- a/src/mc/CommunicationDeterminismChecker.cpp
+++ b/src/mc/CommunicationDeterminismChecker.cpp
@@ -315,11 +315,10 @@ std::vector<std::string> CommunicationDeterminismChecker::getTextualTrace() // o
 {
   std::vector<std::string> trace;
   for (auto const& state : stack_) {
 {
   std::vector<std::string> trace;
   for (auto const& state : stack_) {

-    int value = state->req_num;

     smx_simcall_t req = &state->executed_req;
     if (req)
       trace.push_back(simgrid::mc::request_to_string(
     smx_simcall_t req = &state->executed_req;
     if (req)
       trace.push_back(simgrid::mc::request_to_string(

-        req, value, simgrid::mc::RequestType::executed));
+        req, state->req_num, simgrid::mc::RequestType::executed));

   }
   return trace;
 }
   }
   return trace;
 }


@@ -376,7 +375,6 @@ bool all_communications_are_finished()
 
 int CommunicationDeterminismChecker::main(void)
 {
 
 int CommunicationDeterminismChecker::main(void)
 {

-  int value;

   std::unique_ptr<simgrid::mc::VisitedState> visited_state = nullptr;
   smx_simcall_t req = nullptr;
 
   std::unique_ptr<simgrid::mc::VisitedState> visited_state = nullptr;
   smx_simcall_t req = nullptr;
 


@@ -394,16 +392,18 @@ int CommunicationDeterminismChecker::main(void)
     mc_stats->visited_states++;
 
     if (stack_.size() <= (std::size_t) _sg_mc_max_depth
     mc_stats->visited_states++;
 
     if (stack_.size() <= (std::size_t) _sg_mc_max_depth

-        && (req = MC_state_get_request(state, &value))
+        && (req = MC_state_get_request(state)) != nullptr

         && (visited_state == nullptr)) {
 
         && (visited_state == nullptr)) {
 

+      int req_num = state->req_num;
+

       XBT_DEBUG("Execute: %s",
         simgrid::mc::request_to_string(
       XBT_DEBUG("Execute: %s",
         simgrid::mc::request_to_string(

-          req, value, simgrid::mc::RequestType::simix).c_str());
+          req, req_num, simgrid::mc::RequestType::simix).c_str());

 
       std::string req_str;
       if (dot_output != nullptr)
 
       std::string req_str;
       if (dot_output != nullptr)

-        req_str = simgrid::mc::request_get_dot_output(req, value);
+        req_str = simgrid::mc::request_get_dot_output(req, req_num);

 
       mc_stats->executed_transitions++;
 
 
       mc_stats->executed_transitions++;
 


@@ -413,12 +413,12 @@ int CommunicationDeterminismChecker::main(void)
         call = MC_get_call_type(req);
 
       /* Answer the request */
         call = MC_get_call_type(req);
 
       /* Answer the request */

-      simgrid::mc::handle_simcall(req, value);    /* After this call req is no longer useful */
+      simgrid::mc::handle_simcall(req, req_num);    /* After this call req is no longer useful */

 
       if(!initial_global_state->initial_communications_pattern_done)
 
       if(!initial_global_state->initial_communications_pattern_done)

-        MC_handle_comm_pattern(call, req, value, initial_communications_pattern, 0);
+        MC_handle_comm_pattern(call, req, req_num, initial_communications_pattern, 0);

       else
       else

-        MC_handle_comm_pattern(call, req, value, nullptr, 0);
+        MC_handle_comm_pattern(call, req, req_num, nullptr, 0);

 
       /* Wait for requests (schedules processes) */
       mc_model_checker->wait_for_requests();
 
       /* Wait for requests (schedules processes) */
       mc_model_checker->wait_for_requests();

diff --git a/src/mc/LivenessChecker.cpp b/src/mc/LivenessChecker.cpp
index 80cffd3..61cf565 100644 (file)
--- a/src/mc/LivenessChecker.cpp
+++ b/src/mc/LivenessChecker.cpp
@@ -370,8 +370,8 @@ int LivenessChecker::main(void)
       continue;
     }
 
       continue;
     }
 

-    int value;
-    smx_simcall_t req = MC_state_get_request(current_pair->graph_state.get(), &value);
+    smx_simcall_t req = MC_state_get_request(current_pair->graph_state.get());
+    int req_num = current_pair->graph_state->req_num;

 
     if (dot_output != nullptr) {
       if (initial_global_state->prev_pair != 0 && initial_global_state->prev_pair != current_pair->num) {
 
     if (dot_output != nullptr) {
       if (initial_global_state->prev_pair != 0 && initial_global_state->prev_pair != current_pair->num) {


@@ -381,7 +381,7 @@ int LivenessChecker::main(void)
         initial_global_state->prev_req.clear();
       }
       initial_global_state->prev_pair = current_pair->num;
         initial_global_state->prev_req.clear();
       }
       initial_global_state->prev_pair = current_pair->num;

-      initial_global_state->prev_req = simgrid::mc::request_get_dot_output(req, value);
+      initial_global_state->prev_req = simgrid::mc::request_get_dot_output(req, req_num);

       if (current_pair->search_cycle)
         fprintf(dot_output, "%d [shape=doublecircle];\n", current_pair->num);
       fflush(dot_output);
       if (current_pair->search_cycle)
         fprintf(dot_output, "%d [shape=doublecircle];\n", current_pair->num);
       fflush(dot_output);


@@ -389,7 +389,7 @@ int LivenessChecker::main(void)
 
     XBT_DEBUG("Execute: %s",
       simgrid::mc::request_to_string(
 
     XBT_DEBUG("Execute: %s",
       simgrid::mc::request_to_string(

-        req, value, simgrid::mc::RequestType::simix).c_str());
+        req, req_num, simgrid::mc::RequestType::simix).c_str());

 
     /* Update mc_stats */
     mc_stats->executed_transitions++;
 
     /* Update mc_stats */
     mc_stats->executed_transitions++;


@@ -397,7 +397,7 @@ int LivenessChecker::main(void)
       mc_stats->visited_pairs++;
 
     /* Answer the request */
       mc_stats->visited_pairs++;
 
     /* Answer the request */

-    simgrid::mc::handle_simcall(req, value);
+    simgrid::mc::handle_simcall(req, req_num);

 
     /* Wait for requests (schedules processes) */
     mc_model_checker->wait_for_requests();
 
     /* Wait for requests (schedules processes) */
     mc_model_checker->wait_for_requests();

diff --git a/src/mc/SafetyChecker.cpp b/src/mc/SafetyChecker.cpp
index 664379d..8055c65 100644 (file)
--- a/src/mc/SafetyChecker.cpp
+++ b/src/mc/SafetyChecker.cpp
@@ -89,8 +89,6 @@ int SafetyChecker::run()
 {
   this->init();
 
 {
   this->init();
 

-  int value;
-

   while (!stack_.empty()) {
 
     /* Get current state */
   while (!stack_.empty()) {
 
     /* Get current state */


@@ -108,7 +106,7 @@ int SafetyChecker::run()
     // let's back-track.
     smx_simcall_t req = nullptr;
     if (stack_.size() > (std::size_t) _sg_mc_max_depth
     // let's back-track.
     smx_simcall_t req = nullptr;
     if (stack_.size() > (std::size_t) _sg_mc_max_depth

-        || (req = MC_state_get_request(state, &value)) == nullptr
+        || (req = MC_state_get_request(state)) == nullptr

         || visitedState_ != nullptr) {
       int res = this->backtrack();
       if (res)
         || visitedState_ != nullptr) {
       int res = this->backtrack();
       if (res)


@@ -117,23 +115,25 @@ int SafetyChecker::run()
         continue;
     }
 
         continue;
     }
 

+    int req_num = state->req_num;
+

     // If there are processes to interleave and the maximum depth has not been
     // reached then perform one step of the exploration algorithm.
     XBT_DEBUG("Execute: %s",
       simgrid::mc::request_to_string(
     // If there are processes to interleave and the maximum depth has not been
     // reached then perform one step of the exploration algorithm.
     XBT_DEBUG("Execute: %s",
       simgrid::mc::request_to_string(

-        req, value, simgrid::mc::RequestType::simix).c_str());
+        req, req_num, simgrid::mc::RequestType::simix).c_str());

 
     std::string req_str;
     if (dot_output != nullptr)
 
     std::string req_str;
     if (dot_output != nullptr)

-      req_str = simgrid::mc::request_get_dot_output(req, value);
+      req_str = simgrid::mc::request_get_dot_output(req, req_num);

 
     mc_stats->executed_transitions++;
 
     // TODO, bundle both operations in a single message
 
     mc_stats->executed_transitions++;
 
     // TODO, bundle both operations in a single message

-    //   MC_execute_transition(req, value)
+    //   MC_execute_transition(req, req_num)

 
     /* Answer the request */
 
     /* Answer the request */

-    simgrid::mc::handle_simcall(req, value);
+    simgrid::mc::handle_simcall(req, req_num);

     mc_model_checker->wait_for_requests();
 
     /* Create the new expanded state */
     mc_model_checker->wait_for_requests();
 
     /* Create the new expanded state */

diff --git a/src/mc/mc_state.cpp b/src/mc/mc_state.cpp
index 1a4b90a..a6f51d3 100644 (file)
--- a/src/mc/mc_state.cpp
+++ b/src/mc/mc_state.cpp
@@ -69,7 +69,7 @@ RecordTraceElement State::getRecordElement() const
 }
 
 static inline smx_simcall_t MC_state_get_request_for_process(
 }
 
 static inline smx_simcall_t MC_state_get_request_for_process(

-  simgrid::mc::State* state, int*value, smx_process_t process)
+  simgrid::mc::State* state, smx_process_t process)

 {
   simgrid::mc::ProcessState* procstate = &state->processStates[process->pid];
 
 {
   simgrid::mc::ProcessState* procstate = &state->processStates[process->pid];
 


@@ -81,13 +81,13 @@ static inline smx_simcall_t MC_state_get_request_for_process(
   smx_simcall_t req = nullptr;
   switch (process->simcall.call) {
       case SIMCALL_COMM_WAITANY:
   smx_simcall_t req = nullptr;
   switch (process->simcall.call) {
       case SIMCALL_COMM_WAITANY:

-        *value = -1;
+        state->req_num = -1;

         while (procstate->interleave_count <
               read_length(mc_model_checker->process(),
                 remote(simcall_comm_waitany__get__comms(&process->simcall)))) {
           if (simgrid::mc::request_is_enabled_by_idx(&process->simcall,
               procstate->interleave_count++)) {
         while (procstate->interleave_count <
               read_length(mc_model_checker->process(),
                 remote(simcall_comm_waitany__get__comms(&process->simcall)))) {
           if (simgrid::mc::request_is_enabled_by_idx(&process->simcall,
               procstate->interleave_count++)) {

-            *value = procstate->interleave_count - 1;
+            state->req_num = procstate->interleave_count - 1;

             break;
           }
         }
             break;
           }
         }


@@ -96,19 +96,19 @@ static inline smx_simcall_t MC_state_get_request_for_process(
             simgrid::mc::read_length(mc_model_checker->process(),
               simgrid::mc::remote(simcall_comm_waitany__get__comms(&process->simcall))))
           procstate->setDone();
             simgrid::mc::read_length(mc_model_checker->process(),
               simgrid::mc::remote(simcall_comm_waitany__get__comms(&process->simcall))))
           procstate->setDone();

-        if (*value != -1)
+        if (state->req_num != -1)

           req = &process->simcall;
         break;
 
       case SIMCALL_COMM_TESTANY: {
         unsigned start_count = procstate->interleave_count;
           req = &process->simcall;
         break;
 
       case SIMCALL_COMM_TESTANY: {
         unsigned start_count = procstate->interleave_count;

-        *value = -1;
+        state->req_num = -1;

         while (procstate->interleave_count <
                 read_length(mc_model_checker->process(),
                   remote(simcall_comm_testany__get__comms(&process->simcall))))
           if (simgrid::mc::request_is_enabled_by_idx(&process->simcall,
               procstate->interleave_count++)) {
         while (procstate->interleave_count <
                 read_length(mc_model_checker->process(),
                   remote(simcall_comm_testany__get__comms(&process->simcall))))
           if (simgrid::mc::request_is_enabled_by_idx(&process->simcall,
               procstate->interleave_count++)) {

-            *value = procstate->interleave_count - 1;
+            state->req_num = procstate->interleave_count - 1;

             break;
           }
 
             break;
           }
 


@@ -117,7 +117,7 @@ static inline smx_simcall_t MC_state_get_request_for_process(
               remote(simcall_comm_testany__get__comms(&process->simcall))))
           procstate->setDone();
 
               remote(simcall_comm_testany__get__comms(&process->simcall))))
           procstate->setDone();
 

-        if (*value != -1 || start_count == 0)
+        if (state->req_num != -1 || start_count == 0)

            req = &process->simcall;
 
         break;
            req = &process->simcall;
 
         break;


@@ -129,12 +129,12 @@ static inline smx_simcall_t MC_state_get_request_for_process(
         mc_model_checker->process().read_bytes(
           &act, sizeof(act), remote(remote_act));
         if (act.comm.src_proc && act.comm.dst_proc)
         mc_model_checker->process().read_bytes(
           &act, sizeof(act), remote(remote_act));
         if (act.comm.src_proc && act.comm.dst_proc)

-          *value = 0;
+          state->req_num = 0;

         else if (act.comm.src_proc == nullptr && act.comm.type == SIMIX_COMM_READY
               && act.comm.detached == 1)
         else if (act.comm.src_proc == nullptr && act.comm.type == SIMIX_COMM_READY
               && act.comm.detached == 1)

-          *value = 0;
+          state->req_num = 0;

         else
         else

-          *value = -1;
+          state->req_num = -1;

         procstate->setDone();
         req = &process->simcall;
         break;
         procstate->setDone();
         req = &process->simcall;
         break;


@@ -142,9 +142,9 @@ static inline smx_simcall_t MC_state_get_request_for_process(
 
       case SIMCALL_MC_RANDOM: {
         int min_value = simcall_mc_random__get__min(&process->simcall);
 
       case SIMCALL_MC_RANDOM: {
         int min_value = simcall_mc_random__get__min(&process->simcall);

-        *value = procstate->interleave_count + min_value;
+        state->req_num = procstate->interleave_count + min_value;

         procstate->interleave_count++;
         procstate->interleave_count++;

-        if (*value == simcall_mc_random__get__max(&process->simcall))
+        if (state->req_num == simcall_mc_random__get__max(&process->simcall))

           procstate->setDone();
         req = &process->simcall;
         break;
           procstate->setDone();
         req = &process->simcall;
         break;


@@ -152,7 +152,7 @@ static inline smx_simcall_t MC_state_get_request_for_process(
 
       default:
         procstate->setDone();
 
       default:
         procstate->setDone();

-        *value = 0;
+        state->req_num = 0;

         req = &process->simcall;
         break;
   }
         req = &process->simcall;
         break;
   }


@@ -162,7 +162,6 @@ static inline smx_simcall_t MC_state_get_request_for_process(
   // Fetch the data of the request and translate it:
 
   state->executed_req = *req;
   // Fetch the data of the request and translate it:
 
   state->executed_req = *req;

-  state->req_num = *value;

 
   /* The waitany and testany request are transformed into a wait or test request
    * over the corresponding communication action so it can be treated later by
 
   /* The waitany and testany request are transformed into a wait or test request
    * over the corresponding communication action so it can be treated later by


@@ -174,7 +173,7 @@ static inline smx_simcall_t MC_state_get_request_for_process(
     smx_synchro_t remote_comm;
     read_element(mc_model_checker->process(),
       &remote_comm, remote(simcall_comm_waitany__get__comms(req)),
     smx_synchro_t remote_comm;
     read_element(mc_model_checker->process(),
       &remote_comm, remote(simcall_comm_waitany__get__comms(req)),

-      *value, sizeof(remote_comm));
+      state->req_num, sizeof(remote_comm));

     mc_model_checker->process().read(&state->internal_comm, remote(remote_comm));
     simcall_comm_wait__set__comm(&state->internal_req, &state->internal_comm);
     simcall_comm_wait__set__timeout(&state->internal_req, 0);
     mc_model_checker->process().read(&state->internal_comm, remote(remote_comm));
     simcall_comm_wait__set__comm(&state->internal_req, &state->internal_comm);
     simcall_comm_wait__set__timeout(&state->internal_req, 0);


@@ -185,16 +184,16 @@ static inline smx_simcall_t MC_state_get_request_for_process(
     state->internal_req.call = SIMCALL_COMM_TEST;
     state->internal_req.issuer = req->issuer;
 
     state->internal_req.call = SIMCALL_COMM_TEST;
     state->internal_req.issuer = req->issuer;
 

-    if (*value > 0) {
+    if (state->req_num > 0) {

       smx_synchro_t remote_comm;
       read_element(mc_model_checker->process(),
         &remote_comm, remote(simcall_comm_testany__get__comms(req)),
       smx_synchro_t remote_comm;
       read_element(mc_model_checker->process(),
         &remote_comm, remote(simcall_comm_testany__get__comms(req)),

-        *value, sizeof(remote_comm));
+        state->req_num, sizeof(remote_comm));

       mc_model_checker->process().read(&state->internal_comm, remote(remote_comm));
     }
 
     simcall_comm_test__set__comm(&state->internal_req, &state->internal_comm);
       mc_model_checker->process().read(&state->internal_comm, remote(remote_comm));
     }
 
     simcall_comm_test__set__comm(&state->internal_req, &state->internal_comm);

-    simcall_comm_test__set__result(&state->internal_req, *value);
+    simcall_comm_test__set__result(&state->internal_req, state->req_num);

     break;
 
   case SIMCALL_COMM_WAIT:
     break;
 
   case SIMCALL_COMM_WAIT:


@@ -221,10 +220,10 @@ static inline smx_simcall_t MC_state_get_request_for_process(
   return req;
 }
 
   return req;
 }
 

-smx_simcall_t MC_state_get_request(simgrid::mc::State* state, int *value)
+smx_simcall_t MC_state_get_request(simgrid::mc::State* state)

 {
   for (auto& p : mc_model_checker->process().simix_processes()) {
 {
   for (auto& p : mc_model_checker->process().simix_processes()) {

-    smx_simcall_t res = MC_state_get_request_for_process(state, value, &p.copy);
+    smx_simcall_t res = MC_state_get_request_for_process(state, &p.copy);

     if (res)
       return res;
   }
     if (res)
       return res;
   }

diff --git a/src/mc/mc_state.h b/src/mc/mc_state.h
index 957a080..9681d03 100644 (file)
--- a/src/mc/mc_state.h
+++ b/src/mc/mc_state.h
@@ -166,6 +166,6 @@ XBT_PRIVATE void replay(std::list<std::unique_ptr<simgrid::mc::State>> const& st
 }
 
 XBT_PRIVATE simgrid::mc::State* MC_state_new(void);
 }
 
 XBT_PRIVATE simgrid::mc::State* MC_state_new(void);

-XBT_PRIVATE smx_simcall_t MC_state_get_request(simgrid::mc::State* state, int *value);
+XBT_PRIVATE smx_simcall_t MC_state_get_request(simgrid::mc::State* state);

 
 #endif
 
 #endif