From: Gabriel Corona <gabriel.corona@loria.fr>
Date: Thu, 12 Feb 2015 10:21:37 +0000 (+0100)
Subject: [mc] Make an option for file descriptor snapshot (off by default)
X-Git-Tag: v3_12~732^2~120
X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/eb261664cc90426f7dede99a570454748801a357

[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 5dc7c8c67e..23b17815c7 100644
--- 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_snapshot_fds;
 
 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_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);
diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c
index 82e88c3032..b7dd845b1d 100644
--- 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_protocol.h"
 
 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_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
@@ -797,12 +799,12 @@ void MC_restore_snapshot_regions(mc_snapshot_t snapshot)
 #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)
 {
+  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++){
@@ -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_restore_snapshot_fds(snapshot);
+  if (_sg_mc_snapshot_fds)
+    MC_restore_snapshot_fds(snapshot);
   if (use_soft_dirty) {
     mc_softdirty_reset();
   }
diff --git a/src/mc/mc_config.c b/src/mc/mc_config.c
index 07c9179889..62517120ba 100644
--- 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_snapshot_fds = 0;
 
 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);
 }
 
+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) {
diff --git a/src/simgrid/sg_config.c b/src/simgrid/sg_config.c
index 3fc88bcb1b..18b73fbd10 100644
--- 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");
 
+    /* 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)",