xbt_dynar_foreach(simix_global->process_that_ran, iter, process) {
req = &process->simcall;
if (req->call != SIMCALL_NONE && !MC_request_is_visible(req))
- SIMIX_simcall_pre(req, 0);
+ SIMIX_simcall_enter(req, 0);
}
}
}
return deadlock;
}
+void mc_update_comm_pattern(mc_call_type call_type, smx_simcall_t req, int value, xbt_dynar_t pattern) {
+ switch(call_type) {
+ case MC_CALL_TYPE_NONE:
+ break;
+ case MC_CALL_TYPE_SEND:
+ case MC_CALL_TYPE_RECV:
+ get_comm_pattern(pattern, req, call_type);
+ break;
+ case MC_CALL_TYPE_WAIT:
+ {
+ smx_action_t current_comm = NULL;
+ if (call_type == MC_CALL_TYPE_WAIT)
+ current_comm = simcall_comm_wait__get__comm(req);
+ else
+ current_comm = xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value, smx_action_t);
+ // First wait only must be considered:
+ if (current_comm->comm.refcount == 1)
+ complete_comm_pattern(pattern, current_comm);
+ break;
+ }
+ default:
+ xbt_die("Unexpected call type %i", (int)call_type);
+ }
+}
+
/**
* \brief Re-executes from the state at position start all the transitions indicated by
* a given model-checker stack.
{
int raw_mem = (mmalloc_get_current_heap() == mc_heap);
- int value, i = 1, count = 1, call = 0, j;
+ int value, i = 1, count = 1, j;
char *req_str;
smx_simcall_t req = NULL, saved_req = NULL;
xbt_fifo_item_t item, start_item;
mc_state_t state;
smx_process_t process = NULL;
- smx_action_t current_comm;
XBT_DEBUG("**** Begin Replay ****");
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;
}
}
/* TODO : handle test and testany simcalls */
+ mc_call_type call = MC_CALL_TYPE_NONE;
if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
- if (req->call == SIMCALL_COMM_ISEND)
- call = 1;
- else if (req->call == SIMCALL_COMM_IRECV)
- call = 2;
- else if (req->call == SIMCALL_COMM_WAIT)
- call = 3;
- else if (req->call == SIMCALL_COMM_WAITANY)
- call = 4;
+ call = mc_get_call_type(req);
}
- SIMIX_simcall_pre(req, value);
+ SIMIX_simcall_enter(req, value);
if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
MC_SET_MC_HEAP;
- if (call == 1) { /* Send */
- get_comm_pattern(communications_pattern, req, call);
- } else if (call == 2) { /* Recv */
- get_comm_pattern(communications_pattern, req, call);
- } else if (call == 3) { /* Wait */
- current_comm = simcall_comm_wait__get__comm(req);
- if (current_comm->comm.refcount == 1) /* First wait only must be considered */
- complete_comm_pattern(communications_pattern, current_comm);
- } else if (call == 4) { /* WaitAny */
- current_comm = xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value, smx_action_t);
- if (current_comm->comm.refcount == 1) /* First wait only must be considered */
- complete_comm_pattern(communications_pattern, current_comm);
- }
+ mc_update_comm_pattern(call, req, value, communications_pattern);
MC_SET_STD_HEAP;
- call = 0;
}
-
MC_wait_for_requests();
count++;
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);
}
- SIMIX_simcall_pre(req, value);
+ SIMIX_simcall_enter(req, value);
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)
