- mc_mode = MC_MODE_CLIENT;
- MC_init();
- MC_client_main_loop();
-}
-
-void MC_exit(void)
-{
- xbt_free(mc_time);
-
- MC_memory_exit();
- //xbt_abort();
-}
-
-#ifdef HAVE_MC
-int MC_deadlock_check()
-{
- if (mc_mode == MC_MODE_SERVER) {
- int res;
- if ((res = mc_model_checker->process().send_message(MC_MESSAGE_DEADLOCK_CHECK)))
- xbt_die("Could not check deadlock state");
- s_mc_int_message_t message;
- ssize_t s = mc_model_checker->process().receive_message(message);
- if (s == -1)
- xbt_die("Could not receive message");
- else if (s != sizeof(message) || message.type != MC_MESSAGE_DEADLOCK_CHECK_REPLY) {
- xbt_die("%s received unexpected message %s (%i, size=%i) "
- "expected MC_MESSAGE_DEADLOCK_CHECK_REPLY (%i, size=%i)",
- MC_mode_name(mc_mode),
- MC_message_type_name(message.type), (int) message.type, (int) s,
- (int) MC_MESSAGE_DEADLOCK_CHECK_REPLY, (int) sizeof(message)
- );
- }
- else
- return message.value;
- }
-
- int deadlock = FALSE;
- smx_process_t process;
- if (xbt_swag_size(simix_global->process_list)) {
- deadlock = TRUE;
- xbt_swag_foreach(process, simix_global->process_list) {
- if (MC_process_is_enabled(process)) {
- deadlock = FALSE;
- break;
- }
- }
- }
- return deadlock;
-}
-#endif
-
-/**
- * \brief Re-executes from the state at position start all the transitions indicated by
- * a given model-checker stack.
- * \param stack The stack with the transitions to execute.
- * \param start Start index to begin the re-execution.
- */
-void MC_replay(xbt_fifo_t stack)
-{
- int value, count = 1;
- char *req_str;
- smx_simcall_t req = nullptr, saved_req = NULL;
- xbt_fifo_item_t item, start_item;
- mc_state_t state;
-
- XBT_DEBUG("**** Begin Replay ****");
-
- /* Intermediate backtracking */
- if(_sg_mc_checkpoint > 0 || _sg_mc_termination || _sg_mc_visited > 0) {
- start_item = xbt_fifo_get_first_item(stack);
- state = (mc_state_t)xbt_fifo_get_item_content(start_item);
- if(state->system_state){
- simgrid::mc::restore_snapshot(state->system_state);
- if(_sg_mc_comms_determinism || _sg_mc_send_determinism)
- MC_restore_communications_pattern(state);
- return;
- }
- }
-
-
- /* Restore the initial state */
- simgrid::mc::restore_snapshot(initial_global_state->snapshot);
- /* At the moment of taking the snapshot the raw heap was set, so restoring
- * it will set it back again, we have to unset it to continue */
-
- start_item = xbt_fifo_get_last_item(stack);
-
- if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
- // int n = xbt_dynar_length(incomplete_communications_pattern);
- unsigned n = MC_smx_get_maxpid();
- assert(n == xbt_dynar_length(incomplete_communications_pattern));
- assert(n == xbt_dynar_length(initial_communications_pattern));
- 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;
- }
- }
-
- /* Traverse the stack from the state at position start and re-execute the transitions */
- for (item = start_item;
- item != xbt_fifo_get_first_item(stack);
- item = xbt_fifo_get_prev_item(item)) {
-
- state = (mc_state_t) xbt_fifo_get_item_content(item);
- saved_req = MC_state_get_executed_request(state, &value);
-
- if (saved_req) {
- /* 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 */
-
- const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
- req = &issuer->simcall;
-
- /* Debug information */
- if (XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)) {
- req_str = MC_request_to_string(req, value, MC_REQUEST_SIMIX);
- XBT_DEBUG("Replay: %s (%p)", req_str, state);
- xbt_free(req_str);
- }
-
- /* TODO : handle test and testany simcalls */
- e_mc_call_type_t call = MC_CALL_TYPE_NONE;
- if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
- call = MC_get_call_type(req);
-
- MC_simcall_handle(req, value);
-
- if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
- MC_handle_comm_pattern(call, req, value, nullptr, 1);
-
- mc_model_checker->wait_for_requests();
-
- count++;
- }
-
- /* Update statistics */
- mc_stats->visited_states++;
- mc_stats->executed_transitions++;
-
- }
-
- XBT_DEBUG("**** End Replay ****");
-}
-
-void MC_replay_liveness(xbt_fifo_t stack)
-{
- xbt_fifo_item_t item;
- mc_pair_t pair = nullptr;
- mc_state_t state = nullptr;
- smx_simcall_t req = nullptr, saved_req = NULL;
- int value, depth = 1;
- char *req_str;
-
- XBT_DEBUG("**** Begin Replay ****");
-
- /* Intermediate backtracking */
- if(_sg_mc_checkpoint > 0) {
- item = xbt_fifo_get_first_item(stack);
- pair = (mc_pair_t) xbt_fifo_get_item_content(item);
- if(pair->graph_state->system_state){
- simgrid::mc::restore_snapshot(pair->graph_state->system_state);
- return;
- }
- }
-
- /* Restore the initial state */
- simgrid::mc::restore_snapshot(initial_global_state->snapshot);
-
- /* 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->exploration_started) {
-
- saved_req = MC_state_get_executed_request(state, &value);
-
- if (saved_req != nullptr) {
- /* 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 */
- const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
- req = &issuer->simcall;
-
- /* Debug information */
- if (XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)) {
- req_str = MC_request_to_string(req, value, MC_REQUEST_SIMIX);
- XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
- xbt_free(req_str);
- }
-
- }
-
- MC_simcall_handle(req, value);
- mc_model_checker->wait_for_requests();
- }
-
- /* Update statistics */
- mc_stats->visited_pairs++;
- mc_stats->executed_transitions++;
-
- depth++;
-
- }
-
- XBT_DEBUG("**** End Replay ****");
-}
-
-/**
- * \brief Dumps the contents of a model-checker's stack and shows the actual
- * execution trace
- * \param stack The stack to dump
- */
-void MC_dump_stack_safety(xbt_fifo_t stack)
-{
- MC_show_stack_safety(stack);
-
- mc_state_t state;
-
- while ((state = (mc_state_t) xbt_fifo_pop(stack)) != nullptr)
- MC_state_delete(state, !state->in_visited_states ? 1 : 0);
-}
-
-
-void MC_show_stack_safety(xbt_fifo_t stack)
-{
- int value;
- mc_state_t state;
- xbt_fifo_item_t item;
- smx_simcall_t req;
- char *req_str = nullptr;
-
- for (item = xbt_fifo_get_last_item(stack);
- item; item = xbt_fifo_get_prev_item(item)) {
- state = (mc_state_t)xbt_fifo_get_item_content(item);
- req = MC_state_get_executed_request(state, &value);
- if (req) {
- req_str = MC_request_to_string(req, value, MC_REQUEST_EXECUTED);
- XBT_INFO("%s", req_str);
- xbt_free(req_str);
- }