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
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
)
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
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
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()
#include "xbt/asserts.h"
#include "simgrid/modelchecker.h"
#include <xbt/RngStream.h>
+#include "mc/mc_replay.h"
/** @addtogroup MSG_examples
*
! 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 ****
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
_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()
* @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
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;
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);
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);
--- /dev/null
+/* 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;
+}
+
+}
+}
--- /dev/null
+/* 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
-/* 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
#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
*
* @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;
// ***** 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
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;
*
* @return index of the free page
*/
-size_t s_mc_pages_store::alloc_page()
+size_t PageStore::alloc_page()
{
if (this->free_pages_.empty()) {
}
}
-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);
}
/** 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");
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
#include <memory>
-#include "mc/mc_page_store.h"
+#include "mc/PageStore.hpp"
static int value = 0;
{
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");
}
#endif /* SIMGRID_TEST */
+
+}
-/* 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
#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
*
* 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;
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
};
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
#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
*
*/
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)
{
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
#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
#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;
#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
#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;
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;
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);
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
+}
+
+}
#ifndef MC_BASE_H
#define MC_BASE_H
+#include <xbt/misc.h>
#include <simgrid/simix.h>
#include "simgrid_config.h"
#include "internal_config.h"
/* 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>
#include "mc_protocol.h"
#include "mc_smx.h"
+extern "C" {
+
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_checkpoint, mc,
"Logging specific to mc_checkpoint");
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;
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",
* @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:
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;
}
}
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);
// 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;
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;
#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
* */
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) {
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++;
}
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)
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:
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);
// 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.");
}
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;
// 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;
}
// 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);
}
}
}
-/** @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)
{
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);
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);
}
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++;
}
}
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;
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();
}
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
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) {
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);
}
+
+}
// 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;
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);
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) {
MC_wait_for_requests();
}
}
+
+}
#define MC_CLIENT_H
#include <xbt/misc.h>
+#include "mc_protocol.h"
SG_BEGIN_DECL()
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);
#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");
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();
}
}
// 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);
}
+
+}
#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");
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) {
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);
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);
}
}
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;
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){
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 {
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);
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();
mmalloc_set_current_heap(heap);
}
+
+}
#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");
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)
{
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, ©);
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);
{
MC_list_comm_pattern_free((mc_list_comm_pattern_t) * (void **) p);
}
+
+}
#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"
#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;
extern "C" {
+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_compare, xbt,
+ "Logging specific to mc_compare in mc");
+
/************************** Free functions ****************************/
/********************************************************************/
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;
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;
#include <xbt/config.h>
#include <mc/mc.h>
+#include "mc/mc_replay.h"
#include <simgrid/sg_config.h>
#include "mc_record.h"
+extern "C" {
+
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_config, mc,
"Configuration of MC");
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;
_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) {
}
#endif
+
+}
#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");
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;
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 *));
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 */
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 ++;
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++;
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 ++;
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) {
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) {
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;
}
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;;
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,
} 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
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,
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,
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;
}
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;
// 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;
}
// 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);
}
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)) {
}
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);
/* 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;
}
#endif
+
+}
#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);
*/
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
*
*/
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)
*
*/
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
*
*/
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);
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);
}
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;
}
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);
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))
}
}
- 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,
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);
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);
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 =
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);
// 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:
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);
}
}
}
// 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);
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);
}
}
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)
// 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;
}
// 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) {
}
}
+
+}
#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)
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;
// 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)
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.
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));
}
}
}
+
+}
#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
#include "mc_protocol.h"
#include "mc_client.h"
+extern "C" {
+
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc,
"Logging specific to MC (global)");
}
+#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;
}
/* 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: */
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);
//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) {
}
return deadlock;
}
+#endif
/**
* \brief Re-executes from the state at position start all the transitions indicated by
{
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;
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;
}
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
+
+}
#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:
// #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;
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).
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) {
{
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;
}
+
+}
#include "mc_protocol.h"
#include "mc_client.h"
+extern "C" {
+
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_ignore, mc,
"Logging specific to MC ignore mechanism");
message.addr = address;
message.size = size;
MC_client_send_message(&message, sizeof(message));
+ return;
}
xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
// 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");
// 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);
}
}
}
+
+}
+++ /dev/null
-/* 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
#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");
/* 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);
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;
mmalloc_set_current_heap(heap);
}
+
+}
#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"
/* 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
else
return (void *) state.stack[state.stack_size - 1];
}
+
+}
#include "mc_object_info.h"
#include "mc_private.h"
+extern "C" {
+
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_memory, mc,
"Logging specific to MC (memory)");
if (mc_heap && mc_heap != std_heap)
xbt_mheap_destroy(mc_heap);
}
+
+}
#ifndef MC_MMALLOC_H
#define MC_MMALLOC_H
+#include <xbt/misc.h>
#include <xbt/mmalloc.h>
/** file
* 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;
#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
+++ /dev/null
-/* 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;
-}
+++ /dev/null
-/* 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
+/* 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>
#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;
return NULL;
}
+
+}
// ***** 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
#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:
*
* @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));
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);
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);
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]);
}
}
* @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;
"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);
}
}
#include "mc_liveness.h"
#include "mc_private.h"
+extern "C" {
+
mc_pair_t MC_pair_new()
{
mc_pair_t p = NULL;
{
MC_pair_delete((mc_pair_t) * (void **) p);
}
+
+}
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
void MC_report_assertion_error(void);
+void MC_invalidate_cache(void);
+
SG_END_DECL()
#endif
+/* 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>
#include "mc_smx.h"
#include "mc_server.h"
+extern "C" {
+
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_process, mc,
"MC process information");
}
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)
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);
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;
// 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,
(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,
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;
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");
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);
}
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) {
off += c;
if (off == len) {
len *= 2;
- res = realloc(res, len);
+ res = (char*) realloc(res, len);
}
}
}
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;
}
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)
{
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;
}
}
-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");
}
#include <sys/types.h>
#include "simgrid_config.h"
-
#include <sys/types.h>
#include <xbt/mmalloc.h>
#include "xbt/mmalloc/mmprivate.h"
#endif
+#include <simgrid/simix.h>
#include "simix/popping_private.h"
#include "simix/smx_private.h"
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;
*/
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;
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;
* @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);
*/
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
#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)
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;
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;
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;
}
switch(mode) {
case MC_MODE_NONE:
return "NONE";
- case MC_MODE_STANDALONE:
- return "STANDALONE";
case MC_MODE_CLIENT:
return "CLIENT";
case MC_MODE_SERVER:
return "?";
}
}
+
+}
typedef enum {
MC_MODE_NONE = 0,
- MC_MODE_STANDALONE,
MC_MODE_CLIENT,
MC_MODE_SERVER
} e_mc_mode_t;
} 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);
#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");
xbt_dynar_push(dynar, &item);
// Find next chunk:
- char* end = strchr(current, ';');
+ const char* end = strchr(current, ';');
if(end==NULL)
break;
else
{
mc_time = xbt_new0(double, simix_process_maxpid);
}
+
+}
--- /dev/null
+/* 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
#include "mc_private.h"
#include "mc_smx.h"
+extern "C" {
+
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_request, mc,
"Logging specific to MC (request)");
// 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);
}
// 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";
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
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
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);
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;
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",
// 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:
// 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:
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;
}
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;
}
} 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);
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)
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,
return str;
}
+
+}
#include "xbt/mmalloc/mmprivate.h"
+extern "C" {
+
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
"Logging specific to MC safety verification ");
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);
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;
xbt_abort();
//MC_exit();
}
+
+}
#include <simgrid_config.h>
#include <xbt/dict.h>
-#include "mc_interface.h"
+#include "mc_forward.h"
#include "mc_state.h"
SG_BEGIN_DECL()
#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:
{
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");
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");
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
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;
}
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,
void s_mc_server::loop()
{
- while (mc_model_checker->process.running)
+ while (mc_model_checker->process().running)
this->handle_events();
}
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;
}
}
- 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;
}
}
}
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;
}
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;
}
{
server->loop();
}
+
+}
#ifndef MC_SERVER_H
#define MC_SERVER_H
+#include <poll.h>
+
#include <stdint.h>
#include <stdbool.h>
+++ /dev/null
-/* 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();
-}
-
-};
#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)
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));
// 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;
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);
}
*/
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;
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;
{
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);
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");
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++
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)
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;
+}
+
+}
/** (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;
};
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; \
} \
/** 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
#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
*
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];
* @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);
#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;
}
}
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) {
// 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");
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);
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 */
+
+}
#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 {
};
-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)
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);
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,
{
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
#include "mc_comm_pattern.h"
#include "mc_smx.h"
+extern "C" {
+
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_state, mc,
"Logging specific to MC (state)");
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);
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));
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);
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) {
);
}
break;
+ }
default:
state->internal_req = *req;
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++)) {
}
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;
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++)) {
}
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;
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;
return NULL;
}
+
+}
*/
// We need this for the register indices:
-#define _GNU_SOURCE
+// #define _GNU_SOURCE
#include <string.h>
#include "mc_process.h"
#include "mc_unw.h"
+extern "C" {
+
// ***** Implementation
/** Get frame unwind information (libunwind method)
{
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;
}
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;
return unw_init_remote(cursor, context->process->unw_addr_space, context);
}
+
+}
-#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>
#include "mc_unw.h"
+extern "C" {
+
/** \file
* Libunwind namespace implementation using process_vm_readv.
*.
static inline
pid_t _UPT_getpid(void* arg)
{
- struct _UPT_info* info = arg;
+ struct _UPT_info* info = (_UPT_info*) arg;
return info->pid;
}
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;
.resume = &_UPT_resume,
.get_proc_name = &_UPT_get_proc_name
};
+
+}
#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");
*/
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);
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;
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;
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;
*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);
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.");
}
// 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)");
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;
}
}
}
- 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;
}
mmalloc_set_current_heap(heap);
return -1;
}
+
+}
#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");
/* 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++;
xbt_free(map->regions);
xbt_free(map);
}
+
+}
#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");
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();
}
fflush(stderr);
if (MC_is_active()) {
- MC_do_the_modelcheck_for_real();
+ MC_run();
} else {
SIMIX_run();
}
#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");
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.",
/* 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);
*/
#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) {
#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);
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);
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);
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');
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');
###
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()
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;
}
#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
MC_client_init();
MC_client_hello();
MC_client_handle_messages();
- } else {
- mc_mode = MC_MODE_STANDALONE;
}
}
#endif
#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");
#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");
#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,
#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"
#include "surf/surf.h"
#include "simgrid/sg_config.h"
#include "simgrid/modelchecker.h"
+#include "mc/mc_replay.h"
#ifndef WIN32
#include <sys/mman.h>
#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>
fflush(stderr);
if (MC_is_active()) {
- MC_do_the_modelcheck_for_real();
+ MC_run();
} else {
SIMIX_run();
#ifndef __MMPRIVATE_H
#define __MMPRIVATE_H 1
+#include <xbt/misc.h>
+
#include "portable.h"
#include "xbt/xbt_os_thread.h"
#include "xbt/mmalloc.h"
#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;
size_t mmalloc_get_bytes_used_remote(size_t heaplimit, const malloc_info* heapinfo);
+SG_END_DECL()
+
#endif /* __MMPRIVATE_H */
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()
)
set(testsuite_src
${testsuite_src}
- ${CMAKE_CURRENT_SOURCE_DIR}/dwarf.c
+ ${CMAKE_CURRENT_SOURCE_DIR}/dwarf.cpp
PARENT_SCOPE
)
#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;
}
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);
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;
dw_variable_t var;
dw_type_t type;
-
+
s_mc_process_t p;
mc_process_t process = &p;
MC_process_init(&p, getpid(), -1);
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);
