int _sg_do_model_check = 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_timeout = 0;
int _sg_mc_hash = 0;
_sg_mc_checkpoint = xbt_cfg_get_int(_sg_cfg_set, name);
}
+void _mc_cfg_cb_sparse_checkpoint(const char *name, int pos) {
+ if (_sg_cfg_init_status && !_sg_do_model_check) {
+ xbt_die("You are specifying a checkpointing 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_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) {
}
+mc_model_checker_t mc_model_checker = NULL;
+
void MC_init()
{
-
int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
mc_time = xbt_new0(double, simix_process_maxpid);
MC_SET_MC_HEAP;
+ mc_model_checker = xbt_new0(s_mc_model_checker_t, 1);
+ mc_model_checker->pages = mc_pages_store_new();
+ mc_model_checker->fd_clear_refs = -1;
+ mc_model_checker->fd_pagemap = -1;
+
mc_comp_times = xbt_new0(s_mc_comparison_times_t, 1);
/* Initialize statistics */
MC_ignore_local_variable("ctx", "*");
MC_ignore_local_variable("self", "simcall_BODY_mc_snapshot");
- MC_ignore_local_variable("next_context", "smx_ctx_sysv_suspend_serial");
+ MC_ignore_local_variable("next_cont"
+ "ext", "smx_ctx_sysv_suspend_serial");
MC_ignore_local_variable("i", "smx_ctx_sysv_suspend_serial");
/* Ignore local variable about time used for tracing */
MC_ignore_local_variable("start_time", "*");
+ MC_ignore_global_variable("mc_model_checker");
+
+ // Mot of those things could be moved into mc_model_checker:
MC_ignore_global_variable("compared_pointers");
MC_ignore_global_variable("mc_comp_times");
MC_ignore_global_variable("mc_snapshot_comparison_time");
MC_ignore_global_variable("initial_communications_pattern");
MC_ignore_global_variable("incomplete_communications_pattern");
+ if (MC_is_active()) {
+ MC_ignore_global_variable("mc_diff_info");
+ }
+
MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double));
smx_process_t process;
if (mc_reduce_kind == e_mc_reduce_dpor) {
MC_SET_MC_HEAP;
char *key = bprintf("%lu", saved_req->issuer->pid);
- xbt_dict_remove(first_enabled_state, key);
+ if(xbt_dict_get_or_null(first_enabled_state, key))
+ xbt_dict_remove(first_enabled_state, key);
xbt_free(key);
MC_SET_STD_HEAP;
}
initial_global_state->raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
- int value;
- char *req_str;
- smx_simcall_t req = NULL, saved_req = NULL;
xbt_fifo_item_t item;
- mc_state_t state;
- mc_pair_t pair;
int depth = 1;
XBT_DEBUG("**** Begin Replay ****");
if (!initial_global_state->raw_mem_set)
MC_SET_STD_HEAP;
- if (all_stack) {
-
- item = xbt_fifo_get_last_item(stack);
+ /* Traverse the stack from the initial state and re-execute the transitions */
+ for (item = xbt_fifo_get_last_item(stack);
+ all_stack ? depth <= xbt_fifo_size(stack) : item != xbt_fifo_get_first_item(stack);
+ item = xbt_fifo_get_prev_item(item)) {
- while (depth <= xbt_fifo_size(stack)) {
+ mc_pair_t pair = (mc_pair_t) xbt_fifo_get_item_content(item);
- pair = (mc_pair_t) xbt_fifo_get_item_content(item);
- state = (mc_state_t) pair->graph_state;
+ mc_state_t state = (mc_state_t) pair->graph_state;
+ smx_simcall_t req = NULL, saved_req = NULL;
+ int value;
+ char *req_str;
if (pair->requests > 0) {
//XBT_DEBUG("SavedReq->call %u", saved_req->call);
if (saved_req != NULL) {
- /* because we got a copy of the executed request, we have to fetch the
+ /* because we got a copy of the executed request, we have to fetch the
real one, pointed by the request field of the issuer process */
req = &saved_req->issuer->simcall;
//XBT_DEBUG("Req->call %u", req->call);
MC_wait_for_requests();
}
- depth++;
-
/* Update statistics */
mc_stats->visited_pairs++;
mc_stats->executed_transitions++;
- item = xbt_fifo_get_prev_item(item);
- }
-
- } else {
-
- /* Traverse the stack from the initial state and re-execute the transitions */
- for (item = xbt_fifo_get_last_item(stack);
- item != xbt_fifo_get_first_item(stack);
- item = xbt_fifo_get_prev_item(item)) {
-
- pair = (mc_pair_t) xbt_fifo_get_item_content(item);
- state = (mc_state_t) pair->graph_state;
-
- if (pair->requests > 0) {
-
- saved_req = MC_state_get_executed_request(state, &value);
- //XBT_DEBUG("SavedReq->call %u", saved_req->call);
-
- if (saved_req != NULL) {
- /* because we got a copy of the executed request, we have to fetch the
- real one, pointed by the request field of the issuer process */
- req = &saved_req->issuer->simcall;
- //XBT_DEBUG("Req->call %u", req->call);
-
- /* Debug information */
- if (XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)) {
- req_str = MC_request_to_string(req, value);
- XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
- xbt_free(req_str);
- }
-
- }
-
- SIMIX_simcall_pre(req, value);
- MC_wait_for_requests();
- }
-
depth++;
- /* Update statistics */
- mc_stats->visited_pairs++;
- mc_stats->executed_transitions++;
}
- }
XBT_DEBUG("**** End Replay ****");
void MC_print_statistics(mc_stats_t stats)
{
+ xbt_mheap_t previous_heap = mmalloc_get_current_heap();
+
if (stats->expanded_pairs == 0) {
XBT_INFO("Expanded states = %lu", stats->expanded_states);
XBT_INFO("Visited states = %lu", stats->visited_states);
XBT_INFO("Send-deterministic : %s",
!initial_global_state->send_deterministic ? "No" : "Yes");
}
- MC_SET_STD_HEAP;
+ mmalloc_set_current_heap(previous_heap);
}
void MC_assert(int prop)
