From: Gabriel Corona Date: Wed, 6 Apr 2016 14:05:38 +0000 (+0200) Subject: [mc] Get rid of MC_state_set_executed_request() in order to simplify the Checkers X-Git-Tag: v3_13~138 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/932e745735378c442e2348a3a428d97b69398f86 [mc] Get rid of MC_state_set_executed_request() in order to simplify the Checkers --- diff --git a/src/mc/CommunicationDeterminismChecker.cpp b/src/mc/CommunicationDeterminismChecker.cpp index f983945862..ea3ab38e09 100644 --- a/src/mc/CommunicationDeterminismChecker.cpp +++ b/src/mc/CommunicationDeterminismChecker.cpp @@ -410,7 +410,6 @@ int CommunicationDeterminismChecker::main(void) if (dot_output != nullptr) req_str = simgrid::mc::request_get_dot_output(req, value); - MC_state_set_executed_request(state, req, value); mc_stats->executed_transitions++; /* TODO : handle test and testany simcalls */ diff --git a/src/mc/LivenessChecker.cpp b/src/mc/LivenessChecker.cpp index 567548fbba..be0149b7f4 100644 --- a/src/mc/LivenessChecker.cpp +++ b/src/mc/LivenessChecker.cpp @@ -398,9 +398,6 @@ int LivenessChecker::main(void) simgrid::mc::request_to_string( req, value, simgrid::mc::RequestType::simix).c_str()); - /* Set request as executed */ - MC_state_set_executed_request(current_pair->graph_state.get(), req, value); - /* Update mc_stats */ mc_stats->executed_transitions++; if (!current_pair->exploration_started) diff --git a/src/mc/SafetyChecker.cpp b/src/mc/SafetyChecker.cpp index f79c6b98bf..e7c62e8a3f 100644 --- a/src/mc/SafetyChecker.cpp +++ b/src/mc/SafetyChecker.cpp @@ -132,7 +132,6 @@ int SafetyChecker::run() if (dot_output != nullptr) req_str = simgrid::mc::request_get_dot_output(req, value); - MC_state_set_executed_request(state, req, value); mc_stats->executed_transitions++; // TODO, bundle both operations in a single message diff --git a/src/mc/mc_state.cpp b/src/mc/mc_state.cpp index 5967f1a3a3..d6123a3e9f 100644 --- a/src/mc/mc_state.cpp +++ b/src/mc/mc_state.cpp @@ -69,82 +69,6 @@ void MC_state_interleave_process(simgrid::mc::State* state, smx_process_t proces state->processStates[process->pid].interleave_count = 0; } -void MC_state_set_executed_request(simgrid::mc::State* state, smx_simcall_t req, - int value) -{ - state->executed_req = *req; - state->req_num = value; - - /* The waitany and testany request are transformed into a wait or test request over the - * corresponding communication action so it can be treated later by the dependence - * function. */ - switch (req->call) { - case SIMCALL_COMM_WAITANY: { - state->internal_req.call = SIMCALL_COMM_WAIT; - state->internal_req.issuer = req->issuer; - smx_synchro_t remote_comm; - read_element(mc_model_checker->process(), - &remote_comm, remote(simcall_comm_waitany__get__comms(req)), - value, sizeof(remote_comm)); - mc_model_checker->process().read(&state->internal_comm, remote(remote_comm)); - simcall_comm_wait__set__comm(&state->internal_req, &state->internal_comm); - simcall_comm_wait__set__timeout(&state->internal_req, 0); - break; - } - - case SIMCALL_COMM_TESTANY: - state->internal_req.call = SIMCALL_COMM_TEST; - state->internal_req.issuer = req->issuer; - - if (value > 0) { - smx_synchro_t remote_comm; - read_element(mc_model_checker->process(), - &remote_comm, remote(simcall_comm_testany__get__comms(req)), - value, sizeof(remote_comm)); - mc_model_checker->process().read(&state->internal_comm, remote(remote_comm)); - } - - simcall_comm_test__set__comm(&state->internal_req, &state->internal_comm); - simcall_comm_test__set__result(&state->internal_req, value); - break; - - case SIMCALL_COMM_WAIT: - state->internal_req = *req; - mc_model_checker->process().read_bytes(&state->internal_comm , - sizeof(state->internal_comm), remote(simcall_comm_wait__get__comm(req))); - simcall_comm_wait__set__comm(&state->executed_req, &state->internal_comm); - simcall_comm_wait__set__comm(&state->internal_req, &state->internal_comm); - break; - - case SIMCALL_COMM_TEST: - state->internal_req = *req; - mc_model_checker->process().read_bytes(&state->internal_comm, - sizeof(state->internal_comm), remote(simcall_comm_test__get__comm(req))); - simcall_comm_test__set__comm(&state->executed_req, &state->internal_comm); - simcall_comm_test__set__comm(&state->internal_req, &state->internal_comm); - break; - - case SIMCALL_MC_RANDOM: { - state->internal_req = *req; - int random_max = simcall_mc_random__get__max(req); - if (value != random_max) - for (auto& p : mc_model_checker->process().simix_processes()) { - simgrid::mc::ProcessState* procstate = &state->processStates[p.copy.pid]; - const smx_process_t issuer = MC_smx_simcall_get_issuer(req); - if (p.copy.pid == issuer->pid) { - procstate->state = simgrid::mc::ProcessInterleaveState::more_interleave; - break; - } - } - break; - } - - default: - state->internal_req = *req; - break; - } -} - smx_simcall_t MC_state_get_executed_request(simgrid::mc::State* state, int *value) { *value = state->req_num; @@ -166,8 +90,8 @@ static inline smx_simcall_t MC_state_get_request_for_process( if (!simgrid::mc::process_is_enabled(process)) return nullptr; + smx_simcall_t req = nullptr; switch (process->simcall.call) { - case SIMCALL_COMM_WAITANY: *value = -1; while (procstate->interleave_count < @@ -184,10 +108,8 @@ static inline smx_simcall_t MC_state_get_request_for_process( simgrid::mc::read_length(mc_model_checker->process(), simgrid::mc::remote(simcall_comm_waitany__get__comms(&process->simcall)))) procstate->state = simgrid::mc::ProcessInterleaveState::done; - if (*value != -1) - return &process->simcall; - + req = &process->simcall; break; case SIMCALL_COMM_TESTANY: { @@ -208,7 +130,7 @@ static inline smx_simcall_t MC_state_get_request_for_process( procstate->state = simgrid::mc::ProcessInterleaveState::done; if (*value != -1 || start_count == 0) - return &process->simcall; + req = &process->simcall; break; } @@ -226,7 +148,8 @@ static inline smx_simcall_t MC_state_get_request_for_process( else *value = -1; procstate->state = simgrid::mc::ProcessInterleaveState::done; - return &process->simcall; + req = &process->simcall; + break; } case SIMCALL_MC_RANDOM: @@ -235,14 +158,93 @@ static inline smx_simcall_t MC_state_get_request_for_process( else if (state->req_num < simcall_mc_random__get__max(&process->simcall)) *value = state->req_num + 1; procstate->state = simgrid::mc::ProcessInterleaveState::done; - return &process->simcall; + req = &process->simcall; + break; default: procstate->state = simgrid::mc::ProcessInterleaveState::done; *value = 0; - return &process->simcall; + req = &process->simcall; + break; } - return nullptr; + if (!req) + return nullptr; + + // Fetch the data of the request and translate it: + + state->executed_req = *req; + state->req_num = *value; + + /* The waitany and testany request are transformed into a wait or test request + * over the corresponding communication action so it can be treated later by + * the dependence function. */ + switch (req->call) { + case SIMCALL_COMM_WAITANY: { + state->internal_req.call = SIMCALL_COMM_WAIT; + state->internal_req.issuer = req->issuer; + smx_synchro_t remote_comm; + read_element(mc_model_checker->process(), + &remote_comm, remote(simcall_comm_waitany__get__comms(req)), + *value, sizeof(remote_comm)); + mc_model_checker->process().read(&state->internal_comm, remote(remote_comm)); + simcall_comm_wait__set__comm(&state->internal_req, &state->internal_comm); + simcall_comm_wait__set__timeout(&state->internal_req, 0); + break; + } + + case SIMCALL_COMM_TESTANY: + state->internal_req.call = SIMCALL_COMM_TEST; + state->internal_req.issuer = req->issuer; + + if (*value > 0) { + smx_synchro_t remote_comm; + read_element(mc_model_checker->process(), + &remote_comm, remote(simcall_comm_testany__get__comms(req)), + *value, sizeof(remote_comm)); + mc_model_checker->process().read(&state->internal_comm, remote(remote_comm)); + } + + simcall_comm_test__set__comm(&state->internal_req, &state->internal_comm); + simcall_comm_test__set__result(&state->internal_req, *value); + break; + + case SIMCALL_COMM_WAIT: + state->internal_req = *req; + mc_model_checker->process().read_bytes(&state->internal_comm , + sizeof(state->internal_comm), remote(simcall_comm_wait__get__comm(req))); + simcall_comm_wait__set__comm(&state->executed_req, &state->internal_comm); + simcall_comm_wait__set__comm(&state->internal_req, &state->internal_comm); + break; + + case SIMCALL_COMM_TEST: + state->internal_req = *req; + mc_model_checker->process().read_bytes(&state->internal_comm, + sizeof(state->internal_comm), remote(simcall_comm_test__get__comm(req))); + simcall_comm_test__set__comm(&state->executed_req, &state->internal_comm); + simcall_comm_test__set__comm(&state->internal_req, &state->internal_comm); + break; + + case SIMCALL_MC_RANDOM: { + state->internal_req = *req; + int random_max = simcall_mc_random__get__max(req); + if (*value != random_max) + for (auto& p : mc_model_checker->process().simix_processes()) { + simgrid::mc::ProcessState* procstate = &state->processStates[p.copy.pid]; + const smx_process_t issuer = MC_smx_simcall_get_issuer(req); + if (p.copy.pid == issuer->pid) { + procstate->state = simgrid::mc::ProcessInterleaveState::more_interleave; + break; + } + } + break; + } + + default: + state->internal_req = *req; + break; + } + + return req; } smx_simcall_t MC_state_get_request(simgrid::mc::State* state, int *value) diff --git a/src/mc/mc_state.h b/src/mc/mc_state.h index 5ddfcf9385..032a6e5b4d 100644 --- a/src/mc/mc_state.h +++ b/src/mc/mc_state.h @@ -88,7 +88,7 @@ struct ProcessState { * * The `executed_state` is sometimes transformed into another `internal_req`. * For example WAITANY is transformes into a WAIT and TESTANY into TEST. - * See `MC_state_set_executed_request()`. + * See `MC_state_get_request_for_process()`. */ struct XBT_PRIVATE State { @@ -143,7 +143,6 @@ XBT_PRIVATE void replay(std::list> const& st XBT_PRIVATE simgrid::mc::State* MC_state_new(void); XBT_PRIVATE void MC_state_interleave_process(simgrid::mc::State* state, smx_process_t process); -XBT_PRIVATE void MC_state_set_executed_request(simgrid::mc::State* state, smx_simcall_t req, int value); XBT_PRIVATE smx_simcall_t MC_state_get_executed_request(simgrid::mc::State* state, int *value); XBT_PRIVATE smx_simcall_t MC_state_get_internal_request(simgrid::mc::State* state); XBT_PRIVATE smx_simcall_t MC_state_get_request(simgrid::mc::State* state, int *value);