[mc] Make an option for file descriptor snapshot (off by default)

This option is currently not supported in client/server mode.

diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h
index 5dc7c8c..23b1781 100644 (file)
--- a/src/include/mc/mc.h
+++ b/src/include/mc/mc.h
@@ -51,6 +51,7 @@ extern int _sg_mc_comms_determinism;
 extern int _sg_mc_send_determinism;
 extern int _sg_mc_safety;
 extern int _sg_mc_liveness;
 extern int _sg_mc_send_determinism;
 extern int _sg_mc_safety;
 extern int _sg_mc_liveness;

+extern int _sg_mc_snapshot_fds;

 
 extern xbt_dynar_t mc_heap_comparison_ignore;
 extern xbt_dynar_t stacks_areas;
 
 extern xbt_dynar_t mc_heap_comparison_ignore;
 extern xbt_dynar_t stacks_areas;


@@ -63,6 +64,7 @@ void _mc_cfg_cb_soft_dirty(const char *name, int pos);
 void _mc_cfg_cb_property(const char *name, int pos);
 void _mc_cfg_cb_timeout(const char *name, int pos);
 void _mc_cfg_cb_hash(const char *name, int pos);
 void _mc_cfg_cb_property(const char *name, int pos);
 void _mc_cfg_cb_timeout(const char *name, int pos);
 void _mc_cfg_cb_hash(const char *name, int pos);

+void _mc_cfg_cb_snapshot_fds(const char *name, int pos);

 void _mc_cfg_cb_max_depth(const char *name, int pos);
 void _mc_cfg_cb_visited(const char *name, int pos);
 void _mc_cfg_cb_dot_output(const char *name, int pos);
 void _mc_cfg_cb_max_depth(const char *name, int pos);
 void _mc_cfg_cb_visited(const char *name, int pos);
 void _mc_cfg_cb_dot_output(const char *name, int pos);

diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c
index 82e88c3..b7dd845 100644 (file)
--- a/src/mc/mc_checkpoint.c
+++ b/src/mc/mc_checkpoint.c
@@ -34,6 +34,7 @@
 #include "mc_object_info.h"
 #include "mc_mmu.h"
 #include "mc_unw.h"
 #include "mc_object_info.h"
 #include "mc_mmu.h"
 #include "mc_unw.h"

+#include "mc_protocol.h"

 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_checkpoint, mc,
                                 "Logging specific to mc_checkpoint");
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_checkpoint, mc,
                                 "Logging specific to mc_checkpoint");


@@ -740,7 +741,8 @@ mc_snapshot_t MC_take_snapshot(int num_state)
 
   MC_snapshot_handle_ignore(snapshot);
 
 
   MC_snapshot_handle_ignore(snapshot);
 

-  MC_get_current_fd(snapshot);
+  if (_sg_mc_snapshot_fds)
+    MC_get_current_fd(snapshot);

 
   const bool use_soft_dirty = _sg_mc_sparse_checkpoint
     && _sg_mc_soft_dirty
 
   const bool use_soft_dirty = _sg_mc_sparse_checkpoint
     && _sg_mc_soft_dirty


@@ -797,12 +799,12 @@ void MC_restore_snapshot_regions(mc_snapshot_t snapshot)
 #endif
 }
 
 #endif
 }
 

-// FIXME, cross-process support ~ we need to implement this on the app side
-// or use some form of [remote syscall execution](http://criu.org/Remote_syscall_execution)
-// based on [parasite code execution](http://criu.org/Parasite_code).

 static inline
 void MC_restore_snapshot_fds(mc_snapshot_t snapshot)
 {
 static inline
 void MC_restore_snapshot_fds(mc_snapshot_t snapshot)
 {

+  if (mc_mode == MC_MODE_SERVER)
+    xbt_die("FD snapshot not implemented in client/server mode.");
+

   int new_fd;
   size_t i;
   for(i=0; i < snapshot->total_fd; i++){
   int new_fd;
   size_t i;
   for(i=0; i < snapshot->total_fd; i++){


@@ -828,7 +830,8 @@ void MC_restore_snapshot(mc_snapshot_t snapshot)
     && MC_process_is_self(&mc_model_checker->process);
 
   MC_restore_snapshot_regions(snapshot);
     && MC_process_is_self(&mc_model_checker->process);
 
   MC_restore_snapshot_regions(snapshot);

-  MC_restore_snapshot_fds(snapshot);
+  if (_sg_mc_snapshot_fds)
+    MC_restore_snapshot_fds(snapshot);

   if (use_soft_dirty) {
     mc_softdirty_reset();
   }
   if (use_soft_dirty) {
     mc_softdirty_reset();
   }

diff --git a/src/mc/mc_config.c b/src/mc/mc_config.c
index 07c9179..6251712 100644 (file)
--- a/src/mc/mc_config.c
+++ b/src/mc/mc_config.c
@@ -58,7 +58,7 @@ int _sg_mc_comms_determinism = 0;
 int _sg_mc_send_determinism = 0;
 int _sg_mc_safety = 0;
 int _sg_mc_liveness = 0;
 int _sg_mc_send_determinism = 0;
 int _sg_mc_safety = 0;
 int _sg_mc_liveness = 0;

-
+int _sg_mc_snapshot_fds = 0;

 
 void _mc_cfg_cb_reduce(const char *name, int pos)
 {
 
 void _mc_cfg_cb_reduce(const char *name, int pos)
 {


@@ -118,6 +118,15 @@ void _mc_cfg_cb_hash(const char *name, int pos)
   _sg_mc_hash = xbt_cfg_get_boolean(_sg_cfg_set, name);
 }
 
   _sg_mc_hash = xbt_cfg_get_boolean(_sg_cfg_set, name);
 }
 

+void _mc_cfg_cb_snapshot_fds(const char *name, int pos)
+{
+  if (_sg_cfg_init_status && !_sg_do_model_check) {
+    xbt_die
+        ("You are specifying a value to enable/disable the use of FD snapshoting, but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
+  }
+  _sg_mc_snapshot_fds = xbt_cfg_get_boolean(_sg_cfg_set, name);
+}
+

 void _mc_cfg_cb_max_depth(const char *name, int pos)
 {
   if (_sg_cfg_init_status && !_sg_do_model_check) {
 void _mc_cfg_cb_max_depth(const char *name, int pos)
 {
   if (_sg_cfg_init_status && !_sg_do_model_check) {

diff --git a/src/simgrid/sg_config.c b/src/simgrid/sg_config.c
index 3fc88bc..18b73fb 100644 (file)
--- a/src/simgrid/sg_config.c
+++ b/src/simgrid/sg_config.c
@@ -695,6 +695,12 @@ void sg_config_init(int *argc, char **argv)
                      xbt_cfgelm_boolean, 1, 1, _mc_cfg_cb_hash, NULL);
     xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/hash", "no");
 
                      xbt_cfgelm_boolean, 1, 1, _mc_cfg_cb_hash, NULL);
     xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/hash", "no");
 

+    /* Set max depth exploration */
+    xbt_cfg_register(&_sg_cfg_set, "model-check/snapshot_fds",
+                     "Whether file descriptors must be snapshoted",
+                     xbt_cfgelm_boolean, 1, 1, _mc_cfg_cb_snapshot_fds, NULL);
+    xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/snapshot_fds", "no");
+

     /* Set max depth exploration */
     xbt_cfg_register(&_sg_cfg_set, "model-check/max_depth",
                      "Specify the max depth of exploration (default : 1000)",
     /* Set max depth exploration */
     xbt_cfg_register(&_sg_cfg_set, "model-check/max_depth",
                      "Specify the max depth of exploration (default : 1000)",