model-checker : fix MC_RANDOM simcall

Time doesn't exist in model-checking. However, there are some
protocols, such as Chord, with some periodics operations (random
lookup, check predecessors, ...).  If the model-checker is used with
these examples, these operations are never executed because of the
time which doesn't progress.  With MC_RANDOM simcall, the
model-checker will explore the two cases : the case in which the
periodic operation is executed and the other case in which it is not
executed.  In this way, the verification is exhaustive whatever the
period.

diff --git a/examples/msg/chord/chord.c b/examples/msg/chord/chord.c
index 14af6d0..42b74ca 100644 (file)
--- a/examples/msg/chord/chord.c
+++ b/examples/msg/chord/chord.c
@@ -335,26 +335,42 @@ int node(int argc, char *argv[])
       if (!MSG_comm_test(node.comm_receive)) {
 
         // no task was received: make some periodic calls
       if (!MSG_comm_test(node.comm_receive)) {
 
         // no task was received: make some periodic calls

-        if (MSG_get_clock() >= next_stabilize_date) {
-          stabilize(&node);
-          next_stabilize_date = MSG_get_clock() + periodic_stabilize_delay;
-        }
-        else if (MSG_get_clock() >= next_fix_fingers_date) {
-          fix_fingers(&node);
-          next_fix_fingers_date = MSG_get_clock() + periodic_fix_fingers_delay;
-        }
-        else if (MSG_get_clock() >= next_check_predecessor_date) {
-          check_predecessor(&node);
-          next_check_predecessor_date = MSG_get_clock() + periodic_check_predecessor_delay;
-        }
-        else if (MSG_get_clock() >= next_lookup_date) {
-          random_lookup(&node);
-          next_lookup_date = MSG_get_clock() + periodic_lookup_delay;
-        }
-        else {
-          // nothing to do: sleep for a while
-          MSG_process_sleep(5);
+
+        if(MC_is_active()){
+          if(MC_random()){
+            stabilize(&node);
+          }else if(MC_random()){
+            fix_fingers(&node);
+          }else if(MC_random()){
+            check_predecessor(&node);
+          }else if(MC_random()){
+            random_lookup(&node);
+          }else{
+            MSG_process_sleep(5);
+          }
+        }else{
+          if (MSG_get_clock() >= next_stabilize_date) {
+            stabilize(&node);
+            next_stabilize_date = MSG_get_clock() + periodic_stabilize_delay;
+          }
+          else if (MSG_get_clock() >= next_fix_fingers_date) {
+            fix_fingers(&node);
+            next_fix_fingers_date = MSG_get_clock() + periodic_fix_fingers_delay;
+          }
+          else if (MSG_get_clock() >= next_check_predecessor_date) {
+            check_predecessor(&node);
+            next_check_predecessor_date = MSG_get_clock() + periodic_check_predecessor_delay;
+          }
+          else if (MSG_get_clock() >= next_lookup_date) {
+            random_lookup(&node);
+            next_lookup_date = MSG_get_clock() + periodic_lookup_delay;
+          }
+          else {
+            // nothing to do: sleep for a while
+            MSG_process_sleep(5);
+          }

         }
         }

+

       } else {
         // a transfer has occurred
 
       } else {
         // a transfer has occurred
 

diff --git a/include/simgrid/modelchecker.h b/include/simgrid/modelchecker.h
index ae58a10..18535fd 100644 (file)
--- a/include/simgrid/modelchecker.h
+++ b/include/simgrid/modelchecker.h
@@ -19,7 +19,7 @@ extern int _sg_do_model_check; /* please don't use directly: we inline MC_is_act
 #define MC_is_active() _sg_do_model_check
 
 XBT_PUBLIC(void) MC_assert(int);
 #define MC_is_active() _sg_do_model_check
 
 XBT_PUBLIC(void) MC_assert(int);

-XBT_PUBLIC(int) MC_random(int min, int max);
+XBT_PUBLIC(int) MC_random(void);

 XBT_PUBLIC(void) MC_automaton_new_propositional_symbol(const char* id, void* fct);
 XBT_PUBLIC(void *) MC_snapshot(void);
 XBT_PUBLIC(int) MC_compare_snapshots(void *s1, void *s2);
 XBT_PUBLIC(void) MC_automaton_new_propositional_symbol(const char* id, void* fct);
 XBT_PUBLIC(void *) MC_snapshot(void);
 XBT_PUBLIC(int) MC_compare_snapshots(void *s1, void *s2);

diff --git a/include/simgrid/simix.h b/include/simgrid/simix.h
index 8d3ed6b..bd69b19 100644 (file)
--- a/include/simgrid/simix.h
+++ b/include/simgrid/simix.h
@@ -478,7 +478,7 @@ XBT_PUBLIC(xbt_dict_t) simcall_asr_get_properties(const char *name);
 /************************** MC simcalls   **********************************/
 XBT_PUBLIC(void *) simcall_mc_snapshot(void);
 XBT_PUBLIC(int) simcall_mc_compare_snapshots(void *s1, void *s2);
 /************************** MC simcalls   **********************************/
 XBT_PUBLIC(void *) simcall_mc_snapshot(void);
 XBT_PUBLIC(int) simcall_mc_compare_snapshots(void *s1, void *s2);

-XBT_PUBLIC(int) simcall_mc_random(int min, int max);
+XBT_PUBLIC(int) simcall_mc_random(void);

 
 /************************** New API simcalls **********************************/
 /* TUTORIAL: New API                                                          */
 
 /************************** New API simcalls **********************************/
 /* TUTORIAL: New API                                                          */

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index d67f00d..672765a 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -303,16 +303,16 @@ void MC_exit(void)
   xbt_abort();
 }
 
   xbt_abort();
 }
 

-int SIMIX_pre_mc_random(smx_simcall_t simcall, int min, int max){
+int SIMIX_pre_mc_random(smx_simcall_t simcall){

 
   return simcall->mc_value;
 }
 
 
 
   return simcall->mc_value;
 }
 
 

-int MC_random(int min, int max)
+int MC_random(void)

 {
   /*FIXME: return mc_current_state->executed_transition->random.value;*/
 {
   /*FIXME: return mc_current_state->executed_transition->random.value;*/

-  return simcall_mc_random(min, max);
+  return simcall_mc_random();

 }
 
 /**
 }
 
 /**

diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index 17e8c9a..70b34db 100644 (file)
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -72,8 +72,8 @@ void MC_wait_for_requests(void);
 void MC_show_deadlock(smx_simcall_t req);
 void MC_show_stack_safety(xbt_fifo_t stack);
 void MC_dump_stack_safety(xbt_fifo_t stack);
 void MC_show_deadlock(smx_simcall_t req);
 void MC_show_stack_safety(xbt_fifo_t stack);
 void MC_dump_stack_safety(xbt_fifo_t stack);

-
-int SIMIX_pre_mc_random(smx_simcall_t simcall, int min, int max);
+void MC_init(void);
+int SIMIX_pre_mc_random(smx_simcall_t simcall);

 
 /********************************* Requests ***********************************/
 int MC_request_depend(smx_simcall_t req1, smx_simcall_t req2);
 
 /********************************* Requests ***********************************/
 int MC_request_depend(smx_simcall_t req1, smx_simcall_t req2);


@@ -91,6 +91,7 @@ int MC_process_is_enabled(smx_process_t process);
 typedef enum {
   MC_NOT_INTERLEAVE=0,      /* Do not interleave (do not execute) */
   MC_INTERLEAVE,            /* Interleave the process (one or more request) */
 typedef enum {
   MC_NOT_INTERLEAVE=0,      /* Do not interleave (do not execute) */
   MC_INTERLEAVE,            /* Interleave the process (one or more request) */

+  MC_MORE_INTERLEAVE,       /* Interleave twice the process (for mc_random simcall) */

   MC_DONE                   /* Already interleaved */
 } e_mc_process_state_t;
 
   MC_DONE                   /* Already interleaved */
 } e_mc_process_state_t;
 


@@ -251,7 +252,6 @@ extern mc_global_t initial_state_safety;
 
 void MC_dpor_init(void);
 void MC_dpor(void);
 
 void MC_dpor_init(void);
 void MC_dpor(void);

-void MC_init(void);

 
 typedef struct s_mc_safety_visited_state{
   mc_snapshot_t system_state;
 
 typedef struct s_mc_safety_visited_state{
   mc_snapshot_t system_state;

diff --git a/src/mc/mc_request.c b/src/mc/mc_request.c
index 4e12e96..ea801b5 100644 (file)
--- a/src/mc/mc_request.c
+++ b/src/mc/mc_request.c
@@ -16,10 +16,7 @@ int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2) {
     return TRUE;
 
   if (r1->issuer == r2->issuer)
     return TRUE;
 
   if (r1->issuer == r2->issuer)

-    return FALSE;
-
-  if((r1->call == SIMCALL_MC_RANDOM) || (r2->call == SIMCALL_MC_RANDOM))
-    return FALSE;
+      return FALSE;

 
   if(r1->call == SIMCALL_COMM_ISEND && r2->call == SIMCALL_COMM_IRECV)
     return FALSE;
 
   if(r1->call == SIMCALL_COMM_ISEND && r2->call == SIMCALL_COMM_IRECV)
     return FALSE;


@@ -253,7 +250,7 @@ char *MC_request_to_string(smx_simcall_t req, int value)
 
   case SIMCALL_MC_RANDOM:
     type = xbt_strdup("MC_RANDOM");
 
   case SIMCALL_MC_RANDOM:
     type = xbt_strdup("MC_RANDOM");

-    args = '\0';
+    args = bprintf("%d", value);

     break;
 
   default:
     break;
 
   default:

diff --git a/src/mc/mc_state.c b/src/mc/mc_state.c
index d43a6bc..29621f1 100644 (file)
--- a/src/mc/mc_state.c
+++ b/src/mc/mc_state.c
@@ -64,7 +64,7 @@ unsigned int MC_state_interleave_size(mc_state_t state)
   unsigned int i, size=0;
 
   for(i=0; i < state->max_pid; i++){
   unsigned int i, size=0;
 
   for(i=0; i < state->max_pid; i++){

-    if(state->proc_status[i].state == MC_INTERLEAVE)
+    if((state->proc_status[i].state == MC_INTERLEAVE) || (state->proc_status[i].state == MC_MORE_INTERLEAVE))

       size++;
   }
 
       size++;
   }
 


@@ -79,6 +79,8 @@ void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req, int valu
 {
   state->executed_req = *req;
   state->req_num = value;
 {
   state->executed_req = *req;
   state->req_num = value;

+  smx_process_t process = NULL;
+  mc_procstate_t procstate = NULL;

 
   /* 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 dependence
 
   /* 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 dependence


@@ -120,6 +122,15 @@ void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req, int valu
     case SIMCALL_MC_RANDOM:
       state->internal_req = *req;
       simcall_mc_random__set__result(&state->internal_req, value);
     case SIMCALL_MC_RANDOM:
       state->internal_req = *req;
       simcall_mc_random__set__result(&state->internal_req, value);

+      if(value == 0){
+        xbt_swag_foreach(process, simix_global->process_list){
+          procstate = &state->proc_status[process->pid];
+          if(process->pid == req->issuer->pid){
+            procstate->state = MC_MORE_INTERLEAVE;  
+            break;
+          }        
+        }
+      }

       break;
 
     default:
       break;
 
     default:


@@ -127,7 +138,7 @@ void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req, int valu
       break;
   }
 }
       break;
   }
 }

-
+ 

 smx_simcall_t MC_state_get_executed_request(mc_state_t state, int *value)
 {
   *value = state->req_num;
 smx_simcall_t MC_state_get_executed_request(mc_state_t state, int *value)
 {
   *value = state->req_num;


@@ -144,18 +155,11 @@ smx_simcall_t MC_state_get_request(mc_state_t state, int *value)
   smx_process_t process = NULL;
   mc_procstate_t procstate = NULL;
   unsigned int start_count;
   smx_process_t process = NULL;
   mc_procstate_t procstate = NULL;
   unsigned int start_count;

-  int min, max;
-
-  static int first = 0;
-  if(first == 0){
-    srand(987654321);
-    first = 1;
-  }

 
   xbt_swag_foreach(process, simix_global->process_list){
     procstate = &state->proc_status[process->pid];
 
 
   xbt_swag_foreach(process, simix_global->process_list){
     procstate = &state->proc_status[process->pid];
 

-    if(procstate->state == MC_INTERLEAVE){
+    if(procstate->state == MC_INTERLEAVE || procstate->state == MC_MORE_INTERLEAVE){

       if(MC_process_is_enabled(process)){
         switch(process->simcall.call){
           case SIMCALL_COMM_WAITANY:
       if(MC_process_is_enabled(process)){
         switch(process->simcall.call){
           case SIMCALL_COMM_WAITANY:


@@ -206,9 +210,10 @@ smx_simcall_t MC_state_get_request(mc_state_t state, int *value)
             break;
 
           case SIMCALL_MC_RANDOM:
             break;
 
           case SIMCALL_MC_RANDOM:

-            min = simcall_mc_random__get__min(&process->simcall);
-            max = simcall_mc_random__get__max(&process->simcall);
-            *value = (int)((rand() % ((max-min)+1)) + min);
+            if(procstate->state == MC_INTERLEAVE)
+              *value = 0;
+            else
+              *value = 1;

             procstate->state = MC_DONE;
             return &process->simcall;
             break;
             procstate->state = MC_DONE;
             return &process->simcall;
             break;

diff --git a/src/simix/smx_smurf_private.h b/src/simix/smx_smurf_private.h
index e4224a1..c55fa36 100644 (file)
--- a/src/simix/smx_smurf_private.h
+++ b/src/simix/smx_smurf_private.h
@@ -368,7 +368,7 @@ ACTION(SIMCALL_SET_CATEGORY, set_category, WITH_ANSWER, TVOID(result), TSPEC(act
 #define SIMCALL_LIST4(ACTION, sep) \
 ACTION(SIMCALL_MC_SNAPSHOT, mc_snapshot, WITH_ANSWER, TPTR(result)) sep \
 ACTION(SIMCALL_MC_COMPARE_SNAPSHOTS, mc_compare_snapshots, WITH_ANSWER, TINT(result), TPTR(s1), TPTR(s2)) sep \
 #define SIMCALL_LIST4(ACTION, sep) \
 ACTION(SIMCALL_MC_SNAPSHOT, mc_snapshot, WITH_ANSWER, TPTR(result)) sep \
 ACTION(SIMCALL_MC_COMPARE_SNAPSHOTS, mc_compare_snapshots, WITH_ANSWER, TINT(result), TPTR(s1), TPTR(s2)) sep \

-ACTION(SIMCALL_MC_RANDOM, mc_random, WITH_ANSWER, TINT(result), TINT(min), TINT(max)) sep
+ACTION(SIMCALL_MC_RANDOM, mc_random, WITH_ANSWER, TINT(result)) sep

 #else
 #define SIMCALL_LIST4(ACTION, sep)
 #endif
 #else
 #define SIMCALL_LIST4(ACTION, sep)
 #endif

diff --git a/src/simix/smx_user.c b/src/simix/smx_user.c
index ae4749f..a23e346 100644 (file)
--- a/src/simix/smx_user.c
+++ b/src/simix/smx_user.c
@@ -1161,9 +1161,9 @@ int simcall_mc_compare_snapshots(void *s1, void *s2){
   return simcall_BODY_mc_compare_snapshots(s1, s2);
 }
 
   return simcall_BODY_mc_compare_snapshots(s1, s2);
 }
 

-int simcall_mc_random(int min, int max)
+int simcall_mc_random(void)

 {
 {

-  return simcall_BODY_mc_random(min, max);
+  return simcall_BODY_mc_random();

 }
 
 
 }