Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker : new example bugged1 for stateful dpor
authorMarion Guthmuller <marion.guthmuller@loria.fr>
Tue, 16 Aug 2011 14:01:23 +0000 (16:01 +0200)
committerMarion Guthmuller <marion.guthmuller@loria.fr>
Tue, 25 Oct 2011 11:36:57 +0000 (13:36 +0200)
examples/msg/mc/CMakeLists.txt
examples/msg/mc/bugged1_stateful.c [new file with mode: 0644]
examples/msg/mc/example_automaton.c
include/mc/modelchecker.h
include/msg/msg.h
src/include/mc/mc.h
src/mc/mc_dpor.c
src/mc/mc_global.c
src/mc/private.h
src/msg/global.c

index 4b36391..f1daa84 100644 (file)
@@ -4,6 +4,7 @@ set(EXECUTABLE_OUTPUT_PATH "${CMAKE_CURRENT_BINARY_DIR}")
 
 add_executable(centralized centralized_mutex.c)
 add_executable(bugged1     bugged1.c)
+add_executable(bugged1_stateful bugged1_stateful.c)
 add_executable(bugged2     bugged2.c)
 add_executable(bugged3    bugged3.c)
 add_executable(random_test random_test.c)
@@ -11,6 +12,7 @@ add_executable(example_automaton automaton.c automatonparse_promela.c example_au
 
 target_link_libraries(centralized simgrid m )
 target_link_libraries(bugged1     simgrid m )
+target_link_libraries(bugged1_stateful simgrid m)
 target_link_libraries(bugged2     simgrid m )
 target_link_libraries(bugged3     simgrid m )
 target_link_libraries(random_test     simgrid m )
diff --git a/examples/msg/mc/bugged1_stateful.c b/examples/msg/mc/bugged1_stateful.c
new file mode 100644 (file)
index 0000000..d76edba
--- /dev/null
@@ -0,0 +1,65 @@
+/******************** Non-deterministic message ordering  *********************/
+/* Server assumes a fixed order in the reception of messages from its clients */
+/* which is incorrect because the message ordering is non-deterministic       */
+/******************************************************************************/
+
+#include <msg/msg.h>
+#include <mc/modelchecker.h>
+#define N 3
+
+XBT_LOG_NEW_DEFAULT_CATEGORY(example, "this example");
+
+int server(int argc, char *argv[]);
+int client(int argc, char *argv[]);
+
+int server(int argc, char *argv[])
+{
+  m_task_t task = NULL;
+  int count = 0;
+  while (count < N) {
+    if (task) {
+      MSG_task_destroy(task);
+      task = NULL;
+    }
+    MSG_task_receive(&task, "mymailbox");
+    count++;
+  }
+  MC_assert_stateful(atoi(MSG_task_get_name(task)) == 3);
+
+  XBT_INFO("OK");
+  return 0;
+}
+
+int client(int argc, char *argv[])
+{
+
+  m_task_t task =
+      MSG_task_create(argv[1], 0 /*comp cost */ , 10000 /*comm size */ ,
+                      NULL /*arbitrary data */ );
+
+  MSG_task_send(task, "mymailbox");
+
+  XBT_INFO("Sent!");
+  return 0;
+}
+
+int main(int argc, char *argv[])
+{
+
+  MSG_global_init(&argc, argv);
+
+  MSG_create_environment("platform.xml");
+
+  MSG_function_register("server", server);
+
+  MSG_function_register("client", client);
+
+  MSG_launch_application("deploy_bugged1.xml");
+
+  MSG_main_stateful();
+
+  MSG_clean();
+
+  return 0;
+
+}
index e3849e6..62fc3cf 100644 (file)
@@ -14,7 +14,7 @@ extern xbt_automaton_t automaton;
 
 
 int p=1;
-int r=1;
+int r=0;
 int q=1;
 int e=1;
 int d=1;
index dd65adb..5b1c813 100644 (file)
@@ -1,5 +1,6 @@
 #include "xbt.h"
 
 XBT_PUBLIC(void) MC_assert(int);
+XBT_PUBLIC(void) MC_assert_stateful(int);
 XBT_PUBLIC(void) MC_assert_pair(int);
 XBT_PUBLIC(int) MC_random(int min, int max);
index 89350f1..77b9778 100644 (file)
@@ -22,6 +22,7 @@ XBT_PUBLIC(void) MSG_global_init_args(int *argc, char **argv);
 XBT_PUBLIC(MSG_error_t) MSG_set_channel_number(int number);
 XBT_PUBLIC(int) MSG_get_channel_number(void);
 XBT_PUBLIC(MSG_error_t) MSG_main(void);
+XBT_PUBLIC(MSG_error_t) MSG_main_stateful(void);
 XBT_PUBLIC(MSG_error_t) MSG_main_with_automaton(xbt_automaton_t a);
 XBT_PUBLIC(MSG_error_t) MSG_clean(void);
 XBT_PUBLIC(void) MSG_function_register(const char *name,
index 06cc3eb..7820146 100644 (file)
@@ -29,11 +29,14 @@ SG_BEGIN_DECL()
 
 /********************************* Global *************************************/
 XBT_PUBLIC(void) MC_init(void);
+XBT_PUBLIC(void) MC_init_stateful(void);
 XBT_PUBLIC(void) MC_init_with_automaton(xbt_automaton_t a);
 XBT_PUBLIC(void) MC_exit(void);
 XBT_PUBLIC(void) MC_assert(int);
+XBT_PUBLIC(void) MC_assert_stateful(int);
 XBT_PUBLIC(void) MC_assert_pair(int);
 XBT_PUBLIC(void) MC_modelcheck(void);
+XBT_PUBLIC(void) MC_modelcheck_stateful(void);
 XBT_PUBLIC(void) MC_modelcheck_with_automaton(xbt_automaton_t a);
 XBT_PUBLIC(int) MC_random(int, int);
 XBT_PUBLIC(void) MC_process_clock_add(smx_process_t, double);
index 8cf6361..e51d986 100644 (file)
@@ -189,10 +189,10 @@ mc_state_ws_t new_state_ws(mc_snapshot_t s, mc_state_t gs){
   return sws;
 }
 
-void MC_dpor_with_restore_snapshot_init(){
+void MC_dpor_stateful_init(){
 
   XBT_DEBUG("**************************************************");
-  XBT_DEBUG("DPOR (with restore snapshot) init");
+  XBT_DEBUG("DPOR (stateful) init");
   XBT_DEBUG("**************************************************");
 
   mc_state_t initial_graph_state;
@@ -220,12 +220,10 @@ void MC_dpor_with_restore_snapshot_init(){
   xbt_fifo_unshift(mc_snapshot_stack, initial_state);
 
   MC_UNSET_RAW_MEM;
-         
-  MC_dpor_with_restore_snapshot();
 
 }
 
-void MC_dpor_with_restore_snapshot(){
+void MC_dpor_stateful(){
 
   smx_process_t process = NULL;
   
@@ -250,6 +248,8 @@ void MC_dpor_with_restore_snapshot(){
     
     XBT_DEBUG("**************************************************");
     XBT_DEBUG("Depth : %d, State : %p , %u interleave", xbt_fifo_size(mc_snapshot_stack),current_state, MC_state_interleave_size(current_state->graph_state));
+
+    mc_stats->visited_states++;
     
 
     if((xbt_fifo_size(mc_snapshot_stack) < MAX_DEPTH) && (req = MC_state_get_request(current_state->graph_state, &value))){
@@ -262,7 +262,8 @@ void MC_dpor_with_restore_snapshot(){
       }
 
       MC_state_set_executed_request(current_state->graph_state, req, value);
-
+      mc_stats->executed_transitions++;
+      
       /* Answer the request */
       SIMIX_request_pre(req, value);
       
@@ -298,6 +299,13 @@ void MC_dpor_with_restore_snapshot(){
       xbt_fifo_shift(mc_snapshot_stack);
       MC_UNSET_RAW_MEM;
 
+      /* Check for deadlocks */
+      if(MC_deadlock_check()){
+        MC_show_deadlock_stateful(NULL);
+        return;
+      }
+
+      MC_SET_RAW_MEM;
       while((current_state = xbt_fifo_shift(mc_snapshot_stack)) != NULL){
        req = MC_state_get_internal_request(current_state->graph_state);
        xbt_fifo_foreach(mc_snapshot_stack, item, prev_state, mc_state_ws_t) {
@@ -535,9 +543,9 @@ void MC_dpor2(xbt_automaton_t a, int search_cycle)
        }
       }
 
-      XBT_DEBUG("Enabled processes before pop : %lu", xbt_dynar_length(enabled_processes));
+      //XBT_DEBUG("Enabled processes before pop : %lu", xbt_dynar_length(enabled_processes));
     
-      XBT_DEBUG("Processes already interleaved : %d", pair->interleave);
+      //XBT_DEBUG("Processes already interleaved : %d", pair->interleave);
     
       if(xbt_dynar_length(enabled_processes) > 0){
        for(d=0;d<pair->interleave;d++){
@@ -545,7 +553,7 @@ void MC_dpor2(xbt_automaton_t a, int search_cycle)
        }
       }
 
-      XBT_DEBUG("Enabled processes after pop : %lu", xbt_dynar_length(enabled_processes));
+      //XBT_DEBUG("Enabled processes after pop : %lu", xbt_dynar_length(enabled_processes));
     
       if(pair->fully_expanded == 0){
        if(xbt_dynar_length(enabled_processes) > 0){
@@ -736,3 +744,429 @@ void MC_dpor2(xbt_automaton_t a, int search_cycle)
   MC_UNSET_RAW_MEM;
   return;
 }
+
+/************ DPOR 3 (invisible and independant transitions with coloration of pairs) ************/
+
+int expanded;
+xbt_dynar_t reached_pairs_prop_col;
+xbt_dynar_t visited_pairs_prop_col;
+
+
+
+mc_pair_prop_col_t new_pair_prop_col(mc_snapshot_t sn, mc_state_t sg, xbt_state_t st){
+  
+  mc_pair_prop_col_t pair = NULL;
+  pair = xbt_new0(s_mc_pair_prop_col_t, 1);
+  pair->system_state = sn;
+  pair->automaton_state = st;
+  pair->graph_state = sg;
+  pair->propositions = xbt_dynar_new(sizeof(mc_prop_ato_t), NULL);
+  pair->fully_expanded = 0;
+  pair->interleave = 0;
+  pair->color=ORANGE;
+  mc_stats_pair->expanded_pairs++;
+  //XBT_DEBUG("New pair %p : automaton=%p", pair, st);
+  return pair;
+}
+
+void set_expanded(mc_pair_prop_col_t pair){
+  pair->expanded = expanded;
+}
+
+int reached_prop_col(mc_pair_prop_col_t pair){
+
+  char* hash_reached = malloc(sizeof(char)*160);
+  unsigned int c= 0;
+
+  MC_SET_RAW_MEM;
+  char *hash = malloc(sizeof(char)*160);
+  xbt_sha((char *)&pair, hash);
+  xbt_dynar_foreach(reached_pairs_prop_col, c, hash_reached){
+    if(strcmp(hash, hash_reached) == 0){
+      MC_UNSET_RAW_MEM;
+      return 1;
+    }
+  }
+  
+  MC_UNSET_RAW_MEM;
+  return 0;
+}
+
+void set_pair_prop_col_reached(mc_pair_prop_col_t pair){
+
+  if(reached_prop_col(pair) == 0){
+    MC_SET_RAW_MEM;
+    char *hash = malloc(sizeof(char)*160) ;
+    xbt_sha((char *)&pair, hash);
+    xbt_dynar_push(reached_pairs_prop_col, &hash); 
+    MC_UNSET_RAW_MEM;
+  }
+
+}
+
+int invisible_col(mc_pair_prop_col_t p, mc_pair_prop_col_t np){
+  mc_prop_ato_t prop1;
+  mc_prop_ato_t prop2;
+  int i;
+  for(i=0;i<xbt_dynar_length(p->propositions); i++){
+    prop1 = xbt_dynar_get_as(p->propositions, i, mc_prop_ato_t);
+    prop2 = xbt_dynar_get_as(np->propositions, i, mc_prop_ato_t);
+    //XBT_DEBUG("test invisible : prop 1 = %s : %d / prop 2 = %s : %d", prop1->id, prop1->value, prop2->id, prop2->value);
+    if(prop1->value != prop2->value)
+         return 0;
+  }
+  return 1; 
+
+}
+
+void set_fully_expanded_col(mc_pair_prop_col_t pair){
+  pair->fully_expanded = 1;
+  pair->color = GREEN;
+}
+
+void set_pair_prop_col_visited(mc_pair_prop_col_t pair, int sc){
+
+  MC_SET_RAW_MEM;
+  mc_visited_pair_prop_col_t p = NULL;
+  p = xbt_new0(s_mc_visited_pair_prop_col_t, 1);
+  p->pair = pair;
+  p->search_cycle = sc;
+  char *hash = malloc(sizeof(char)*160);
+  xbt_sha((char *)&p, hash);
+  xbt_dynar_push(visited_pairs_prop_col, &hash); 
+  MC_UNSET_RAW_MEM;    
+
+}
+
+int visited_pair_prop_col(mc_pair_prop_col_t pair, int sc){
+
+  char* hash_visited = malloc(sizeof(char)*160);
+  unsigned int c= 0;
+
+  MC_SET_RAW_MEM;
+  mc_visited_pair_prop_col_t p = NULL;
+  p = xbt_new0(s_mc_visited_pair_prop_col_t, 1);
+  p->pair = pair;
+  p->search_cycle = sc;
+  char *hash = malloc(sizeof(char)*160);
+  xbt_sha((char *)&p, hash);
+  xbt_dynar_foreach(visited_pairs_prop_col, c, hash_visited){
+    if(strcmp(hash, hash_visited) == 0){
+      MC_UNSET_RAW_MEM;
+      return 1;
+    }
+  }
+  
+  MC_UNSET_RAW_MEM;
+  return 0;
+
+}
+
+void MC_dpor3_init(xbt_automaton_t a)
+{
+  mc_pair_prop_col_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;
+
+  MC_SET_RAW_MEM;
+  initial_graph_state = MC_state_new();
+  MC_UNSET_RAW_MEM;
+
+  /* Wait for requests (schedules processes) */
+  MC_wait_for_requests();
+
+  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(initial_automaton_state != NULL)
+      break;
+  }
+
+  if(initial_automaton_state == NULL){
+    cursor = 0;
+    xbt_dynar_foreach(a->states, cursor, automaton_state){
+      if(automaton_state->type == -1){
+       initial_automaton_state = automaton_state;
+       break;
+      }
+    }
+  }
+
+  reached_pairs_prop_col = xbt_dynar_new(sizeof(char *), NULL); 
+  visited_pairs_prop_col = xbt_dynar_new(sizeof(char *), NULL); 
+  visible_transitions = xbt_dynar_new(sizeof(s_smx_req_t), NULL);
+  enabled_processes = xbt_dynar_new(sizeof(smx_process_t), NULL);
+  expanded = 0;
+
+  MC_SET_RAW_MEM;
+  initial_system_state = xbt_new0(s_mc_snapshot_t, 1);
+  MC_take_snapshot(initial_system_state);
+  initial_pair = new_pair_prop_col(initial_system_state, initial_graph_state, initial_automaton_state);
+  cursor = 0;
+  xbt_propositional_symbol_t ps;
+  xbt_dynar_foreach(a->propositional_symbols, cursor, ps){
+    int (*f)() = ps->function;
+    int val = (*f)();
+    mc_prop_ato_t pa = new_proposition(ps->pred, val);
+    xbt_dynar_push(initial_pair->propositions, &pa);
+  } 
+  xbt_fifo_unshift(mc_snapshot_stack, initial_pair);
+  MC_UNSET_RAW_MEM;
+
+
+  XBT_DEBUG("**************************************************");
+  XBT_DEBUG("Initial pair");
+
+  MC_dpor3(a, 0);
+    
+}
+
+
+void MC_dpor3(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_prop_col_t pair = NULL, next_pair = NULL, prev_pair = NULL;
+  smx_process_t process = NULL;
+  xbt_fifo_item_t item = NULL;
+  int d;
+
+
+  while (xbt_fifo_size(mc_snapshot_stack) > 0) {
+
+    /* Get current pair */
+    pair = (mc_pair_prop_col_t) 
+      xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack));
+
+    XBT_DEBUG("**************************************************");
+    XBT_DEBUG("Exploration depth=%d (pair=%p) (%d interleave)",
+             xbt_fifo_size(mc_snapshot_stack), pair, MC_state_interleave_size(pair->graph_state));
+
+    if(MC_state_interleave_size(pair->graph_state) == 0){
+    
+      xbt_dynar_reset(enabled_processes);
+
+      MC_SET_RAW_MEM;
+    
+      xbt_swag_foreach(process, simix_global->process_list){
+       if(MC_process_is_enabled(process)){ 
+         xbt_dynar_push(enabled_processes, &process);
+         //XBT_DEBUG("Process : pid=%lu",process->pid);
+       }
+      }
+
+      //XBT_DEBUG("Enabled processes before pop : %lu", xbt_dynar_length(enabled_processes));
+    
+      //XBT_DEBUG("Processes already interleaved : %d", pair->interleave);
+    
+      if(xbt_dynar_length(enabled_processes) > 0){
+       for(d=0;d<pair->interleave;d++){
+         xbt_dynar_shift(enabled_processes, NULL);
+       }
+      }
+
+      //XBT_DEBUG("Enabled processes after pop : %lu", xbt_dynar_length(enabled_processes));
+    
+      if(pair->fully_expanded == 0){
+       if(xbt_dynar_length(enabled_processes) > 0){
+         MC_state_interleave_process(pair->graph_state, xbt_dynar_get_as(enabled_processes, 0, smx_process_t));
+         //XBT_DEBUG("Interleave process");
+       }
+      }
+    
+      MC_UNSET_RAW_MEM;
+
+    }
+
+
+    /* Update statistics */
+    mc_stats_pair->visited_pairs++;
+    //sleep(1);
+
+    /* Test acceptance pair and acceptance cycle*/
+
+    if(pair->automaton_state->type == 1){
+      if(search_cycle == 0){
+       set_pair_prop_col_reached(pair);
+       XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", pair->graph_state, pair->automaton_state, pair->automaton_state->id);
+      }else{
+       if(reached_prop_col(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))) {
+
+      set_pair_prop_col_visited(pair, search_cycle);
+      
+      /* 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);
+
+      /* 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;
+
+      pair->interleave++;
+
+      next_graph_state = MC_state_new();
+
+      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_prop_col(next_system_state, next_graph_state, next_automaton_state);
+      cursor = 0;
+      xbt_propositional_symbol_t ps;
+      xbt_dynar_foreach(a->propositional_symbols, cursor, ps){
+       int (*f)() = ps->function;
+       int val = (*f)();
+       mc_prop_ato_t pa = new_proposition(ps->pred, val);
+       xbt_dynar_push(next_pair->propositions, &pa);
+      } 
+      xbt_fifo_unshift(mc_snapshot_stack, next_pair);
+      
+      cursor = 0;
+      if((invisible_col(pair, next_pair) == 0) && (pair->fully_expanded == 0)){
+       set_fully_expanded_col(pair);
+       if(xbt_dynar_length(enabled_processes) > 1){ // Si 1 seul process activé, déjà exécuté juste avant donc état complètement étudié
+         xbt_dynar_foreach(enabled_processes, cursor, process){
+           MC_state_interleave_process(pair->graph_state, process);
+         }
+       }
+       XBT_DEBUG("Pair %p fully expanded (%u interleave)", pair, MC_state_interleave_size(pair->graph_state));
+      }
+
+      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_prop_col_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(prev_pair->fully_expanded == 0){
+             if(!MC_state_process_is_done(prev_pair->graph_state, req->issuer)){
+               MC_state_interleave_process(prev_pair->graph_state, req->issuer);
+               XBT_DEBUG("Process %p (%lu) interleaved in pair %p", req->issuer, req->issuer->pid, prev_pair);
+             }else{
+               XBT_DEBUG("Process %p (%lu) is in done set", req->issuer, req->issuer->pid);
+             }
+           }
+      
+            break;
+          }
+        }
+
+       
+        if (MC_state_interleave_size(pair->graph_state) > 0) {
+          /* 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 839c96b..aaac6e5 100644 (file)
@@ -54,6 +54,32 @@ void MC_init(void)
   MC_UNSET_RAW_MEM;
 }
 
+void MC_init_stateful(void){
+  
+   /* Check if MC is already initialized */
+  if (initial_snapshot)
+    return;
+
+  mc_time = xbt_new0(double, simix_process_maxpid);
+
+  /* Initialize the data structures that must be persistent across every
+     iteration of the model-checker (in RAW memory) */
+  MC_SET_RAW_MEM;
+
+  /* Initialize statistics */
+  mc_stats = xbt_new0(s_mc_stats_t, 1);
+  mc_stats->state_size = 1;
+
+  /* Create exploration stack */
+  mc_snapshot_stack = xbt_fifo_new();
+
+  MC_UNSET_RAW_MEM;
+
+  MC_dpor_stateful_init();
+
+
+}
+
 void MC_init_with_automaton(xbt_automaton_t a){
 
   XBT_DEBUG("Start init mc");
@@ -75,11 +101,13 @@ void MC_init_with_automaton(xbt_automaton_t a){
  /* Create exploration stack */
   mc_snapshot_stack = xbt_fifo_new();
 
+
   MC_UNSET_RAW_MEM;
 
   //MC_vddfs_with_restore_snapshot_init(a);
   //MC_ddfs_with_restore_snapshot_init(a);
   MC_dpor2_init(a);
+  //MC_dpor3_init(a);
 }
 
 
@@ -90,6 +118,13 @@ void MC_modelcheck(void)
   MC_exit();
 }
 
+void MC_modelcheck_stateful(void)
+{
+  MC_init_stateful();
+  MC_dpor_stateful();
+  MC_exit();
+}
+
 void MC_modelcheck_with_automaton(xbt_automaton_t a){
   MC_init_with_automaton(a);
   MC_exit_with_automaton();
@@ -109,6 +144,7 @@ void MC_exit(void)
   MC_memory_exit();
 }
 
+
 int MC_random(int min, int max)
 {
   /*FIXME: return mc_current_state->executed_transition->random.value;*/
@@ -220,6 +256,7 @@ void MC_dump_stack(xbt_fifo_t stack)
   MC_UNSET_RAW_MEM;
 }
 
+
 void MC_show_stack(xbt_fifo_t stack)
 {
   int value;
@@ -254,6 +291,53 @@ void MC_show_deadlock(smx_req_t req)
   MC_dump_stack(mc_stack);
 }
 
+void MC_show_deadlock_stateful(smx_req_t req)
+{
+  /*char *req_str = NULL;*/
+  XBT_INFO("**************************");
+  XBT_INFO("*** DEAD-LOCK DETECTED ***");
+  XBT_INFO("**************************");
+  XBT_INFO("Locked request:");
+  /*req_str = MC_request_to_string(req);
+  XBT_INFO("%s", req_str);
+  xbt_free(req_str);*/
+  XBT_INFO("Counter-example execution trace:");
+  MC_show_stack_stateful(mc_snapshot_stack);
+}
+
+void MC_dump_stack_stateful(xbt_fifo_t stack)
+{
+  //mc_state_ws_t state;
+
+  MC_show_stack_stateful(stack);
+
+  /*MC_SET_RAW_MEM;
+  while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)
+    MC_state_delete(state);
+    MC_UNSET_RAW_MEM;*/
+}
+
+
+void MC_show_stack_stateful(xbt_fifo_t stack)
+{
+  int value;
+  mc_state_ws_t state;
+  xbt_fifo_item_t item;
+  smx_req_t req;
+  char *req_str = NULL;
+  
+  for (item = xbt_fifo_get_last_item(stack);
+       (item ? (state = (mc_state_ws_t) (xbt_fifo_get_item_content(item)))
+        : (NULL)); item = xbt_fifo_get_prev_item(item)) {
+    req = MC_state_get_executed_request(state->graph_state, &value);
+    if(req){
+      req_str = MC_request_to_string(req, value);
+      XBT_INFO("%s", req_str);
+      xbt_free(req_str);
+    }
+  }
+}
+
 void MC_print_statistics(mc_stats_t stats)
 {
   XBT_INFO("State space size ~= %lu", stats->state_size);
@@ -290,6 +374,19 @@ void MC_assert(int prop)
   }
 }
 
+void MC_assert_stateful(int prop)
+{
+  if (MC_IS_ENABLED && !prop) {
+    XBT_INFO("**************************");
+    XBT_INFO("*** PROPERTY NOT VALID ***");
+    XBT_INFO("**************************");
+    XBT_INFO("Counter-example execution trace:");
+    MC_dump_stack_stateful(mc_snapshot_stack);
+    MC_print_statistics(mc_stats);
+    xbt_abort();
+  }
+}
+
 void MC_assert_pair(int prop){
   if (MC_IS_ENABLED && !prop) {
     XBT_INFO("**************************");
index d2e676c..5456347 100644 (file)
@@ -51,6 +51,9 @@ void MC_get_enabled_processes();
 void MC_show_deadlock(smx_req_t req);
 void MC_show_stack(xbt_fifo_t stack);
 void MC_dump_stack(xbt_fifo_t stack);
+void MC_show_deadlock_stateful(smx_req_t req);
+void MC_show_stack_stateful(xbt_fifo_t stack);
+void MC_dump_stack_stateful(xbt_fifo_t stack);
 
 /********************************* Requests ***********************************/
 int MC_request_depend(smx_req_t req1, smx_req_t req2);
@@ -220,16 +223,19 @@ void set_pair_visited(mc_pair_t p, int search_cycle);
 int visited(mc_pair_t p, int search_cycle);
 
 
-/* **** DPOR Cristian with restore snapshot **** */
+/* **** DPOR Cristian stateful **** */
 
 typedef struct s_mc_state_with_snapshot{
   mc_snapshot_t system_state;
   mc_state_t graph_state;
 }s_mc_state_ws_t, *mc_state_ws_t;
 
+void MC_init_stateful(void);
+void MC_modelcheck_stateful(void);
 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_stateful_init(void);
+void MC_dpor_stateful(void);
+void MC_exit_stateful(void);
 
 /* **** DPOR 2 (invisible and independant transitions) **** */
 
@@ -248,7 +254,6 @@ typedef struct s_mc_pair_prop{
   int interleave;
 }s_mc_pair_prop_t, *mc_pair_prop_t;
 
-
 mc_prop_ato_t new_proposition(char* id, int value);
 mc_pair_prop_t new_pair_prop(mc_snapshot_t sn, mc_state_t sg, xbt_state_t st);
 int reached_prop(mc_pair_prop_t pair);
@@ -258,4 +263,40 @@ void MC_dpor2(xbt_automaton_t a, int search_cycle);
 int invisible(mc_pair_prop_t p, mc_pair_prop_t np);
 void set_fully_expanded(mc_pair_prop_t pair);
 
+/* **** DPOR 3 (invisible and independant transitions with coloration of pairs) **** */
+
+typedef enum {
+  GREEN=0,      
+  ORANGE,           
+  RED              
+} e_mc_color_pair_t;
+
+typedef struct s_mc_pair_prop_col{
+  mc_snapshot_t system_state;
+  mc_state_t graph_state;
+  xbt_state_t automaton_state;
+  int num;
+  xbt_dynar_t propositions;
+  int fully_expanded;
+  int interleave;
+  e_mc_color_pair_t color;
+  int expanded;
+}s_mc_pair_prop_col_t, *mc_pair_prop_col_t;
+
+typedef struct s_mc_visited_pair_prop_col{
+  mc_pair_prop_col_t pair;
+  int search_cycle;
+}s_mc_visited_pair_prop_col_t, *mc_visited_pair_prop_col_t;
+
+void MC_dpor3_init(xbt_automaton_t a);
+void MC_dpor3(xbt_automaton_t a, int search_cycle);
+mc_pair_prop_col_t new_pair_prop_col(mc_snapshot_t sn, mc_state_t sg, xbt_state_t st);
+void set_expanded(mc_pair_prop_col_t pair);
+int reached_prop_col(mc_pair_prop_col_t pair);
+void set_pair_prop_col_reached(mc_pair_prop_col_t pair);
+int invisible_col(mc_pair_prop_col_t p, mc_pair_prop_col_t np);
+void set_fully_expanded_col(mc_pair_prop_col_t pair);
+void set_pair_prop_col_visited(mc_pair_prop_col_t pair, int sc);
+int visited_pair_prop_col(mc_pair_prop_col_t pair, int sc);
+
 #endif
index 386057b..f17edf0 100644 (file)
@@ -153,6 +153,21 @@ MSG_error_t MSG_main(void)
   return MSG_OK;
 }
 
+MSG_error_t MSG_main_stateful(void)
+{
+  /* Clean IO before the run */
+  fflush(stdout);
+  fflush(stderr);
+
+  if (MC_IS_ENABLED) {
+    MC_modelcheck_stateful();
+  }
+  else {
+    SIMIX_run();
+  }
+  return MSG_OK;
+}
+
 MSG_error_t MSG_main_with_automaton(xbt_automaton_t a)
 {
   /* Clean IO before the run */