Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker : DPOR (independant transitions) algorithm for liveness properties
authorMarion Guthmuller <marion.guthmuller@loria.fr>
Tue, 5 Jul 2011 09:16:08 +0000 (11:16 +0200)
committerMarion Guthmuller <marion.guthmuller@loria.fr>
Tue, 25 Oct 2011 11:36:56 +0000 (13:36 +0200)
examples/msg/mc/example_automaton.c
src/mc/mc_dpor.c
src/mc/mc_global.c
src/mc/mc_liveness.c
src/mc/private.h

index a5094ad..62fc3cf 100644 (file)
@@ -16,7 +16,7 @@ extern xbt_automaton_t automaton;
 int p=1;
 int r=0;
 int q=1;
 int p=1;
 int r=0;
 int q=1;
-int e=0;
+int e=1;
 int d=1;
 
 
 int d=1;
 
 
@@ -55,8 +55,7 @@ int server(int argc, char *argv[])
     }
     MSG_task_receive(&task, "mymailbox");
     count++;
     }
     MSG_task_receive(&task, "mymailbox");
     count++;
-    //e=(e+1)%2;
-    //d=(d+1)%2;
+    //r=(r+1)%2;
     //XBT_INFO("r (server) = %d", r);
      
   }
     //XBT_INFO("r (server) = %d", r);
      
   }
index 9378ddd..267e610 100644 (file)
@@ -342,3 +342,249 @@ void MC_dpor_with_restore_snapshot(){
   return;
 }
 
   return;
 }
 
+
+
+/************ DPOR 2 (invisible and independant transitions) ************/
+
+
+void MC_dpor2_init(xbt_automaton_t a)
+{
+  mc_pair_t initial_pair = NULL;
+  mc_state_t initial_graph_state = NULL;
+  mc_snapshot_t initial_system_state = NULL;
+  xbt_state_t initial_automaton_state = NULL;
+  smx_process_t process;
+  
+
+  MC_SET_RAW_MEM;
+  initial_graph_state = MC_state_new();
+  MC_UNSET_RAW_MEM;
+
+  /* Wait for requests (schedules processes) */
+  MC_wait_for_requests();
+
+  MC_SET_RAW_MEM;
+  xbt_swag_foreach(process, simix_global->process_list){
+    if(MC_process_is_enabled(process)){
+      MC_state_interleave_process(initial_graph_state, process);
+      break;
+    }
+  }
+  MC_UNSET_RAW_MEM;
+
+  unsigned int cursor = 0;
+  unsigned int cursor2 = 0;
+  xbt_state_t automaton_state = NULL;
+  int res;
+  xbt_transition_t transition_succ;
+
+  xbt_dynar_foreach(a->states, cursor, automaton_state){
+    if(automaton_state->type == -1){
+      xbt_dynar_foreach(automaton_state->out, cursor2, transition_succ){
+       res = MC_automaton_evaluate_label(a, transition_succ->label);
+       if((res == 1) || (res == 2)){
+         initial_automaton_state = transition_succ->dst;
+         break;
+       }
+      }
+    }
+
+    if(xbt_fifo_size(mc_snapshot_stack) > 0)
+      break;
+  }
+
+  if(xbt_fifo_size(mc_snapshot_stack) == 0){
+    cursor = 0;
+    xbt_dynar_foreach(a->states, cursor, automaton_state){
+      if(automaton_state->type == -1){
+       initial_automaton_state = automaton_state;
+       break;
+      }
+    }
+  }
+
+  MC_SET_RAW_MEM;
+  initial_system_state = xbt_new0(s_mc_snapshot_t, 1);
+  MC_take_snapshot(initial_system_state);
+  initial_pair = new_pair(initial_system_state, initial_graph_state, initial_automaton_state);
+  xbt_fifo_unshift(mc_snapshot_stack, initial_pair);
+  MC_UNSET_RAW_MEM;
+
+  XBT_DEBUG("**************************************************");
+  XBT_DEBUG("Initial pair");
+
+  MC_dpor2(a, 0);
+    
+}
+
+
+void MC_dpor2(xbt_automaton_t a, int search_cycle)
+{
+  char *req_str;
+  int value;
+  smx_req_t req = NULL, prev_req = NULL;
+  mc_state_t next_graph_state = NULL;
+  mc_snapshot_t next_system_state = NULL;
+  xbt_state_t next_automaton_state = NULL;
+  xbt_transition_t transition_succ;
+  unsigned int cursor;
+  int res;
+  mc_pair_t pair = NULL, next_pair = NULL, prev_pair = NULL;
+  smx_process_t process = NULL;
+  xbt_fifo_item_t item = NULL;
+
+  while (xbt_fifo_size(mc_snapshot_stack) > 0) {
+
+    /* Get current pair */
+    pair = (mc_pair_t) 
+      xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack));
+
+    XBT_DEBUG("**************************************************");
+    XBT_DEBUG("Exploration depth=%d (pair=%p)(%u interleave)",
+           xbt_fifo_size(mc_snapshot_stack), pair,
+           MC_state_interleave_size(pair->graph_state));
+
+    /* Update statistics */
+    mc_stats_pair->visited_pairs++;
+
+    /* Test acceptance pair and acceptance cycle*/
+
+    if(pair->automaton_state->type == 1){
+      if(search_cycle == 0){
+       set_pair_reached(pair);
+       XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", pair->graph_state, pair->automaton_state, pair->automaton_state->id);
+      }else{
+       if(reached(pair) == 1){
+         XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
+         XBT_INFO("|             ACCEPTANCE CYCLE            |");
+         XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
+         XBT_INFO("Counter-example that violates formula :");
+         MC_show_snapshot_stack(mc_snapshot_stack);
+         MC_dump_snapshot_stack(mc_snapshot_stack);
+         MC_print_statistics_pairs(mc_stats_pair);
+         exit(0);
+       }
+      }
+    }
+
+    /* If there are processes to interleave and the maximum depth has not been reached
+       then perform one step of the exploration algorithm */
+    if (xbt_fifo_size(mc_snapshot_stack) < MAX_DEPTH &&
+        (req = MC_state_get_request(pair->graph_state, &value))) {
+
+      /* Debug information */
+      if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
+        req_str = MC_request_to_string(req, value);
+        XBT_DEBUG("Execute: %s", req_str);
+        xbt_free(req_str);
+      }
+
+      MC_state_set_executed_request(pair->graph_state, req, value);
+      //mc_stats_pairs->executed_transitions++;
+
+      /* Answer the request */
+      SIMIX_request_pre(req, value); /* After this call req is no longer usefull */
+
+      /* Wait for requests (schedules processes) */
+      MC_wait_for_requests();
+
+      /* Create the new expanded state */
+      MC_SET_RAW_MEM;
+      next_graph_state = MC_state_new();
+
+      /* Get an enabled process and insert it in the interleave set of the next state */
+      xbt_swag_foreach(process, simix_global->process_list){
+        if(MC_process_is_enabled(process)){
+          MC_state_interleave_process(next_graph_state, process);
+          break;
+        }
+      }
+
+      next_system_state = xbt_new0(s_mc_snapshot_t, 1);
+      MC_take_snapshot(next_system_state);
+      MC_UNSET_RAW_MEM;
+
+      cursor = 0;
+      xbt_dynar_foreach(pair->automaton_state->out, cursor, transition_succ){
+       res = MC_automaton_evaluate_label(a, transition_succ->label);   
+       if((res == 1) || (res == 2)){ // enabled transition in automaton
+         next_automaton_state = transition_succ->dst;
+         break;
+       }
+      }
+
+      if(next_automaton_state == NULL){
+       next_automaton_state = pair->automaton_state;
+      }
+      
+      MC_SET_RAW_MEM;
+      next_pair = new_pair(next_system_state, next_graph_state, next_automaton_state);
+      xbt_fifo_unshift(mc_snapshot_stack, next_pair);
+      MC_UNSET_RAW_MEM;
+
+      /* Let's loop again */
+
+      /* The interleave set is empty or the maximum depth is reached, let's back-track */
+    } else {
+      XBT_DEBUG("There are no more processes to interleave.");
+
+      /* Trash the current state, no longer needed */
+      MC_SET_RAW_MEM;
+      xbt_fifo_shift(mc_snapshot_stack);
+      //MC_state_delete(state);
+      MC_UNSET_RAW_MEM;
+
+      /* Check for deadlocks */
+      if(MC_deadlock_check()){
+        MC_show_deadlock(NULL);
+        return;
+      }
+
+      MC_SET_RAW_MEM;
+      /* 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 
+         (from it's predecesor state), depends on any other previous request 
+         executed before it. If it does then add it to the interleave set of the
+         state that executed that previous request. */
+      while ((pair = xbt_fifo_shift(mc_snapshot_stack)) != NULL) {
+        req = MC_state_get_internal_request(pair->graph_state);
+        xbt_fifo_foreach(mc_snapshot_stack, item, prev_pair, mc_pair_t) {
+          if(MC_request_depend(req, MC_state_get_internal_request(prev_pair->graph_state))){
+            if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
+              XBT_DEBUG("Dependent Transitions:");
+              prev_req = MC_state_get_executed_request(prev_pair->graph_state, &value);
+              req_str = MC_request_to_string(prev_req, value);
+              XBT_DEBUG("%s (pair=%p)", req_str, prev_pair);
+              xbt_free(req_str);
+              prev_req = MC_state_get_executed_request(pair->graph_state, &value);
+              req_str = MC_request_to_string(prev_req, value);
+              XBT_DEBUG("%s (pair=%p)", req_str, pair);
+              xbt_free(req_str);              
+            }
+
+            if(!MC_state_process_is_done(prev_pair->graph_state, req->issuer))
+              MC_state_interleave_process(prev_pair->graph_state, req->issuer);
+            else
+              XBT_DEBUG("Process %p is in done set", req->issuer);
+
+            break;
+          }
+        }
+        if (MC_state_interleave_size(pair->graph_state)) {
+          /* We found a back-tracking point, let's loop */
+         MC_restore_snapshot(pair->system_state);
+          xbt_fifo_unshift(mc_snapshot_stack, pair);
+          XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_snapshot_stack));
+          MC_UNSET_RAW_MEM;
+          break;
+        } else {
+          //MC_state_delete(state);
+        }
+      }
+      MC_UNSET_RAW_MEM;
+    }
+  }
+  MC_UNSET_RAW_MEM;
+  return;
+}
index 492d9e4..839c96b 100644 (file)
@@ -67,6 +67,7 @@ void MC_init_with_automaton(xbt_automaton_t a){
 
   /* Initialize statistics */
   mc_stats_pair = xbt_new0(s_mc_stats_pair_t, 1);
 
   /* Initialize statistics */
   mc_stats_pair = xbt_new0(s_mc_stats_pair_t, 1);
+  mc_stats = xbt_new0(s_mc_stats_t, 1);
   //mc_stats_pair->pair_size = 1;
 
   XBT_DEBUG("Creating snapshot_stack");
   //mc_stats_pair->pair_size = 1;
 
   XBT_DEBUG("Creating snapshot_stack");
@@ -77,7 +78,8 @@ void MC_init_with_automaton(xbt_automaton_t a){
   MC_UNSET_RAW_MEM;
 
   //MC_vddfs_with_restore_snapshot_init(a);
   MC_UNSET_RAW_MEM;
 
   //MC_vddfs_with_restore_snapshot_init(a);
-  MC_ddfs_with_restore_snapshot_init(a);
+  //MC_ddfs_with_restore_snapshot_init(a);
+  MC_dpor2_init(a);
 }
 
 
 }
 
 
index f28b56f..9b92e21 100644 (file)
@@ -455,6 +455,7 @@ void MC_vddfs_with_restore_snapshot(xbt_automaton_t a, int search_cycle, int res
 
 /********************* Double-DFS without visited state *******************/
 
 
 /********************* Double-DFS without visited state *******************/
 
+
 void MC_ddfs_with_restore_snapshot_init(xbt_automaton_t a){
 
   XBT_DEBUG("**************************************************");
 void MC_ddfs_with_restore_snapshot_init(xbt_automaton_t a){
 
   XBT_DEBUG("**************************************************");
@@ -720,3 +721,4 @@ void MC_ddfs_with_restore_snapshot(xbt_automaton_t a, int search_cycle, int rest
   MC_UNSET_RAW_MEM;
 
 }
   MC_UNSET_RAW_MEM;
 
 }
+
index 02c10df..fc931b6 100644 (file)
@@ -220,7 +220,7 @@ void set_pair_visited(mc_pair_t p, int search_cycle);
 int visited(mc_pair_t p, int search_cycle);
 
 
 int visited(mc_pair_t p, int search_cycle);
 
 
-/* **** DPOR with restore snapshot **** */
+/* **** DPOR Cristian with restore snapshot **** */
 
 typedef struct s_mc_state_with_snapshot{
   mc_snapshot_t system_state;
 
 typedef struct s_mc_state_with_snapshot{
   mc_snapshot_t system_state;
@@ -231,4 +231,10 @@ mc_state_ws_t new_state_ws(mc_snapshot_t s, mc_state_t gs);
 void MC_dpor_with_restore_snapshot_init(void);
 void MC_dpor_with_restore_snapshot(void);
 
 void MC_dpor_with_restore_snapshot_init(void);
 void MC_dpor_with_restore_snapshot(void);
 
+/* **** DPOR 2 (invisible and independant transitions) **** */
+
+
+void MC_dpor2_init(xbt_automaton_t a);
+void MC_dpor2(xbt_automaton_t a, int search_cycle);
+
 #endif
 #endif