Improve independence detection and request pretty printing.

[simgrid.git] / src / mc / mc_dpor.c

diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c
index 1970b9c..b16f19f 100644 (file)
--- a/src/mc/mc_dpor.c
+++ b/src/mc/mc_dpor.c
@@ -32,8 +32,8 @@ void MC_dpor_init()
   MC_SET_RAW_MEM;
   /* Get an enabled process and insert it in the interleave set of the initial state */
   xbt_swag_foreach(process, simix_global->process_list){
   MC_SET_RAW_MEM;
   /* Get an enabled process and insert it in the interleave set of the initial state */
   xbt_swag_foreach(process, simix_global->process_list){

-    if(SIMIX_process_is_enabled(process)){
-      MC_state_add_to_interleave(initial_state, process);
+    if(MC_process_is_enabled(process)){
+      MC_state_interleave_process(initial_state, process);

       break;
     }
   }
       break;
     }
   }


@@ -52,8 +52,8 @@ void MC_dpor_init()
 void MC_dpor(void)
 {
   char *req_str;
 void MC_dpor(void)
 {
   char *req_str;

-  char value;
-  smx_req_t req = NULL;
+  int value;
+  smx_req_t req = NULL, prev_req = NULL;

   mc_state_t state = NULL, prev_state = NULL, next_state = NULL;
   smx_process_t process = NULL;
   xbt_fifo_item_t item = NULL;
   mc_state_t state = NULL, prev_state = NULL, next_state = NULL;
   smx_process_t process = NULL;
   xbt_fifo_item_t item = NULL;


@@ -79,16 +79,21 @@ void MC_dpor(void)
 
       /* Debug information */
       if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 
       /* Debug information */
       if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){

-        req_str = MC_request_to_string(req);
-        DEBUG1("Execute: %s", req_str);
+        req_str = MC_request_to_string(req, value);
+        if(req->call == REQ_COMM_WAITANY)
+          DEBUG3("Execute: %s (%u of %lu)", req_str, value, xbt_dynar_length(req->comm_waitany.comms));
+        else if(req->call == REQ_COMM_TESTANY)
+          DEBUG3("Execute: %s (%u of %lu)", req_str, value, xbt_dynar_length(req->comm_testany.comms));
+        else
+          DEBUG1("Execute: %s", req_str);

         xbt_free(req_str);
       }
 
         xbt_free(req_str);
       }
 

-      MC_state_set_executed_request(state, req);
+      MC_state_set_executed_request(state, req, value);

       mc_stats->executed_transitions++;
 
       /* Answer the request */
       mc_stats->executed_transitions++;
 
       /* Answer the request */

-      SIMIX_request_pre(req); /* After this call req is no longer usefull */
+      SIMIX_request_pre(req, value); /* After this call req is no longer usefull */

 
       /* Wait for requests (schedules processes) */
       MC_wait_for_requests();
 
       /* Wait for requests (schedules processes) */
       MC_wait_for_requests();


@@ -98,11 +103,10 @@ void MC_dpor(void)
       next_state = MC_state_new();
       xbt_fifo_unshift(mc_stack, next_state);
 
       next_state = MC_state_new();
       xbt_fifo_unshift(mc_stack, next_state);
 

-

       /* Get an enabled process and insert it in the interleave set of the next state */
       xbt_swag_foreach(process, simix_global->process_list){
       /* Get an enabled process and insert it in the interleave set of the next state */
       xbt_swag_foreach(process, simix_global->process_list){

-        if(SIMIX_process_is_enabled(process)){
-          MC_state_add_to_interleave(next_state, process);
+        if(MC_process_is_enabled(process)){
+          MC_state_interleave_process(next_state, process);

           break;
         }
       }
           break;
         }
       }


@@ -118,17 +122,19 @@ void MC_dpor(void)
     } else {
       DEBUG0("There are no more processes to interleave.");
 
     } else {
       DEBUG0("There are no more processes to interleave.");
 

+      /* Trash the current state, no longer needed */
+      MC_SET_RAW_MEM;
+      xbt_fifo_shift(mc_stack);
+      MC_state_delete(state);
+      MC_UNSET_RAW_MEM;
+

       /* Check for deadlocks */
       if(MC_deadlock_check()){
       /* Check for deadlocks */
       if(MC_deadlock_check()){

-        MC_show_deadlock(&process->request);
+        MC_show_deadlock(NULL);

         return;
       }
 
         return;
       }
 

-      /* Trash the current state, no longer needed */

       MC_SET_RAW_MEM;
       MC_SET_RAW_MEM;

-      xbt_fifo_shift(mc_stack);
-      MC_state_delete(state);
-

       /* Traverse the stack backwards until a state with a non empty interleave
          set is found, deleting all the states that have it empty in the way.
          For each deleted state, check if the request that has generated it 
       /* Traverse the stack backwards until a state with a non empty interleave
          set is found, deleting all the states that have it empty in the way.
          For each deleted state, check if the request that has generated it 


@@ -136,21 +142,23 @@ void MC_dpor(void)
          executed before it. If it does then add it to the interleave set of the
          state that executed that previous request. */
       while ((state = xbt_fifo_shift(mc_stack)) != NULL) {
          executed before it. If it does then add it to the interleave set of the
          state that executed that previous request. */
       while ((state = xbt_fifo_shift(mc_stack)) != NULL) {

-        req = MC_state_get_executed_request(state);
+        req = MC_state_get_internal_request(state);

         xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
         xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {

-          if(MC_request_depend(req, MC_state_get_executed_request(prev_state))){
+          if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){

             if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
               DEBUG0("Dependent Transitions:");
             if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
               DEBUG0("Dependent Transitions:");

-              req_str = MC_request_to_string(MC_state_get_executed_request(prev_state));
+              prev_req = MC_state_get_executed_request(prev_state, &value);
+              req_str = MC_request_to_string(prev_req, value);

               DEBUG2("%s (state=%p)", req_str, prev_state);
               xbt_free(req_str);
               DEBUG2("%s (state=%p)", req_str, prev_state);
               xbt_free(req_str);

-              req_str = MC_request_to_string(req);
+              prev_req = MC_state_get_executed_request(state, &value);
+              req_str = MC_request_to_string(prev_req, value);

               DEBUG2("%s (state=%p)", req_str, state);
               xbt_free(req_str);              
             }
 
             if(!MC_state_process_is_done(prev_state, req->issuer))
               DEBUG2("%s (state=%p)", req_str, state);
               xbt_free(req_str);              
             }
 
             if(!MC_state_process_is_done(prev_state, req->issuer))

-              MC_state_add_to_interleave(prev_state, req->issuer);
+              MC_state_interleave_process(prev_state, req->issuer);

             else
               DEBUG1("Process %p is in done set", req->issuer);
 
             else
               DEBUG1("Process %p is in done set", req->issuer);