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.cpp
+ src/mc/ModelChecker.hpp
+ src/mc/ModelChecker.cpp
src/mc/mc_object_info.h
src/mc/mc_object_info.cpp
src/mc/mc_checkpoint.cpp
--- /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 <cassert>
+
+#include "ModelChecker.hpp"
+#include "mc_page_store.h"
+
+::simgrid::mc::ModelChecker* mc_model_checker = NULL;
+
+namespace simgrid {
+namespace mc {
+
+ModelChecker::ModelChecker(pid_t pid, int socket)
+{
+ this->page_store_ = mc_pages_store_new();
+ this->fd_clear_refs_ = -1;
+ this->hostnames_ = xbt_dict_new();
+ MC_process_init(&this->process(), pid, socket);
+}
+
+ModelChecker::~ModelChecker()
+{
+ mc_pages_store_delete(this->page_store_);
+ if(this->record_)
+ xbt_dynar_free(&this->record_);
+ 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;
+}
+
+}
+}
#include "mc_page_store.h"
#include "mc_protocol.h"
-SG_BEGIN_DECL()
+namespace simgrid {
+namespace mc {
-/** @brief State of the model-checker (global variables for the model checker)
+/** 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.
+ * on the model-checker heap, we avoid those issues.
*/
-struct s_mc_model_checker {
+class ModelChecker {
// This is the parent snapshot of the current state:
- mc_snapshot_t parent_snapshot;
- mc_pages_store_t pages;
- int fd_clear_refs;
- xbt_dynar_t record;
- s_mc_process_t process;
+ mc_pages_store_t page_store_;
+ int fd_clear_refs_;
+ xbt_dynar_t record_;
+ s_mc_process_t process_;
/** String pool for host names */
- xbt_dict_t /* <hostname, NULL> */ hosts;
+ // 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_;
+ }
+ s_mc_pages_store_t& page_store()
+ {
+ return *page_store_;
+ }
+ const char* get_host_name(const char* name);
};
-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
#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"
{
#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_ADDRESS_SPACE_READ_FLAGS_NONE,
+ 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_ADDRESS_SPACE_READ_FLAGS_NONE,
+ 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_ADDRESS_SPACE_READ_FLAGS_NONE,
+ 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;
#ifndef HAVE_MC
SIMIX_simcall_handle(req, value);
#else
- if (MC_process_is_self(&mc_model_checker->process)) {
+ 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) {
+ 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);
+ MC_server_simcall_handle(&mc_model_checker->process(), pi->copy.pid, value);
return;
}
}
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",
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);
+ mc_region_restore_sparse(&mc_model_checker->process(), region);
break;
case MC_REGION_STORAGE_TYPE_PRIVATIZED:
// Read smpi_privatisation_regions from MCed:
smpi_privatisation_region_t remote_smpi_privatisation_regions;
- MC_process_read_variable(&mc_model_checker->process,
+ MC_process_read_variable(&mc_model_checker->process(),
"smpi_privatisation_regions",
&remote_smpi_privatisation_regions, sizeof(remote_smpi_privatisation_regions));
s_smpi_privatisation_region_t privatisation_regions[process_count];
- MC_process_read_simple(&mc_model_checker->process, &privatisation_regions,
+ MC_process_read_simple(&mc_model_checker->process(), &privatisation_regions,
remote_smpi_privatisation_regions, sizeof(privatisation_regions));
for (size_t i = 0; i < process_count; i++) {
#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
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.");
}
// 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)
{
{
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_restore_snapshot_fds(snapshot);
MC_snapshot_ignore_restore(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)
// 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"
#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" {
// 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);
}
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 {
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);
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;
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;
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 */
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;
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;
/* 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;
#include <xbt/misc.h>
#include <mc/datatypes.h>
-SG_BEGIN_DECL()
+#ifdef __cplusplus
+
+namespace simgrid {
+namespace mc {
+ class ModelChecker;
+}
+}
+
+typedef ::simgrid::mc::ModelChecker s_mc_model_checker_t;
+
+#else
+
+typedef struct _s_mc_model_checker s_mc_model_checker_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 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;
-extern mc_model_checker_t mc_model_checker;
+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
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;
}
{
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) {
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
}
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) {
// 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
-/* 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"
-
-extern "C" {
-
-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_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)
-{
- unsigned long maxpid;
- MC_process_read_variable(&mc_model_checker->process, "simix_process_maxpid",
- &maxpid, sizeof(maxpid));
- return maxpid;
-}
-
-}
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);
}
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]);
}
}
for (size_t i=0; i!=page_count; ++i) {
// 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);
}
}
mc_mem_region_t mc_region_new_sparse(mc_region_type_t region_type,
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;
void MC_report_assertion_error(void);
+void MC_invalidate_cache(void);
+
SG_END_DECL()
#endif
*/
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
#ifdef HAVE_MC
#include "mc_private.h"
-#include "mc_model_checker.h"
#include "mc_state.h"
#include "mc_smx.h"
#endif
// 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:
// 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,
#include <xbt/log.h>
-#include "mc_model_checker.h"
+#include "ModelChecker.hpp"
#include "mc_protocol.h"
#include "mc_server.h"
#include "mc_private.h"
{
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");
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));
+ 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) {
+ while (mc_model_checker->process().running) {
if (!mc_server->handle_events())
return;
}
#include "simix/smx_private.h"
#include "mc_smx.h"
-#include "mc_model_checker.h"
+#include "ModelChecker.hpp"
extern "C" {
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));
*/
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
_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) {
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;
}
#include <xbt/dynar.h>
#include "mc_forward.h"
-#include "mc_model_checker.h"
+#include "ModelChecker.hpp"
#include "mc_page_store.h"
#include "mc_mmalloc.h"
#include "mc_address_space.h"
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_page_store_get_page(
+ &mc_model_checker->page_store(), 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);
void mc_free_page_snapshot_region(size_t* pagenos, size_t page_count);
{
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
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);
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;
*/
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;
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;
}
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;
}
#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"
#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);
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');
#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
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);