Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Merge branch 'master' into mc
authorGabriel Corona <gabriel.corona@loria.fr>
Mon, 27 Apr 2015 08:33:01 +0000 (10:33 +0200)
committerGabriel Corona <gabriel.corona@loria.fr>
Mon, 27 Apr 2015 08:33:41 +0000 (10:33 +0200)
Conflicts:
buildtools/Cmake/DefinePackages.cmake
src/mc/mc_request.cpp

86 files changed:
.gitignore
buildtools/Cmake/DefinePackages.cmake
buildtools/Cmake/Flags.cmake
buildtools/Cmake/UnitTesting.cmake
examples/msg/chord/chord.c
examples/smpi/mc/only_send_deterministic.tesh
include/simgrid/modelchecker.h
include/xbt/dynar.h
include/xbt/swag.h
src/include/mc/mc.h
src/mc/ModelChecker.cpp [new file with mode: 0644]
src/mc/ModelChecker.hpp [new file with mode: 0644]
src/mc/PageStore.cpp [moved from src/mc/mc_page_store.cpp with 90% similarity]
src/mc/PageStore.hpp [moved from src/mc/mc_page_store.h with 88% similarity]
src/mc/mc_address_space.cpp [moved from src/mc/mc_address_space.c with 100% similarity]
src/mc/mc_address_space.h
src/mc/mc_base.cpp [moved from src/mc/mc_base.c with 78% similarity]
src/mc/mc_base.h
src/mc/mc_checkpoint.cpp [moved from src/mc/mc_checkpoint.c with 84% similarity]
src/mc/mc_client.cpp [moved from src/mc/mc_client.c with 95% similarity]
src/mc/mc_client.h
src/mc/mc_client_api.cpp [moved from src/mc/mc_client_api.c with 84% similarity]
src/mc/mc_comm_determinism.cpp [moved from src/mc/mc_comm_determinism.c with 94% similarity]
src/mc/mc_comm_pattern.cpp [moved from src/mc/mc_comm_pattern.c with 97% similarity]
src/mc/mc_compare.cpp
src/mc/mc_config.cpp [moved from src/mc/mc_config.c with 94% similarity]
src/mc/mc_diff.cpp [moved from src/mc/mc_diff.c with 94% similarity]
src/mc/mc_dwarf.cpp [moved from src/mc/mc_dwarf.c with 94% similarity]
src/mc/mc_dwarf_expression.cpp [moved from src/mc/mc_dwarf_expression.c with 99% similarity]
src/mc/mc_forward.h
src/mc/mc_global.cpp [moved from src/mc/mc_global.c with 91% similarity]
src/mc/mc_hash.cpp [moved from src/mc/mc_hash.c with 97% similarity]
src/mc/mc_ignore.cpp [moved from src/mc/mc_ignore.c with 98% similarity]
src/mc/mc_interface.h [deleted file]
src/mc/mc_liveness.cpp [moved from src/mc/mc_liveness.c with 97% similarity]
src/mc/mc_location.h
src/mc/mc_member.cpp [moved from src/mc/mc_member.c with 97% similarity]
src/mc/mc_memory.cpp [moved from src/mc/mc_memory.c with 99% similarity]
src/mc/mc_mmalloc.h
src/mc/mc_model_checker.c [deleted file]
src/mc/mc_model_checker.h [deleted file]
src/mc/mc_object_info.cpp [moved from src/mc/mc_object_info.c with 75% similarity]
src/mc/mc_object_info.h
src/mc/mc_page_snapshot.cpp
src/mc/mc_pair.cpp [moved from src/mc/mc_pair.c with 98% similarity]
src/mc/mc_private.h
src/mc/mc_process.cpp [moved from src/mc/mc_process.c with 92% similarity]
src/mc/mc_process.h
src/mc/mc_protocol.cpp [moved from src/mc/mc_protocol.c with 94% similarity]
src/mc/mc_protocol.h
src/mc/mc_record.cpp [moved from src/mc/mc_record.c with 98% similarity]
src/mc/mc_replay.h [new file with mode: 0644]
src/mc/mc_request.cpp [moved from src/mc/mc_request.c with 94% similarity]
src/mc/mc_safety.cpp [moved from src/mc/mc_safety.c with 96% similarity]
src/mc/mc_safety.h
src/mc/mc_server.cpp
src/mc/mc_server.h
src/mc/mc_set.cpp [deleted file]
src/mc/mc_smx.cpp [moved from src/mc/mc_smx.c with 79% similarity]
src/mc/mc_smx.h
src/mc/mc_snapshot.cpp [moved from src/mc/mc_snapshot.c with 92% similarity]
src/mc/mc_snapshot.h
src/mc/mc_state.cpp [moved from src/mc/mc_state.c with 95% similarity]
src/mc/mc_unw.cpp [moved from src/mc/mc_unw.c with 96% similarity]
src/mc/mc_unw_vmread.cpp [moved from src/mc/mc_unw_vmread.c with 87% similarity]
src/mc/mc_visited.cpp [moved from src/mc/mc_visited.c with 95% similarity]
src/mc/memory_map.cpp [moved from src/mc/memory_map.c with 98% similarity]
src/mc/simgrid_mc.cpp
src/msg/msg_global.c
src/simgrid/sg_config.c
src/simix/libsmx.c
src/simix/popping_bodies.c
src/simix/popping_generated.c
src/simix/popping_private.h
src/simix/simcalls.py
src/simix/smx_context_sysv.c
src/simix/smx_global.c
src/simix/smx_host.c
src/simix/smx_network.c
src/simix/smx_process.c
src/smpi/smpi_base.c
src/smpi/smpi_bench.c
src/smpi/smpi_global.c
src/xbt/mmalloc/mmprivate.h
teshsuite/mc/dwarf/CMakeLists.txt
teshsuite/mc/dwarf/dwarf.cpp [moved from teshsuite/mc/dwarf/dwarf.c with 94% similarity]

index 973db9c..a3bc468 100644 (file)
@@ -1057,7 +1057,7 @@ examples/smpi/mc/smpi_non_deterministic
 examples/smpi/mc/smpi_send_deterministic
 simgrid.jar_finalized
 simgrid_full.jar
-src/mc_page_store_unit.cpp
+src/PageStore_unit.cpp
 src/bindings/java/MANIFEST.MF
 NATIVE/
 VERSION
index 79652e1..d62ea0c 100644 (file)
@@ -6,7 +6,7 @@ set(EXTRA_DIST
   src/include/mc/datatypes.h
   src/include/mc/mc.h
   src/mc/mc_mmu.h
-  src/mc/mc_page_store.h
+  src/mc/PageStore.hpp
   src/mc/mc_record.h
   src/include/simgrid/platf_interface.h
   src/include/simgrid/sg_config.h
@@ -579,74 +579,73 @@ set(JEDULE_SRC
   )
 
 set(MC_SRC_BASE
-  src/mc/mc_base.c
+  src/mc/mc_base.cpp
   src/mc/mc_base.h
   src/mc/mc_record.h
-  src/mc/mc_record.c
-  src/mc/mc_config.c
-  src/mc/mc_global.c
+  src/mc/mc_replay.h
+  src/mc/mc_record.cpp
+  src/mc/mc_config.cpp
+  src/mc/mc_global.cpp
   )
 
 set(MC_SRC
   src/mc/mc_address_space.h
-  src/mc/mc_address_space.c
+  src/mc/mc_address_space.cpp
   src/mc/mc_forward.h
   src/mc/mc_process.h
-  src/mc/mc_process.c
+  src/mc/mc_process.cpp
   src/mc/mc_unw.h
-  src/mc/mc_unw.c
-  src/mc/mc_unw_vmread.c
+  src/mc/mc_unw.cpp
+  src/mc/mc_unw_vmread.cpp
   src/mc/mc_mmalloc.h
-  src/mc/mc_model_checker.h
-  src/mc/mc_model_checker.c
+  src/mc/ModelChecker.hpp
+  src/mc/ModelChecker.cpp
   src/mc/mc_object_info.h
-  src/mc/mc_object_info.c
-  src/mc/mc_checkpoint.c
+  src/mc/mc_object_info.cpp
+  src/mc/mc_checkpoint.cpp
   src/mc/mc_snapshot.h
-  src/mc/mc_snapshot.c
-  src/mc/mc_page_store.h
-  src/mc/mc_page_store.cpp
+  src/mc/mc_snapshot.cpp
+  src/mc/PageStore.hpp
+  src/mc/PageStore.cpp
   src/mc/mc_page_snapshot.cpp
   src/mc/mc_comm_pattern.h
-  src/mc/mc_comm_pattern.c
-  src/mc/mc_comm_determinism.c
+  src/mc/mc_comm_pattern.cpp
+  src/mc/mc_comm_determinism.cpp
   src/mc/mc_compare.cpp
-  src/mc/mc_diff.c
-  src/mc/mc_dwarf.c
+  src/mc/mc_diff.cpp
+  src/mc/mc_dwarf.cpp
   src/mc/mc_dwarf_attrnames.h
-  src/mc/mc_dwarf_expression.c
+  src/mc/mc_dwarf_expression.cpp
   src/mc/mc_dwarf_tagnames.h
-  src/mc/mc_hash.c
-  src/mc/mc_ignore.c
+  src/mc/mc_hash.cpp
+  src/mc/mc_ignore.cpp
   src/mc/mc_ignore.h
-  src/mc/mc_interface.h
   src/mc/mc_liveness.h
   src/mc/mc_location.h
-  src/mc/mc_liveness.c
-  src/mc/mc_record.c
-  src/mc/mc_member.c
-  src/mc/mc_memory.c
-  src/mc/mc_pair.c
+  src/mc/mc_liveness.cpp
+  src/mc/mc_record.cpp
+  src/mc/mc_member.cpp
+  src/mc/mc_memory.cpp
+  src/mc/mc_pair.cpp
   src/mc/mc_private.h
   src/mc/mc_request.h
-  src/mc/mc_request.c
+  src/mc/mc_request.cpp
   src/mc/mc_safety.h
-  src/mc/mc_safety.c
-  src/mc/mc_set.cpp
+  src/mc/mc_safety.cpp
   src/mc/mc_state.h
-  src/mc/mc_state.c
-  src/mc/mc_visited.c
+  src/mc/mc_state.cpp
+  src/mc/mc_visited.cpp
   src/mc/mc_memory_map.h
-  src/mc/memory_map.c
-  src/mc/mc_client.c
-  src/mc/mc_client_api.c
+  src/mc/memory_map.cpp
+  src/mc/mc_client.cpp
+  src/mc/mc_client_api.cpp
   src/mc/mc_client.h
   src/mc/mc_protocol.h
-  src/mc/mc_protocol.c
+  src/mc/mc_protocol.cpp
   src/mc/mc_server.cpp
   src/mc/mc_server.h
   src/mc/mc_smx.h
-  src/mc/mc_smx.c
+  src/mc/mc_smx.cpp
   )
 
 set(MC_SIMGRID_MC_SRC
index 27aa988..ec05853 100644 (file)
@@ -37,7 +37,7 @@ if(enable_compile_warnings)
     endif()
   endif()
 
-  set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wall -Wextra  -Wunused -Wpointer-arith -Wchar-subscripts -Wcomment -Wno-unknown-warning-option -Wformat -Wwrite-strings -Wno-unused-function -Wno-unused-parameter -Wno-strict-aliasing -Wclobbered -Wno-error=clobbered -Wno-format-nonliteral -Werror")
+  set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wall -Wextra  -Wunused -Wpointer-arith -Wchar-subscripts -Wcomment  -Wformat -Wwrite-strings -Wno-unused-function -Wno-unused-parameter -Wno-strict-aliasing -Wclobbered -Wno-error=clobbered -Wno-format-nonliteral -Werror")
 
   set(CMAKE_Fortran_FLAGS "${CMAKE_Fortran_FLAGS} -Wall") # FIXME: Q&D hack
 
index 4cfedb0..2435bf6 100644 (file)
@@ -30,12 +30,12 @@ set(TEST_UNITS
 
 if(HAVE_MC)
   set(TEST_CFILES ${TEST_CFILES}
-      src/mc/mc_page_store.cpp
-      src/mc/mc_snapshot.c
+      src/mc/PageStore.cpp
+      src/mc/mc_snapshot.cpp
       )
   set(TEST_UNITS ${TEST_UNITS}
-     ${CMAKE_CURRENT_BINARY_DIR}/src/mc_page_store_unit.cpp
-     ${CMAKE_CURRENT_BINARY_DIR}/src/mc_snapshot_unit.c
+     ${CMAKE_CURRENT_BINARY_DIR}/src/PageStore_unit.cpp
+     ${CMAKE_CURRENT_BINARY_DIR}/src/mc_snapshot_unit.cpp
      )
 endif()
 
index 2cf3234..ff34bf3 100644 (file)
@@ -10,6 +10,7 @@
 #include "xbt/asserts.h"
 #include "simgrid/modelchecker.h"
 #include <xbt/RngStream.h>
+#include "mc/mc_replay.h"
 
 /** @addtogroup MSG_examples
  *
index 0ebb4ec..cc85d75 100644 (file)
@@ -2,7 +2,7 @@
 
 ! timeout 60
 $ ../../../smpi_script/bin/smpirun -wrapper "${bindir:=.}/../../../bin/simgrid-mc" --log=xbt_cfg.thresh:warning -hostfile ${srcdir:=.}/hostfile_only_send_deterministic  -platform ${srcdir:=.}/../../platforms/cluster.xml --cfg=model-check:1 --cfg=model-check/communications_determinism:1 --cfg=smpi/send_is_detached_thres:0 --cfg=smpi/running_power:1e9 ./smpi_only_send_deterministic
-> [0.000000] [mc_global/INFO] Check communication determinism
+> [0.000000] [mc_comm_determinism/INFO] Check communication determinism
 > [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
 > [0.000000] [mc_global/INFO] ******************************************************
 > [0.000000] [mc_global/INFO] **** Only-send-deterministic communication pattern ****
index 3cc7e2d..15b877d 100644 (file)
 
 SG_BEGIN_DECL()
 
-/** Replay path (if any) in string representation
- *
- *  This is a path as generated by `MC_record_stack_to_string()`.
- */
-XBT_PUBLIC_DATA(char*) MC_record_path;
-
-/** Whether the replay mode is enabled */
-static inline bool MC_record_replay_is_active(void) {
-  return MC_record_path;
-}
-
 XBT_PUBLIC(int) MC_random(int min, int max);
 
 #ifdef HAVE_MC
index 31b5adb..1b34514 100644 (file)
@@ -284,11 +284,17 @@ xbt_dynar_foreach (dyn,cpt,str) {
       _xbt_dynar_cursor_get(_dynar,_cursor,&_data) ; \
             (_cursor)++         )
 
+#ifndef __cplusplus
 #define xbt_dynar_foreach_ptr(_dynar,_cursor,_ptr) \
        for (_xbt_dynar_cursor_first(_dynar,&(_cursor))       ; \
       (_ptr = _cursor < _dynar->used ? xbt_dynar_get_ptr(_dynar,_cursor) : NULL) ; \
             (_cursor)++         )
-
+#else
+#define xbt_dynar_foreach_ptr(_dynar,_cursor,_ptr) \
+       for (_xbt_dynar_cursor_first(_dynar,&(_cursor))       ; \
+      (_ptr = _cursor < _dynar->used ? (decltype(_ptr)) xbt_dynar_get_ptr(_dynar,_cursor) : NULL) ; \
+            (_cursor)++         )
+#endif
 /** @} */
 
 SG_END_DECL()
index df2bdfd..0017a38 100644 (file)
@@ -149,11 +149,17 @@ static XBT_INLINE void *xbt_swag_getFirst(xbt_swag_t swag)
   *  @param swag what to iterate over
   *  @warning you cannot modify the \a swag while using this loop
   *  @hideinitializer */
+#ifndef __cplusplus
 #define xbt_swag_foreach(obj,swag)                            \
    for((obj)=xbt_swag_getFirst((swag));                       \
        (obj)!=NULL;                                           \
        (obj)=xbt_swag_getNext((obj),(swag)->offset))
-
+#else
+#define xbt_swag_foreach(obj,swag)                            \
+   for((obj)=(decltype(obj)) xbt_swag_getFirst((swag));         \
+       (obj)!=NULL;                                           \
+       (obj)=(decltype(obj)) xbt_swag_getNext((obj),(swag)->offset))
+#endif
 /**
  * @brief A safe swag iterator 
  * @param obj the indice of the loop
index 23be47f..7cce56c 100644 (file)
@@ -40,7 +40,6 @@ extern int _sg_do_model_check;
 extern int _sg_do_model_check_record;
 extern int _sg_mc_checkpoint;
 extern int _sg_mc_sparse_checkpoint;
-extern int _sg_mc_soft_dirty;
 extern char* _sg_mc_property_file;
 extern int _sg_mc_timeout;
 extern int _sg_mc_hash;
@@ -61,7 +60,6 @@ extern xbt_dynar_t stacks_areas;
 void _mc_cfg_cb_reduce(const char *name, int pos);
 void _mc_cfg_cb_checkpoint(const char *name, int pos);
 void _mc_cfg_cb_sparse_checkpoint(const char *name, int pos);
-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);
@@ -73,7 +71,7 @@ void _mc_cfg_cb_comms_determinism(const char *name, int pos);
 void _mc_cfg_cb_send_determinism(const char *name, int pos);
 void _mc_cfg_cb_termination(const char *name, int pos);
 
-XBT_PUBLIC(void) MC_do_the_modelcheck_for_real(void);
+XBT_PUBLIC(void) MC_run(void);
 XBT_PUBLIC(void) MC_init(void);
 XBT_PUBLIC(void) MC_exit(void);
 XBT_PUBLIC(void) MC_process_clock_add(smx_process_t, double);
diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
new file mode 100644 (file)
index 0000000..b78bf83
--- /dev/null
@@ -0,0 +1,45 @@
+/* Copyright (c) 2008-2015. The SimGrid Team.
+ * All rights reserved.                                                     */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#include <cassert>
+
+#include "ModelChecker.hpp"
+#include "PageStore.hpp"
+
+::simgrid::mc::ModelChecker* mc_model_checker = NULL;
+
+namespace simgrid {
+namespace mc {
+
+ModelChecker::ModelChecker(pid_t pid, int socket)
+  : page_store_(500)
+{
+  this->hostnames_ = xbt_dict_new();
+  MC_process_init(&this->process(), pid, socket);
+}
+
+ModelChecker::~ModelChecker()
+{
+  MC_process_clear(&this->process_);
+  xbt_dict_free(&this->hostnames_);
+}
+
+const char* ModelChecker::get_host_name(const char* hostname)
+{
+  // Lookup the host name in the dictionary (or create it):
+  xbt_dictelm_t elt = xbt_dict_get_elm_or_null(this->hostnames_, hostname);
+  if (!elt) {
+    xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
+    xbt_dict_set(this->hostnames_, hostname, NULL, NULL);
+    elt = xbt_dict_get_elm_or_null(this->hostnames_, hostname);
+    assert(elt);
+    mmalloc_set_current_heap(heap);
+  }
+  return elt->key;
+}
+
+}
+}
diff --git a/src/mc/ModelChecker.hpp b/src/mc/ModelChecker.hpp
new file mode 100644 (file)
index 0000000..4e3a565
--- /dev/null
@@ -0,0 +1,56 @@
+/* Copyright (c) 2007-2015. The SimGrid Team.
+ * All rights reserved.                                                     */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+#ifndef MC_MODEL_CHECKER_H
+#define MC_MODEL_CHECKER_H
+
+#include <sys/types.h>
+
+#include <simgrid_config.h>
+#include <xbt/dynar.h>
+
+#include "mc_forward.h"
+#include "mc_process.h"
+#include "PageStore.hpp"
+#include "mc_protocol.h"
+
+namespace simgrid {
+namespace mc {
+
+/** State of the model-checker (global variables for the model checker)
+ *
+ *  Each part of the state of the model chercker represented as a global
+ *  variable prevents some sharing between snapshots and must be ignored.
+ *  By moving as much state as possible in this structure allocated
+ *  on the model-checker heap, we avoid those issues.
+ */
+class ModelChecker {
+  // This is the parent snapshot of the current state:
+  s_mc_pages_store_t page_store_;
+  s_mc_process_t process_;
+  /** String pool for host names */
+  // TODO, use std::unordered_set with heterogeneous comparison lookup (C++14)
+  xbt_dict_t /* <hostname, NULL> */ hostnames_;
+public:
+  ModelChecker(ModelChecker const&) = delete;
+  ModelChecker& operator=(ModelChecker const&) = delete;
+  ModelChecker(pid_t pid, int socket);
+  ~ModelChecker();
+  s_mc_process_t& process()
+  {
+    return process_;
+  }
+  PageStore& page_store()
+  {
+    return page_store_;
+  }
+  const char* get_host_name(const char* name);
+};
+
+}
+}
+
+#endif
similarity index 90%
rename from src/mc/mc_page_store.cpp
rename to src/mc/PageStore.cpp
index 222f3a7..05df2a8 100644 (file)
@@ -1,4 +1,4 @@
-/* Copyright (c) 2014. The SimGrid Team.
+/* Copyright (c) 2015. The SimGrid Team.
  * All rights reserved.                                                     */
 
 /* This program is free software; you can redistribute it and/or modify it
@@ -13,7 +13,7 @@
 
 #include <xbt.h>
 
-#include "mc_page_store.h"
+#include "PageStore.hpp"
 
 #ifdef MC_PAGE_STORE_MD4
 #include <nettle/md4.h>
 
 #include "mc_mmu.h"
 
+extern "C" {
+
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_page_snapshot, mc,
                                 "Logging specific to mc_page_snapshot");
 
-// ***** Utility:
+namespace simgrid {
+namespace mc {
 
 /** @brief Compte a hash for the given memory page
  *
@@ -35,7 +38,7 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_page_snapshot, mc,
  *  @return hash off the page
  */
 static inline  __attribute__ ((always_inline))
-s_mc_pages_store::hash_type mc_hash_page(const void* data)
+PageStore::hash_type mc_hash_page(const void* data)
 {
 #ifdef MC_PAGE_STORE_MD4
    boost::array<uint64_t,2> result;
@@ -59,7 +62,7 @@ s_mc_pages_store::hash_type mc_hash_page(const void* data)
 
 // ***** snapshot_page_manager
 
-s_mc_pages_store::s_mc_pages_store(size_t size) :
+PageStore::PageStore(size_t size) :
   memory_(NULL), capacity_(0), top_index_(0)
 {
   // Using mmap in order to be able to expand the region
@@ -76,12 +79,12 @@ s_mc_pages_store::s_mc_pages_store(size_t size) :
   this->page_counts_.resize(size);
 }
 
-s_mc_pages_store::~s_mc_pages_store()
+PageStore::~PageStore()
 {
   ::munmap(this->memory_, this->capacity_ << xbt_pagebits);
 }
 
-void s_mc_pages_store::resize(size_t size)
+void PageStore::resize(size_t size)
 {
   size_t old_bytesize = this->capacity_ << xbt_pagebits;
   size_t new_bytesize = size << xbt_pagebits;
@@ -102,7 +105,7 @@ void s_mc_pages_store::resize(size_t size)
  *
  *  @return index of the free page
  */
-size_t s_mc_pages_store::alloc_page()
+size_t PageStore::alloc_page()
 {
   if (this->free_pages_.empty()) {
 
@@ -125,7 +128,7 @@ size_t s_mc_pages_store::alloc_page()
   }
 }
 
-void s_mc_pages_store::remove_page(size_t pageno)
+void PageStore::remove_page(size_t pageno)
 {
   this->free_pages_.push_back(pageno);
   const void* page = this->get_page(pageno);
@@ -138,7 +141,7 @@ void s_mc_pages_store::remove_page(size_t pageno)
 }
 
 /** Store a page in memory */
-size_t s_mc_pages_store::store_page(void* page)
+size_t PageStore::store_page(void* page)
 {
   xbt_assert(top_index_ <= this->capacity_, "top_index is not consistent");
 
@@ -190,20 +193,7 @@ size_t s_mc_pages_store::store_page(void* page)
   return pageno;
 }
 
-// ***** Main C API
-
-extern "C" {
-
-mc_pages_store_t mc_pages_store_new()
-{
-  return new s_mc_pages_store_t(500);
-}
-
-void mc_pages_store_delete(mc_pages_store_t store)
-{
-  delete store;
 }
-
 }
 
 #ifdef SIMGRID_TEST
@@ -216,7 +206,7 @@ void mc_pages_store_delete(mc_pages_store_t store)
 
 #include <memory>
 
-#include "mc/mc_page_store.h"
+#include "mc/PageStore.hpp"
 
 static int value = 0;
 
@@ -238,7 +228,8 @@ XBT_TEST_UNIT("base", test_mc_page_store, "Test adding/removing pages in the sto
 {
   xbt_test_add("Init");
   size_t pagesize = (size_t) getpagesize();
-  std::unique_ptr<s_mc_pages_store_t> store = std::unique_ptr<s_mc_pages_store_t>(new s_mc_pages_store(500));
+  std::unique_ptr<simgrid::mc::PageStore> store
+    = std::unique_ptr<simgrid::mc::PageStore>(new simgrid::mc::PageStore(500));
   void* data = getpage();
   xbt_test_assert(store->size()==0, "Bad size");
 
@@ -280,3 +271,5 @@ XBT_TEST_UNIT("base", test_mc_page_store, "Test adding/removing pages in the sto
 }
 
 #endif /* SIMGRID_TEST */
+
+}
similarity index 88%
rename from src/mc/mc_page_store.h
rename to src/mc/PageStore.hpp
index 2f79705..3491f58 100644 (file)
@@ -1,4 +1,4 @@
-/* Copyright (c) 2014. The SimGrid Team.
+/* Copyright (c) 2015. The SimGrid Team.
  * All rights reserved.                                                     */
 
 /* This program is free software; you can redistribute it and/or modify it
@@ -23,9 +23,8 @@
 #ifndef MC_PAGE_STORE_H
 #define MC_PAGE_STORE_H
 
-struct s_mc_pages_store;
-
-#ifdef __cplusplus
+namespace simgrid {
+namespace mc {
 
 /** @brief Storage for snapshot memory pages
  *
@@ -79,7 +78,7 @@ struct s_mc_pages_store;
  *    we must be able to store multiple indices for the same hash.
  *
  */
-struct s_mc_pages_store {
+class PageStore {
 public: // Types
 #ifdef MC_PAGE_STORE_MD4
   typedef boost::array<uint64_t,2> hash_type;
@@ -123,8 +122,10 @@ private: // Methods
   void remove_page(size_t pageno);
 
 public: // Constructors
-  explicit s_mc_pages_store(size_t size);
-  ~s_mc_pages_store();
+  PageStore(PageStore const&) = delete;
+  PageStore& operator=(PageStore const&) = delete;
+  explicit PageStore(size_t size);
+  ~PageStore();
 
 public: // Methods
 
@@ -178,54 +179,38 @@ public: // Debug/test methods
 };
 
 inline __attribute__((always_inline))
-void s_mc_pages_store::unref_page(size_t pageno) {
+void PageStore::unref_page(size_t pageno) {
   if ((--this->page_counts_[pageno]) == 0) {
     this->remove_page(pageno);
   }
 }
 
 inline __attribute__((always_inline))
-void s_mc_pages_store::ref_page(size_t pageno) {
+void PageStore::ref_page(size_t pageno) {
   ++this->page_counts_[pageno];
 }
 
 inline __attribute__((always_inline))
-const void* s_mc_pages_store::get_page(size_t pageno) const {
+const void* PageStore::get_page(size_t pageno) const {
   return mc_page_from_number(this->memory_, pageno);
 }
 
 inline __attribute__((always_inline))
-size_t s_mc_pages_store::get_ref(size_t pageno)  {
+size_t PageStore::get_ref(size_t pageno)  {
   return this->page_counts_[pageno];
 }
 
 inline __attribute__((always_inline))
-size_t s_mc_pages_store::size() {
+size_t PageStore::size() {
   return this->top_index_ - this->free_pages_.size();
 }
 
 inline __attribute__((always_inline))
-size_t s_mc_pages_store::capacity() {
+size_t PageStore::capacity() {
   return this->capacity_;
 }
 
-#endif
-
-SG_BEGIN_DECL()
-
-mc_pages_store_t mc_pages_store_new(void);
-void mc_pages_store_delete(mc_pages_store_t store);
-
-/**
- */
-static inline __attribute__((always_inline))
-const void* mc_page_store_get_page(mc_pages_store_t page_store, size_t pageno)
-{
-  // This is page_store->memory_:
-  void* memory = *(void**)page_store;
-  return mc_page_from_number(memory, pageno);
 }
-
-SG_END_DECL()
+}
 
 #endif
index a8724bc..a64b07c 100644 (file)
@@ -7,22 +7,25 @@
 #ifndef MC_ADDRESS_SPACE_H
 #define MC_ADDRESS_SPACE_H
 
+#include <xbt/misc.h>
+
 #include <stdint.h>
 
 #include "mc_forward.h"
 
-// ***** Data types
+SG_BEGIN_DECL()
 
-typedef enum e_adress_space_read_flags {
-  MC_ADDRESS_SPACE_READ_FLAGS_NONE = 0,
+// ***** Data types
 
-  /** Avoid a copy for when the data is available in the current process.
-   *
-   *  In this case, the return value of a MC_address_space_read might
-   *  be different from the provided buffer.
-   */
-  MC_ADDRESS_SPACE_READ_FLAGS_LAZY = 1
-} e_adress_space_read_flags_t;
+/** Options for the read() operation
+ *
+ *  - MC_ADDRESS_SPACE_READ_FLAGS_LAZY, avoid a copy when the data is
+ *    available in the current process. In this case, the return value
+ *    of MC_address_space_read might be different from the provided one.
+ */
+typedef int adress_space_read_flags_t;
+#define MC_ADDRESS_SPACE_READ_FLAGS_NONE 0
+#define MC_ADDRESS_SPACE_READ_FLAGS_LAZY 1
 
 /** Process index used when no process is available
  *
@@ -56,21 +59,27 @@ struct s_mc_address_space {
  */
 struct s_mc_address_space_class {
   const void* (*read)(
-    mc_address_space_t address_space, e_adress_space_read_flags_t flags,
+    mc_address_space_t address_space, adress_space_read_flags_t flags,
     void* target, const void* addr, size_t size,
     int process_index);
   mc_process_t (*get_process)(mc_address_space_t address_space);
 };
 
+typedef const void* (*mc_address_space_class_read_callback_t)(
+  mc_address_space_t address_space, adress_space_read_flags_t flags,
+  void* target, const void* addr, size_t size,
+  int process_index);
+typedef mc_process_t (*mc_address_space_class_get_process_callback_t)(mc_address_space_t address_space);
+
 // ***** Virtual/non-final methods
 
 /** Read data from the given address space
  *
- *  Dynamic dispatch.
+ *  Dysnamic dispatch.
  */
 static inline __attribute__((always_inline))
 const void* MC_address_space_read(
-  mc_address_space_t address_space, e_adress_space_read_flags_t flags,
+  mc_address_space_t address_space, adress_space_read_flags_t flags,
   void* target, const void* addr, size_t size,
   int process_index)
 {
@@ -82,8 +91,12 @@ const void* MC_address_space_read(
 static inline __attribute__((always_inline))
 const void* MC_address_space_get_process(mc_address_space_t address_space)
 {
-  return address_space->address_space_class->get_process(address_space);
+  if (address_space->address_space_class->get_process)
+    return address_space->address_space_class->get_process(address_space);
+  else
+    return NULL;
 }
 
+SG_END_DECL()
 
 #endif
similarity index 78%
rename from src/mc/mc_base.c
rename to src/mc/mc_base.cpp
index 65052ef..9144932 100644 (file)
 
 #include "mc_base.h"
 #include "../simix/smx_private.h"
-#include "mc_record.h"
+#include "mc/mc_record.h"
+#include "mc/mc_replay.h"
+#include "mc/mc.h"
 
 #ifdef HAVE_MC
 #include "mc_process.h"
-#include "mc_model_checker.h"
+#include "ModelChecker.hpp"
 #include "mc_protocol.h"
 #include "mc_smx.h"
 #include "mc_server.h"
 #endif
 
+extern "C" {
+
 XBT_LOG_NEW_CATEGORY(mc, "All MC categories");
 
 void MC_wait_for_requests(void)
 {
 #ifdef HAVE_MC
   if (mc_mode == MC_MODE_SERVER) {
-    MC_server_wait_client(&mc_model_checker->process);
+    MC_server_wait_client(&mc_model_checker->process());
     return;
   }
 #endif
@@ -63,8 +67,8 @@ int MC_request_is_enabled(smx_simcall_t req)
 
 #ifdef HAVE_MC
     // Fetch from MCed memory:
-    if (!MC_process_is_self(&mc_model_checker->process)) {
-      MC_process_read(&mc_model_checker->process, MC_PROCESS_NO_FLAG,
+    if (!MC_process_is_self(&mc_model_checker->process())) {
+      MC_process_read(&mc_model_checker->process(), MC_ADDRESS_SPACE_READ_FLAGS_NONE,
         &temp_synchro, act, sizeof(temp_synchro),
         MC_PROCESS_INDEX_ANY);
       act = &temp_synchro;
@@ -88,13 +92,13 @@ int MC_request_is_enabled(smx_simcall_t req)
 #ifdef HAVE_MC
     // Read dynar:
     s_xbt_dynar_t comms;
-    MC_process_read_simple(&mc_model_checker->process,
+    MC_process_read_simple(&mc_model_checker->process(),
       &comms, simcall_comm_waitany__get__comms(req), sizeof(comms));
     // Read dynar buffer:
     assert(comms.elmsize == sizeof(act));
     size_t buffer_size = comms.elmsize * comms.used;
     char buffer[buffer_size];
-    MC_process_read_simple(&mc_model_checker->process,
+    MC_process_read_simple(&mc_model_checker->process(),
       buffer, comms.data, sizeof(buffer));
 #endif
 
@@ -107,8 +111,8 @@ int MC_request_is_enabled(smx_simcall_t req)
 
 #ifdef HAVE_MC
       // Fetch from MCed memory:
-      if (!MC_process_is_self(&mc_model_checker->process)) {
-        MC_process_read(&mc_model_checker->process, MC_PROCESS_NO_FLAG,
+      if (!MC_process_is_self(&mc_model_checker->process())) {
+        MC_process_read(&mc_model_checker->process(), MC_ADDRESS_SPACE_READ_FLAGS_NONE,
           &temp_synchro, act, sizeof(temp_synchro),
           MC_PROCESS_INDEX_ANY);
         act = &temp_synchro;
@@ -125,8 +129,8 @@ int MC_request_is_enabled(smx_simcall_t req)
     smx_mutex_t mutex = simcall_mutex_lock__get__mutex(req);
 #ifdef HAVE_MC
     s_smx_mutex_t temp_mutex;
-    if (!MC_process_is_self(&mc_model_checker->process)) {
-      MC_process_read(&mc_model_checker->process, MC_PROCESS_NO_FLAG,
+    if (!MC_process_is_self(&mc_model_checker->process())) {
+      MC_process_read(&mc_model_checker->process(), MC_ADDRESS_SPACE_READ_FLAGS_NONE,
         &temp_mutex, mutex, sizeof(temp_mutex),
         MC_PROCESS_INDEX_ANY);
       mutex = &temp_mutex;
@@ -181,12 +185,12 @@ static int prng_random(int min, int max)
   unsigned long accept_size = input_size - reject_size; // module*accept_size
 
   // Use rejection in order to avoid skew
-  long x;
+  unsigned long x;
   do {
 #ifndef _XBT_WIN32
-    x = random();
+    x = (unsigned long) random();
 #else
-    x = rand();
+    x = (unsigned long) rand();
 #endif
   } while( x >= accept_size );
   return min + (x % output_size);
@@ -200,3 +204,29 @@ int simcall_HANDLER_mc_random(smx_simcall_t simcall, int min, int max)
 
   return simcall->mc_value;
 }
+
+void MC_simcall_handle(smx_simcall_t req, int value)
+{
+#ifndef HAVE_MC
+  SIMIX_simcall_handle(req, value);
+#else
+  if (MC_process_is_self(&mc_model_checker->process())) {
+    SIMIX_simcall_handle(req, value);
+    return;
+  }
+
+  unsigned i;
+  mc_smx_process_info_t pi = NULL;
+
+  xbt_dynar_foreach_ptr(mc_model_checker->process().smx_process_infos, i, pi) {
+    if (req == &pi->copy.simcall) {
+      MC_server_simcall_handle(&mc_model_checker->process(), pi->copy.pid, value);
+      return;
+    }
+  }
+
+  xbt_die("Could not find the request");
+#endif
+}
+
+}
index c21a00b..d972c52 100644 (file)
@@ -7,6 +7,7 @@
 #ifndef MC_BASE_H
 #define MC_BASE_H
 
+#include <xbt/misc.h>
 #include <simgrid/simix.h>
 #include "simgrid_config.h"
 #include "internal_config.h"
similarity index 84%
rename from src/mc/mc_checkpoint.c
rename to src/mc/mc_checkpoint.cpp
index b2a0538..1fc08e1 100644 (file)
@@ -4,8 +4,6 @@
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
-#define _GNU_SOURCE
-
 #include <unistd.h>
 
 #include <string.h>
@@ -37,6 +35,8 @@
 #include "mc_protocol.h"
 #include "mc_smx.h"
 
+extern "C" {
+
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_checkpoint, mc,
                                 "Logging specific to mc_checkpoint");
 
@@ -116,7 +116,7 @@ void MC_free_snapshot(mc_snapshot_t snapshot)
 
 static mc_mem_region_t mc_region_new_dense(
   mc_region_type_t region_type,
-  void *start_addr, void* permanent_addr, size_t size, mc_mem_region_t ref_reg)
+  void *start_addr, void* permanent_addr, size_t size)
 {
   mc_mem_region_t region = xbt_new(s_mc_mem_region_t, 1);
   region->region_type = region_type;
@@ -125,7 +125,7 @@ static mc_mem_region_t mc_region_new_dense(
   region->permanent_addr = permanent_addr;
   region->size = size;
   region->flat.data = xbt_malloc(size);
-  MC_process_read(&mc_model_checker->process, MC_ADDRESS_SPACE_READ_FLAGS_NONE,
+  MC_process_read(&mc_model_checker->process(), MC_ADDRESS_SPACE_READ_FLAGS_NONE,
     region->flat.data, permanent_addr, size,
     MC_PROCESS_INDEX_DISABLED);
   XBT_DEBUG("New region : type : %d, data : %p (real addr %p), size : %zu",
@@ -139,28 +139,22 @@ static mc_mem_region_t mc_region_new_dense(
  * @param start_addr   Address of the region in the simulated process
  * @param permanent_addr Permanent address of this data (for privatized variables, this is the virtual address of the privatized mapping)
  * @param size         Size of the data*
- * @param ref_reg      Reference corresponding region
  */
-static mc_mem_region_t MC_region_new(mc_region_type_t type, void *start_addr, void* permanent_addr, size_t size, mc_mem_region_t ref_reg)
+static mc_mem_region_t MC_region_new(
+  mc_region_type_t type, void *start_addr, void* permanent_addr, size_t size)
 {
   if (_sg_mc_sparse_checkpoint) {
-    return mc_region_new_sparse(type, start_addr, permanent_addr, size, ref_reg);
+    return mc_region_new_sparse(type, start_addr, permanent_addr, size);
   } else  {
-    return mc_region_new_dense(type, start_addr, permanent_addr, size, ref_reg);
+    return mc_region_new_dense(type, start_addr, permanent_addr, size);
   }
 }
 
 /** @brief Restore a region from a snapshot
  *
- *  If we are using per page snapshots, it is possible to use the reference
- *  region in order to do an incremental restoration of the region: the
- *  softclean pages which are shared between the two snapshots do not need
- *  to be restored.
- *
  *  @param reg     Target region
- *  @param reg_reg Current region (if not NULL), used for lazy per page restoration
  */
-static void MC_region_restore(mc_mem_region_t region, mc_mem_region_t ref_region)
+static void MC_region_restore(mc_mem_region_t region)
 {
   switch(region->storage_type) {
   case MC_REGION_STORAGE_TYPE_NONE:
@@ -169,22 +163,19 @@ static void MC_region_restore(mc_mem_region_t region, mc_mem_region_t ref_region
     break;
 
   case MC_REGION_STORAGE_TYPE_FLAT:
-    MC_process_write(&mc_model_checker->process, region->flat.data,
+    MC_process_write(&mc_model_checker->process(), region->flat.data,
       region->permanent_addr, region->size);
     break;
 
   case MC_REGION_STORAGE_TYPE_CHUNKED:
-    mc_region_restore_sparse(&mc_model_checker->process, region, ref_region);
+    mc_region_restore_sparse(&mc_model_checker->process(), region);
     break;
 
   case MC_REGION_STORAGE_TYPE_PRIVATIZED:
     {
-      bool has_ref_regions = ref_region &&
-        ref_region->storage_type == MC_REGION_STORAGE_TYPE_PRIVATIZED;
       size_t process_count = region->privatized.regions_count;
       for (size_t i = 0; i < process_count; i++) {
-        MC_region_restore(region->privatized.regions[i],
-          has_ref_regions ? ref_region->privatized.regions[i] : NULL);
+        MC_region_restore(region->privatized.regions[i]);
       }
       break;
     }
@@ -192,8 +183,8 @@ static void MC_region_restore(mc_mem_region_t region, mc_mem_region_t ref_region
 }
 
 static mc_mem_region_t MC_region_new_privatized(
-    mc_region_type_t region_type, void *start_addr, void* permanent_addr, size_t size,
-    mc_mem_region_t ref_reg)
+    mc_region_type_t region_type, void *start_addr, void* permanent_addr, size_t size
+    )
 {
   size_t process_count = MC_smpi_process_count();
   mc_mem_region_t region = xbt_new(s_mc_mem_region_t, 1);
@@ -207,21 +198,17 @@ static mc_mem_region_t MC_region_new_privatized(
 
   // Read smpi_privatisation_regions from MCed:
   smpi_privatisation_region_t remote_smpi_privatisation_regions;
-  MC_process_read_variable(&mc_model_checker->process,
+  MC_process_read_variable(&mc_model_checker->process(),
     "smpi_privatisation_regions",
     &remote_smpi_privatisation_regions, sizeof(remote_smpi_privatisation_regions));
   s_smpi_privatisation_region_t privatisation_regions[process_count];
-  MC_process_read_simple(&mc_model_checker->process, &privatisation_regions,
+  MC_process_read_simple(&mc_model_checker->process(), &privatisation_regions,
     remote_smpi_privatisation_regions, sizeof(privatisation_regions));
 
   for (size_t i = 0; i < process_count; i++) {
-    mc_mem_region_t ref_subreg = NULL;
-    if (ref_reg && ref_reg->storage_type == MC_REGION_STORAGE_TYPE_PRIVATIZED)
-      ref_subreg = ref_reg->privatized.regions[i];
     region->privatized.regions[i] =
       MC_region_new(region_type, start_addr,
-        privatisation_regions[i].address, size,
-        ref_subreg);
+        privatisation_regions[i].address, size);
   }
 
   return region;
@@ -236,16 +223,12 @@ static void MC_snapshot_add_region(int index, mc_snapshot_t snapshot, mc_region_
   else if (type == MC_REGION_TYPE_HEAP)
     xbt_assert(!object_info, "Unexpected object info for heap region.");
 
-  mc_mem_region_t ref_reg = NULL;
-  if (mc_model_checker->parent_snapshot)
-    ref_reg = mc_model_checker->parent_snapshot->snapshot_regions[index];
-
   mc_mem_region_t region;
   const bool privatization_aware = MC_object_info_is_privatized(object_info);
   if (privatization_aware && MC_smpi_process_count())
-    region = MC_region_new_privatized(type, start_addr, permanent_addr, size, ref_reg);
+    region = MC_region_new_privatized(type, start_addr, permanent_addr, size);
   else
-    region = MC_region_new(type, start_addr, permanent_addr, size, ref_reg);
+    region = MC_region_new(type, start_addr, permanent_addr, size);
 
   region->object_info = object_info;
   snapshot->snapshot_regions[index] = region;
@@ -279,7 +262,7 @@ static void MC_get_memory_regions(mc_process_t process, mc_snapshot_t snapshot)
 #ifdef HAVE_SMPI
   if (smpi_privatize_global_variables && MC_smpi_process_count()) {
     // snapshot->privatization_index = smpi_loaded_page
-    MC_process_read_variable(&mc_model_checker->process,
+    MC_process_read_variable(&mc_model_checker->process(),
       "smpi_loaded_page", &snapshot->privatization_index,
       sizeof(snapshot->privatization_index));
   } else
@@ -295,7 +278,7 @@ static void MC_get_memory_regions(mc_process_t process, mc_snapshot_t snapshot)
  * */
 void MC_find_object_address(memory_map_t maps, mc_object_info_t result)
 {
-  unsigned int i = 0;
+  ssize_t i = 0;
   s_map_region_t reg;
   const char *name = basename(result->file_name);
   while (i < maps->mapsize) {
@@ -307,26 +290,26 @@ void MC_find_object_address(memory_map_t maps, mc_object_info_t result)
       xbt_assert(!result->start_rw,
                  "Multiple read-write segments for %s, not supported",
                  maps->regions[i].pathname);
-      result->start_rw = reg.start_addr;
-      result->end_rw = reg.end_addr;
+      result->start_rw = (char*) reg.start_addr;
+      result->end_rw = (char*) reg.end_addr;
       // .bss is usually after the .data:
       s_map_region_t *next = &(maps->regions[i + 1]);
       if (next->pathname == NULL && (next->prot & PROT_WRITE)
           && next->start_addr == reg.end_addr) {
-        result->end_rw = maps->regions[i + 1].end_addr;
+        result->end_rw = (char*) maps->regions[i + 1].end_addr;
       }
     } else if ((reg.prot & PROT_READ) && (reg.prot & PROT_EXEC)) {
       xbt_assert(!result->start_exec,
                  "Multiple executable segments for %s, not supported",
                  maps->regions[i].pathname);
-      result->start_exec = reg.start_addr;
-      result->end_exec = reg.end_addr;
+      result->start_exec = (char*) reg.start_addr;
+      result->end_exec = (char*) reg.end_addr;
     } else if ((reg.prot & PROT_READ) && !(reg.prot & PROT_EXEC)) {
       xbt_assert(!result->start_ro,
                  "Multiple read only segments for %s, not supported",
                  maps->regions[i].pathname);
-      result->start_ro = reg.start_addr;
-      result->end_ro = reg.end_addr;
+      result->start_ro = (char*) reg.start_addr;
+      result->end_ro = (char*) reg.end_addr;
     }
     i++;
   }
@@ -373,7 +356,7 @@ static bool mc_valid_variable(dw_variable_t var, dw_frame_t scope,
 static void mc_fill_local_variables_values(mc_stack_frame_t stack_frame,
                                            dw_frame_t scope, int process_index, xbt_dynar_t result)
 {
-  mc_process_t process = &mc_model_checker->process;
+  mc_process_t process = &mc_model_checker->process();
 
   void *ip = (void *) stack_frame->ip;
   if (ip < scope->low_pc || ip >= scope->high_pc)
@@ -409,7 +392,7 @@ static void mc_fill_local_variables_values(mc_stack_frame_t stack_frame,
         current_variable->object_info,
         &(stack_frame->unw_cursor),
         (void *) stack_frame->frame_base,
-        (mc_address_space_t) &mc_model_checker->process, process_index);
+        (mc_address_space_t) &mc_model_checker->process(), process_index);
 
       switch(mc_get_location_type(&location)) {
       case MC_LOCATION_TYPE_ADDRESS:
@@ -460,7 +443,7 @@ static void MC_stack_frame_free_voipd(void *s)
 
 static xbt_dynar_t MC_unwind_stack_frames(mc_unw_context_t stack_context)
 {
-  mc_process_t process = &mc_model_checker->process;
+  mc_process_t process = &mc_model_checker->process();
   xbt_dynar_t result =
       xbt_dynar_new(sizeof(mc_stack_frame_t), MC_stack_frame_free_voipd);
 
@@ -538,11 +521,11 @@ static xbt_dynar_t MC_take_snapshot_stacks(mc_snapshot_t * snapshot)
 
     // Read the context from remote process:
     unw_context_t context;
-    MC_process_read_simple(&mc_model_checker->process,
+    MC_process_read_simple(&mc_model_checker->process(),
       &context, (unw_context_t*) current_stack->context, sizeof(context));
 
     st->context = xbt_new0(s_mc_unw_context_t, 1);
-    if (mc_unw_init_context(st->context, &mc_model_checker->process,
+    if (mc_unw_init_context(st->context, &mc_model_checker->process(),
       &context) < 0) {
       xbt_die("Could not initialise the libunwind context.");
     }
@@ -554,7 +537,7 @@ static xbt_dynar_t MC_take_snapshot_stacks(mc_snapshot_t * snapshot)
     unw_word_t sp = xbt_dynar_get_as(st->stack_frames, 0, mc_stack_frame_t)->sp;
 
     xbt_dynar_push(res, &st);
-    (*snapshot)->stack_sizes =
+    (*snapshot)->stack_sizes = (size_t*)
         xbt_realloc((*snapshot)->stack_sizes, (cursor + 1) * sizeof(size_t));
     (*snapshot)->stack_sizes[cursor] =
       (char*) current_stack->address + current_stack->size - (char*) sp;
@@ -604,7 +587,7 @@ static void MC_snapshot_handle_ignore(mc_snapshot_t snapshot)
   // Copy the memory:
   unsigned int cursor = 0;
   mc_checkpoint_ignore_region_t region;
-  xbt_dynar_foreach (mc_model_checker->process.checkpoint_ignore, cursor, region) {
+  xbt_dynar_foreach (mc_model_checker->process().checkpoint_ignore, cursor, region) {
     s_mc_snapshot_ignored_data_t ignored_data;
     ignored_data.start = region->addr;
     ignored_data.size = region->size;
@@ -617,7 +600,7 @@ static void MC_snapshot_handle_ignore(mc_snapshot_t snapshot)
   }
 
   // Zero the memory:
-  xbt_dynar_foreach (mc_model_checker->process.checkpoint_ignore, cursor, region) {
+  xbt_dynar_foreach (mc_model_checker->process().checkpoint_ignore, cursor, region) {
     MC_process_clear_memory(snapshot->process, region->addr, region->size);
   }
 
@@ -633,25 +616,6 @@ static void MC_snapshot_ignore_restore(mc_snapshot_t snapshot)
   }
 }
 
-/** @brief Can we remove this snapshot?
- *
- * Some snapshots cannot be removed (yet) because we need them
- * at this point.
- *
- * @param snapshot
- */
-int mc_important_snapshot(mc_snapshot_t snapshot)
-{
-  // We need this snapshot in order to know which
-  // pages needs to be stored in the next snapshot.
-  // This field is only non-NULL when using soft-dirty
-  // page tracking.
-  if (snapshot == mc_model_checker->parent_snapshot)
-    return true;
-
-  return false;
-}
-
 static void MC_get_current_fd(mc_snapshot_t snapshot)
 {
 
@@ -659,8 +623,10 @@ static void MC_get_current_fd(mc_snapshot_t snapshot)
 
   const size_t fd_dir_path_size = 20;
   char fd_dir_path[fd_dir_path_size];
-  if (snprintf(fd_dir_path, fd_dir_path_size,
-    "/proc/%lli/fd", (long long int) snapshot->process->pid) > fd_dir_path_size)
+  int res = snprintf(fd_dir_path, fd_dir_path_size,
+    "/proc/%lli/fd", (long long int) snapshot->process->pid);
+  xbt_assert(res >= 0);
+  if ((size_t) res > fd_dir_path_size)
     xbt_die("Unexpected buffer is too small for fd_dir_path");
 
   DIR* fd_dir = opendir(fd_dir_path);
@@ -678,13 +644,15 @@ static void MC_get_current_fd(mc_snapshot_t snapshot)
 
     const size_t source_size = 25;
     char source[25];
-    if (snprintf(source, source_size, "/proc/%lli/fd/%s",
-        (long long int) snapshot->process->pid, fd_number->d_name) > source_size)
+    int res = snprintf(source, source_size, "/proc/%lli/fd/%s",
+        (long long int) snapshot->process->pid, fd_number->d_name);
+    xbt_assert(res >= 0);
+    if ((size_t) res > source_size)
       xbt_die("Unexpected buffer is too small for fd %s", fd_number->d_name);
 
     const size_t link_size = 200;
     char link[200];
-    int res = readlink(source, link, link_size);
+    res = readlink(source, link, link_size);
     if (res<0) {
       xbt_die("Could not read link for %s", source);
     }
@@ -720,7 +688,7 @@ static void MC_get_current_fd(mc_snapshot_t snapshot)
     fd->number = fd_value;
     fd->flags = fcntl(fd_value, F_GETFL) | fcntl(fd_value, F_GETFD) ;
     fd->current_position = lseek(fd_value, 0, SEEK_CUR);
-    snapshot->current_fd = xbt_realloc(snapshot->current_fd, (total_fd + 1) * sizeof(fd_infos_t));
+    snapshot->current_fd = (fd_infos_t*) xbt_realloc(snapshot->current_fd, (total_fd + 1) * sizeof(fd_infos_t));
     snapshot->current_fd[total_fd] = fd;
     total_fd++;
   }
@@ -730,14 +698,15 @@ static void MC_get_current_fd(mc_snapshot_t snapshot)
 }
 
 static s_mc_address_space_class_t mc_snapshot_class = {
-  .read = (void*) &MC_snapshot_read
+  .read = (mc_address_space_class_read_callback_t) &MC_snapshot_read,
+  .get_process = NULL
 };
 
 mc_snapshot_t MC_take_snapshot(int num_state)
 {
   XBT_DEBUG("Taking snapshot %i", num_state);
 
-  mc_process_t mc_process = &mc_model_checker->process;
+  mc_process_t mc_process = &mc_model_checker->process();
   mc_snapshot_t snapshot = xbt_new0(s_mc_snapshot_t, 1);
   snapshot->process = mc_process;
   snapshot->num_state = num_state;
@@ -754,14 +723,8 @@ mc_snapshot_t MC_take_snapshot(int num_state)
   if (_sg_mc_snapshot_fds)
     MC_get_current_fd(snapshot);
 
-  const bool use_soft_dirty = _sg_mc_sparse_checkpoint
-    && _sg_mc_soft_dirty
-    && MC_process_is_self(mc_process);
-
   /* Save the std heap and the writable mapped pages of libsimgrid and binary */
   MC_get_memory_regions(mc_process, snapshot);
-  if (use_soft_dirty)
-    mc_softdirty_reset();
 
   snapshot->to_ignore = MC_take_snapshot_ignore();
 
@@ -778,22 +741,17 @@ mc_snapshot_t MC_take_snapshot(int num_state)
   }
 
   MC_snapshot_ignore_restore(snapshot);
-  if (use_soft_dirty)
-    mc_model_checker->parent_snapshot = snapshot;
   return snapshot;
 }
 
 static inline
 void MC_restore_snapshot_regions(mc_snapshot_t snapshot)
 {
-  mc_snapshot_t parent_snapshot = mc_model_checker->parent_snapshot;
-
   const size_t n = snapshot->snapshot_regions_count;
   for (size_t i = 0; i < n; i++) {
     // For privatized, variables we decided it was not necessary to take the snapshot:
     if (snapshot->snapshot_regions[i])
-      MC_region_restore(snapshot->snapshot_regions[i],
-        parent_snapshot ? parent_snapshot->snapshot_regions[i] : NULL);
+      MC_region_restore(snapshot->snapshot_regions[i]);
   }
 
 #ifdef HAVE_SMPI
@@ -817,8 +775,7 @@ void MC_restore_snapshot_fds(mc_snapshot_t snapshot)
     xbt_die("FD snapshot not implemented in client/server mode.");
 
   int new_fd;
-  size_t i;
-  for(i=0; i < snapshot->total_fd; i++){
+  for (int i=0; i < snapshot->total_fd; i++) {
     
     new_fd = open(snapshot->current_fd[i]->filename, snapshot->current_fd[i]->flags);
     if (new_fd <0) {
@@ -837,26 +794,16 @@ void MC_restore_snapshot_fds(mc_snapshot_t snapshot)
 void MC_restore_snapshot(mc_snapshot_t snapshot)
 {
   XBT_DEBUG("Restore snapshot %i", snapshot->num_state);
-
-  const bool use_soft_dirty = _sg_mc_sparse_checkpoint
-    && _sg_mc_soft_dirty
-    && MC_process_is_self(&mc_model_checker->process);
-
   MC_restore_snapshot_regions(snapshot);
   if (_sg_mc_snapshot_fds)
     MC_restore_snapshot_fds(snapshot);
-  if (use_soft_dirty) {
-    mc_softdirty_reset();
-  }
   MC_snapshot_ignore_restore(snapshot);
-  if (use_soft_dirty) {
-    mc_model_checker->parent_snapshot = snapshot;
-  }
-
-  mc_model_checker->process.cache_flags = 0;
+  mc_model_checker->process().cache_flags = 0;
 }
 
 mc_snapshot_t simcall_HANDLER_mc_snapshot(smx_simcall_t simcall)
 {
   return MC_take_snapshot(1);
 }
+
+}
similarity index 95%
rename from src/mc/mc_client.c
rename to src/mc/mc_client.cpp
index 7403eb2..6109240 100644 (file)
 // We won't need those once the separation MCer/MCed is complete:
 #include "mc_mmalloc.h"
 #include "mc_ignore.h"
-#include "mc_model_checker.h"
 #include "mc_private.h" // MC_deadlock_check()
 #include "mc_smx.h"
 
+extern "C" {
+
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_client, mc, "MC client logic");
 
 mc_client_t mc_client;
@@ -68,7 +69,7 @@ void MC_client_send_message(void* message, size_t size)
     xbt_die("Could not send message %i", (int) ((mc_message_t)message)->type);
 }
 
-void MC_client_send_simple_message(int type)
+void MC_client_send_simple_message(e_mc_message_type type)
 {
   if (MC_protocol_send_simple_message(mc_client->fd, type))
     xbt_die("Could not send message %i", type);
@@ -80,12 +81,12 @@ void MC_client_handle_messages(void)
     XBT_DEBUG("Waiting messages from model-checker");
 
     char message_buffer[MC_MESSAGE_LENGTH];
-    size_t s;
-    if ((s = MC_receive_message(mc_client->fd, &message_buffer, sizeof(message_buffer), 0)) == -1)
+    ssize_t s;
+    if ((s = MC_receive_message(mc_client->fd, &message_buffer, sizeof(message_buffer), 0)) < 0)
       xbt_die("Could not receive commands from the model-checker");
 
     s_mc_message_t message;
-    if (s < sizeof(message))
+    if ((size_t) s < sizeof(message))
       xbt_die("Received message is too small");
     memcpy(&message, message_buffer, sizeof(message));
     switch (message.type) {
@@ -136,3 +137,5 @@ void MC_client_main_loop(void)
     MC_wait_for_requests();
   }
 }
+
+}
index 7f82c11..6e1bdb5 100644 (file)
@@ -8,6 +8,7 @@
 #define MC_CLIENT_H
 
 #include <xbt/misc.h>
+#include "mc_protocol.h"
 
 SG_BEGIN_DECL()
 
@@ -22,7 +23,7 @@ void MC_client_init(void);
 void MC_client_hello(void);
 void MC_client_handle_messages(void);
 void MC_client_send_message(void* message, size_t size);
-void MC_client_send_simple_message(int type);
+void MC_client_send_simple_message(e_mc_message_type type);
 
 #ifdef HAVE_MC
 void MC_ignore(void* addr, size_t size);
similarity index 84%
rename from src/mc/mc_client_api.c
rename to src/mc/mc_client_api.cpp
index f9d58db..179033b 100644 (file)
 #include "mc_record.h"
 #include "mc_private.h"
 #include "mc_mmalloc.h"
-#include "mc_model_checker.h"
 #include "mc_ignore.h"
 #include "mc_protocol.h"
 #include "mc_client.h"
+#include "ModelChecker.hpp"
+
+extern "C" {
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_client_api, mc,
   "Public API for the model-checked application");
@@ -23,12 +25,8 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_client_api, mc,
 void MC_assert(int prop)
 {
   if (MC_is_active() && !prop) {
-    if (mc_mode == MC_MODE_STANDALONE) {
-      MC_report_assertion_error();
-    } else {
-      MC_client_send_simple_message(MC_MESSAGE_ASSERTION_FAILED);
-      MC_client_handle_messages();
-    }
+    MC_client_send_simple_message(MC_MESSAGE_ASSERTION_FAILED);
+    MC_client_handle_messages();
   }
 }
 
@@ -67,6 +65,8 @@ void MC_ignore(void* addr, size_t size)
 
   // TODO, remove this once the migration has been completed
   xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
-  MC_process_ignore_memory(&mc_model_checker->process, addr, size);
+  MC_process_ignore_memory(&mc_model_checker->process(), addr, size);
   mmalloc_set_current_heap(heap);
 }
+
+}
similarity index 94%
rename from src/mc/mc_comm_determinism.c
rename to src/mc/mc_comm_determinism.cpp
index 2ae9d1c..bede558 100644 (file)
@@ -13,6 +13,8 @@
 #include "mc_smx.h"
 #include "mc_client.h"
 
+extern "C" {
+
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_comm_determinism, mc,
                                 "Logging specific to MC communication determinism detection");
 
@@ -37,15 +39,15 @@ static e_mc_comm_pattern_difference_t compare_comm_pattern(mc_comm_pattern_t com
   if (comm1->data_size != comm2->data_size)
     return DATA_SIZE_DIFF;
   if(comm1->data == NULL && comm2->data == NULL)
-    return 0;
+    return NONE_DIFF;
   if(comm1->data != NULL && comm2->data !=NULL) {
     if (!memcmp(comm1->data, comm2->data, comm1->data_size))
-      return 0;
+      return NONE_DIFF;
     return DATA_DIFF;
   }else{
     return DATA_DIFF;
   }
-  return 0;
+  return NONE_DIFF;
 }
 
 static char* print_determinism_result(e_mc_comm_pattern_difference_t diff, int process, mc_comm_pattern_t comm, unsigned int cursor) {
@@ -89,7 +91,7 @@ static char* print_determinism_result(e_mc_comm_pattern_difference_t diff, int p
 static void update_comm_pattern(mc_comm_pattern_t comm_pattern, smx_synchro_t comm_addr)
 {
   s_smx_synchro_t comm;
-  MC_process_read_simple(&mc_model_checker->process,
+  MC_process_read_simple(&mc_model_checker->process(),
     &comm, comm_addr, sizeof(comm));
 
   smx_process_t src_proc = MC_smx_resolve_process(comm.comm.src_proc);
@@ -100,11 +102,11 @@ static void update_comm_pattern(mc_comm_pattern_t comm_pattern, smx_synchro_t co
   comm_pattern->dst_host = MC_smx_process_get_host_name(dst_proc);
   if (comm_pattern->data_size == -1 && comm.comm.src_buff != NULL) {
     size_t buff_size;
-    MC_process_read_simple(&mc_model_checker->process,
+    MC_process_read_simple(&mc_model_checker->process(),
       &buff_size, comm.comm.dst_buff_size, sizeof(buff_size));
     comm_pattern->data_size = buff_size;
     comm_pattern->data = xbt_malloc0(comm_pattern->data_size);
-    MC_process_read_simple(&mc_model_checker->process,
+    MC_process_read_simple(&mc_model_checker->process(),
       comm_pattern->data, comm.comm.src_buff, comm_pattern->data_size);
   }
 }
@@ -183,20 +185,20 @@ void MC_get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type
     pattern->comm_addr = simcall_comm_isend__get__result(request);
 
     s_smx_synchro_t synchro;
-    MC_process_read_simple(&mc_model_checker->process,
+    MC_process_read_simple(&mc_model_checker->process(),
       &synchro, pattern->comm_addr, sizeof(synchro));
 
     char* remote_name;
-    MC_process_read_simple(&mc_model_checker->process, &remote_name,
+    MC_process_read_simple(&mc_model_checker->process(), &remote_name,
       synchro.comm.rdv ? &synchro.comm.rdv->name : &synchro.comm.rdv_cpy->name,
       sizeof(remote_name));
     pattern->rdv =
-      MC_process_read_string(&mc_model_checker->process, remote_name);
+      MC_process_read_string(&mc_model_checker->process(), remote_name);
     pattern->src_proc = MC_smx_resolve_process(synchro.comm.src_proc)->pid;
     pattern->src_host = MC_smx_process_get_host_name(issuer);
 
     struct s_smpi_mpi_request mpi_request;
-    MC_process_read_simple(&mc_model_checker->process,
+    MC_process_read_simple(&mc_model_checker->process(),
       &mpi_request, (MPI_Request) simcall_comm_isend__get__data(request),
       sizeof(mpi_request));
     pattern->tag = mpi_request.tag;
@@ -204,7 +206,7 @@ void MC_get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type
     if(synchro.comm.src_buff != NULL){
       pattern->data_size = synchro.comm.src_buff_size;
       pattern->data = xbt_malloc0(pattern->data_size);
-      MC_process_read_simple(&mc_model_checker->process,
+      MC_process_read_simple(&mc_model_checker->process(),
         pattern->data, synchro.comm.src_buff, pattern->data_size);
     }
     if(mpi_request.detached){
@@ -229,21 +231,21 @@ void MC_get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type
     pattern->comm_addr = simcall_comm_irecv__get__result(request);
 
     struct s_smpi_mpi_request mpi_request;
-    MC_process_read_simple(&mc_model_checker->process,
+    MC_process_read_simple(&mc_model_checker->process(),
       &mpi_request, (MPI_Request) simcall_comm_irecv__get__data(request),
       sizeof(mpi_request));
     pattern->tag = mpi_request.tag;
 
     s_smx_synchro_t synchro;
-    MC_process_read_simple(&mc_model_checker->process,
+    MC_process_read_simple(&mc_model_checker->process(),
       &synchro, pattern->comm_addr, sizeof(synchro));
 
     char* remote_name;
-    MC_process_read_simple(&mc_model_checker->process, &remote_name,
+    MC_process_read_simple(&mc_model_checker->process(), &remote_name,
       synchro.comm.rdv ? &synchro.comm.rdv->name : &synchro.comm.rdv_cpy->name,
       sizeof(remote_name));
     pattern->rdv =
-      MC_process_read_string(&mc_model_checker->process, remote_name);
+      MC_process_read_string(&mc_model_checker->process(), remote_name);
     pattern->dst_proc = MC_smx_resolve_process(synchro.comm.dst_proc)->pid;
     pattern->dst_host = MC_smx_process_get_host_name(issuer);
   } else {
@@ -469,7 +471,7 @@ static void MC_modelcheck_comm_determinism_main(void)
 
       MC_SET_MC_HEAP;
 
-      while ((state = xbt_fifo_shift(mc_stack)) != NULL) {
+      while ((state = (mc_state_t) xbt_fifo_shift(mc_stack)) != NULL) {
         if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) {
           /* We found a back-tracking point, let's loop */
           XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
@@ -499,6 +501,10 @@ static void MC_modelcheck_comm_determinism_main(void)
 
 void MC_modelcheck_comm_determinism(void)
 {
+  XBT_INFO("Check communication determinism");
+  mc_reduce_kind = e_mc_reduce_none;
+  MC_wait_for_requests();
+
   if (mc_mode == MC_MODE_CLIENT) {
     // This will move somehwere else:
     MC_client_handle_messages();
@@ -528,3 +534,5 @@ void MC_modelcheck_comm_determinism(void)
 
   mmalloc_set_current_heap(heap);
 }
+
+}
similarity index 97%
rename from src/mc/mc_comm_pattern.c
rename to src/mc/mc_comm_pattern.cpp
index 37a90b3..a5b6e49 100644 (file)
@@ -12,6 +12,8 @@
 #include "mc_comm_pattern.h"
 #include "mc_smx.h"
 
+extern "C" {
+
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_comm_pattern, mc,
                                 "Logging specific to MC communication patterns");
 
@@ -74,7 +76,7 @@ void MC_restore_communications_pattern(mc_state_t state)
     list_process_comm->index_comm = (int)xbt_dynar_get_as(state->index_comm, cursor, int);
   }
 
-  for (int i = 0; i < MC_smx_get_maxpid(); i++) {
+  for (unsigned i = 0; i < MC_smx_get_maxpid(); i++) {
     MC_patterns_copy(
       xbt_dynar_get_as(incomplete_communications_pattern, i, xbt_dynar_t),
       xbt_dynar_get_as(state->incomplete_comm_pattern, i, xbt_dynar_t)
@@ -86,8 +88,7 @@ void MC_state_copy_incomplete_communications_pattern(mc_state_t state)
 {
   state->incomplete_comm_pattern = xbt_dynar_new(sizeof(xbt_dynar_t), xbt_dynar_free_voidp);
 
-  int i;
-  for (i=0; i < MC_smx_get_maxpid(); i++) {
+  for (unsigned i=0; i < MC_smx_get_maxpid(); i++) {
     xbt_dynar_t comms = xbt_dynar_get_as(incomplete_communications_pattern, i, xbt_dynar_t);
     xbt_dynar_t copy = MC_comm_patterns_dup(comms);
     xbt_dynar_insert_at(state->incomplete_comm_pattern, i, &copy);
@@ -124,7 +125,7 @@ void MC_handle_comm_pattern(
         comm_addr = simcall_comm_wait__get__comm(req);
       else
         // comm_addr = REMOTE(xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value, smx_synchro_t)):
-        MC_process_read_dynar_element(&mc_model_checker->process, &comm_addr,
+        MC_process_read_dynar_element(&mc_model_checker->process(), &comm_addr,
           simcall_comm_waitany__get__comms(req), value, sizeof(comm_addr));
       MC_complete_comm_pattern(pattern, comm_addr,
         MC_smx_simcall_get_issuer(req)->pid, backtracking);
@@ -160,3 +161,5 @@ void MC_list_comm_pattern_free_voidp(void *p)
 {
   MC_list_comm_pattern_free((mc_list_comm_pattern_t) * (void **) p);
 }
+
+}
index 3420b02..1cfbd3c 100644 (file)
@@ -8,6 +8,8 @@
 #include <inttypes.h>
 #include <boost/unordered_set.hpp>
 
+#include <xbt/sysdep.h>
+
 #include "internal_config.h"
 #include "mc_object_info.h"
 #include "mc_safety.h"
@@ -24,9 +26,6 @@
 
 #include <xbt/probes.h>
 
-XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_compare, mc,
-                                "Logging specific to mc_compare");
-
 typedef struct s_pointers_pair {
   void *p1;
   void *p2;
@@ -55,6 +54,9 @@ struct mc_compare_state {
 
 extern "C" {
 
+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_compare, xbt,
+                                "Logging specific to mc_compare in mc");
+
 /************************** Free functions ****************************/
 /********************************************************************/
 
@@ -102,7 +104,7 @@ static int compare_areas_with_type(struct mc_compare_state& state,
                                    void* real_area2, mc_snapshot_t snapshot2, mc_mem_region_t region2,
                                    dw_type_t type, int pointer_level)
 {
-  mc_process_t process = &mc_model_checker->process;
+  mc_process_t process = &mc_model_checker->process();
 
   unsigned int cursor = 0;
   dw_type_t member, subtype, subsubtype;
@@ -385,7 +387,7 @@ static int compare_local_variables(int process_index,
 
 int snapshot_compare(void *state1, void *state2)
 {
-  mc_process_t process = &mc_model_checker->process;
+  mc_process_t process = &mc_model_checker->process();
 
   mc_snapshot_t s1, s2;
   int num1, num2;
similarity index 94%
rename from src/mc/mc_config.c
rename to src/mc/mc_config.cpp
index 79e2be3..bf9eae8 100644 (file)
@@ -10,6 +10,7 @@
 #include <xbt/config.h>
 
 #include <mc/mc.h>
+#include "mc/mc_replay.h"
 
 #include <simgrid/sg_config.h>
 
@@ -20,6 +21,8 @@
 
 #include "mc_record.h"
 
+extern "C" {
+
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_config, mc,
                                 "Configuration of MC");
 
@@ -48,7 +51,6 @@ int _sg_do_model_check = 0;
 int _sg_do_model_check_record = 0;
 int _sg_mc_checkpoint = 0;
 int _sg_mc_sparse_checkpoint = 0;
-int _sg_mc_soft_dirty = 0;
 char *_sg_mc_property_file = NULL;
 int _sg_mc_hash = 0;
 int _sg_mc_max_depth = 1000;
@@ -94,13 +96,6 @@ void _mc_cfg_cb_sparse_checkpoint(const char *name, int pos) {
   _sg_mc_sparse_checkpoint = xbt_cfg_get_boolean(_sg_cfg_set, name);
 }
 
-void _mc_cfg_cb_soft_dirty(const char *name, int pos) {
-  if (_sg_cfg_init_status && !_sg_do_model_check) {
-    xbt_die("You are specifying a soft dirty value after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
-  }
-  _sg_mc_soft_dirty = xbt_cfg_get_boolean(_sg_cfg_set, name);
-}
-
 void _mc_cfg_cb_property(const char *name, int pos)
 {
   if (_sg_cfg_init_status && !_sg_do_model_check) {
@@ -183,3 +178,5 @@ void _mc_cfg_cb_termination(const char *name, int pos)
 }
 
 #endif
+
+}
similarity index 94%
rename from src/mc/mc_diff.c
rename to src/mc/mc_diff.cpp
index c526fe9..b8fc44c 100644 (file)
@@ -15,6 +15,8 @@
 #include "mc/mc_private.h"
 #include "mc/mc_snapshot.h"
 
+extern "C" {
+
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_diff, xbt,
                                 "Logging specific to mc_diff in mc");
 
@@ -366,7 +368,7 @@ int init_heap_information(xbt_mheap_t heap1, xbt_mheap_t heap2, xbt_dynar_t i1,
 
   state->heaplimit = ((struct mdesc *) heap1)->heaplimit;
   
-  state->std_heap_copy = *MC_process_get_heap(&mc_model_checker->process);
+  state->std_heap_copy = *MC_process_get_heap(&mc_model_checker->process());
 
   state->heapsize1 = heap1->heapsize;
   state->heapsize2 = heap2->heapsize;
@@ -375,19 +377,19 @@ int init_heap_information(xbt_mheap_t heap1, xbt_mheap_t heap2, xbt_dynar_t i1,
   state->to_ignore2 = i2;
 
   if (state->heaplimit > state->available) {
-    state->equals_to1 =
+    state->equals_to1 = (s_heap_area_t*)
         realloc(state->equals_to1,
                 state->heaplimit * MAX_FRAGMENT_PER_BLOCK *
                 sizeof(s_heap_area_t));
-    state->types1 =
+    state->types1 = (s_dw_type**)
         realloc(state->types1,
                 state->heaplimit * MAX_FRAGMENT_PER_BLOCK *
                 sizeof(type_name *));
-    state->equals_to2 =
+    state->equals_to2 = (s_heap_area_t*)
         realloc(state->equals_to2,
                 state->heaplimit * MAX_FRAGMENT_PER_BLOCK *
                 sizeof(s_heap_area_t));
-    state->types2 =
+    state->types2 = (s_dw_type**)
         realloc(state->types2,
                 state->heaplimit * MAX_FRAGMENT_PER_BLOCK *
                 sizeof(type_name *));
@@ -427,7 +429,7 @@ mc_mem_region_t MC_get_heap_region(mc_snapshot_t snapshot)
 
 int mmalloc_compare_heap(mc_snapshot_t snapshot1, mc_snapshot_t snapshot2)
 {
-  mc_process_t process = &mc_model_checker->process;
+  mc_process_t process = &mc_model_checker->process();
   struct s_mc_diff *state = mc_diff_info;
 
   /* Start comparison */
@@ -451,13 +453,13 @@ int mmalloc_compare_heap(mc_snapshot_t snapshot1, mc_snapshot_t snapshot2)
   void* heapinfo_address = &((xbt_mheap_t) process->heap_address)->heapinfo;
 
   // This is in snapshot do not use them directly:
-  const malloc_info* heapinfos1 = MC_snapshot_read_pointer(snapshot1, heapinfo_address, MC_PROCESS_INDEX_MISSING);
-  const malloc_info* heapinfos2 = MC_snapshot_read_pointer(snapshot2, heapinfo_address, MC_PROCESS_INDEX_MISSING);
+  const malloc_info* heapinfos1 = (const malloc_info*) MC_snapshot_read_pointer(snapshot1, heapinfo_address, MC_PROCESS_INDEX_MISSING);
+  const malloc_info* heapinfos2 = (const malloc_info*) MC_snapshot_read_pointer(snapshot2, heapinfo_address, MC_PROCESS_INDEX_MISSING);
 
   while (i1 <= state->heaplimit) {
 
-    const malloc_info* heapinfo1 = MC_region_read(heap_region1, &heapinfo_temp1, &heapinfos1[i1], sizeof(malloc_info));
-    const malloc_info* heapinfo2 = MC_region_read(heap_region2, &heapinfo_temp2, &heapinfos2[i1], sizeof(malloc_info));
+    const malloc_info* heapinfo1 = (const malloc_info*) MC_region_read(heap_region1, &heapinfo_temp1, &heapinfos1[i1], sizeof(malloc_info));
+    const malloc_info* heapinfo2 = (const malloc_info*) MC_region_read(heap_region2, &heapinfo_temp2, &heapinfos2[i1], sizeof(malloc_info));
 
     if (heapinfo1->type == MMALLOC_TYPE_FREE || heapinfo1->type == MMALLOC_TYPE_HEAPINFO) {      /* Free block */
       i1 ++;
@@ -528,7 +530,7 @@ int mmalloc_compare_heap(mc_snapshot_t snapshot1, mc_snapshot_t snapshot2)
           continue;
         }
 
-        const malloc_info* heapinfo2b = MC_region_read(heap_region2, &heapinfo_temp2b, &heapinfos2[i2], sizeof(malloc_info));
+        const malloc_info* heapinfo2b = (const malloc_info*) MC_region_read(heap_region2, &heapinfo_temp2b, &heapinfos2[i2], sizeof(malloc_info));
 
         if (heapinfo2b->type != MMALLOC_TYPE_UNFRAGMENTED) {
           i2++;
@@ -605,7 +607,9 @@ int mmalloc_compare_heap(mc_snapshot_t snapshot1, mc_snapshot_t snapshot2)
 
         while (i2 <= state->heaplimit && !equal) {
 
-          const malloc_info* heapinfo2b = MC_region_read(heap_region2, &heapinfo_temp2b, &heapinfos2[i2], sizeof(malloc_info));
+          const malloc_info* heapinfo2b = (const malloc_info*) MC_region_read(
+            heap_region2, &heapinfo_temp2b, &heapinfos2[i2],
+            sizeof(malloc_info));
 
           if (heapinfo2b->type == MMALLOC_TYPE_FREE || heapinfo2b->type == MMALLOC_TYPE_HEAPINFO) {
             i2 ++;
@@ -676,7 +680,8 @@ int mmalloc_compare_heap(mc_snapshot_t snapshot1, mc_snapshot_t snapshot2)
   size_t i = 1, j = 0;
 
   for(i = 1; i <= state->heaplimit; i++) {
-    const malloc_info* heapinfo1 = MC_region_read(heap_region1, &heapinfo_temp1, &heapinfos1[i], sizeof(malloc_info));
+    const malloc_info* heapinfo1 = (const malloc_info*) MC_region_read(
+      heap_region1, &heapinfo_temp1, &heapinfos1[i], sizeof(malloc_info));
     if (heapinfo1->type == MMALLOC_TYPE_UNFRAGMENTED) {
       if (i1 == state->heaplimit) {
         if (heapinfo1->busy_block.busy_size > 0) {
@@ -717,7 +722,8 @@ int mmalloc_compare_heap(mc_snapshot_t snapshot1, mc_snapshot_t snapshot2)
     XBT_DEBUG("Number of blocks/fragments not found in heap1 : %d", nb_diff1);
 
   for (i=1; i <= state->heaplimit; i++) {
-    const malloc_info* heapinfo2 = MC_region_read(heap_region2, &heapinfo_temp2, &heapinfos2[i], sizeof(malloc_info));
+    const malloc_info* heapinfo2 = (const malloc_info*) MC_region_read(
+      heap_region2, &heapinfo_temp2, &heapinfos2[i], sizeof(malloc_info));
     if (heapinfo2->type == MMALLOC_TYPE_UNFRAGMENTED) {
       if (i1 == state->heaplimit) {
         if (heapinfo2->busy_block.busy_size > 0) {
@@ -778,7 +784,7 @@ static int compare_heap_area_without_type(struct s_mc_diff *state, int process_i
                                           xbt_dynar_t previous, int size,
                                           int check_ignore)
 {
-  mc_process_t process = &mc_model_checker->process;
+  mc_process_t process = &mc_model_checker->process();
 
   int i = 0;
   const void *addr_pointed1, *addr_pointed2;
@@ -885,7 +891,7 @@ top:
   }
 
   dw_type_t subtype, subsubtype;
-  int res, elm_size, i;
+  int res, elm_size;
   unsigned int cursor = 0;
   dw_type_t member;
   const void *addr_pointed1, *addr_pointed2;;
@@ -955,7 +961,7 @@ top:
       return 0;
       break;
     }
-    for (i = 0; i < type->element_count; i++) {
+    for (int i = 0; i < type->element_count; i++) {
       // TODO, add support for variable stride (DW_AT_byte_stride)
       res =
           compare_heap_area_with_type(state, process_index,
@@ -978,7 +984,7 @@ top:
     } else {
       pointer_level++;
       if (pointer_level > 1) {  /* Array of pointers */
-        for (i = 0; i < (area_size / sizeof(void *)); i++) {
+        for (size_t i = 0; i < (area_size / sizeof(void *)); i++) {
           addr_pointed1 = MC_snapshot_read_pointer(snapshot1, (char*) real_area1 + i * sizeof(void *), process_index);
           addr_pointed2 = MC_snapshot_read_pointer(snapshot2, (char*) real_area2 + i * sizeof(void *), process_index);
           if (addr_pointed1 > state->std_heap_copy.heapbase
@@ -1015,7 +1021,7 @@ top:
       type = type->full_type;
     if (area_size != -1 && type->byte_size != area_size) {
       if (area_size > type->byte_size && area_size % type->byte_size == 0) {
-        for (i = 0; i < (area_size / type->byte_size); i++) {
+        for (size_t i = 0; i < (size_t)(area_size / type->byte_size); i++) {
           res =
               compare_heap_area_with_type(state, process_index,
                                           (char *) real_area1 + i * type->byte_size,
@@ -1032,9 +1038,9 @@ top:
       cursor = 0;
       xbt_dynar_foreach(type->members, cursor, member) {
         // TODO, optimize this? (for the offset case)
-        char *real_member1 =
+        void *real_member1 =
             mc_member_resolve(real_area1, type, member, (mc_address_space_t) snapshot1, process_index);
-        char *real_member2 =
+        void *real_member2 =
             mc_member_resolve(real_area2, type, member, (mc_address_space_t) snapshot2, process_index);
         res =
             compare_heap_area_with_type(state, process_index, real_member1, real_member2,
@@ -1100,9 +1106,10 @@ static dw_type_t get_offset_type(void *real_base_address, dw_type_t type,
           if (member->offset == offset)
             return member->subtype;
         } else {
-          char *real_member =
-              mc_member_resolve(real_base_address, type, member, (mc_address_space_t) snapshot, process_index);
-          if (real_member - (char *) real_base_address == offset)
+          void *real_member =
+            mc_member_resolve(real_base_address, type, member,
+              (mc_address_space_t) snapshot, process_index);
+          if ((char*) real_member - (char *) real_base_address == offset)
             return member->subtype;
         }
 
@@ -1132,7 +1139,7 @@ int compare_heap_area(int process_index, const void *area1, const void *area2, m
                       mc_snapshot_t snapshot2, xbt_dynar_t previous,
                       dw_type_t type, int pointer_level)
 {
-  mc_process_t process = &mc_model_checker->process;
+  mc_process_t process = &mc_model_checker->process();
 
   struct s_mc_diff *state = mc_diff_info;
 
@@ -1152,8 +1159,10 @@ int compare_heap_area(int process_index, const void *area1, const void *area2, m
   // This is the address of std_heap->heapinfo in the application process:
   void* heapinfo_address = &((xbt_mheap_t) process->heap_address)->heapinfo;
 
-  const malloc_info* heapinfos1 = MC_snapshot_read_pointer(snapshot1, heapinfo_address, process_index);
-  const malloc_info* heapinfos2 = MC_snapshot_read_pointer(snapshot2, heapinfo_address, process_index);
+  const malloc_info* heapinfos1 = (const malloc_info*) MC_snapshot_read_pointer(
+    snapshot1, heapinfo_address, process_index);
+  const malloc_info* heapinfos2 = (const malloc_info*) MC_snapshot_read_pointer(
+    snapshot2, heapinfo_address, process_index);
 
   malloc_info heapinfo_temp1, heapinfo_temp2;
 
@@ -1181,9 +1190,9 @@ int compare_heap_area(int process_index, const void *area1, const void *area2, m
   }
   // If either block is not in the expected area of memory:
   if (((char *) area1 < (char *) state->std_heap_copy.heapbase)
-      || (block1 > state->heapsize1) || (block1 < 1)
+      || (block1 > (ssize_t) state->heapsize1) || (block1 < 1)
       || ((char *) area2 < (char *) state->std_heap_copy.heapbase)
-      || (block2 > state->heapsize2) || (block2 < 1)) {
+      || (block2 > (ssize_t) state->heapsize2) || (block2 < 1)) {
     if (match_pairs) {
       xbt_dynar_free(&previous);
     }
@@ -1218,8 +1227,10 @@ int compare_heap_area(int process_index, const void *area1, const void *area2, m
   mc_mem_region_t heap_region1 = MC_get_heap_region(snapshot1);
   mc_mem_region_t heap_region2 = MC_get_heap_region(snapshot2);
 
-  const malloc_info* heapinfo1 = MC_region_read(heap_region1, &heapinfo_temp1, &heapinfos1[block1], sizeof(malloc_info));
-  const malloc_info* heapinfo2 = MC_region_read(heap_region2, &heapinfo_temp2, &heapinfos2[block2], sizeof(malloc_info));
+  const malloc_info* heapinfo1 = (const malloc_info*) MC_region_read(
+    heap_region1, &heapinfo_temp1, &heapinfos1[block1], sizeof(malloc_info));
+  const malloc_info* heapinfo2 = (const malloc_info*) MC_region_read(
+    heap_region2, &heapinfo_temp2, &heapinfos2[block2], sizeof(malloc_info));
 
   if ((heapinfo1->type == MMALLOC_TYPE_FREE || heapinfo1->type==MMALLOC_TYPE_HEAPINFO)
     && (heapinfo2->type == MMALLOC_TYPE_FREE || heapinfo2->type ==MMALLOC_TYPE_HEAPINFO)) {
@@ -1252,8 +1263,8 @@ int compare_heap_area(int process_index, const void *area1, const void *area2, m
     }
 
     if (type_size != -1) {
-      if (type_size != heapinfo1->busy_block.busy_size
-          && type_size != heapinfo2->busy_block.busy_size
+      if (type_size != (ssize_t) heapinfo1->busy_block.busy_size
+          && type_size != (ssize_t)   heapinfo2->busy_block.busy_size
           && (type->name == NULL || !strcmp(type->name, "struct s_smx_context"))) {
         if (match_pairs) {
           match_equals(state, previous);
@@ -1599,7 +1610,7 @@ int mmalloc_linear_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2)
   /* Heap information */
   state->heaplimit = ((struct mdesc *) heap1)->heaplimit;
 
-  state->std_heap_copy = *MC_process_get_heap(&mc_model_checker->process);
+  state->std_heap_copy = *MC_process_get_heap(&mc_model_checker->process());
 
   state->heapbase1 = (char *) heap1 + BLOCKSIZE;
   state->heapbase2 = (char *) heap2 + BLOCKSIZE;
@@ -1732,3 +1743,5 @@ int mmalloc_linear_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2)
 
 }
 #endif
+
+}
similarity index 94%
rename from src/mc/mc_dwarf.c
rename to src/mc/mc_dwarf.cpp
index 55de42e..1fb7db1 100644 (file)
@@ -17,6 +17,8 @@
 #include "mc_object_info.h"
 #include "mc_private.h"
 
+extern "C" {
+
 static void MC_dwarf_register_global_variable(mc_object_info_t info, dw_variable_t variable);
 static void MC_register_variable(mc_object_info_t info, dw_frame_t frame, dw_variable_t variable);
 static void MC_dwarf_register_non_global_variable(mc_object_info_t info, dw_frame_t frame, dw_variable_t variable);
@@ -61,13 +63,13 @@ static uint64_t MC_dwarf_array_element_count(Dwarf_Die * die, Dwarf_Die * unit);
  */
 static void MC_dwarf_handle_die(mc_object_info_t info, Dwarf_Die * die,
                                 Dwarf_Die * unit, dw_frame_t frame,
-                                const char *namespace);
+                                const char *ns);
 
 /** \brief Process a type DIE
  */
 static void MC_dwarf_handle_type_die(mc_object_info_t info, Dwarf_Die * die,
                                      Dwarf_Die * unit, dw_frame_t frame,
-                                     const char *namespace);
+                                     const char *ns);
 
 /** \brief Calls MC_dwarf_handle_die on all childrend of the given die
  *
@@ -78,7 +80,7 @@ static void MC_dwarf_handle_type_die(mc_object_info_t info, Dwarf_Die * die,
  */
 static void MC_dwarf_handle_children(mc_object_info_t info, Dwarf_Die * die,
                                      Dwarf_Die * unit, dw_frame_t frame,
-                                     const char *namespace);
+                                     const char *ns);
 
 /** \brief Handle a variable (DW_TAG_variable or other)
  *
@@ -89,7 +91,7 @@ static void MC_dwarf_handle_children(mc_object_info_t info, Dwarf_Die * die,
  */
 static void MC_dwarf_handle_variable_die(mc_object_info_t info, Dwarf_Die * die,
                                          Dwarf_Die * unit, dw_frame_t frame,
-                                         const char *namespace);
+                                         const char *ns);
 
 /** \brief Get the DW_TAG_type of the DIE
  *
@@ -632,7 +634,7 @@ static void MC_dwarf_add_members(mc_object_info_t info, Dwarf_Die * die,
  */
 static dw_type_t MC_dwarf_die_to_type(mc_object_info_t info, Dwarf_Die * die,
                                       Dwarf_Die * unit, dw_frame_t frame,
-                                      const char *namespace)
+                                      const char *ns)
 {
 
   dw_type_t type = xbt_new0(s_dw_type_t, 1);
@@ -669,7 +671,7 @@ static dw_type_t MC_dwarf_die_to_type(mc_object_info_t info, Dwarf_Die * die,
   const char *name = MC_dwarf_attr_integrate_string(die, DW_AT_name);
   if (name != NULL) {
     type->name =
-        namespace ? bprintf("%s%s::%s", prefix, namespace,
+        ns ? bprintf("%s%s::%s", prefix, ns,
                             name) : bprintf("%s%s", prefix, name);
   }
 
@@ -703,10 +705,10 @@ static dw_type_t MC_dwarf_die_to_type(mc_object_info_t info, Dwarf_Die * die,
   case DW_TAG_union_type:
   case DW_TAG_class_type:
     MC_dwarf_add_members(info, die, unit, type);
-    char *new_namespace = namespace == NULL ? xbt_strdup(type->name)
-        : bprintf("%s::%s", namespace, name);
-    MC_dwarf_handle_children(info, die, unit, frame, new_namespace);
-    free(new_namespace);
+    char *new_ns = ns == NULL ? xbt_strdup(type->name)
+        : bprintf("%s::%s", ns, name);
+    MC_dwarf_handle_children(info, die, unit, frame, new_ns);
+    free(new_ns);
     break;
   }
 
@@ -715,9 +717,9 @@ static dw_type_t MC_dwarf_die_to_type(mc_object_info_t info, Dwarf_Die * die,
 
 static void MC_dwarf_handle_type_die(mc_object_info_t info, Dwarf_Die * die,
                                      Dwarf_Die * unit, dw_frame_t frame,
-                                     const char *namespace)
+                                     const char *ns)
 {
-  dw_type_t type = MC_dwarf_die_to_type(info, die, unit, frame, namespace);
+  dw_type_t type = MC_dwarf_die_to_type(info, die, unit, frame, ns);
 
   char *key = bprintf("%" PRIx64, (uint64_t) type->id);
   xbt_dict_set(info->types, key, type, NULL);
@@ -732,7 +734,7 @@ static int mc_anonymous_variable_index = 0;
 
 static dw_variable_t MC_die_to_variable(mc_object_info_t info, Dwarf_Die * die,
                                         Dwarf_Die * unit, dw_frame_t frame,
-                                        const char *namespace)
+                                        const char *ns)
 {
   // Skip declarations:
   if (MC_dwarf_attr_flag(die, DW_AT_declaration, false))
@@ -821,9 +823,9 @@ static dw_variable_t MC_die_to_variable(mc_object_info_t info, Dwarf_Die * die,
     }
   }
 
-  if (namespace && variable->global) {
+  if (ns && variable->global) {
     char *old_name = variable->name;
-    variable->name = bprintf("%s::%s", namespace, old_name);
+    variable->name = bprintf("%s::%s", ns, old_name);
     free(old_name);
   }
   // The current code needs a variable name,
@@ -837,10 +839,10 @@ static dw_variable_t MC_die_to_variable(mc_object_info_t info, Dwarf_Die * die,
 
 static void MC_dwarf_handle_variable_die(mc_object_info_t info, Dwarf_Die * die,
                                          Dwarf_Die * unit, dw_frame_t frame,
-                                         const char *namespace)
+                                         const char *ns)
 {
   dw_variable_t variable =
-      MC_die_to_variable(info, die, unit, frame, namespace);
+      MC_die_to_variable(info, die, unit, frame, ns);
   if (variable == NULL)
     return;
   MC_dwarf_register_variable(info, frame, variable);
@@ -854,7 +856,7 @@ static void mc_frame_free_voipd(dw_frame_t * p)
 
 static void MC_dwarf_handle_scope_die(mc_object_info_t info, Dwarf_Die * die,
                                       Dwarf_Die * unit, dw_frame_t parent_frame,
-                                      const char *namespace)
+                                      const char *ns)
 {
   // TODO, handle DW_TAG_type/DW_TAG_location for DW_TAG_with_stmt
   int tag = dwarf_tag(die);
@@ -877,7 +879,7 @@ static void MC_dwarf_handle_scope_die(mc_object_info_t info, Dwarf_Die * die,
   if (klass == mc_tag_subprogram) {
     const char *name = MC_dwarf_attr_integrate_string(die, DW_AT_name);
     frame->name =
-        namespace ? bprintf("%s::%s", namespace, name) : xbt_strdup(name);
+        ns ? bprintf("%s::%s", ns, name) : xbt_strdup(name);
   }
 
   frame->abstract_origin_id =
@@ -947,39 +949,39 @@ static void MC_dwarf_handle_scope_die(mc_object_info_t info, Dwarf_Die * die,
     xbt_dynar_push(parent_frame->scopes, &frame);
   }
   // Handle children:
-  MC_dwarf_handle_children(info, die, unit, frame, namespace);
+  MC_dwarf_handle_children(info, die, unit, frame, ns);
 }
 
 static void mc_dwarf_handle_namespace_die(mc_object_info_t info,
                                           Dwarf_Die * die, Dwarf_Die * unit,
                                           dw_frame_t frame,
-                                          const char *namespace)
+                                          const char *ns)
 {
   const char *name = MC_dwarf_attr_integrate_string(die, DW_AT_name);
   if (frame)
     xbt_die("Unexpected namespace in a subprogram");
-  char *new_namespace = namespace == NULL ? xbt_strdup(name)
-      : bprintf("%s::%s", namespace, name);
-  MC_dwarf_handle_children(info, die, unit, frame, new_namespace);
-  xbt_free(new_namespace);
+  char *new_ns = ns == NULL ? xbt_strdup(name)
+      : bprintf("%s::%s", ns, name);
+  MC_dwarf_handle_children(info, die, unit, frame, new_ns);
+  xbt_free(new_ns);
 }
 
 static void MC_dwarf_handle_children(mc_object_info_t info, Dwarf_Die * die,
                                      Dwarf_Die * unit, dw_frame_t frame,
-                                     const char *namespace)
+                                     const char *ns)
 {
   // For each child DIE:
   Dwarf_Die child;
   int res;
   for (res = dwarf_child(die, &child); res == 0;
        res = dwarf_siblingof(&child, &child)) {
-    MC_dwarf_handle_die(info, &child, unit, frame, namespace);
+    MC_dwarf_handle_die(info, &child, unit, frame, ns);
   }
 }
 
 static void MC_dwarf_handle_die(mc_object_info_t info, Dwarf_Die * die,
                                 Dwarf_Die * unit, dw_frame_t frame,
-                                const char *namespace)
+                                const char *ns)
 {
   int tag = dwarf_tag(die);
   mc_tag_class klass = MC_dwarf_tag_classify(tag);
@@ -987,22 +989,22 @@ static void MC_dwarf_handle_die(mc_object_info_t info, Dwarf_Die * die,
 
     // Type:
   case mc_tag_type:
-    MC_dwarf_handle_type_die(info, die, unit, frame, namespace);
+    MC_dwarf_handle_type_die(info, die, unit, frame, ns);
     break;
 
     // Subprogram or scope:
   case mc_tag_subprogram:
   case mc_tag_scope:
-    MC_dwarf_handle_scope_die(info, die, unit, frame, namespace);
+    MC_dwarf_handle_scope_die(info, die, unit, frame, ns);
     return;
 
     // Variable:
   case mc_tag_variable:
-    MC_dwarf_handle_variable_die(info, die, unit, frame, namespace);
+    MC_dwarf_handle_variable_die(info, die, unit, frame, ns);
     break;
 
   case mc_tag_namespace:
-    mc_dwarf_handle_namespace_die(info, die, unit, frame, namespace);
+    mc_dwarf_handle_namespace_die(info, die, unit, frame, ns);
     break;
 
   default:
@@ -1178,7 +1180,7 @@ static void MC_post_process_variables(mc_object_info_t info)
   dw_variable_t variable = NULL;
   xbt_dynar_foreach(info->global_variables, cursor, variable) {
     if (variable->type_origin) {
-      variable->type = xbt_dict_get_or_null(info->types, variable->type_origin);
+      variable->type = (dw_type_t) xbt_dict_get_or_null(info->types, variable->type_origin);
     }
   }
 }
@@ -1190,7 +1192,7 @@ static void mc_post_process_scope(mc_object_info_t info, dw_frame_t scope)
 
     // Attach correct namespaced name in inlined subroutine:
     char *key = bprintf("%" PRIx64, (uint64_t) scope->abstract_origin_id);
-    dw_frame_t abstract_origin = xbt_dict_get_or_null(info->subprograms, key);
+    dw_frame_t abstract_origin = (dw_frame_t) xbt_dict_get_or_null(info->subprograms, key);
     xbt_assert(abstract_origin, "Could not lookup abstract origin %s", key);
     xbt_free(key);
     scope->name = xbt_strdup(abstract_origin->name);
@@ -1201,7 +1203,7 @@ static void mc_post_process_scope(mc_object_info_t info, dw_frame_t scope)
   dw_variable_t variable = NULL;
   xbt_dynar_foreach(scope->variables, cursor, variable) {
     if (variable->type_origin) {
-      variable->type = xbt_dict_get_or_null(info->types, variable->type_origin);
+      variable->type = (dw_type_t) xbt_dict_get_or_null(info->types, variable->type_origin);
     }
   }
 
@@ -1230,7 +1232,7 @@ static void MC_resolve_subtype(mc_object_info_t info, dw_type_t type)
 
   if (type->dw_type_id == NULL)
     return;
-  type->subtype = xbt_dict_get_or_null(info->types, type->dw_type_id);
+  type->subtype = (dw_type_t) xbt_dict_get_or_null(info->types, type->dw_type_id);
   if (type->subtype == NULL)
     return;
   if (type->subtype->byte_size != 0)
@@ -1241,7 +1243,7 @@ static void MC_resolve_subtype(mc_object_info_t info, dw_type_t type)
   // We need to fix in order to support C++.
 
   dw_type_t subtype =
-      xbt_dict_get_or_null(info->full_types_by_name, type->subtype->name);
+    (dw_type_t) xbt_dict_get_or_null(info->full_types_by_name, type->subtype->name);
   if (subtype != NULL) {
     type->subtype = subtype;
   }
@@ -1385,7 +1387,7 @@ void MC_post_process_object_info(mc_process_t process, mc_object_info_t info)
     // Resolve full_type:
     if (subtype->name && subtype->byte_size == 0) {
       for (size_t i = 0; i != process->object_infos_size; ++i) {
-        dw_type_t same_type =
+        dw_type_t same_type = (dw_type_t)
             xbt_dict_get_or_null(process->object_infos[i]->full_types_by_name,
                                  subtype->name);
         if (same_type && same_type->name && same_type->byte_size) {
@@ -1397,3 +1399,5 @@ void MC_post_process_object_info(mc_process_t process, mc_object_info_t info)
 
   }
 }
+
+}
similarity index 99%
rename from src/mc/mc_dwarf_expression.c
rename to src/mc/mc_dwarf_expression.cpp
index adcf360..3d2bc36 100644 (file)
@@ -13,6 +13,8 @@
 #include "mc_object_info.h"
 #include "mc_private.h"
 
+extern "C" {
+
 static int mc_dwarf_push_value(mc_expression_state_t state, Dwarf_Off value)
 {
   if (state->stack_size >= MC_EXPRESSION_STACK_SIZE)
@@ -96,7 +98,7 @@ static int mc_dwarf_register_to_libunwind(int dwarf_register)
 int mc_dwarf_execute_expression(size_t n, const Dwarf_Op * ops,
                                 mc_expression_state_t state)
 {
-  for (int i = 0; i != n; ++i) {
+  for (size_t i = 0; i != n; ++i) {
     int error = 0;
     const Dwarf_Op *op = ops + i;
     uint8_t atom = op->atom;
@@ -220,7 +222,7 @@ int mc_dwarf_execute_expression(size_t n, const Dwarf_Op * ops,
 
       // Address from the base address of this ELF object.
       // Push the address on the stack (base_address + argument).
-    case DW_OP_addr:
+    case DW_OP_addr: {
       if (!state->object_info)
         return MC_EXPRESSION_E_NO_BASE_ADDRESS;
       if (state->stack_size == MC_EXPRESSION_STACK_SIZE)
@@ -229,6 +231,7 @@ int mc_dwarf_execute_expression(size_t n, const Dwarf_Op * ops,
         MC_object_base_address(state->object_info) + op->number;
       error = mc_dwarf_push_value(state, addr);
       break;
+    }
 
       // General constants:
       // Push the constant argument on the stack.
@@ -555,7 +558,7 @@ void mc_dwarf_expression_init(mc_expression_t expression, size_t len,
   expression->lowpc = NULL;
   expression->highpc = NULL;
   expression->size = len;
-  expression->ops = xbt_malloc(len * sizeof(Dwarf_Op));
+  expression->ops = (Dwarf_Op*) xbt_malloc(len * sizeof(Dwarf_Op));
   memcpy(expression->ops, ops, len * sizeof(Dwarf_Op));
 }
 
@@ -606,3 +609,5 @@ void mc_dwarf_location_list_init(mc_location_list_t list, mc_object_info_t info,
   }
 
 }
+
+}
index bd78e99..2152fe8 100644 (file)
@@ -7,20 +7,40 @@
 #ifndef MC_FORWARD_H
 #define MC_FORWARD_H
 
+#include <xbt/misc.h>
 #include <mc/datatypes.h>
-#include "mc_interface.h"
+
+#ifdef __cplusplus
+
+namespace simgrid {
+namespace mc {
+  class PageStore;
+  class ModelChecker;
+}
+}
+
+typedef ::simgrid::mc::ModelChecker s_mc_model_checker_t;
+typedef ::simgrid::mc::PageStore s_mc_pages_store_t;
+
+#else
+
+typedef struct _s_mc_model_checker s_mc_model_checker_t;
+typedef struct _s_mc_pages_store s_mc_pages_store_t;
+
+#endif
 
 typedef struct s_mc_object_info s_mc_object_info_t, *mc_object_info_t;
 typedef struct s_dw_type s_dw_type_t, *dw_type_t;
 typedef struct s_memory_map s_memory_map_t, *memory_map_t;
 typedef struct s_dw_variable s_dw_variable_t, *dw_variable_t;
 typedef struct s_dw_frame s_dw_frame_t, *dw_frame_t;
-
-typedef struct s_mc_pages_store s_mc_pages_store_t, *mc_pages_store_t;
+typedef s_mc_pages_store_t *mc_pages_store_t;
 typedef struct s_mc_snapshot s_mc_snapshot_t, *mc_snapshot_t;
-
 typedef struct s_mc_process s_mc_process_t, * mc_process_t;
-typedef struct s_mc_model_checker s_mc_model_checker_t, *mc_model_checker_t;
+typedef s_mc_model_checker_t *mc_model_checker_t;
+
+SG_BEGIN_DECL()
 extern mc_model_checker_t mc_model_checker;
+SG_END_DECL()
 
 #endif
similarity index 91%
rename from src/mc/mc_global.c
rename to src/mc/mc_global.cpp
index faf1eaf..7a9ebfd 100644 (file)
@@ -44,6 +44,8 @@
 #include "mc_protocol.h"
 #include "mc_client.h"
 
+extern "C" {
+
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc,
                                 "Logging specific to MC (global)");
 
@@ -104,34 +106,24 @@ static void MC_init_dot_output()
 
 }
 
+#ifdef HAVE_MC
 void MC_init()
 {
   MC_init_pid(getpid(), -1);
 }
 
-static void MC_init_mode(void)
-{
-  if (mc_mode == MC_MODE_NONE) {
-    if (getenv(MC_ENV_SOCKET_FD)) {
-      mc_mode = MC_MODE_CLIENT;
-    } else {
-      mc_mode = MC_MODE_STANDALONE;
-    }
-  }
-}
-
 void MC_init_pid(pid_t pid, int socket)
 {
   /* Initialize the data structures that must be persistent across every
      iteration of the model-checker (in RAW memory) */
 
   xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
-  mc_model_checker = MC_model_checker_new(pid, socket);
+  mc_model_checker = new simgrid::mc::ModelChecker(pid, socket);
 
   // It's not useful anymore:
   if (0 && mc_mode == MC_MODE_SERVER) {
     unsigned long maxpid;
-    MC_process_read_variable(&mc_model_checker->process, "simix_process_maxpid",
+    MC_process_read_variable(&mc_model_checker->process(), "simix_process_maxpid",
       &maxpid, sizeof(maxpid));
     simix_process_maxpid = maxpid;
   }
@@ -193,7 +185,7 @@ void MC_init_pid(pid_t pid, int socket)
     /* SIMIX */
     MC_ignore_global_variable("smx_total_comms");
 
-    if (mc_mode == MC_MODE_STANDALONE || mc_mode == MC_MODE_CLIENT) {
+    if (mc_mode == MC_MODE_CLIENT) {
       /* Those requests are handled on the client side and propagated by message
        * to the server: */
 
@@ -209,62 +201,18 @@ void MC_init_pid(pid_t pid, int socket)
 
   mmalloc_set_current_heap(heap);
 }
+#endif
 
 /*******************************  Core of MC *******************************/
 /**************************************************************************/
 
-void MC_do_the_modelcheck_for_real()
+void MC_run()
 {
-  MC_init_mode();
-
-  switch(mc_mode) {
-  default:
-    xbt_die("Unexpected mc mode");
-    break;
-  case MC_MODE_CLIENT:
-    MC_init();
-    MC_client_main_loop();
-    return;
-  case MC_MODE_SERVER:
-    break;
-  case MC_MODE_STANDALONE:
-    MC_init();
-    break;
-  }
-
-  if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
-    XBT_INFO("Check communication determinism");
-    mc_reduce_kind = e_mc_reduce_none;
-    MC_wait_for_requests();
-    MC_modelcheck_comm_determinism();
-  }
-
-  else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0') {
-    if(_sg_mc_termination)
-      mc_reduce_kind = e_mc_reduce_none;
-    else if (mc_reduce_kind == e_mc_reduce_unset)
-      mc_reduce_kind = e_mc_reduce_dpor;
-    _sg_mc_safety = 1;
-    if (_sg_mc_termination)
-      XBT_INFO("Check non progressive cycles");
-    else
-      XBT_INFO("Check a safety property");
-    MC_wait_for_requests();
-    MC_modelcheck_safety();
-  }
-
-  else {
-    if (mc_reduce_kind == e_mc_reduce_unset)
-      mc_reduce_kind = e_mc_reduce_none;
-    XBT_INFO("Check the liveness property %s", _sg_mc_property_file);
-    MC_automaton_load(_sg_mc_property_file);
-    MC_wait_for_requests();
-    MC_modelcheck_liveness();
-  }
-
+  mc_mode = MC_MODE_CLIENT;
+  MC_init();
+  MC_client_main_loop();
 }
 
-
 void MC_exit(void)
 {
   xbt_free(mc_time);
@@ -273,15 +221,16 @@ void MC_exit(void)
   //xbt_abort();
 }
 
+#ifdef HAVE_MC
 int MC_deadlock_check()
 {
   if (mc_mode == MC_MODE_SERVER) {
     int res;
-    if ((res = MC_protocol_send_simple_message(mc_model_checker->process.socket,
+    if ((res = MC_protocol_send_simple_message(mc_model_checker->process().socket,
       MC_MESSAGE_DEADLOCK_CHECK)))
       xbt_die("Could not check deadlock state");
     s_mc_int_message_t message;
-    ssize_t s = MC_receive_message(mc_model_checker->process.socket, &message, sizeof(message), 0);
+    ssize_t s = MC_receive_message(mc_model_checker->process().socket, &message, sizeof(message), 0);
     if (s == -1)
       xbt_die("Could not receive message");
     else if (s != sizeof(message) || message.type != MC_MESSAGE_DEADLOCK_CHECK_REPLY) {
@@ -309,6 +258,7 @@ int MC_deadlock_check()
   }
   return deadlock;
 }
+#endif
 
 /**
  * \brief Re-executes from the state at position start all the transitions indicated by
@@ -320,7 +270,7 @@ void MC_replay(xbt_fifo_t stack)
 {
   xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
 
-  int value, count = 1, j;
+  int value, count = 1;
   char *req_str;
   smx_simcall_t req = NULL, saved_req = NULL;
   xbt_fifo_item_t item, start_item;
@@ -354,10 +304,10 @@ void MC_replay(xbt_fifo_t stack)
 
   if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
     // int n = xbt_dynar_length(incomplete_communications_pattern);
-    int n = MC_smx_get_maxpid();
+    unsigned n = MC_smx_get_maxpid();
     assert(n == xbt_dynar_length(incomplete_communications_pattern));
     assert(n == xbt_dynar_length(initial_communications_pattern));
-    for (j=0; j < n ; j++) {
+    for (unsigned j=0; j < n ; j++) {
       xbt_dynar_reset((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, j, xbt_dynar_t));
       xbt_dynar_get_as(initial_communications_pattern, j, mc_list_comm_pattern_t)->index_comm = 0;
     }
@@ -759,4 +709,12 @@ void MC_report_assertion_error(void)
   MC_dump_stack_safety(mc_stack);
   MC_print_statistics(mc_stats);
 }
+
+void MC_invalidate_cache(void)
+{
+  if (mc_model_checker)
+    mc_model_checker->process().cache_flags = 0;
+}
 #endif
+
+}
similarity index 97%
rename from src/mc/mc_hash.c
rename to src/mc/mc_hash.cpp
index b83bc83..628b2eb 100644 (file)
@@ -11,6 +11,8 @@
 #include "mc/datatypes.h"
 #include <mc/mc.h>
 
+extern "C" {
+
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_hash, mc, "Logging specific to mc_hash");
 
 // This is djb2:
@@ -20,10 +22,11 @@ typedef uint64_t mc_hash_t;
 // #define MC_HASH(hash, value) hash = (((hash << 5) + hash) + (uint64_t) value)
 #define MC_HASH(hash, value) \
   { hash = (((hash << 5) + hash) + (uint64_t) value);\
-  XBT_DEBUG("%s:%i: %"PRIx64" -> %"PRIx64, __FILE__, __LINE__, (uint64_t) value, hash); }
+  XBT_DEBUG("%s:%i: %" PRIx64 " -> %" PRIx64, __FILE__, __LINE__, (uint64_t) value, hash); }
 
 // ***** Hash state
 
+#if 0
 typedef struct s_mc_hashing_state {
   // Set of pointers/addresses already processed (avoid loops):
   mc_address_set_t handled_addresses;
@@ -62,14 +65,12 @@ static bool mc_ignored(const void *address, size_t size)
 
 static void mc_hash_binary(mc_hash_t * hash, const void *s, size_t len)
 {
-  const char *p = (const void *) s;
-  int i;
-  for (i = 0; i != len; ++i) {
+  const char *p = (const char*) s;
+  for (size_t i = 0; i != len; ++i) {
     MC_HASH(*hash, p[i]);
   }
 }
 
-#if 0
 /** \brief Compute a hash for a given value of a given type
  *
  *  We try to be very conservative (do not hash too ambiguous things).
@@ -81,7 +82,7 @@ static void mc_hash_value(mc_hash_t * hash, mc_hashing_state * state,
                           mc_object_info_t info, const void *address,
                           dw_type_t type)
 {
-  mc_process_t process = &mc_model_checker->process;
+  mc_process_t process = &mc_model_checker->process();
 top:
 
   switch (type->type) {
@@ -323,18 +324,23 @@ uint64_t mc_hash_processes_state(int num_state, xbt_dynar_t stacks)
 {
   XBT_DEBUG("START hash %i", num_state);
 
+#if 0
   mc_hashing_state state;
   mc_hash_state_init(&state);
+#endif
 
   mc_hash_t hash = MC_HASH_INIT;
 
   MC_HASH(hash, xbt_swag_size(simix_global->process_list));     // process count
+#if 0
   // mc_hash_object_globals(&hash, &state, binary_info);
   // mc_hash_object_globals(&hash, &state, libsimgrid_info);
   // mc_hash_stacks(&hash, &state, stacks);
-
   mc_hash_state_destroy(&state);
+#endif
 
   XBT_DEBUG("END hash %i", num_state);
   return hash;
 }
+
+}
similarity index 98%
rename from src/mc/mc_ignore.c
rename to src/mc/mc_ignore.cpp
index 051a1f4..1239c3c 100644 (file)
@@ -13,6 +13,8 @@
 #include "mc_protocol.h"
 #include "mc_client.h"
 
+extern "C" {
+
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_ignore, mc,
                                 "Logging specific to MC ignore mechanism");
 
@@ -163,6 +165,7 @@ void MC_remove_ignore_heap(void *address, size_t size)
     message.addr = address;
     message.size = size;
     MC_client_send_message(&message, sizeof(message));
+    return;
   }
 
   xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
@@ -204,7 +207,7 @@ void MC_remove_ignore_heap(void *address, size_t size)
 // MCer
 void MC_ignore_global_variable(const char *name)
 {
-  mc_process_t process = &mc_model_checker->process;
+  mc_process_t process = &mc_model_checker->process();
   xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
   xbt_assert(process->object_infos, "MC subsystem not initialized");
 
@@ -313,7 +316,7 @@ static void MC_ignore_local_variable_in_object(const char *var_name,
 // MCer
 void MC_ignore_local_variable(const char *var_name, const char *frame_name)
 {
-  mc_process_t process = &mc_model_checker->process;
+  mc_process_t process = &mc_model_checker->process();
   if (strcmp(frame_name, "*") == 0)
     frame_name = NULL;
   xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
@@ -427,3 +430,5 @@ void MC_process_ignore_memory(mc_process_t process, void *addr, size_t size)
     }
   }
 }
+
+}
diff --git a/src/mc/mc_interface.h b/src/mc/mc_interface.h
deleted file mode 100644 (file)
index 0bf35d0..0000000
+++ /dev/null
@@ -1,18 +0,0 @@
-/* MC interface: definitions that non-MC modules must see, but not the user */
-
-/* Copyright (c) 2007-2014. The SimGrid Team.  All rights reserved.         */
-
-/* This program is free software; you can redistribute it and/or modify it
- * under the terms of the license (GNU LGPL) which comes with this package. */
-
-#ifndef MC_INTERFACE_H
-#define MC_INTERFACE_H
-#include "mc/mc.h"
-
-SG_BEGIN_DECL()
-
-typedef struct s_mc_snapshot s_mc_snapshot_t, *mc_snapshot_t;
-
-SG_END_DECL()
-
-#endif
similarity index 97%
rename from src/mc/mc_liveness.c
rename to src/mc/mc_liveness.cpp
index 8505daf..41be27f 100644 (file)
 #include "mc_record.h"
 #include "mc_smx.h"
 #include "mc_client.h"
+#include "mc_replay.h"
+#include "mc_safety.h"
+
+extern "C" {
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
                                 "Logging specific to algorithms for liveness properties verification");
@@ -376,7 +380,7 @@ static void MC_modelcheck_liveness_main(void)
     
       /* Traverse the stack backwards until a pair with a non empty interleave
          set is found, deleting all the pairs that have it empty in the way. */
-      while ((current_pair = xbt_fifo_shift(mc_stack)) != NULL) {
+      while ((current_pair = (mc_pair_t) xbt_fifo_shift(mc_stack)) != NULL) {
         if (current_pair->requests > 0) {
           /* We found a backtracking point */
           XBT_DEBUG("Backtracking to depth %d", current_pair->depth);
@@ -403,6 +407,12 @@ static void MC_modelcheck_liveness_main(void)
 
 void MC_modelcheck_liveness(void)
 {
+  if (mc_reduce_kind == e_mc_reduce_unset)
+    mc_reduce_kind = e_mc_reduce_none;
+  XBT_INFO("Check the liveness property %s", _sg_mc_property_file);
+  MC_automaton_load(_sg_mc_property_file);
+  MC_wait_for_requests();
+
   XBT_DEBUG("Starting the liveness algorithm");
   _sg_mc_liveness = 1;
 
@@ -425,3 +435,5 @@ void MC_modelcheck_liveness(void)
   mmalloc_set_current_heap(heap);
 
 }
+
+}
index 5c450ca..4f07cb8 100644 (file)
@@ -14,7 +14,7 @@
 #include <elfutils/libdw.h>
 
 #include <simgrid_config.h>
-#include "mc_interface.h"
+#include "mc_forward.h"
 #include "mc_object_info.h"
 #include "mc_forward.h"
 #include "mc_address_space.h"
similarity index 97%
rename from src/mc/mc_member.c
rename to src/mc/mc_member.cpp
index 666a246..a75a9af 100644 (file)
@@ -4,9 +4,13 @@
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
+#include <xbt/misc.h>
+
 #include "mc_object_info.h"
 #include "mc_private.h"
 
+extern "C" {
+
 /** Resolve snapshot in the process address space
  *
  * @param object   Process address of the struct/class
@@ -39,3 +43,5 @@ void *mc_member_resolve(const void *base, dw_type_t type, dw_type_t member,
   else
     return (void *) state.stack[state.stack_size - 1];
 }
+
+}
similarity index 99%
rename from src/mc/mc_memory.c
rename to src/mc/mc_memory.cpp
index 72f51a9..6f83983 100644 (file)
@@ -15,6 +15,8 @@
 #include "mc_object_info.h"
 #include "mc_private.h"
 
+extern "C" {
+
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_memory, mc,
                                 "Logging specific to MC (memory)");
 
@@ -49,3 +51,5 @@ void MC_memory_exit(void)
   if (mc_heap && mc_heap != std_heap)
     xbt_mheap_destroy(mc_heap);
 }
+
+}
index 4ceecbd..b59d7d7 100644 (file)
@@ -7,6 +7,7 @@
 #ifndef MC_MMALLOC_H
 #define MC_MMALLOC_H
 
+#include <xbt/misc.h>
 #include <xbt/mmalloc.h>
 
 /** file
@@ -16,7 +17,9 @@
  *  Normally the system should operate in std, for switching to raw mode
  *  you must wrap the code between MC_SET_RAW_MODE and MC_UNSET_RAW_MODE.
  */
+
+SG_BEGIN_DECL()
+
 extern xbt_mheap_t std_heap;
 extern xbt_mheap_t mc_heap;
 
@@ -35,4 +38,6 @@ extern xbt_mheap_t mc_heap;
 #define MC_SET_MC_HEAP    mmalloc_set_current_heap(mc_heap)
 #define MC_SET_STD_HEAP  mmalloc_set_current_heap(std_heap)
 
+SG_END_DECL()
+
 #endif
diff --git a/src/mc/mc_model_checker.c b/src/mc/mc_model_checker.c
deleted file mode 100644 (file)
index 98aa299..0000000
+++ /dev/null
@@ -1,41 +0,0 @@
-/* Copyright (c) 2008-2014. The SimGrid Team.
- * All rights reserved.                                                     */
-
-/* This program is free software; you can redistribute it and/or modify it
- * under the terms of the license (GNU LGPL) which comes with this package. */
-
-#include "mc_model_checker.h"
-#include "mc_page_store.h"
-
-mc_model_checker_t mc_model_checker = NULL;
-
-mc_model_checker_t MC_model_checker_new(pid_t pid, int socket)
-{
-  mc_model_checker_t mc = xbt_new0(s_mc_model_checker_t, 1);
-  mc->pages = mc_pages_store_new();
-  mc->fd_clear_refs = -1;
-  mc->fd_pagemap = -1;
-  MC_process_init(&mc->process, pid, socket);
-  mc->hosts = xbt_dict_new();
-  return mc;
-}
-
-void MC_model_checker_delete(mc_model_checker_t mc)
-{
-  mc_pages_store_delete(mc->pages);
-  if(mc->record)
-    xbt_dynar_free(&mc->record);
-  MC_process_clear(&mc->process);
-  xbt_dict_free(&mc->hosts);
-}
-
-unsigned long MC_smx_get_maxpid(void)
-{
-  if (mc_mode == MC_MODE_STANDALONE)
-    return simix_process_maxpid;
-
-  unsigned long maxpid;
-  MC_process_read_variable(&mc_model_checker->process, "simix_process_maxpid",
-    &maxpid, sizeof(maxpid));
-  return maxpid;
-}
diff --git a/src/mc/mc_model_checker.h b/src/mc/mc_model_checker.h
deleted file mode 100644 (file)
index 1dee19e..0000000
+++ /dev/null
@@ -1,47 +0,0 @@
-/* Copyright (c) 2007-2014. The SimGrid Team.
- * All rights reserved.                                                     */
-
-/* This program is free software; you can redistribute it and/or modify it
- * under the terms of the license (GNU LGPL) which comes with this package. */
-#ifndef MC_MODEL_CHECKER_H
-#define MC_MODEL_CHECKER_H
-
-#include <sys/types.h>
-
-#include <simgrid_config.h>
-#include <xbt/dynar.h>
-
-#include "mc_forward.h"
-#include "mc_process.h"
-#include "mc_page_store.h"
-#include "mc_protocol.h"
-
-SG_BEGIN_DECL()
-
-/** @brief State of the model-checker (global variables for the model checker)
- *
- *  Each part of the state of the model chercker represented as a global
- *  variable prevents some sharing between snapshots and must be ignored.
- *  By moving as much state as possible in this structure allocated
- *  on the model-chercker heap, we avoid those issues.
- */
-struct s_mc_model_checker {
-  // This is the parent snapshot of the current state:
-  mc_snapshot_t parent_snapshot;
-  mc_pages_store_t pages;
-  int fd_clear_refs;
-  int fd_pagemap;
-  xbt_dynar_t record;
-  s_mc_process_t process;
-  /** String pool for host names */
-  xbt_dict_t /* <hostname, NULL> */ hosts;
-};
-
-mc_model_checker_t MC_model_checker_new(pid_t pid, int socket);
-void MC_model_checker_delete(mc_model_checker_t mc);
-unsigned long MC_smx_get_maxpid(void);
-
-SG_END_DECL()
-
-#endif
similarity index 75%
rename from src/mc/mc_object_info.c
rename to src/mc/mc_object_info.cpp
index 874235c..95f9e2a 100644 (file)
@@ -1,3 +1,9 @@
+/* Copyright (c) 2014-2015. The SimGrid Team.
+ * All rights reserved.                                                     */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
 #include <stddef.h>
 
 #include <xbt/dynar.h>
@@ -5,6 +11,8 @@
 #include "mc_object_info.h"
 #include "mc_private.h"
 
+extern "C" {
+
 dw_frame_t MC_file_object_info_find_function(mc_object_info_t info, const void *ip)
 {
   xbt_dynar_t dynar = info->functions_index;
@@ -36,3 +44,5 @@ dw_variable_t MC_file_object_info_find_variable_by_name(mc_object_info_t info, c
 
   return NULL;
 }
+
+}
index 9914c56..bb5814b 100644 (file)
@@ -53,13 +53,13 @@ void dw_variable_free_voidp(void *t);
 
 // ***** Object info
 
-enum mc_object_info_flags {
-  MC_OBJECT_INFO_NONE = 0,
-  MC_OBJECT_INFO_EXECUTABLE = 1
-};
+/** Bit field of options */
+typedef int mc_object_info_flags;
+#define MC_OBJECT_INFO_NONE 0
+#define MC_OBJECT_INFO_EXECUTABLE 1
 
 struct s_mc_object_info {
-  enum mc_object_info_flags flags;
+  mc_object_info_flags flags;
   char* file_name;
   const void* start, *end;
   char *start_exec, *end_exec; // Executable segment
index 72997ba..72d71c1 100644 (file)
@@ -7,16 +7,13 @@
 
 #include <unistd.h> // pread, pwrite
 
-#include "mc_page_store.h"
+#include "PageStore.hpp"
 #include "mc_mmu.h"
 #include "mc_private.h"
 #include "mc_snapshot.h"
 
 #include <xbt/mmalloc.h>
 
-#define SOFT_DIRTY_BIT_NUMBER 55
-#define SOFT_DIRTY (((uint64_t)1) << SOFT_DIRTY_BIT_NUMBER)
-
 extern "C" {
 
 // ***** Region management:
@@ -25,12 +22,10 @@ extern "C" {
  *
  *  @param data            The start of the region (must be at the beginning of a page)
  *  @param pag_count       Number of pages of the region
- *  @param pagemap         Linux kernel pagemap values fot this region (or NULL)
- *  @param reference_pages Snapshot page numbers of the previous soft_dirty_reset (or NULL)
  *  @return                Snapshot page numbers of this new snapshot
  */
 size_t* mc_take_page_snapshot_region(mc_process_t process,
-  void* data, size_t page_count, uint64_t* pagemap, size_t* reference_pages)
+  void* data, size_t page_count)
 {
   size_t* pagenos = (size_t*) malloc(page_count * sizeof(size_t));
 
@@ -41,12 +36,7 @@ size_t* mc_take_page_snapshot_region(mc_process_t process,
     temp = malloc(xbt_pagesize);
 
   for (size_t i=0; i!=page_count; ++i) {
-    bool softclean = pagemap && !(pagemap[i] & SOFT_DIRTY);
-    if (softclean && reference_pages) {
-      // The page is softclean, it is the same page as the reference page:
-      pagenos[i] = reference_pages[i];
-      mc_model_checker->pages->ref_page(reference_pages[i]);
-    } else {
+
       // Otherwise, we need to store the page the hard way
       // (by reading its content):
       void* page = (char*) data + (i << xbt_pagebits);
@@ -66,8 +56,8 @@ size_t* mc_take_page_snapshot_region(mc_process_t process,
         MC_process_read(process, MC_ADDRESS_SPACE_READ_FLAGS_NONE,
           temp, page, xbt_pagesize, MC_PROCESS_INDEX_DISABLED);
       }
-      pagenos[i] = mc_model_checker->pages->store_page(page_data);
-    }
+      pagenos[i] = mc_model_checker->page_store().store_page(page_data);
+
   }
 
   free(temp);
@@ -77,7 +67,7 @@ size_t* mc_take_page_snapshot_region(mc_process_t process,
 void mc_free_page_snapshot_region(size_t* pagenos, size_t page_count)
 {
   for (size_t i=0; i!=page_count; ++i) {
-    mc_model_checker->pages->unref_page(pagenos[i]);
+    mc_model_checker->page_store().unref_page(pagenos[i]);
   }
 }
 
@@ -89,115 +79,24 @@ void mc_free_page_snapshot_region(size_t* pagenos, size_t page_count)
  *  @param start_addr
  *  @param page_count       Number of pages of the region
  *  @param pagenos
- *  @param pagemap         Linux kernel pagemap values fot this region (or NULL)
- *  @param reference_pages Snapshot page numbers of the previous soft_dirty_reset (or NULL)
  */
 void mc_restore_page_snapshot_region(mc_process_t process,
-  void* start_addr, size_t page_count, size_t* pagenos, uint64_t* pagemap, size_t* reference_pagenos)
+  void* start_addr, size_t page_count, size_t* pagenos)
 {
   for (size_t i=0; i!=page_count; ++i) {
-
-    bool softclean = pagemap && !(pagemap[i] & SOFT_DIRTY);
-    if (softclean && reference_pagenos && pagenos[i] == reference_pagenos[i]) {
-      // The page is softclean and is the same as the reference one:
-      // the page is already in the target state.
-      continue;
-    }
-
     // Otherwise, copy the page:
     void* target_page = mc_page_from_number(start_addr, i);
-    const void* source_page = mc_model_checker->pages->get_page(pagenos[i]);
+    const void* source_page = mc_model_checker->page_store().get_page(pagenos[i]);
     MC_process_write(process, source_page, target_page, xbt_pagesize);
   }
 }
 
-// ***** Soft dirty tracking
-
-/** @brief Like pread() but without partial reads */
-static size_t pread_whole(int fd, void* buf, size_t count, off_t offset) {
-  size_t res = 0;
-
-  char* data = (char*) buf;
-  while(count) {
-    ssize_t n = pread(fd, buf, count, offset);
-    // EOF
-    if (n==0)
-      return res;
-
-    // Error (or EINTR):
-    if (n==-1) {
-      if (errno == EINTR)
-        continue;
-      else
-        return -1;
-    }
-
-    // It might be a partial read:
-    count -= n;
-    data += n;
-    offset += n;
-    res += n;
-  }
-
-  return res;
-}
-
-static inline  __attribute__ ((always_inline))
-void mc_ensure_fd(int* fd, const char* path, int flags) {
-  if (*fd != -1)
-    return;
-  *fd = open(path, flags);
-  if (*fd == -1) {
-    xbt_die("Could not open file %s", path);
-  }
-}
-
-/** @brief Reset the soft-dirty bits
- *
- *  This is done after checkpointing and after checkpoint restoration
- *  (if per page checkpoiting is used) in order to know which pages were
- *  modified.
- *
- *  See https://www.kernel.org/doc/Documentation/vm/soft-dirty.txt
- * */
-void mc_softdirty_reset() {
-  mc_ensure_fd(&mc_model_checker->fd_clear_refs, "/proc/self/clear_refs", O_WRONLY|O_CLOEXEC);
-  if( ::write(mc_model_checker->fd_clear_refs, "4\n", 2) != 2) {
-    xbt_die("Could not reset softdirty bits");
-  }
-}
-
-/** @brief Read memory page informations
- *
- *  For each virtual memory page of the process,
- *  /proc/self/pagemap provides a 64 bit field of information.
- *  We are interested in the soft-dirty bit: with this we can track which
- *  pages were modified between snapshots/restorations and avoid
- *  copying data which was not modified.
- *
- *  See https://www.kernel.org/doc/Documentation/vm/pagemap.txt
- *
- *  @param pagemap    Output buffer for pagemap informations
- *  @param start_addr Address of the first page
- *  @param page_count Number of pages
- */
-static void mc_read_pagemap(uint64_t* pagemap, size_t page_start, size_t page_count)
-{
-  mc_ensure_fd(&mc_model_checker->fd_pagemap, "/proc/self/pagemap", O_RDONLY|O_CLOEXEC);
-  size_t bytesize = sizeof(uint64_t) * page_count;
-  off_t offset = sizeof(uint64_t) * page_start;
-  if (pread_whole(mc_model_checker->fd_pagemap, pagemap, bytesize, offset) != bytesize) {
-    xbt_die("Could not read pagemap");
-  }
-}
-
 // ***** High level API
 
 mc_mem_region_t mc_region_new_sparse(mc_region_type_t region_type,
-  void *start_addr, void* permanent_addr, size_t size,
-  mc_mem_region_t ref_reg)
+  void *start_addr, void* permanent_addr, size_t size)
 {
-  mc_process_t process = &mc_model_checker->process;
+  mc_process_t process = &mc_model_checker->process();
 
   mc_mem_region_t region = xbt_new(s_mc_mem_region_t, 1);
   region->region_type = region_type;
@@ -212,54 +111,21 @@ mc_mem_region_t mc_region_new_sparse(mc_region_type_t region_type,
     "Not at the beginning of a page");
   size_t page_count = mc_page_count(size);
 
-  uint64_t* pagemap = NULL;
-  if (_sg_mc_soft_dirty && mc_model_checker->parent_snapshot &&
-      MC_process_is_self(process)) {
-      pagemap = (uint64_t*) malloc_no_memset(sizeof(uint64_t) * page_count);
-      mc_read_pagemap(pagemap, mc_page_number(NULL, permanent_addr), page_count);
-  }
-
-  size_t* reg_page_numbers = NULL;
-  if (ref_reg!=NULL && ref_reg->storage_type == MC_REGION_STORAGE_TYPE_CHUNKED)
-    reg_page_numbers = ref_reg->chunked.page_numbers;
-
   // Take incremental snapshot:
   region->chunked.page_numbers = mc_take_page_snapshot_region(process,
-    permanent_addr, page_count, pagemap, reg_page_numbers);
+    permanent_addr, page_count);
 
-  if(pagemap) {
-    mfree(mc_heap, pagemap);
-  }
   return region;
 }
 
-void mc_region_restore_sparse(mc_process_t process, mc_mem_region_t reg, mc_mem_region_t ref_reg)
+void mc_region_restore_sparse(mc_process_t process, mc_mem_region_t reg)
 {
   xbt_assert((((uintptr_t)reg->permanent_addr) & (xbt_pagesize-1)) == 0,
     "Not at the beginning of a page");
   size_t page_count = mc_page_count(reg->size);
 
-  uint64_t* pagemap = NULL;
-
-  // Read soft-dirty bits if necessary in order to know which pages have changed:
-  if (_sg_mc_soft_dirty && mc_model_checker->parent_snapshot
-      && MC_process_is_self(process)) {
-    pagemap = (uint64_t*) malloc_no_memset(sizeof(uint64_t) * page_count);
-    mc_read_pagemap(pagemap, mc_page_number(NULL, reg->permanent_addr), page_count);
-  }
-
-  // Incremental per-page snapshot restoration:s
-  size_t* reg_page_numbers = NULL;
-  if (ref_reg && ref_reg->storage_type == MC_REGION_STORAGE_TYPE_CHUNKED)
-    reg_page_numbers = ref_reg->chunked.page_numbers;
-
   mc_restore_page_snapshot_region(process,
-    reg->permanent_addr, page_count, reg->chunked.page_numbers,
-    pagemap, reg_page_numbers);
-
-  if(pagemap) {
-    free(pagemap);
-  }
+    reg->permanent_addr, page_count, reg->chunked.page_numbers);
 }
 
 }
similarity index 98%
rename from src/mc/mc_pair.c
rename to src/mc/mc_pair.cpp
index ee3ad5d..7f754cd 100644 (file)
@@ -8,6 +8,8 @@
 #include "mc_liveness.h"
 #include "mc_private.h"
 
+extern "C" {
+
 mc_pair_t MC_pair_new()
 {
   mc_pair_t p = NULL;
@@ -33,3 +35,5 @@ void mc_pair_free_voidp(void *p)
 {
   MC_pair_delete((mc_pair_t) * (void **) p);
 }
+
+}
index c19aa1f..85e0f21 100644 (file)
@@ -124,15 +124,6 @@ typedef struct s_local_variable{
   int region;
 }s_local_variable_t, *local_variable_t;
 
-/* *********** Sets *********** */
-
-typedef struct s_mc_address_set *mc_address_set_t;
-
-mc_address_set_t mc_address_set_new(void);
-void mc_address_set_free(mc_address_set_t* p);
-void mc_address_add(mc_address_set_t p, const void* value);
-bool mc_address_test(mc_address_set_t p, const void* value);
-
 /* *********** Hash *********** */
 
 /** \brief Hash the current state
@@ -153,6 +144,8 @@ void MC_dump_stacks(FILE* file);
 
 void MC_report_assertion_error(void);
 
+void MC_invalidate_cache(void);
+
 SG_END_DECL()
 
 #endif
similarity index 92%
rename from src/mc/mc_process.c
rename to src/mc/mc_process.cpp
index e49a7e2..31e79cf 100644 (file)
@@ -1,3 +1,9 @@
+/* Copyright (c) 2014-2015. The SimGrid Team.
+ * All rights reserved.                                                     */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
 #include <assert.h>
 #include <stddef.h>
 #include <stdbool.h>
@@ -28,6 +34,8 @@
 #include "mc_smx.h"
 #include "mc_server.h"
 
+extern "C" {
+
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_process, mc,
                                 "MC process information");
 
@@ -43,8 +51,8 @@ static mc_process_t MC_process_get_process(mc_process_t p) {
 }
 
 static const s_mc_address_space_class_t mc_process_class = {
-  .read = (void*) &MC_process_read,
-  .get_process = (void*) MC_process_get_process
+  .read = (mc_address_space_class_read_callback_t) &MC_process_read,
+  .get_process = (mc_address_space_class_get_process_callback_t) MC_process_get_process
 };
 
 bool MC_is_process(mc_address_space_t p)
@@ -66,7 +74,7 @@ void MC_process_init(mc_process_t process, pid_t pid, int sockfd)
   process->status = 0;
   process->memory_map = MC_get_memory_map(pid);
   process->memory_file = -1;
-  process->cache_flags = 0;
+  process->cache_flags = MC_PROCESS_CACHE_FLAG_NONE;
   process->heap = NULL;
   process->heap_info = NULL;
   MC_process_init_memory_map_info(process);
@@ -135,7 +143,7 @@ void MC_process_clear(mc_process_t process)
   unw_destroy_addr_space(process->unw_addr_space);
   process->unw_addr_space = NULL;
 
-  process->cache_flags = 0;
+  process->cache_flags = MC_PROCESS_CACHE_FLAG_NONE;
 
   free(process->heap);
   process->heap = NULL;
@@ -150,7 +158,7 @@ void MC_process_refresh_heap(mc_process_t process)
   // Read/dereference/refresh the std_heap pointer:
   if (!process->heap) {
     xbt_mheap_t oldheap  = mmalloc_set_current_heap(mc_heap);
-    process->heap = malloc(sizeof(struct mdesc));
+    process->heap = (struct mdesc*) malloc(sizeof(struct mdesc));
     mmalloc_set_current_heap(oldheap);
   }
   MC_process_read(process, MC_ADDRESS_SPACE_READ_FLAGS_NONE,
@@ -169,7 +177,7 @@ void MC_process_refresh_malloc_info(mc_process_t process)
     (process->heap->heaplimit + 1) * sizeof(malloc_info);
 
   xbt_mheap_t heap  = mmalloc_set_current_heap(mc_heap);
-  process->heap_info = realloc(process->heap_info, malloc_info_bytesize);
+  process->heap_info = (malloc_info*) realloc(process->heap_info, malloc_info_bytesize);
   mmalloc_set_current_heap(heap);
 
   MC_process_read(process, MC_ADDRESS_SPACE_READ_FLAGS_NONE,
@@ -262,8 +270,7 @@ static void MC_process_init_memory_map_info(mc_process_t process)
 
   const char* current_name = NULL;
 
-  size_t i = 0;
-  for (i=0; i < maps->mapsize; i++) {
+  for (ssize_t i=0; i < maps->mapsize; i++) {
     map_region_t reg = &(maps->regions[i]);
     const char* pathname = maps->regions[i].pathname;
 
@@ -319,7 +326,7 @@ static void MC_process_init_memory_map_info(mc_process_t process)
   regfree(&res.version_re);
 
   // Resolve time (including accress differents objects):
-  for (i=0; i!=process->object_infos_size; ++i)
+  for (size_t i=0; i!=process->object_infos_size; ++i)
     MC_post_process_object_info(process, process->object_infos[i]);
 
   xbt_assert(process->maestro_stack_start, "Did not find maestro_stack_start");
@@ -408,10 +415,10 @@ void MC_process_read_variable(mc_process_t process, const char* name, void* targ
     xbt_die("No simple location for this variable");
   if (!var->type->full_type)
     xbt_die("Partial type for %s, cannot check size", name);
-  if (var->type->full_type->byte_size != size)
+  if ((size_t) var->type->full_type->byte_size != size)
     xbt_die("Unexpected size for %s (expected %zi, was %zi)",
       name, size, (size_t) var->type->full_type->byte_size);
-  MC_process_read(process, MC_PROCESS_NO_FLAG, target, var->address, size,
+  MC_process_read(process, MC_ADDRESS_SPACE_READ_FLAGS_NONE, target, var->address, size,
     MC_PROCESS_INDEX_ANY);
 }
 
@@ -422,8 +429,8 @@ char* MC_process_read_string(mc_process_t process, void* address)
   if (MC_process_is_self(process))
     return strdup((char*) address);
 
-  size_t len = 128;
-  char* res = malloc(len);
+  off_t len = 128;
+  char* res = (char*) malloc(len);
   off_t off = 0;
 
   while (1) {
@@ -444,7 +451,7 @@ char* MC_process_read_string(mc_process_t process, void* address)
     off += c;
     if (off == len) {
       len *= 2;
-      res = realloc(res, len);
+      res = (char*) realloc(res, len);
     }
   }
 }
@@ -456,7 +463,7 @@ int MC_process_vm_open(pid_t pid, int flags)
   const size_t buffer_size = 30;
   char buffer[buffer_size];
   int res = snprintf(buffer, buffer_size, "/proc/%lli/mem", (long long) pid);
-  if (res < 0 || res >= buffer_size) {
+  if (res < 0 || (size_t) res >= buffer_size) {
     errno = ENAMETOOLONG;
     return -1;
   }
@@ -512,7 +519,7 @@ static ssize_t pwrite_whole(int fd, const void *buf, size_t count, off_t offset)
   return real_count;
 }
 
-const void* MC_process_read(mc_process_t process, e_adress_space_read_flags_t flags,
+const void* MC_process_read(mc_process_t process, adress_space_read_flags_t flags,
   void* local, const void* remote, size_t len,
   int process_index)
 {
@@ -545,7 +552,7 @@ const void* MC_process_read(mc_process_t process, e_adress_space_read_flags_t fl
 const void* MC_process_read_simple(mc_process_t process,
   void* local, const void* remote, size_t len)
 {
-  e_adress_space_read_flags_t flags = MC_PROCESS_NO_FLAG;
+  adress_space_read_flags_t flags = MC_ADDRESS_SPACE_READ_FLAGS_NONE;
   int index = MC_PROCESS_INDEX_ANY;
    MC_process_read(process, flags, local, remote, len, index);
    return local;
@@ -614,22 +621,4 @@ void MC_process_clear_memory(mc_process_t process, void* remote, size_t len)
   }
 }
 
-void MC_simcall_handle(smx_simcall_t req, int value)
-{
-  if (MC_process_is_self(&mc_model_checker->process)) {
-    SIMIX_simcall_handle(req, value);
-    return;
-  }
-
-  unsigned i;
-  mc_smx_process_info_t pi = NULL;
-
-  xbt_dynar_foreach_ptr(mc_model_checker->process.smx_process_infos, i, pi) {
-    if (req == &pi->copy.simcall) {
-      MC_server_simcall_handle(&mc_model_checker->process, pi->copy.pid, value);
-      return;
-    }
-  }
-
-  xbt_die("Could not find the request");
 }
index 5e2175c..d10a28c 100644 (file)
@@ -11,7 +11,6 @@
 #include <sys/types.h>
 
 #include "simgrid_config.h"
-
 #include <sys/types.h>
 
 #include <xbt/mmalloc.h>
@@ -20,6 +19,7 @@
 #include "xbt/mmalloc/mmprivate.h"
 #endif
 
+#include <simgrid/simix.h>
 #include "simix/popping_private.h"
 #include "simix/smx_private.h"
 
@@ -33,18 +33,17 @@ SG_BEGIN_DECL()
 
 int MC_process_vm_open(pid_t pid, int flags);
 
-typedef enum {
-  MC_PROCESS_NO_FLAG = 0,
-  MC_PROCESS_SELF_FLAG = 1,
-} e_mc_process_flags_t;
+typedef int mc_process_flags_t;
+#define MC_PROCESS_NO_FLAG 0
+#define MC_PROCESS_SELF_FLAG 1
 
 // Those flags are used to track down which cached information
 // is still up to date and which information needs to be updated.
-typedef enum {
-  MC_PROCESS_CACHE_FLAG_HEAP = 1,
-  MC_PROCESS_CACHE_FLAG_MALLOC_INFO = 2,
-  MC_PROCESS_CACHE_FLAG_SIMIX_PROCESSES = 4,
-} e_mc_process_cache_flags_t ;
+typedef int mc_process_cache_flags_t;
+#define MC_PROCESS_CACHE_FLAG_NONE 0
+#define MC_PROCESS_CACHE_FLAG_HEAP 1
+#define MC_PROCESS_CACHE_FLAG_MALLOC_INFO 2
+#define MC_PROCESS_CACHE_FLAG_SIMIX_PROCESSES 4
 
 typedef struct s_mc_smx_process_info s_mc_smx_process_info_t, *mc_smx_process_info_t;
 
@@ -52,7 +51,7 @@ typedef struct s_mc_smx_process_info s_mc_smx_process_info_t, *mc_smx_process_in
  */
 struct s_mc_process {
   s_mc_address_space_t address_space;
-  e_mc_process_flags_t process_flags;
+  mc_process_flags_t process_flags;
   pid_t pid;
   int socket;
   int status;
@@ -78,7 +77,7 @@ struct s_mc_process {
   xbt_dynar_t smx_old_process_infos;
 
   /** State of the cache (which variables are up to date) */
-  e_mc_process_cache_flags_t cache_flags;
+  mc_process_cache_flags_t cache_flags;
 
   /** Address of the heap structure in the MCed process. */
   void* heap_address;
@@ -158,7 +157,7 @@ bool MC_process_is_self(mc_process_t process)
  *  @param len     data size
  */
 const void* MC_process_read(mc_process_t process,
-  e_adress_space_read_flags_t flags,
+  adress_space_read_flags_t flags,
   void* local, const void* remote, size_t len,
   int process_index);
 
@@ -213,6 +212,8 @@ static inline malloc_info* MC_process_get_malloc_info(mc_process_t process)
  */
 dw_variable_t MC_process_find_variable_by_name(mc_process_t process, const char* name);
 
+void MC_invalidate_cache(void);
+
 SG_END_DECL()
 
 #endif
similarity index 94%
rename from src/mc/mc_protocol.c
rename to src/mc/mc_protocol.cpp
index c519797..01c4f9d 100644 (file)
@@ -15,6 +15,8 @@
 #include "mc_protocol.h"
 #include "mc_client.h"
 
+extern "C" {
+
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_protocol, mc, "Generic MC protocol logic");
 
 int MC_protocol_send(int socket, void* message, size_t size)
@@ -32,7 +34,7 @@ int MC_protocol_send(int socket, void* message, size_t size)
   return 0;
 }
 
-int MC_protocol_send_simple_message(int socket, int type)
+int MC_protocol_send_simple_message(int socket, e_mc_message_type type)
 {
   s_mc_message_t message;
   message.type = type;
@@ -50,7 +52,7 @@ int MC_protocol_hello(int socket)
   s_mc_message_t message;
   message.type = MC_MESSAGE_NONE;
 
-  size_t s;
+  ssize_t s;
   while ((s = MC_receive_message(socket, &message, sizeof(message), 0)) == -1) {
     if (errno == EINTR)
       continue;
@@ -59,7 +61,7 @@ int MC_protocol_hello(int socket)
       return 2;
     }
   }
-  if (s < sizeof(message) || message.type != MC_MESSAGE_HELLO) {
+  if ((size_t) s < sizeof(message) || message.type != MC_MESSAGE_HELLO) {
     XBT_ERROR("Did not receive suitable HELLO message. Who are you?");
     return 3;
   }
@@ -117,8 +119,6 @@ const char* MC_mode_name(e_mc_mode_t mode)
   switch(mode) {
   case MC_MODE_NONE:
     return "NONE";
-  case MC_MODE_STANDALONE:
-    return "STANDALONE";
   case MC_MODE_CLIENT:
     return "CLIENT";
   case MC_MODE_SERVER:
@@ -127,3 +127,5 @@ const char* MC_mode_name(e_mc_mode_t mode)
     return "?";
   }
 }
+
+}
index b6507f4..722c71d 100644 (file)
@@ -27,7 +27,6 @@ SG_BEGIN_DECL()
 
 typedef enum {
   MC_MODE_NONE = 0,
-  MC_MODE_STANDALONE,
   MC_MODE_CLIENT,
   MC_MODE_SERVER
 } e_mc_mode_t;
@@ -105,7 +104,7 @@ typedef struct s_mc_register_symbol_message {
 } s_mc_register_symbol_message_t, * mc_register_symbol_message_t;
 
 int MC_protocol_send(int socket, void* message, size_t size);
-int MC_protocol_send_simple_message(int socket, int type);
+int MC_protocol_send_simple_message(int socket, e_mc_message_type type);
 int MC_protocol_hello(int socket);
 ssize_t MC_receive_message(int socket, void* message, size_t size, int options);
 
similarity index 98%
rename from src/mc/mc_record.c
rename to src/mc/mc_record.cpp
index d578168..6734597 100644 (file)
 
 #ifdef HAVE_MC
 #include "mc_private.h"
-#include "mc_model_checker.h"
 #include "mc_state.h"
 #include "mc_smx.h"
 #endif
 
+extern "C" {
+
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_record, mc,
   " Logging specific to MC record/replay facility");
 
@@ -73,7 +74,7 @@ xbt_dynar_t MC_record_from_string(const char* data)
     xbt_dynar_push(dynar, &item);
 
     // Find next chunk:
-    char* end = strchr(current, ';');
+    const char* end = strchr(current, ';');
     if(end==NULL)
       break;
     else
@@ -146,3 +147,5 @@ void MC_record_replay_init()
 {
   mc_time = xbt_new0(double, simix_process_maxpid);
 }
+
+}
diff --git a/src/mc/mc_replay.h b/src/mc/mc_replay.h
new file mode 100644 (file)
index 0000000..2918305
--- /dev/null
@@ -0,0 +1,29 @@
+/* simgrid/modelchecker.h - Formal Verification made possible in SimGrid    */
+
+/* Copyright (c) 2008-2014. The SimGrid Team.
+ * All rights reserved.                                                     */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#include <xbt/misc.h>
+
+#ifndef SIMGRID_MC_REPLAY_H
+#define SIMGRID_MC_REPLAY_H
+
+SG_BEGIN_DECL()
+
+/** Replay path (if any) in string representation
+ *
+ *  This is a path as generated by `MC_record_stack_to_string()`.
+ */
+XBT_PUBLIC_DATA(char*) MC_record_path;
+
+/** Whether the replay mode is enabled */
+static inline int MC_record_replay_is_active(void) {
+  return MC_record_path != 0;
+}
+
+SG_END_DECL()
+
+#endif
similarity index 94%
rename from src/mc/mc_request.c
rename to src/mc/mc_request.cpp
index 2af0bdb..4d0ebf4 100644 (file)
@@ -11,6 +11,8 @@
 #include "mc_private.h"
 #include "mc_smx.h"
 
+extern "C" {
+
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_request, mc,
                                 "Logging specific to MC (request)");
 
@@ -40,7 +42,7 @@ int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2)
 
   // Those are internal requests, we do not need indirection
   // because those objects are copies:
-  smx_synchro_t synchro1= NULL, synchro2=NULL;
+  smx_synchro_t synchro1 = NULL, synchro2 = NULL;
   if (r1->call == SIMCALL_COMM_WAIT) {
     synchro1 = simcall_comm_wait__get__comm(r1);
   }
@@ -273,7 +275,7 @@ char *MC_request_to_string(smx_simcall_t req, int value, e_mc_request_type_t req
     // size_t size = size_pointer ? *size_pointer : 0;
     size_t size = 0;
     if (remote_size)
-      MC_process_read_simple(&mc_model_checker->process, &size,
+      MC_process_read_simple(&mc_model_checker->process(), &size,
         remote_size, sizeof(size));
 
     type = "iRecv";
@@ -309,7 +311,7 @@ char *MC_request_to_string(smx_simcall_t req, int value, e_mc_request_type_t req
       s_smx_synchro_t synchro;
       smx_synchro_t act;
       if (use_remote_comm) {
-        MC_process_read_simple(&mc_model_checker->process, &synchro,
+        MC_process_read_simple(&mc_model_checker->process(), &synchro,
           remote_act, sizeof(synchro));
         act = &synchro;
       } else
@@ -334,7 +336,7 @@ char *MC_request_to_string(smx_simcall_t req, int value, e_mc_request_type_t req
     s_smx_synchro_t synchro;
       smx_synchro_t act;
       if (use_remote_comm) {
-        MC_process_read_simple(&mc_model_checker->process, &synchro,
+        MC_process_read_simple(&mc_model_checker->process(), &synchro,
           remote_act, sizeof(synchro));
         act = &synchro;
       } else
@@ -366,11 +368,11 @@ char *MC_request_to_string(smx_simcall_t req, int value, e_mc_request_type_t req
   case SIMCALL_COMM_WAITANY: {
     type = "WaitAny";
     s_xbt_dynar_t comms;
-    MC_process_read_simple(&mc_model_checker->process,
+    MC_process_read_simple(&mc_model_checker->process(),
       &comms,  simcall_comm_waitany__get__comms(req), sizeof(comms));
     if (!xbt_dynar_is_empty(&comms)) {
       smx_synchro_t remote_sync;
-      MC_process_read_dynar_element(&mc_model_checker->process,
+      MC_process_read_dynar_element(&mc_model_checker->process(),
         &remote_sync, simcall_comm_waitany__get__comms(req), value,
         sizeof(remote_sync));
       char* p = pointer_to_string(remote_sync);
@@ -391,7 +393,7 @@ char *MC_request_to_string(smx_simcall_t req, int value, e_mc_request_type_t req
       type = "TestAny";
       args =
           bprintf("(%d of %lu)", value + 1,
-                  MC_process_read_dynar_length(&mc_model_checker->process,
+                  MC_process_read_dynar_length(&mc_model_checker->process(),
                     simcall_comm_testany__get__comms(req)));
     }
     break;
@@ -400,10 +402,10 @@ char *MC_request_to_string(smx_simcall_t req, int value, e_mc_request_type_t req
     type = "Mutex LOCK";
 
     s_smx_mutex_t mutex;
-    MC_process_read_simple(&mc_model_checker->process, &mutex,
+    MC_process_read_simple(&mc_model_checker->process(), &mutex,
       simcall_mutex_lock__get__mutex(req), sizeof(mutex));
     s_xbt_swag_t mutex_sleeping;
-    MC_process_read_simple(&mc_model_checker->process, &mutex_sleeping,
+    MC_process_read_simple(&mc_model_checker->process(), &mutex_sleeping,
       mutex.sleeping, sizeof(mutex_sleeping));
 
     args = bprintf("locked = %d, owner = %d, sleeping = %d",
@@ -456,13 +458,13 @@ unsigned int MC_request_testany_fail(smx_simcall_t req)
 
   // Read the dynar:
   s_xbt_dynar_t comms;
-  MC_process_read_simple(&mc_model_checker->process,
+  MC_process_read_simple(&mc_model_checker->process(),
     &comms, simcall_comm_testany__get__comms(req), sizeof(comms));
 
   // Read ther dynar buffer:
   size_t buffer_size = comms.elmsize * comms.used;
   char buffer[buffer_size];
-  MC_process_read_simple(&mc_model_checker->process,
+  MC_process_read_simple(&mc_model_checker->process(),
     buffer, comms.data, buffer_size);
 
   // Iterate over the elements:
@@ -472,11 +474,11 @@ unsigned int MC_request_testany_fail(smx_simcall_t req)
 
     // Get the element:
     smx_synchro_t remote_action = NULL;
-    memcpy(buffer + comms.elmsize * cursor, &remote_action, sizeof(remote_action));
+    memcpy(&remote_action, buffer + comms.elmsize * cursor, sizeof(remote_action));
 
     // Dereference the pointer:
     s_smx_synchro_t action;
-    MC_process_read_simple(&mc_model_checker->process,
+    MC_process_read_simple(&mc_model_checker->process(),
       &action, remote_action, sizeof(action));
 
     // Finally so something useful about it:
@@ -499,14 +501,14 @@ int MC_request_is_enabled_by_idx(smx_simcall_t req, unsigned int idx)
 
   case SIMCALL_COMM_WAITANY: {
     MC_process_read_dynar_element(
-      &mc_model_checker->process, &remote_act, simcall_comm_waitany__get__comms(req),
+      &mc_model_checker->process(), &remote_act, simcall_comm_waitany__get__comms(req),
       idx, sizeof(remote_act));
     }
     break;
 
   case SIMCALL_COMM_TESTANY: {
     MC_process_read_dynar_element(
-      &mc_model_checker->process, &remote_act, simcall_comm_testany__get__comms(req),
+      &mc_model_checker->process(), &remote_act, simcall_comm_testany__get__comms(req),
       idx, sizeof(remote_act));
     }
     break;
@@ -516,7 +518,7 @@ int MC_request_is_enabled_by_idx(smx_simcall_t req, unsigned int idx)
   }
 
   s_smx_synchro_t synchro;
-  MC_process_read_simple(&mc_model_checker->process,
+  MC_process_read_simple(&mc_model_checker->process(),
     &synchro, remote_act, sizeof(synchro));
   return synchro.comm.src_proc && synchro.comm.dst_proc;
 }
@@ -562,7 +564,7 @@ char *MC_request_get_dot_output(smx_simcall_t req, int value)
     } else {
       smx_synchro_t remote_act = simcall_comm_wait__get__comm(req);
       s_smx_synchro_t synchro;
-      MC_process_read_simple(&mc_model_checker->process, &synchro,
+      MC_process_read_simple(&mc_model_checker->process(), &synchro,
         remote_act, sizeof(synchro));
 
       smx_process_t src_proc = MC_smx_resolve_process(synchro.comm.src_proc);
@@ -585,7 +587,7 @@ char *MC_request_get_dot_output(smx_simcall_t req, int value)
   case SIMCALL_COMM_TEST: {
     smx_synchro_t remote_act = simcall_comm_test__get__comm(req);
     s_smx_synchro_t synchro;
-    MC_process_read_simple(&mc_model_checker->process, &synchro,
+    MC_process_read_simple(&mc_model_checker->process(), &synchro,
       remote_act, sizeof(synchro));
     if (synchro.comm.src_proc == NULL || synchro.comm.dst_proc == NULL) {
       if (issuer->smx_host)
@@ -607,7 +609,7 @@ char *MC_request_get_dot_output(smx_simcall_t req, int value)
 
   case SIMCALL_COMM_WAITANY: {
     unsigned long comms_size = MC_process_read_dynar_length(
-      &mc_model_checker->process, simcall_comm_waitany__get__comms(req));
+      &mc_model_checker->process(), simcall_comm_waitany__get__comms(req));
     if (issuer->smx_host)
       label =
           bprintf("[(%lu)%s] WaitAny [%d of %lu]", issuer->pid,
@@ -684,3 +686,5 @@ char *MC_request_get_dot_output(smx_simcall_t req, int value)
   return str;
 
 }
+
+}
similarity index 96%
rename from src/mc/mc_safety.c
rename to src/mc/mc_safety.cpp
index 2efe90a..f05de06 100644 (file)
@@ -16,6 +16,8 @@
 
 #include "xbt/mmalloc/mmprivate.h"
 
+extern "C" {
+
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
                                 "Logging specific to MC safety verification ");
 
@@ -204,7 +206,7 @@ static void MC_modelcheck_safety_main(void)
          executed before it. If it does then add it to the interleave set of the
          state that executed that previous request. */
 
-      while ((state = xbt_fifo_shift(mc_stack)) != NULL) {
+      while ((state = (mc_state_t) xbt_fifo_shift(mc_stack))) {
         if (mc_reduce_kind == e_mc_reduce_dpor) {
           req = MC_state_get_internal_request(state);
           const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
@@ -270,6 +272,17 @@ static void MC_modelcheck_safety_main(void)
 
 void MC_modelcheck_safety(void)
 {
+  if(_sg_mc_termination)
+    mc_reduce_kind = e_mc_reduce_none;
+  else if (mc_reduce_kind == e_mc_reduce_unset)
+    mc_reduce_kind = e_mc_reduce_dpor;
+  _sg_mc_safety = 1;
+  if (_sg_mc_termination)
+    XBT_INFO("Check non progressive cycles");
+  else
+    XBT_INFO("Check a safety property");
+  MC_wait_for_requests();
+
   XBT_DEBUG("Starting the safety algorithm");
 
   _sg_mc_safety = 1;
@@ -296,3 +309,5 @@ void MC_modelcheck_safety(void)
   xbt_abort();
   //MC_exit();
 }
+
+}
index 52ca5da..0c82769 100644 (file)
@@ -11,7 +11,7 @@
 
 #include <simgrid_config.h>
 #include <xbt/dict.h>
-#include "mc_interface.h"
+#include "mc_forward.h"
 #include "mc_state.h"
 
 SG_BEGIN_DECL()
index 4b8da8b..deffb42 100644 (file)
 
 #include <xbt/log.h>
 
-#include "mc_model_checker.h"
+#include "ModelChecker.hpp"
 #include "mc_protocol.h"
 #include "mc_server.h"
 #include "mc_private.h"
 #include "mc_ignore.h"
 
+extern "C" {
+
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_server, mc, "MC server logic");
 
 // HArdcoded index for now:
@@ -90,7 +92,7 @@ void s_mc_server::shutdown()
 {
   XBT_DEBUG("Shuting down model-checker");
 
-  mc_process_t process = &mc_model_checker->process;
+  mc_process_t process = &mc_model_checker->process();
   int status = process->status;
   if (process->running) {
     XBT_DEBUG("Killing process");
@@ -105,13 +107,13 @@ void s_mc_server::shutdown()
 void s_mc_server::exit()
 {
   // Finished:
-  int status = mc_model_checker->process.status;
+  int status = mc_model_checker->process().status;
   if (WIFEXITED(status))
     ::exit(WEXITSTATUS(status));
   else if (WIFSIGNALED(status)) {
     // Try to uplicate the signal of the model-checked process.
     // This is a temporary hack so we don't try too hard.
-    kill(mc_model_checker->process.pid, WTERMSIG(status));
+    kill(mc_model_checker->process().pid, WTERMSIG(status));
     abort();
   } else {
     xbt_die("Unexpected status from model-checked process");
@@ -124,7 +126,7 @@ void s_mc_server::resume(mc_process_t process)
   int res = MC_protocol_send_simple_message(socket, MC_MESSAGE_CONTINUE);
   if (res)
     throw std::system_error(res, std::system_category());
-  process->cache_flags = (e_mc_process_cache_flags_t) 0;
+  process->cache_flags = (mc_process_cache_flags_t) 0;
 }
 
 static
@@ -194,7 +196,7 @@ bool s_mc_server::handle_events()
           if (size != sizeof(message))
             xbt_die("Broken messsage");
           memcpy(&message, buffer, sizeof(message));
-          MC_process_ignore_memory(&mc_model_checker->process,
+          MC_process_ignore_memory(&mc_model_checker->process(),
             message.addr, message.size);
           break;
         }
@@ -222,7 +224,7 @@ bool s_mc_server::handle_events()
           XBT_DEBUG("Received symbol: %s", message.name);
 
           struct mc_symbol_pointer_callback* callback = xbt_new(struct mc_symbol_pointer_callback, 1);
-          callback->process = &mc_model_checker->process;
+          callback->process = &mc_model_checker->process();
           callback->value   = message.data;
 
           MC_automaton_new_propositional_symbol_callback(message.name,
@@ -268,7 +270,7 @@ bool s_mc_server::handle_events()
 
 void s_mc_server::loop()
 {
-  while (mc_model_checker->process.running)
+  while (mc_model_checker->process().running)
     this->handle_events();
 }
 
@@ -301,7 +303,7 @@ void s_mc_server::handle_waitpid()
     if (pid == -1) {
       if (errno == ECHILD) {
         // No more children:
-        if (mc_model_checker->process.running)
+        if (mc_model_checker->process().running)
           xbt_die("Inconsistent state");
         else
           break;
@@ -311,11 +313,11 @@ void s_mc_server::handle_waitpid()
       }
     }
 
-    if (pid == mc_model_checker->process.pid) {
+    if (pid == mc_model_checker->process().pid) {
       if (WIFEXITED(status) || WIFSIGNALED(status)) {
         XBT_DEBUG("Child process is over");
-        mc_model_checker->process.status = status;
-        mc_model_checker->process.running = false;
+        mc_model_checker->process().status = status;
+        mc_model_checker->process().running = false;
       }
     }
   }
@@ -335,7 +337,7 @@ void s_mc_server::on_signal(const struct signalfd_siginfo* info)
 void MC_server_wait_client(mc_process_t process)
 {
   mc_server->resume(process);
-  while (mc_model_checker->process.running) {
+  while (mc_model_checker->process().running) {
     if (!mc_server->handle_events())
       return;
   }
@@ -348,9 +350,9 @@ void MC_server_simcall_handle(mc_process_t process, unsigned long pid, int value
   m.type  = MC_MESSAGE_SIMCALL_HANDLE;
   m.pid   = pid;
   m.value = value;
-  MC_protocol_send(mc_model_checker->process.socket, &m, sizeof(m));
-  process->cache_flags = (e_mc_process_cache_flags_t) 0;
-  while (mc_model_checker->process.running) {
+  MC_protocol_send(mc_model_checker->process().socket, &m, sizeof(m));
+  process->cache_flags = (mc_process_cache_flags_t) 0;
+  while (mc_model_checker->process().running) {
     if (!mc_server->handle_events())
       return;
   }
@@ -360,3 +362,5 @@ void MC_server_loop(mc_server_t server)
 {
   server->loop();
 }
+
+}
index 860cfac..e07d6e6 100644 (file)
@@ -7,6 +7,8 @@
 #ifndef MC_SERVER_H
 #define MC_SERVER_H
 
+#include <poll.h>
+
 #include <stdint.h>
 #include <stdbool.h>
 
diff --git a/src/mc/mc_set.cpp b/src/mc/mc_set.cpp
deleted file mode 100644 (file)
index 03613c4..0000000
+++ /dev/null
@@ -1,36 +0,0 @@
-/* Copyright (c) 2007-2014. The SimGrid Team.
- * All rights reserved.                                                     */
-
-/* This program is free software; you can redistribute it and/or modify it
- * under the terms of the license (GNU LGPL) which comes with this package. */
-
-#include <stddef.h>
-#include <set>
-
-typedef std::set<const void*>*  mc_address_set_t;
-
-extern "C" {
-
-mc_address_set_t mc_address_set_new();
-void mc_address_set_free(mc_address_set_t* p);
-void mc_address_add(mc_address_set_t p, const void* value);
-bool mc_address_test(mc_address_set_t p, const void* value);
-
-mc_address_set_t mc_address_set_new() {
-  return new std::set<const void*>();
-}
-
-void mc_address_set_free(mc_address_set_t* p) {
-  delete *p;
-  *p = NULL;
-}
-
-void mc_address_add(mc_address_set_t p, const void* value) {
-  p->insert(value);
-}
-
-bool mc_address_test(mc_address_set_t p, const void* value) {
-  return p->find(value) != p->end();
-}
-
-};
similarity index 79%
rename from src/mc/mc_smx.c
rename to src/mc/mc_smx.cpp
index 358e21b..12d9216 100644 (file)
@@ -11,7 +11,9 @@
 #include "simix/smx_private.h"
 
 #include "mc_smx.h"
-#include "mc_model_checker.h"
+#include "ModelChecker.hpp"
+
+extern "C" {
 
 static
 void MC_smx_process_info_clear(mc_smx_process_info_t p)
@@ -42,8 +44,8 @@ bool is_in_dynar(smx_process_t p, xbt_dynar_t dynar)
 static inline
 mc_smx_process_info_t MC_smx_process_get_info(smx_process_t p)
 {
-  assert(is_in_dynar(p, mc_model_checker->process.smx_process_infos)
-    || is_in_dynar(p, mc_model_checker->process.smx_old_process_infos));
+  assert(is_in_dynar(p, mc_model_checker->process().smx_process_infos)
+    || is_in_dynar(p, mc_model_checker->process().smx_old_process_infos));
   mc_smx_process_info_t process_info =
     (mc_smx_process_info_t)
       ((char*) p - offsetof(s_mc_smx_process_info_t, copy));
@@ -70,7 +72,7 @@ static void MC_process_refresh_simix_process_list(
 
   // Load each element of the dynar from the MCed process:
   int i = 0;
-  for (p = swag.head; p; ++i) {
+  for (p = (smx_process_t) swag.head; p; ++i) {
 
     s_mc_smx_process_info_t info;
     info.address = p;
@@ -81,7 +83,7 @@ static void MC_process_refresh_simix_process_list(
     xbt_dynar_push(target, &info);
 
     // Lookup next process address:
-    p = xbt_swag_getNext(&info.copy, swag.offset);
+    p = (smx_process_t) xbt_swag_getNext(&info.copy, swag.offset);
   }
   assert(i == swag.count);
 }
@@ -124,10 +126,10 @@ void MC_process_smx_refresh(mc_process_t process)
  */
 smx_process_t MC_smx_simcall_get_issuer(smx_simcall_t req)
 {
-  if (MC_process_is_self(&mc_model_checker->process))
+  if (MC_process_is_self(&mc_model_checker->process()))
     return req->issuer;
 
-  MC_process_smx_refresh(&mc_model_checker->process);
+  MC_process_smx_refresh(&mc_model_checker->process());
 
   // This is the address of the smx_process in the MCed process:
   void* address = req->issuer;
@@ -136,10 +138,10 @@ smx_process_t MC_smx_simcall_get_issuer(smx_simcall_t req)
   mc_smx_process_info_t p;
 
   // Lookup by address:
-  xbt_dynar_foreach_ptr(mc_model_checker->process.smx_process_infos, i, p)
+  xbt_dynar_foreach_ptr(mc_model_checker->process().smx_process_infos, i, p)
     if (p->address == address)
       return &p->copy;
-  xbt_dynar_foreach_ptr(mc_model_checker->process.smx_old_process_infos, i, p)
+  xbt_dynar_foreach_ptr(mc_model_checker->process().smx_old_process_infos, i, p)
     if (p->address == address)
       return &p->copy;
 
@@ -150,7 +152,7 @@ smx_process_t MC_smx_resolve_process(smx_process_t process_remote_address)
 {
   if (!process_remote_address)
     return NULL;
-  if (MC_process_is_self(&mc_model_checker->process))
+  if (MC_process_is_self(&mc_model_checker->process()))
     return process_remote_address;
 
   mc_smx_process_info_t process_info = MC_smx_resolve_process_info(process_remote_address);
@@ -162,15 +164,15 @@ smx_process_t MC_smx_resolve_process(smx_process_t process_remote_address)
 
 mc_smx_process_info_t MC_smx_resolve_process_info(smx_process_t process_remote_address)
 {
-  if (MC_process_is_self(&mc_model_checker->process))
+  if (MC_process_is_self(&mc_model_checker->process()))
     xbt_die("No process_info for local process is not enabled.");
 
   unsigned index;
   mc_smx_process_info_t process_info;
-  xbt_dynar_foreach_ptr(mc_model_checker->process.smx_process_infos, index, process_info)
+  xbt_dynar_foreach_ptr(mc_model_checker->process().smx_process_infos, index, process_info)
     if (process_info->address == process_remote_address)
       return process_info;
-  xbt_dynar_foreach_ptr(mc_model_checker->process.smx_old_process_infos, index, process_info)
+  xbt_dynar_foreach_ptr(mc_model_checker->process().smx_old_process_infos, index, process_info)
     if (process_info->address == process_remote_address)
       return process_info;
   xbt_die("Process info not found");
@@ -178,10 +180,10 @@ mc_smx_process_info_t MC_smx_resolve_process_info(smx_process_t process_remote_a
 
 const char* MC_smx_process_get_host_name(smx_process_t p)
 {
-  if (MC_process_is_self(&mc_model_checker->process))
+  if (MC_process_is_self(&mc_model_checker->process()))
     return SIMIX_host_get_name(p->smx_host);
 
-  mc_process_t process = &mc_model_checker->process;
+  mc_process_t process = &mc_model_checker->process();
 
   // Currently, smx_host_t = xbt_dictelm_t.
   // TODO, add an static_assert on this if switching to C++
@@ -195,25 +197,14 @@ const char* MC_smx_process_get_host_name(smx_process_t p)
     int len = host_copy.key_len + 1;
     char hostname[len];
     MC_process_read_simple(process, hostname, host_copy.key, len);
-
-    // Lookup the host name in the dictionary (or create it):
-    xbt_dictelm_t elt = xbt_dict_get_elm_or_null(mc_model_checker->hosts, hostname);
-    if (!elt) {
-      xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
-      xbt_dict_set(mc_model_checker->hosts, hostname, NULL, NULL);
-      elt = xbt_dict_get_elm_or_null(mc_model_checker->hosts, hostname);
-      assert(elt);
-      mmalloc_set_current_heap(heap);
-    }
-
-    info->hostname = elt->key;
+    info->hostname = mc_model_checker->get_host_name(hostname);
   }
   return info->hostname;
 }
 
 const char* MC_smx_process_get_name(smx_process_t p)
 {
-  mc_process_t process = &mc_model_checker->process;
+  mc_process_t process = &mc_model_checker->process();
   if (MC_process_is_self(process))
     return p->name;
   if (!p->name)
@@ -230,12 +221,22 @@ const char* MC_smx_process_get_name(smx_process_t p)
 
 int MC_smpi_process_count(void)
 {
-  if (MC_process_is_self(&mc_model_checker->process))
+  if (MC_process_is_self(&mc_model_checker->process()))
     return smpi_process_count();
   else {
     int res;
-    MC_process_read_variable(&mc_model_checker->process, "process_count",
+    MC_process_read_variable(&mc_model_checker->process(), "process_count",
       &res, sizeof(res));
     return res;
   }
 }
+
+unsigned long MC_smx_get_maxpid(void)
+{
+  unsigned long maxpid;
+  MC_process_read_variable(&mc_model_checker->process(), "simix_process_maxpid",
+    &maxpid, sizeof(maxpid));
+  return maxpid;
+}
+
+}
index 5cd2e1d..123052c 100644 (file)
@@ -45,7 +45,7 @@ struct s_mc_smx_process_info {
   /** (Flat) Copy of the process data structure */
   struct s_smx_process copy;
   /** Hostname (owned by `mc_modelchecker->hostnames`) */
-  char* hostname;
+  const char* hostname;
   char* name;
 };
 
@@ -68,15 +68,15 @@ const char* MC_smx_process_get_name(smx_process_t p);
 const char* MC_smx_process_get_host_name(smx_process_t p);
 
 #define MC_EACH_SIMIX_PROCESS(process, code) \
-  if (MC_process_is_self(&mc_model_checker->process)) { \
+  if (MC_process_is_self(&mc_model_checker->process())) { \
     xbt_swag_foreach(process, simix_global->process_list) { \
       code; \
     } \
   } else { \
-    MC_process_smx_refresh(&mc_model_checker->process); \
+    MC_process_smx_refresh(&mc_model_checker->process()); \
     unsigned int _smx_process_index; \
     mc_smx_process_info_t _smx_process_info; \
-    xbt_dynar_foreach_ptr(mc_model_checker->process.smx_process_infos, _smx_process_index, _smx_process_info) { \
+    xbt_dynar_foreach_ptr(mc_model_checker->process().smx_process_infos, _smx_process_index, _smx_process_info) { \
       smx_process_t process = &_smx_process_info->copy; \
       code; \
     } \
@@ -96,6 +96,8 @@ smx_process_t MC_smx_resolve_process(smx_process_t process_remote_address);
 /** Get the process info structure from the process remote address */
 mc_smx_process_info_t MC_smx_resolve_process_info(smx_process_t process_remote_address);
 
+unsigned long MC_smx_get_maxpid(void);
+
 SG_END_DECL()
 
 #endif
similarity index 92%
rename from src/mc/mc_snapshot.c
rename to src/mc/mc_snapshot.cpp
index 0a4f4f5..f1a1c66 100644 (file)
@@ -12,7 +12,9 @@
 #include "mc_snapshot.h"
 #include "mc_private.h"
 #include "mc_mmu.h"
-#include "mc_page_store.h"
+#include "PageStore.hpp"
+
+extern "C" {
 
 /** @brief Find the snapshoted region from a pointer
  *
@@ -38,7 +40,7 @@ mc_mem_region_t mc_get_snapshot_region(const void* addr, mc_snapshot_t snapshot,
       if (process_index < 0) {
         xbt_die("Missing process index");
       }
-      if (process_index >= region->privatized.regions_count) {
+      if (process_index >= (int) region->privatized.regions_count) {
         xbt_die("Invalid process index");
       }
       mc_mem_region_t priv_region = region->privatized.regions[process_index];
@@ -104,7 +106,7 @@ const void* MC_region_read_fragmented(mc_mem_region_t region, void* target, cons
  *  @return Pointer where the data is located (target buffer or original location)
  */
 const void* MC_snapshot_read(
-  mc_snapshot_t snapshot, e_adress_space_read_flags_t flags,
+  mc_snapshot_t snapshot, adress_space_read_flags_t flags,
   void* target, const void* addr, size_t size, int process_index)
 {
   mc_mem_region_t region = mc_get_snapshot_region(addr, snapshot, process_index);
@@ -177,12 +179,14 @@ int MC_snapshot_memcmp(
 #include "mc/mc_snapshot.h"
 #include "mc/mc_mmu.h"
 
+extern "C" {
+
 XBT_TEST_SUITE("mc_snapshot", "Snapshots");
 
 static inline void init_memory(void* mem, size_t size)
 {
   char* dest = (char*) mem;
-  for (int i=0; i!=size; ++i) {
+  for (size_t i = 0; i < size; ++i) {
     dest[i] = rand() & 255;
   }
 }
@@ -204,12 +208,10 @@ XBT_TEST_UNIT("flat_snapshot", test_flat_snapshots, "Test flat snapshots")
 static void test_snapshot(bool sparse_checkpoint) {
 
   xbt_test_add("Initialisation");
-  _sg_mc_soft_dirty = 0;
   _sg_mc_sparse_checkpoint = sparse_checkpoint;
   xbt_assert(xbt_pagesize == getpagesize());
   xbt_assert(1 << xbt_pagebits == xbt_pagesize);
-  mc_model_checker = xbt_new0(s_mc_model_checker_t, 1);
-  mc_model_checker->pages = mc_pages_store_new();
+  mc_model_checker = new ::simgrid::mc::ModelChecker(getpid(), -1);
 
   for(int n=1; n!=256; ++n) {
 
@@ -220,11 +222,13 @@ static void test_snapshot(bool sparse_checkpoint) {
 
     // Init memory and take snapshots:
     init_memory(source, byte_size);
-    mc_mem_region_t region0 = mc_region_new_sparse(MC_REGION_TYPE_UNKNOWN, source, source, byte_size, NULL);
+    mc_mem_region_t region0 = mc_region_new_sparse(
+      MC_REGION_TYPE_UNKNOWN, source, source, byte_size);
     for(int i=0; i<n; i+=2) {
       init_memory((char*) source + i*xbt_pagesize, xbt_pagesize);
     }
-    mc_mem_region_t region = mc_region_new_sparse(MC_REGION_TYPE_UNKNOWN, source, source, byte_size, NULL);
+    mc_mem_region_t region = mc_region_new_sparse(
+      MC_REGION_TYPE_UNKNOWN, source, source, byte_size);
 
     void* destination = mmap(NULL, byte_size, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0);
     xbt_assert(source!=MAP_FAILED, "Could not allocate destination memory");
@@ -267,7 +271,8 @@ static void test_snapshot(bool sparse_checkpoint) {
     if (n==1) {
       xbt_test_add("Read pointer for %i page(s)", n);
       memcpy(source, &mc_model_checker, sizeof(void*));
-      mc_mem_region_t region2 = mc_region_new_sparse(MC_REGION_TYPE_UNKNOWN, source, source, byte_size, NULL);
+      mc_mem_region_t region2 = mc_region_new_sparse(
+        MC_REGION_TYPE_UNKNOWN, source, source, byte_size);
       xbt_test_assert(MC_region_read_pointer(region2, source) == mc_model_checker,
         "Mismtach in MC_region_read_pointer()");
       MC_region_destroy(region2);
@@ -279,9 +284,12 @@ static void test_snapshot(bool sparse_checkpoint) {
     munmap(source, byte_size);
   }
 
-  mc_pages_store_delete(mc_model_checker->pages);
-  xbt_free(mc_model_checker);
+  delete mc_model_checker;
   mc_model_checker = NULL;
 }
 
+}
+
 #endif /* SIMGRID_TEST */
+
+}
index 7591a31..738fee3 100644 (file)
 #include <xbt/dynar.h>
 
 #include "mc_forward.h"
-#include "mc_model_checker.h"
-#include "mc_page_store.h"
+#include "ModelChecker.hpp"
+#include "PageStore.hpp"
 #include "mc_mmalloc.h"
 #include "mc_address_space.h"
 #include "mc_unw.h"
 
 SG_BEGIN_DECL()
 
-void mc_softdirty_reset(void);
-
 // ***** Snapshot region
 
 typedef enum e_mc_region_type_t {
@@ -99,9 +97,10 @@ struct s_mc_mem_region {
 
 };
 
-mc_mem_region_t mc_region_new_sparse(mc_region_type_t type, void *start_addr, void* data_addr, size_t size, mc_mem_region_t ref_reg);
+mc_mem_region_t mc_region_new_sparse(
+  mc_region_type_t type, void *start_addr, void* data_addr, size_t size);
 void MC_region_destroy(mc_mem_region_t reg);
-void mc_region_restore_sparse(mc_process_t process, mc_mem_region_t reg, mc_mem_region_t ref_reg);
+void mc_region_restore_sparse(mc_process_t process, mc_mem_region_t reg);
 
 static inline  __attribute__ ((always_inline))
 bool mc_region_contain(mc_mem_region_t region, const void* p)
@@ -113,10 +112,11 @@ bool mc_region_contain(mc_mem_region_t region, const void* p)
 static inline __attribute__((always_inline))
 void* mc_translate_address_region(uintptr_t addr, mc_mem_region_t region)
 {
-    size_t pageno = mc_page_number(region->start_addr, (void*) addr);
-    size_t snapshot_pageno = region->chunked.page_numbers[pageno];
-    const void* snapshot_page = mc_page_store_get_page(mc_model_checker->pages, snapshot_pageno);
-    return (char*) snapshot_page + mc_page_offset((void*) addr);
+  size_t pageno = mc_page_number(region->start_addr, (void*) addr);
+  size_t snapshot_pageno = region->chunked.page_numbers[pageno];
+  const void* snapshot_page =
+    mc_model_checker->page_store().get_page(snapshot_pageno);
+  return (char*) snapshot_page + mc_page_offset((void*) addr);
 }
 
 mc_mem_region_t mc_get_snapshot_region(const void* addr, mc_snapshot_t snapshot, int process_index);
@@ -269,19 +269,16 @@ mc_snapshot_t MC_take_snapshot(int num_state);
 void MC_restore_snapshot(mc_snapshot_t);
 void MC_free_snapshot(mc_snapshot_t);
 
-int mc_important_snapshot(mc_snapshot_t snapshot);
-
 size_t* mc_take_page_snapshot_region(mc_process_t process,
-  void* data, size_t page_count, uint64_t* pagemap, size_t* reference_pages);
+  void* data, size_t page_count);
 void mc_free_page_snapshot_region(size_t* pagenos, size_t page_count);
 void mc_restore_page_snapshot_region(
   mc_process_t process,
-  void* start_addr, size_t page_count, size_t* pagenos,
-  uint64_t* pagemap, size_t* reference_pagenos);
+  void* start_addr, size_t page_count, size_t* pagenos);
 
 const void* MC_region_read_fragmented(mc_mem_region_t region, void* target, const void* addr, size_t size);
 
-const void* MC_snapshot_read(mc_snapshot_t snapshot, e_adress_space_read_flags_t flags,
+const void* MC_snapshot_read(mc_snapshot_t snapshot, adress_space_read_flags_t flags,
   void* target, const void* addr, size_t size, int process_index);
 int MC_snapshot_region_memcmp(
   const void* addr1, mc_mem_region_t region1,
@@ -303,7 +300,7 @@ const void* mc_snapshot_get_heap_end(mc_snapshot_t snapshot)
 {
   if(snapshot==NULL)
       xbt_die("snapshot is NULL");
-  return MC_process_get_heap(&mc_model_checker->process)->breakval;
+  return MC_process_get_heap(&mc_model_checker->process())->breakval;
 }
 
 /** @brief Read memory from a snapshot region
similarity index 95%
rename from src/mc/mc_state.c
rename to src/mc/mc_state.cpp
index 8e707b2..0ebde42 100644 (file)
@@ -14,6 +14,8 @@
 #include "mc_comm_pattern.h"
 #include "mc_smx.h"
 
+extern "C" {
+
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_state, mc,
                                 "Logging specific to MC (state)");
 
@@ -103,7 +105,7 @@ void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req,
   case SIMCALL_COMM_WAITANY:
     state->internal_req.call = SIMCALL_COMM_WAIT;
     state->internal_req.issuer = req->issuer;
-    MC_process_read_dynar_element(&mc_model_checker->process,
+    MC_process_read_dynar_element(&mc_model_checker->process(),
       &state->internal_comm, simcall_comm_waitany__get__comms(req),
       value, sizeof(state->internal_comm));
     simcall_comm_wait__set__comm(&state->internal_req, &state->internal_comm);
@@ -115,7 +117,7 @@ void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req,
     state->internal_req.issuer = req->issuer;
 
     if (value > 0)
-        MC_process_read_dynar_element(&mc_model_checker->process,
+        MC_process_read_dynar_element(&mc_model_checker->process(),
           &state->internal_comm, simcall_comm_testany__get__comms(req),
           value, sizeof(state->internal_comm));
 
@@ -125,7 +127,7 @@ void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req,
 
   case SIMCALL_COMM_WAIT:
     state->internal_req = *req;
-    MC_process_read_simple(&mc_model_checker->process, &state->internal_comm ,
+    MC_process_read_simple(&mc_model_checker->process(), &state->internal_comm ,
       simcall_comm_wait__get__comm(req), sizeof(state->internal_comm));
     simcall_comm_wait__set__comm(&state->executed_req, &state->internal_comm);
     simcall_comm_wait__set__comm(&state->internal_req, &state->internal_comm);
@@ -133,13 +135,13 @@ void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req,
 
   case SIMCALL_COMM_TEST:
     state->internal_req = *req;
-    MC_process_read_simple(&mc_model_checker->process, &state->internal_comm,
+    MC_process_read_simple(&mc_model_checker->process(), &state->internal_comm,
       simcall_comm_test__get__comm(req), sizeof(state->internal_comm));
     simcall_comm_test__set__comm(&state->executed_req, &state->internal_comm);
     simcall_comm_test__set__comm(&state->internal_req, &state->internal_comm);
     break;
 
-  case SIMCALL_MC_RANDOM:
+  case SIMCALL_MC_RANDOM: {
     state->internal_req = *req;
     int random_max = simcall_mc_random__get__max(req);
     if (value != random_max) {
@@ -153,6 +155,7 @@ void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req,
       );
     }
     break;
+  }
 
   default:
     state->internal_req = *req;
@@ -187,7 +190,7 @@ static inline smx_simcall_t MC_state_get_request_for_process(
       case SIMCALL_COMM_WAITANY:
         *value = -1;
         while (procstate->interleave_count <
-              MC_process_read_dynar_length(&mc_model_checker->process,
+              MC_process_read_dynar_length(&mc_model_checker->process(),
                 simcall_comm_waitany__get__comms(&process->simcall))) {
           if (MC_request_is_enabled_by_idx
               (&process->simcall, procstate->interleave_count++)) {
@@ -197,7 +200,7 @@ static inline smx_simcall_t MC_state_get_request_for_process(
         }
 
         if (procstate->interleave_count >=
-            MC_process_read_dynar_length(&mc_model_checker->process,
+            MC_process_read_dynar_length(&mc_model_checker->process(),
               simcall_comm_waitany__get__comms(&process->simcall)))
           procstate->state = MC_DONE;
 
@@ -210,7 +213,7 @@ static inline smx_simcall_t MC_state_get_request_for_process(
         unsigned start_count = procstate->interleave_count;
         *value = -1;
         while (procstate->interleave_count <
-                MC_process_read_dynar_length(&mc_model_checker->process,
+                MC_process_read_dynar_length(&mc_model_checker->process(),
                   simcall_comm_testany__get__comms(&process->simcall))) {
           if (MC_request_is_enabled_by_idx
               (&process->simcall, procstate->interleave_count++)) {
@@ -220,7 +223,7 @@ static inline smx_simcall_t MC_state_get_request_for_process(
         }
 
         if (procstate->interleave_count >=
-            MC_process_read_dynar_length(&mc_model_checker->process,
+            MC_process_read_dynar_length(&mc_model_checker->process(),
               simcall_comm_testany__get__comms(&process->simcall)))
           procstate->state = MC_DONE;
 
@@ -233,7 +236,7 @@ static inline smx_simcall_t MC_state_get_request_for_process(
       case SIMCALL_COMM_WAIT: {
         smx_synchro_t remote_act = simcall_comm_wait__get__comm(&process->simcall);
         s_smx_synchro_t act;
-        MC_process_read_simple(&mc_model_checker->process,
+        MC_process_read_simple(&mc_model_checker->process(),
           &act, remote_act, sizeof(act));
         if (act.comm.src_proc && act.comm.dst_proc) {
           *value = 0;
@@ -277,3 +280,5 @@ smx_simcall_t MC_state_get_request(mc_state_t state, int *value)
 
   return NULL;
 }
+
+}
similarity index 96%
rename from src/mc/mc_unw.c
rename to src/mc/mc_unw.cpp
index ee67176..a141f09 100644 (file)
@@ -9,7 +9,7 @@
  */
 
 // We need this for the register indices:
-#define _GNU_SOURCE
+// #define _GNU_SOURCE
 
 #include <string.h>
 
@@ -22,6 +22,8 @@
 #include "mc_process.h"
 #include "mc_unw.h"
 
+extern "C" {
+
 // ***** Implementation
 
 /** Get frame unwind information (libunwind method)
@@ -78,9 +80,9 @@ static int access_mem(unw_addr_space_t as,
 {
   mc_unw_context_t context = (mc_unw_context_t) arg;
   if (write)
-    return -UNW_EREADONLYREG;
+    return - UNW_EREADONLYREG;
   MC_address_space_read(context->address_space,
-    0, valp, (void*) addr, sizeof(unw_word_t), MC_PROCESS_INDEX_ANY);
+    MC_ADDRESS_SPACE_READ_FLAGS_NONE, valp, (void*) addr, sizeof(unw_word_t), MC_PROCESS_INDEX_ANY);
   // We don't handle failure gracefully.
   return 0;
 }
@@ -124,7 +126,7 @@ static int access_reg(unw_addr_space_t as,
   unw_context_t* context = &as_context->context;
   if (write)
     return -UNW_EREADONLYREG;
-  greg_t* preg = get_reg(context, regnum);
+  greg_t* preg = (greg_t*) get_reg(context, regnum);
   if (!preg)
     return -UNW_EBADREG;
   *valp = *preg;
@@ -236,3 +238,5 @@ int mc_unw_init_cursor(unw_cursor_t *cursor, mc_unw_context_t context)
 
   return unw_init_remote(cursor, context->process->unw_addr_space, context);
 }
+
+}
similarity index 87%
rename from src/mc/mc_unw_vmread.c
rename to src/mc/mc_unw_vmread.cpp
index 2d7cb1e..a4e5677 100644 (file)
@@ -1,4 +1,8 @@
-#define _GNU_SOURCE
+/* Copyright (c) 2015. The SimGrid Team.
+ * All rights reserved.                                                     */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
 
 #include <sys/types.h>
 #include <sys/uio.h>
@@ -8,6 +12,8 @@
 
 #include "mc_unw.h"
 
+extern "C" {
+
 /** \file
  *  Libunwind namespace implementation using process_vm_readv.
  *.
@@ -30,7 +36,7 @@ struct _UPT_info {
 static inline
 pid_t _UPT_getpid(void* arg)
 {
-  struct _UPT_info* info = arg;
+  struct _UPT_info* info = (_UPT_info*) arg;
   return info->pid;
 }
 
@@ -53,7 +59,7 @@ static int access_mem(const unw_addr_space_t as,
   struct iovec remote = { (void*) addr, size };
   ssize_t s = process_vm_readv(pid, &local, 1, &remote, 1, 0);
   if (s >= 0) {
-    if (s != size)
+    if ((size_t) s != size)
       return - UNW_EINVAL;
     else
       return 0;
@@ -105,3 +111,5 @@ unw_accessors_t mc_unw_vmread_accessors =
     .resume                     = &_UPT_resume,
     .get_proc_name              = &_UPT_get_proc_name
   };
+
+}
similarity index 95%
rename from src/mc/mc_visited.c
rename to src/mc/mc_visited.cpp
index c644abf..968965f 100644 (file)
@@ -14,6 +14,8 @@
 #include "mc_process.h"
 #include "mc_smx.h"
 
+extern "C" {
+
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_visited, mc,
                                 "Logging specific to state equaity detection mechanisms");
 
@@ -53,18 +55,18 @@ void visited_state_free_voidp(void *s)
  */
 static mc_visited_state_t visited_state_new()
 {
-  mc_process_t process = &(mc_model_checker->process);
+  mc_process_t process = &(mc_model_checker->process());
   mc_visited_state_t new_state = xbt_new0(s_mc_visited_state_t, 1);
   new_state->heap_bytes_used = mmalloc_get_bytes_used_remote(
     MC_process_get_heap(process)->heaplimit,
     MC_process_get_malloc_info(process));
 
-  if (MC_process_is_self(&mc_model_checker->process)) {
+  if (MC_process_is_self(&mc_model_checker->process())) {
     new_state->nb_processes = xbt_swag_size(simix_global->process_list);
   } else {
-    MC_process_smx_refresh(&mc_model_checker->process);
+    MC_process_smx_refresh(&mc_model_checker->process());
     new_state->nb_processes = xbt_dynar_length(
-      mc_model_checker->process.smx_process_infos);
+      mc_model_checker->process().smx_process_infos);
   }
 
   new_state->system_state = MC_take_snapshot(mc_stats->expanded_states);
@@ -75,7 +77,7 @@ static mc_visited_state_t visited_state_new()
 
 mc_visited_pair_t MC_visited_pair_new(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, mc_state_t graph_state)
 {
-  mc_process_t process = &(mc_model_checker->process);
+  mc_process_t process = &(mc_model_checker->process());
   mc_visited_pair_t pair = NULL;
   pair = xbt_new0(s_mc_visited_pair_t, 1);
   pair->graph_state = graph_state;
@@ -84,12 +86,12 @@ mc_visited_pair_t MC_visited_pair_new(int pair_num, xbt_automaton_state_t automa
   pair->heap_bytes_used = mmalloc_get_bytes_used_remote(
     MC_process_get_heap(process)->heaplimit,
     MC_process_get_malloc_info(process));
-  if (MC_process_is_self(&mc_model_checker->process)) {
+  if (MC_process_is_self(&mc_model_checker->process())) {
     pair->nb_processes = xbt_swag_size(simix_global->process_list);
   } else {
-    MC_process_smx_refresh(&mc_model_checker->process);
+    MC_process_smx_refresh(&mc_model_checker->process());
     pair->nb_processes = xbt_dynar_length(
-      mc_model_checker->process.smx_process_infos);
+      mc_model_checker->process().smx_process_infos);
   }
   pair->automaton_state = automaton_state;
   pair->num = pair_num;
@@ -148,7 +150,7 @@ int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max)
 
   xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
 
-  int cursor = 0, previous_cursor, next_cursor;
+  int cursor = 0, previous_cursor;
   int nb_processes, heap_bytes_used, nb_processes_test, heap_bytes_used_test;
   void *ref_test;
 
@@ -201,7 +203,7 @@ int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max)
           *min = previous_cursor;
           previous_cursor--;
         }
-        next_cursor = cursor + 1;
+        size_t next_cursor = cursor + 1;
         while (next_cursor < xbt_dynar_length(list)) {
           if (_sg_mc_liveness) {
             ref_test = (mc_visited_pair_t) xbt_dynar_get_as(list, next_cursor, mc_visited_pair_t);
@@ -244,7 +246,7 @@ mc_visited_state_t is_visited_state(mc_state_t graph_state)
      communications are not finished (at least, data are transfered). These communications 
      are incomplete and they cannot be analyzed and compared with the initial pattern. */
   if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
-    int current_process = 1;
+    size_t current_process = 1;
     while (current_process < MC_smx_get_maxpid()) {
       if (!xbt_dynar_is_empty((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, current_process, xbt_dynar_t))){
         XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited.");
@@ -351,7 +353,7 @@ mc_visited_state_t is_visited_state(mc_state_t graph_state)
     }
 
     // We have reached the maximum number of stored states;
-    if (xbt_dynar_length(visited_states) > _sg_mc_visited) {
+    if ((ssize_t) xbt_dynar_length(visited_states) > _sg_mc_visited) {
 
       XBT_DEBUG("Try to remove visited state (maximum number of stored states reached)");
 
@@ -360,7 +362,7 @@ mc_visited_state_t is_visited_state(mc_state_t graph_state)
       unsigned int cursor2 = 0;
       unsigned int index2 = 0;
       xbt_dynar_foreach(visited_states, cursor2, state_test){
-        if (!mc_important_snapshot(state_test->system_state) && state_test->num < min2) {
+        if (state_test->num < min2) {
           index2 = cursor2;
           min2 = state_test->num;
         }
@@ -478,12 +480,12 @@ int is_visited_pair(mc_visited_pair_t visited_pair, mc_pair_t pair) {
       }
     }
 
-    if (xbt_dynar_length(visited_pairs) > _sg_mc_visited) {
+    if ((ssize_t) xbt_dynar_length(visited_pairs) > _sg_mc_visited) {
       int min2 = mc_stats->expanded_pairs;
       unsigned int cursor2 = 0;
       unsigned int index2 = 0;
       xbt_dynar_foreach(visited_pairs, cursor2, pair_test) {
-        if (!mc_important_snapshot(pair_test->graph_state->system_state) && pair_test->num < min2) {
+        if (pair_test->num < min2) {
           index2 = cursor2;
           min2 = pair_test->num;
         }
@@ -503,3 +505,5 @@ int is_visited_pair(mc_visited_pair_t visited_pair, mc_pair_t pair) {
   mmalloc_set_current_heap(heap);
   return -1;
 }
+
+}
similarity index 98%
rename from src/mc/memory_map.c
rename to src/mc/memory_map.cpp
index 337ed9d..db0fcce 100644 (file)
@@ -11,6 +11,8 @@
 #include "mc_memory_map.h"
 #include "mc_private.h"
 
+extern "C" {
+
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_memory_map, mc,
                                 "Logging specific to algorithms for memory_map");
 
@@ -143,7 +145,7 @@ memory_map_t MC_get_memory_map(pid_t pid)
     /* parsed stuff from the temporal memreg variable */
     XBT_DEBUG("Found region for %s",
       memreg.pathname ? memreg.pathname : "(null)");
-    ret->regions =
+    ret->regions = (map_region_t)
         xbt_realloc(ret->regions, sizeof(memreg) * (ret->mapsize + 1));
     memcpy(ret->regions + ret->mapsize, &memreg, sizeof(memreg));
     ret->mapsize++;
@@ -164,3 +166,5 @@ void MC_free_memory_map(memory_map_t map){
   xbt_free(map->regions);
   xbt_free(map);
 }
+
+}
index 71d0388..29d5fe2 100644 (file)
@@ -29,8 +29,9 @@
 #include "mc_private.h"
 #include "mc_protocol.h"
 #include "mc_server.h"
-#include "mc_model_checker.h"
 #include "mc_safety.h"
+#include "mc_comm_pattern.h"
+#include "mc_liveness.h"
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_main, mc, "Entry point for simgrid-mc");
 
@@ -82,7 +83,12 @@ static int do_parent(int socket, pid_t child)
     mc_server = new s_mc_server(child, socket);
     mc_server->start();
     MC_init_pid(child, socket);
-    MC_do_the_modelcheck_for_real();
+    if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
+      MC_modelcheck_comm_determinism();
+    else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0')
+      MC_modelcheck_safety();
+    else
+      MC_modelcheck_liveness();
     mc_server->shutdown();
     mc_server->exit();
   }
index b9351e8..6deb895 100644 (file)
@@ -122,7 +122,7 @@ msg_error_t MSG_main(void)
   fflush(stderr);
 
   if (MC_is_active()) {
-    MC_do_the_modelcheck_for_real();
+    MC_run();
   } else {
     SIMIX_run();
   }
index ad2bbb8..7f8e392 100644 (file)
@@ -22,6 +22,7 @@
 #include "mc/mc.h"
 #include "mc/mc_record.h"
 #include "simgrid/instr.h"
+#include "mc/mc_replay.h"
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(surf_config, surf,
                                 "About the configuration of simgrid");
@@ -649,12 +650,6 @@ void sg_config_init(int *argc, char **argv)
                      xbt_cfgelm_boolean, 1, 1, _mc_cfg_cb_sparse_checkpoint, NULL);
     xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/sparse-checkpoint", "no");
 
-    /* do stateful model-checking */
-    xbt_cfg_register(&_sg_cfg_set, "model-check/soft-dirty",
-                     "Use sparse per-page snapshots.",
-                     xbt_cfgelm_boolean, 1, 1, _mc_cfg_cb_soft_dirty, NULL);
-    xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/soft-dirty", "no");
-
     /* do liveness model-checking */
     xbt_cfg_register(&_sg_cfg_set, "model-check/property",
                      "Specify the name of the file containing the property. It must be the result of the ltl2ba program.",
index f604cec..9a182a1 100644 (file)
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package.   */
 
+#include "mc/mc_replay.h"
 #include "smx_private.h"
-#include "mc/mc_interface.h"
+#include "mc/mc_forward.h"
 #include "xbt/ex.h"
 #include <math.h>         /* isfinite() */
+#include "mc/mc.h"
 
 XBT_LOG_EXTERNAL_DEFAULT_CATEGORY(simix);
 
index 0b413a2..4169dbd 100644 (file)
@@ -14,7 +14,7 @@
  */
 
 #include "smx_private.h"
-#include "mc/mc_interface.h"
+#include "mc/mc_forward.h"
 #include "xbt/ex.h"
   
 inline static smx_host_t simcall_BODY_host_get_by_name(const char* name) {
index c8a3c3c..9f8e55c 100644 (file)
@@ -16,7 +16,6 @@
 #include "smx_private.h"
 #ifdef HAVE_MC
 #include "mc/mc_process.h"
-#include "mc/mc_model_checker.h"
 #endif
 
 XBT_LOG_EXTERNAL_DEFAULT_CATEGORY(simix_popping);
@@ -163,7 +162,7 @@ void SIMIX_simcall_handle(smx_simcall_t simcall, int value) {
   XBT_DEBUG("Handling simcall %p: %s", simcall, SIMIX_simcall_name(simcall->call));
   #ifdef HAVE_MC
   if (mc_model_checker) {
-    mc_model_checker->process.cache_flags = 0;
+    MC_invalidate_cache();
   }
   #endif
   SIMCALL_SET_MC_VALUE(simcall, value);
index 8eefe72..dc8c59d 100644 (file)
@@ -13,7 +13,7 @@ SG_BEGIN_DECL()
 XBT_PUBLIC(const char*) simcall_names[]; /* Name of each simcall */
 
 #include "popping_enum.h" /* Definition of e_smx_simcall_t, with one value per simcall */
-#include "mc/mc_interface.h" /* Definition of mc_snapshot_t, used by one simcall */
+#include "mc/mc_forward.h" /* Definition of mc_snapshot_t, used by one simcall */
 
 typedef int (*simix_match_func_t)(void *, void *, smx_synchro_t);
 typedef void (*simix_copy_data_func_t)(smx_synchro_t, void*, size_t);
index 321a63b..997a60b 100755 (executable)
@@ -282,7 +282,6 @@ if __name__=='__main__':
   fd.write('#include "smx_private.h"\n');
   fd.write('#ifdef HAVE_MC\n');
   fd.write('#include "mc/mc_process.h"\n');
-  fd.write('#include "mc/mc_model_checker.h"\n');
   fd.write('#endif\n');
   fd.write('\n');
   fd.write('XBT_LOG_EXTERNAL_DEFAULT_CATEGORY(simix_popping);\n\n');
@@ -305,7 +304,7 @@ if __name__=='__main__':
   fd.write('  XBT_DEBUG("Handling simcall %p: %s", simcall, SIMIX_simcall_name(simcall->call));\n');
   fd.write('  #ifdef HAVE_MC\n');
   fd.write('  if (mc_model_checker) {\n');
-  fd.write('    mc_model_checker->process.cache_flags = 0;\n');
+  fd.write('    MC_invalidate_cache();\n');
   fd.write('  }\n');
   fd.write('  #endif\n');
   fd.write('  SIMCALL_SET_MC_VALUE(simcall, value);\n');
@@ -334,7 +333,7 @@ if __name__=='__main__':
   ###
   fd = header('popping_bodies.c')
   fd.write('#include "smx_private.h"\n')
-  fd.write('#include "mc/mc_interface.h"\n')
+  fd.write('#include "mc/mc_forward.h"\n')
   fd.write('#include "xbt/ex.h"\n')
   handle(fd, Simcall.body, simcalls, simcalls_dict)
   fd.close()
index e074c52..6144555 100644 (file)
@@ -152,10 +152,12 @@ smx_ctx_sysv_create_context(xbt_main_func_t code, int argc, char **argv,
       sysv_maestro_context = context;
   }
 
+#ifdef HAVE_MC
   if (MC_is_active() && code) {
     MC_new_stack_area(context->stack, ((smx_context_t)context)->process,
                       &(context->uc), smx_context_usable_stack_size);
   }
+#endif
 
   return (smx_context_t) context;
 }
index 2689131..afbc67c 100644 (file)
 #include "xbt/str.h"
 #include "xbt/ex.h"             /* ex_backtrace_display */
 #include "mc/mc.h"
+#include "mc/mc_replay.h"
 #include "simgrid/sg_config.h"
 
 #ifdef HAVE_MC
 #include "mc/mc_private.h"
-#include "mc/mc_model_checker.h"
 #include "mc/mc_protocol.h"
 #include "mc/mc_client.h"
 #endif
@@ -220,8 +220,6 @@ void SIMIX_global_init(int *argc, char **argv)
       MC_client_init();
       MC_client_hello();
       MC_client_handle_messages();
-    } else {
-      mc_mode = MC_MODE_STANDALONE;
     }
   }
 #endif
index be58fe5..20e7abb 100644 (file)
@@ -9,6 +9,7 @@
 #include "xbt/log.h"
 #include "xbt/dict.h"
 #include "mc/mc.h"
+#include "mc/mc_replay.h"
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(simix_host, simix,
                                 "SIMIX hosts");
index 942deb5..fbeb548 100644 (file)
@@ -7,10 +7,10 @@
 #include "smx_private.h"
 #include "xbt/log.h"
 #include "mc/mc.h"
+#include "mc/mc_replay.h"
 #include "xbt/dict.h"
 #include "smpi/private.h"
 
-
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(simix_network, simix,
                                 "SIMIX network-related synchronization");
 
index d466c2c..21a4ef8 100644 (file)
@@ -9,6 +9,7 @@
 #include "xbt/log.h"
 #include "xbt/dict.h"
 #include "mc/mc.h"
+#include "mc/mc_replay.h"
 #include "mc/mc_client.h"
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(simix_process, simix,
index c75e51d..af7deeb 100644 (file)
@@ -7,6 +7,7 @@
 #include "private.h"
 #include "xbt/virtu.h"
 #include "mc/mc.h"
+#include "mc/mc_replay.h"
 #include "xbt/replay.h"
 #include <errno.h>
 #include "simix/smx_private.h"
index 35971e2..b6b56e8 100644 (file)
@@ -13,6 +13,7 @@
 #include "surf/surf.h"
 #include "simgrid/sg_config.h"
 #include "simgrid/modelchecker.h"
+#include "mc/mc_replay.h"
 
 #ifndef WIN32
 #include <sys/mman.h>
index ac3cd86..f47536e 100644 (file)
@@ -12,6 +12,7 @@
 #include "surf/surf.h"
 #include "simix/smx_private.h"
 #include "simgrid/sg_config.h"
+#include "mc/mc_replay.h"
 
 #include <float.h>              /* DBL_MAX */
 #include <stdint.h>
@@ -666,7 +667,7 @@ int smpi_main(int (*realmain) (int argc, char *argv[]), int argc, char *argv[])
   fflush(stderr);
 
   if (MC_is_active()) {
-    MC_do_the_modelcheck_for_real();
+    MC_run();
   } else {
   
     SIMIX_run();
index 8a40c48..07ef47d 100644 (file)
@@ -14,6 +14,8 @@
 #ifndef __MMPRIVATE_H
 #define __MMPRIVATE_H 1
 
+#include <xbt/misc.h>
+
 #include "portable.h"
 #include "xbt/xbt_os_thread.h"
 #include "xbt/mmalloc.h"
@@ -94,6 +96,8 @@
 
 #define ADDRESS(B) ((void*) (((ADDR2UINT(B)) - 1) * BLOCKSIZE + (char*) mdp -> heapbase))
 
+SG_BEGIN_DECL()
+
 /* Doubly linked lists of free fragments.  */
 struct list {
   struct list *next;
@@ -328,4 +332,6 @@ void mmalloc_ensure_using_mm(int argc, const char** argv);
 
 size_t mmalloc_get_bytes_used_remote(size_t heaplimit, const malloc_info* heapinfo);
 
+SG_END_DECL()
+
 #endif                          /* __MMPRIVATE_H */
index 89dd9ea..00e46e9 100644 (file)
@@ -3,7 +3,7 @@ cmake_minimum_required(VERSION 2.6)
 if(HAVE_MC)
   set(EXECUTABLE_OUTPUT_PATH "${CMAKE_CURRENT_BINARY_DIR}")
 
-  add_executable(dwarf dwarf.c)
+  add_executable(dwarf dwarf.cpp)
   target_link_libraries(dwarf simgrid)
 endif()
 
@@ -14,6 +14,6 @@ set(tesh_files
   )
 set(testsuite_src
   ${testsuite_src}
-  ${CMAKE_CURRENT_SOURCE_DIR}/dwarf.c
+  ${CMAKE_CURRENT_SOURCE_DIR}/dwarf.cpp
   PARENT_SCOPE
   )
similarity index 94%
rename from teshsuite/mc/dwarf/dwarf.c
rename to teshsuite/mc/dwarf/dwarf.cpp
index c7ad31c..adbe05d 100644 (file)
@@ -17,7 +17,6 @@
 #include "../../src/include/mc/datatypes.h"
 #include "../../src/mc/mc_object_info.h"
 #include "../../src/mc/mc_private.h"
-#include "../../src/mc/mc_model_checker.h"
 
 int test_some_array[4][5][6];
 struct some_struct { int first; int second[4][5]; } test_some_struct;
@@ -87,7 +86,7 @@ static void test_local_variable(mc_object_info_t info, const char* function, con
 }
 
 static dw_variable_t test_global_variable(mc_process_t process, mc_object_info_t info, const char* name, void* address, long byte_size) {
-  
+
   dw_variable_t variable = MC_file_object_info_find_variable_by_name(info, name);
   xbt_assert(variable, "Global variable %s was not found", name);
   xbt_assert(!strcmp(variable->name, name), "Name mismatch for %s", name);
@@ -95,7 +94,7 @@ static dw_variable_t test_global_variable(mc_process_t process, mc_object_info_t
   xbt_assert(variable->address == address,
       "Address mismatch for %s : %p expected but %p found", name, address, variable->address);
 
-  dw_type_t type = xbt_dict_get_or_null(process->binary_info->types, variable->type_origin);
+  dw_type_t type = (dw_type_t) xbt_dict_get_or_null(process->binary_info->types, variable->type_origin);
   xbt_assert(type!=NULL, "Missing type for %s", name);
   xbt_assert(type->byte_size = byte_size, "Byte size mismatch for %s", name);
   return variable;
@@ -125,7 +124,7 @@ int main(int argc, char** argv)
 
   dw_variable_t var;
   dw_type_t type;
-  
+
   s_mc_process_t p;
   mc_process_t process = &p;
   MC_process_init(&p, getpid(), -1);
@@ -133,11 +132,11 @@ int main(int argc, char** argv)
   test_global_variable(process, process->binary_info, "some_local_variable", &some_local_variable, sizeof(int));
 
   var = test_global_variable(process, process->binary_info, "test_some_array", &test_some_array, sizeof(test_some_array));
-  type = xbt_dict_get_or_null(process->binary_info->types, var->type_origin);
+  type = (dw_type_t) xbt_dict_get_or_null(process->binary_info->types, var->type_origin);
   xbt_assert(type->element_count == 6*5*4, "element_count mismatch in test_some_array : %i / %i", type->element_count, 6*5*4);
 
   var = test_global_variable(process, process->binary_info, "test_some_struct", &test_some_struct, sizeof(test_some_struct));
-  type = xbt_dict_get_or_null(process->binary_info->types, var->type_origin);
+  type = (dw_type_t) xbt_dict_get_or_null(process->binary_info->types, var->type_origin);
   assert(find_member(process->binary_info, "first", type)->offset == 0);
   assert(find_member(process->binary_info, "second", type)->offset
       == ((const char*)&test_some_struct.second) - (const char*)&test_some_struct);