model-checker : New public functions to take a snapshot and compare two snapshots...

diff --git a/include/simgrid/modelchecker.h b/include/simgrid/modelchecker.h
index 52b2ed7..d5f8bca 100644 (file)
--- a/include/simgrid/modelchecker.h
+++ b/include/simgrid/modelchecker.h
@@ -21,6 +21,8 @@ extern int _surf_do_model_check; /* please don't use directly: we inline MC_is_a
 XBT_PUBLIC(void) MC_assert(int);
 XBT_PUBLIC(int) MC_random(int min, int max);
 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);
 
 #else
 

diff --git a/include/simgrid/simix.h b/include/simgrid/simix.h
index bc7dc42..121b2cc 100644 (file)
--- a/include/simgrid/simix.h
+++ b/include/simgrid/simix.h
@@ -467,6 +467,10 @@ XBT_PUBLIC(xbt_dict_t) SIMIX_asr_get_properties(const char *name);
 /************************** AS router simcalls ***************************/
 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);
+
 /************************** New API simcalls **********************************/
 /* TUTORIAL: New API                                                          */
 /******************************************************************************/

diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c
index 0703b17..6f53924 100644 (file)
--- a/src/mc/mc_checkpoint.c
+++ b/src/mc/mc_checkpoint.c
@@ -614,3 +614,9 @@ static void snapshot_stack_free(mc_snapshot_stack_t s){
 void snapshot_stack_free_voidp(void *s){
   snapshot_stack_free((mc_snapshot_stack_t) * (void **) s);
 }
+
+void *MC_snapshot(void){
+
+  return simcall_mc_snapshot();
+  
+}

diff --git a/src/mc/mc_compare.c b/src/mc/mc_compare.c
index 083301b..0b20726 100644 (file)
--- a/src/mc/mc_compare.c
+++ b/src/mc/mc_compare.c
@@ -407,3 +407,8 @@ static int compare_stack(stack_region_t s1, stack_region_t s2, void *sp1, void *
   return nb_diff;
 }
 
+int MC_compare_snapshots(void *s1, void *s2){
+
+  return simcall_mc_compare_snapshots(s1, s2);
+
+}

diff --git a/src/mc/mc_request.c b/src/mc/mc_request.c
index ec73bfd..50c7cd2 100644 (file)
--- a/src/mc/mc_request.c
+++ b/src/mc/mc_request.c
@@ -239,6 +239,16 @@ char *MC_request_to_string(smx_simcall_t req, int value)
     }
     break;
 
+  case SIMCALL_MC_SNAPSHOT:
+    type = xbt_strdup("MC_SNAPSHOT");
+    args = '\0';
+    break;
+
+  case SIMCALL_MC_COMPARE_SNAPSHOTS:
+    type = xbt_strdup("MC_COMPARE_SNAPSHOTS");
+    args = '\0';
+    break;
+
   default:
     THROW_UNIMPLEMENTED;
   }
@@ -271,7 +281,9 @@ int MC_request_is_visible(smx_simcall_t req)
     || req->call == SIMCALL_COMM_WAIT
     || req->call == SIMCALL_COMM_WAITANY
     || req->call == SIMCALL_COMM_TEST
-    || req->call == SIMCALL_COMM_TESTANY;
+    || req->call == SIMCALL_COMM_TESTANY
+    || req->call == SIMCALL_MC_SNAPSHOT
+    || req->call == SIMCALL_MC_COMPARE_SNAPSHOTS;
 }
 
 int MC_request_is_enabled(smx_simcall_t req)

diff --git a/src/simix/smx_smurf.c b/src/simix/smx_smurf.c
index 973dd82..f3ebc52 100644 (file)
--- a/src/simix/smx_smurf.c
+++ b/src/simix/smx_smurf.c
@@ -1,6 +1,7 @@
 #include "smx_private.h"
 #include "xbt/fifo.h"
 #include "xbt/xbt_os_thread.h"
+#include "../mc/mc_private.h"
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(simix_smurf, simix,
                                 "Logging specific to SIMIX (SMURF)");
@@ -557,6 +558,17 @@ void SIMIX_simcall_pre(smx_simcall_t simcall, int value)
       SIMIX_simcall_answer(simcall);
       break;
 
+    case SIMCALL_MC_SNAPSHOT:
+      simcall->mc_snapshot.s = MC_take_snapshot_liveness();
+      SIMIX_simcall_answer(simcall);
+      break;
+
+    case SIMCALL_MC_COMPARE_SNAPSHOTS:
+      simcall->mc_compare_snapshots.result =
+        snapshot_compare(simcall->mc_compare_snapshots.snapshot1, simcall->mc_compare_snapshots.snapshot2);
+      SIMIX_simcall_answer(simcall);
+      break;
+   
     case SIMCALL_NONE:
       THROWF(arg_error,0,"Asked to do the noop syscall on %s@%s",
           SIMIX_process_get_name(simcall->issuer),

diff --git a/src/simix/smx_smurf_private.h b/src/simix/smx_smurf_private.h
index adff451..2009207 100644 (file)
--- a/src/simix/smx_smurf_private.h
+++ b/src/simix/smx_smurf_private.h
@@ -98,6 +98,8 @@ SIMCALL_ENUM_ELEMENT(SIMCALL_FILE_STAT), \
 SIMCALL_ENUM_ELEMENT(SIMCALL_FILE_UNLINK),\
 SIMCALL_ENUM_ELEMENT(SIMCALL_FILE_LS),\
 SIMCALL_ENUM_ELEMENT(SIMCALL_ASR_GET_PROPERTIES), \
+SIMCALL_ENUM_ELEMENT(SIMCALL_MC_SNAPSHOT), \
+SIMCALL_ENUM_ELEMENT(SIMCALL_MC_COMPARE_SNAPSHOTS), \
 /* ****************************************************************************************** */ \
 /* TUTORIAL: New API                                                                        */ \
 /* ****************************************************************************************** */ \
@@ -607,6 +609,16 @@ typedef struct s_smx_simcall {
       xbt_dict_t result;
     } asr_get_properties;
 
+    struct{
+      void *s;
+    } mc_snapshot;
+
+    struct{
+      void *snapshot1;
+      void *snapshot2;
+      int result;
+    } mc_compare_snapshots;
+
     /* ****************************************************************************************** */
     /* TUTORIAL: New API                                                                        */
     /* ****************************************************************************************** */

diff --git a/src/simix/smx_user.c b/src/simix/smx_user.c
index a6415b5..84ce825 100644 (file)
--- a/src/simix/smx_user.c
+++ b/src/simix/smx_user.c
@@ -1651,6 +1651,32 @@ xbt_dict_t simcall_file_ls(const char* mount, const char* path)
   return simcall->file_ls.result;
 }
 
+void *simcall_mc_snapshot(void)
+{
+  smx_simcall_t simcall = SIMIX_simcall_mine();
+  simcall->call = SIMCALL_MC_SNAPSHOT;
+  
+  SIMIX_simcall_push(simcall->issuer);
+
+  return simcall->mc_snapshot.s;
+}
+
+int simcall_mc_compare_snapshots(void *s1, void *s2){
+  
+  smx_simcall_t simcall = SIMIX_simcall_mine();
+  simcall->call = SIMCALL_MC_COMPARE_SNAPSHOTS;
+  simcall->mc_compare_snapshots.snapshot1 = s1;
+  simcall->mc_compare_snapshots.snapshot2 = s2;
+  
+  if(MC_is_active()) /* Initialize result to a default value for snapshot comparison done during simcall */
+    simcall->mc_compare_snapshots.result = -1;
+  
+  SIMIX_simcall_push(simcall->issuer);
+  
+  return simcall->mc_compare_snapshots.result;
+}
+
+
 /* ****************************************************************************************** */
 /* TUTORIAL: New API                                                                          */
 /* All functions for simcall                                                                  */