/* 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 "mc_state.h"
+#include "mc_request.h"
+#include "mc_safety.h"
#include "mc_private.h"
+#include "mc_record.h"
+#include "mc_smx.h"
+#include "mc_client.h"
#include "xbt/mmalloc/mmprivate.h"
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
"Logging specific to MC safety verification ");
-xbt_dict_t first_enabled_state;
+static int is_exploration_stack_state(mc_state_t current_state){
+
+ xbt_fifo_item_t item;
+ mc_state_t stack_state;
+ for(item = xbt_fifo_get_first_item(mc_stack); item != NULL; item = xbt_fifo_get_next_item(item)) {
+ stack_state = (mc_state_t) xbt_fifo_get_item_content(item);
+ if(snapshot_compare(stack_state, current_state) == 0){
+ XBT_INFO("Non-progressive cycle : state %d -> state %d", stack_state->num, current_state->num);
+ return 1;
+ }
+ }
+ return 0;
+}
/**
* \brief Initialize the DPOR exploration algorithm
*/
-void MC_pre_modelcheck_safety()
+static void MC_pre_modelcheck_safety()
{
-
- int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
-
- mc_state_t initial_state = NULL;
- smx_process_t process;
-
- /* Create the initial state and push it into the exploration stack */
- if (!mc_mem_set)
- MC_SET_MC_HEAP;
+ xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
if (_sg_mc_visited > 0)
- visited_states =
- xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
-
- if (mc_reduce_kind == e_mc_reduce_dpor)
- first_enabled_state = xbt_dict_new_homogeneous(&xbt_free_f);
-
- initial_state = MC_state_new();
+ visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
+ mc_state_t initial_state = MC_state_new();
MC_SET_STD_HEAP;
XBT_DEBUG("**************************************************");
MC_SET_MC_HEAP;
/* Get an enabled process and insert it in the interleave set of the initial state */
- xbt_swag_foreach(process, simix_global->process_list) {
+ smx_process_t process;
+ MC_EACH_SIMIX_PROCESS(process,
if (MC_process_is_enabled(process)) {
MC_state_interleave_process(initial_state, process);
if (mc_reduce_kind != e_mc_reduce_none)
break;
}
- }
+ );
xbt_fifo_unshift(mc_stack, initial_state);
-
- if (mc_reduce_kind == e_mc_reduce_dpor) {
- /* To ensure the soundness of DPOR, we have to keep a list of
- processes which are still enabled at each step of the exploration.
- If max depth is reached, we interleave them in the state in which they have
- been enabled for the first time. */
- xbt_swag_foreach(process, simix_global->process_list) {
- if (MC_process_is_enabled(process)) {
- char *key = bprintf("%lu", process->pid);
- char *data = bprintf("%d", xbt_fifo_size(mc_stack));
- xbt_dict_set(first_enabled_state, key, data, NULL);
- xbt_free(key);
- }
- }
- }
-
- if (!mc_mem_set)
- MC_SET_STD_HEAP;
+ mmalloc_set_current_heap(heap);
}
/** \brief Model-check the application using a DFS exploration
* with DPOR (Dynamic Partial Order Reductions)
*/
-void MC_modelcheck_safety(void)
+static void MC_modelcheck_safety_main(void)
{
-
char *req_str = NULL;
int value;
- smx_simcall_t req = NULL, prev_req = NULL;
- mc_state_t state = NULL, prev_state = NULL, next_state =
- NULL, restored_state = NULL;
- smx_process_t process = NULL;
+ smx_simcall_t req = NULL;
+ mc_state_t state = NULL, prev_state = NULL, next_state = NULL;
xbt_fifo_item_t item = NULL;
- mc_state_t state_test = NULL;
- int pos;
mc_visited_state_t visited_state = NULL;
- int enabled = 0;
while (xbt_fifo_size(mc_stack) > 0) {
/* Get current state */
- state = (mc_state_t)
- xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
+ state = (mc_state_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
XBT_DEBUG("**************************************************");
XBT_DEBUG
- ("Exploration depth=%d (state=%p, num %d)(%u interleave, user_max_depth %d, first_enabled_state size : %d)",
+ ("Exploration depth=%d (state=%p, num %d)(%u interleave, user_max_depth %d)",
xbt_fifo_size(mc_stack), state, state->num,
- MC_state_interleave_size(state), user_max_depth_reached,
- xbt_dict_size(first_enabled_state));
+ MC_state_interleave_size(state), user_max_depth_reached);
/* Update statistics */
mc_stats->visited_states++;
if (xbt_fifo_size(mc_stack) <= _sg_mc_max_depth && !user_max_depth_reached
&& (req = MC_state_get_request(state, &value)) && visited_state == NULL) {
- MC_LOG_REQUEST(mc_safety, req, value);
+ req_str = MC_request_to_string(req, value, MC_REQUEST_SIMIX);
+ XBT_DEBUG("Execute: %s", req_str);
+ xbt_free(req_str);
if (dot_output != NULL) {
MC_SET_MC_HEAP;
MC_state_set_executed_request(state, req, value);
mc_stats->executed_transitions++;
- if (mc_reduce_kind == e_mc_reduce_dpor) {
- MC_SET_MC_HEAP;
- char *key = bprintf("%lu", req->issuer->pid);
- xbt_dict_remove(first_enabled_state, key);
- xbt_free(key);
- MC_SET_STD_HEAP;
- }
+ // TODO, bundle both operations in a single message
+ // MC_execute_transition(req, value)
/* Answer the request */
- SIMIX_simcall_enter(req, value);
-
- /* Wait for requests (schedules processes) */
+ MC_simcall_handle(req, value);
MC_wait_for_requests();
/* Create the new expanded state */
next_state = MC_state_new();
- if ((visited_state = is_visited_state()) == NULL) {
+ if(_sg_mc_termination && is_exploration_stack_state(next_state)){
+ MC_show_non_termination();
+ return;
+ }
+
+ if ((visited_state = is_visited_state(next_state)) == NULL) {
/* Get an enabled process and insert it in the interleave set of the next state */
- xbt_swag_foreach(process, simix_global->process_list) {
+ smx_process_t process = NULL;
+ MC_EACH_SIMIX_PROCESS(process,
if (MC_process_is_enabled(process)) {
MC_state_interleave_process(next_state, process);
if (mc_reduce_kind != e_mc_reduce_none)
break;
}
- }
-
- if (_sg_mc_checkpoint
- && ((xbt_fifo_size(mc_stack) + 1) % _sg_mc_checkpoint == 0)) {
- next_state->system_state = MC_take_snapshot(next_state->num);
- }
+ );
if (dot_output != NULL)
- fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,
- next_state->num, req_str);
+ fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
} else {
if (dot_output != NULL)
- fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,
- visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
+ fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
}
xbt_fifo_unshift(mc_stack, next_state);
- if (mc_reduce_kind == e_mc_reduce_dpor) {
- /* Insert in dict all enabled processes, if not included yet */
- xbt_swag_foreach(process, simix_global->process_list) {
- if (MC_process_is_enabled(process)) {
- char *key = bprintf("%lu", process->pid);
- if (xbt_dict_get_or_null(first_enabled_state, key) == NULL) {
- char *data = bprintf("%d", xbt_fifo_size(mc_stack));
- xbt_dict_set(first_enabled_state, key, data, NULL);
- }
- xbt_free(key);
- }
- }
- }
-
if (dot_output != NULL)
xbt_free(req_str);
/* The interleave set is empty or the maximum depth is reached, let's back-track */
} else {
- if ((xbt_fifo_size(mc_stack) > _sg_mc_max_depth) || user_max_depth_reached
- || visited_state != NULL) {
+ if ((xbt_fifo_size(mc_stack) > _sg_mc_max_depth) || user_max_depth_reached || visited_state != NULL) {
if (user_max_depth_reached && visited_state == NULL)
XBT_DEBUG("User max depth reached !");
else
XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.", visited_state->other_num == -1 ? visited_state->num : visited_state->other_num);
- if (mc_reduce_kind == e_mc_reduce_dpor) {
- /* Interleave enabled processes in the state in which they have been enabled for the first time */
- xbt_swag_foreach(process, simix_global->process_list) {
- if (MC_process_is_enabled(process)) {
- char *key = bprintf("%lu", process->pid);
- enabled =
- (int) strtoul(xbt_dict_get_or_null(first_enabled_state, key),
- 0, 10);
- xbt_free(key);
- int cursor = xbt_fifo_size(mc_stack);
- xbt_fifo_foreach(mc_stack, item, state_test, mc_state_t) {
- if (cursor-- == enabled) {
- if (!MC_state_process_is_done(state_test, process)
- && state_test->num != state->num) {
- XBT_DEBUG("Interleave process %lu in state %d",
- process->pid, state_test->num);
- MC_state_interleave_process(state_test, process);
- break;
- }
- }
- }
- }
- }
- }
-
} else {
- XBT_DEBUG("There are no more processes to interleave. (depth %d)",
- xbt_fifo_size(mc_stack) + 1);
+ XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack) + 1);
}
/* Trash the current state, no longer needed */
xbt_fifo_shift(mc_stack);
- MC_state_delete(state);
- XBT_DEBUG("Delete state %d at depth %d", state->num,
- xbt_fifo_size(mc_stack) + 1);
+ XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
+ MC_state_delete(state, !state->in_visited_states ? 1 : 0);
MC_SET_STD_HEAP;
while ((state = xbt_fifo_shift(mc_stack)) != NULL) {
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);
xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
- if (MC_request_depend
- (req, MC_state_get_internal_request(prev_state))) {
+ if (MC_request_depend(req, MC_state_get_internal_request(prev_state))) {
if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
XBT_DEBUG("Dependent Transitions:");
- prev_req = MC_state_get_executed_request(prev_state, &value);
- req_str = MC_request_to_string(prev_req, value);
+ smx_simcall_t prev_req = MC_state_get_executed_request(prev_state, &value);
+ req_str = MC_request_to_string(prev_req, value, MC_REQUEST_INTERNAL);
XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
xbt_free(req_str);
prev_req = MC_state_get_executed_request(state, &value);
- req_str = MC_request_to_string(prev_req, value);
+ req_str = MC_request_to_string(prev_req, value, MC_REQUEST_EXECUTED);
XBT_DEBUG("%s (state=%d)", req_str, state->num);
xbt_free(req_str);
}
- if (!MC_state_process_is_done(prev_state, req->issuer))
- MC_state_interleave_process(prev_state, req->issuer);
+ if (!MC_state_process_is_done(prev_state, issuer))
+ MC_state_interleave_process(prev_state, issuer);
else
XBT_DEBUG("Process %p is in done set", req->issuer);
break;
- } else if (req->issuer ==
- MC_state_get_internal_request(prev_state)->issuer) {
+ } else if (req->issuer == MC_state_get_internal_request(prev_state)->issuer) {
- XBT_DEBUG("Simcall %d and %d with same issuer", req->call,
- MC_state_get_internal_request(prev_state)->call);
+ XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
break;
} else {
- XBT_DEBUG
- ("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
- req->call, req->issuer->pid, state->num,
- MC_state_get_internal_request(prev_state)->call,
- MC_state_get_internal_request(prev_state)->issuer->pid,
- prev_state->num);
+ const smx_process_t previous_issuer = MC_smx_simcall_get_issuer(MC_state_get_internal_request(prev_state));
+ XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
+ req->call, issuer->pid, state->num,
+ MC_state_get_internal_request(prev_state)->call,
+ previous_issuer->pid,
+ prev_state->num);
}
}
}
- if (MC_state_interleave_size(state)
- && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) {
+ 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);
- if (_sg_mc_checkpoint) {
- if (state->system_state != NULL) {
- MC_restore_snapshot(state->system_state);
- xbt_fifo_unshift(mc_stack, state);
- MC_SET_STD_HEAP;
- } else {
- pos = xbt_fifo_size(mc_stack);
- item = xbt_fifo_get_first_item(mc_stack);
- while (pos > 0) {
- restored_state = (mc_state_t) xbt_fifo_get_item_content(item);
- if (restored_state->system_state != NULL) {
- break;
- } else {
- item = xbt_fifo_get_next_item(item);
- pos--;
- }
- }
- MC_restore_snapshot(restored_state->system_state);
- xbt_fifo_unshift(mc_stack, state);
- MC_SET_STD_HEAP;
- MC_replay(mc_stack, pos);
- }
- } else {
- xbt_fifo_unshift(mc_stack, state);
- MC_SET_STD_HEAP;
- MC_replay(mc_stack, -1);
- }
- XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num,
- xbt_fifo_size(mc_stack));
+ XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
+ xbt_fifo_unshift(mc_stack, state);
+ MC_replay(mc_stack);
+ XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, xbt_fifo_size(mc_stack));
break;
} else {
- XBT_DEBUG("Delete state %d at depth %d", state->num,
- xbt_fifo_size(mc_stack) + 1);
- MC_state_delete(state);
+ XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
+ MC_state_delete(state, !state->in_visited_states ? 1 : 0);
}
}
MC_SET_STD_HEAP;
return;
}
+
+void MC_modelcheck_safety(void)
+{
+ XBT_DEBUG("Starting the safety algorithm");
+ xbt_assert(mc_mode == MC_MODE_SERVER);
+
+ _sg_mc_safety = 1;
+
+ xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
+
+ /* Create exploration stack */
+ mc_stack = xbt_fifo_new();
+
+ MC_SET_STD_HEAP;
+
+ MC_pre_modelcheck_safety();
+
+ MC_SET_MC_HEAP;
+ /* Save the initial state */
+ initial_global_state = xbt_new0(s_mc_global_t, 1);
+ initial_global_state->snapshot = MC_take_snapshot(0);
+ MC_SET_STD_HEAP;
+
+ MC_modelcheck_safety_main();
+
+ mmalloc_set_current_heap(heap);
+
+ xbt_abort();
+ //MC_exit();
+}