From: Gabriel Corona Date: Thu, 7 Apr 2016 10:39:18 +0000 (+0200) Subject: [mc] Get rid of the ugly "value" out parameter in MC_state_get_request() X-Git-Tag: v3_13~132 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/67592b097ee1e3d2bc4c1e79d8401732d8d6f869?hp=9e8ba3861df85d86342342252be58cd546df2d08 [mc] Get rid of the ugly "value" out parameter in MC_state_get_request() --- diff --git a/src/mc/CommunicationDeterminismChecker.cpp b/src/mc/CommunicationDeterminismChecker.cpp index 174b7e0693..86b26cc83a 100644 --- a/src/mc/CommunicationDeterminismChecker.cpp +++ b/src/mc/CommunicationDeterminismChecker.cpp @@ -315,11 +315,10 @@ std::vector CommunicationDeterminismChecker::getTextualTrace() // o { std::vector trace; for (auto const& state : stack_) { - int value = state->req_num; smx_simcall_t req = &state->executed_req; if (req) trace.push_back(simgrid::mc::request_to_string( - req, value, simgrid::mc::RequestType::executed)); + req, state->req_num, simgrid::mc::RequestType::executed)); } return trace; } @@ -376,7 +375,6 @@ bool all_communications_are_finished() int CommunicationDeterminismChecker::main(void) { - int value; std::unique_ptr visited_state = nullptr; smx_simcall_t req = nullptr; @@ -394,16 +392,18 @@ int CommunicationDeterminismChecker::main(void) mc_stats->visited_states++; if (stack_.size() <= (std::size_t) _sg_mc_max_depth - && (req = MC_state_get_request(state, &value)) + && (req = MC_state_get_request(state)) != nullptr && (visited_state == nullptr)) { + int req_num = state->req_num; + XBT_DEBUG("Execute: %s", simgrid::mc::request_to_string( - req, value, simgrid::mc::RequestType::simix).c_str()); + req, req_num, simgrid::mc::RequestType::simix).c_str()); std::string req_str; if (dot_output != nullptr) - req_str = simgrid::mc::request_get_dot_output(req, value); + req_str = simgrid::mc::request_get_dot_output(req, req_num); mc_stats->executed_transitions++; @@ -413,12 +413,12 @@ int CommunicationDeterminismChecker::main(void) call = MC_get_call_type(req); /* Answer the request */ - simgrid::mc::handle_simcall(req, value); /* After this call req is no longer useful */ + simgrid::mc::handle_simcall(req, req_num); /* After this call req is no longer useful */ if(!initial_global_state->initial_communications_pattern_done) - MC_handle_comm_pattern(call, req, value, initial_communications_pattern, 0); + MC_handle_comm_pattern(call, req, req_num, initial_communications_pattern, 0); else - MC_handle_comm_pattern(call, req, value, nullptr, 0); + MC_handle_comm_pattern(call, req, req_num, nullptr, 0); /* Wait for requests (schedules processes) */ mc_model_checker->wait_for_requests(); diff --git a/src/mc/LivenessChecker.cpp b/src/mc/LivenessChecker.cpp index 80cffd37e5..61cf565b16 100644 --- a/src/mc/LivenessChecker.cpp +++ b/src/mc/LivenessChecker.cpp @@ -370,8 +370,8 @@ int LivenessChecker::main(void) continue; } - int value; - smx_simcall_t req = MC_state_get_request(current_pair->graph_state.get(), &value); + smx_simcall_t req = MC_state_get_request(current_pair->graph_state.get()); + int req_num = current_pair->graph_state->req_num; if (dot_output != nullptr) { if (initial_global_state->prev_pair != 0 && initial_global_state->prev_pair != current_pair->num) { @@ -381,7 +381,7 @@ int LivenessChecker::main(void) initial_global_state->prev_req.clear(); } initial_global_state->prev_pair = current_pair->num; - initial_global_state->prev_req = simgrid::mc::request_get_dot_output(req, value); + initial_global_state->prev_req = simgrid::mc::request_get_dot_output(req, req_num); if (current_pair->search_cycle) fprintf(dot_output, "%d [shape=doublecircle];\n", current_pair->num); fflush(dot_output); @@ -389,7 +389,7 @@ int LivenessChecker::main(void) XBT_DEBUG("Execute: %s", simgrid::mc::request_to_string( - req, value, simgrid::mc::RequestType::simix).c_str()); + req, req_num, simgrid::mc::RequestType::simix).c_str()); /* Update mc_stats */ mc_stats->executed_transitions++; @@ -397,7 +397,7 @@ int LivenessChecker::main(void) mc_stats->visited_pairs++; /* Answer the request */ - simgrid::mc::handle_simcall(req, value); + simgrid::mc::handle_simcall(req, req_num); /* Wait for requests (schedules processes) */ mc_model_checker->wait_for_requests(); diff --git a/src/mc/SafetyChecker.cpp b/src/mc/SafetyChecker.cpp index 664379d2fd..8055c65b60 100644 --- a/src/mc/SafetyChecker.cpp +++ b/src/mc/SafetyChecker.cpp @@ -89,8 +89,6 @@ int SafetyChecker::run() { this->init(); - int value; - while (!stack_.empty()) { /* Get current state */ @@ -108,7 +106,7 @@ int SafetyChecker::run() // let's back-track. smx_simcall_t req = nullptr; if (stack_.size() > (std::size_t) _sg_mc_max_depth - || (req = MC_state_get_request(state, &value)) == nullptr + || (req = MC_state_get_request(state)) == nullptr || visitedState_ != nullptr) { int res = this->backtrack(); if (res) @@ -117,23 +115,25 @@ int SafetyChecker::run() continue; } + int req_num = state->req_num; + // If there are processes to interleave and the maximum depth has not been // reached then perform one step of the exploration algorithm. XBT_DEBUG("Execute: %s", simgrid::mc::request_to_string( - req, value, simgrid::mc::RequestType::simix).c_str()); + req, req_num, simgrid::mc::RequestType::simix).c_str()); std::string req_str; if (dot_output != nullptr) - req_str = simgrid::mc::request_get_dot_output(req, value); + req_str = simgrid::mc::request_get_dot_output(req, req_num); mc_stats->executed_transitions++; // TODO, bundle both operations in a single message - // MC_execute_transition(req, value) + // MC_execute_transition(req, req_num) /* Answer the request */ - simgrid::mc::handle_simcall(req, value); + simgrid::mc::handle_simcall(req, req_num); mc_model_checker->wait_for_requests(); /* Create the new expanded state */ diff --git a/src/mc/mc_state.cpp b/src/mc/mc_state.cpp index 1a4b90a6ef..a6f51d354b 100644 --- a/src/mc/mc_state.cpp +++ b/src/mc/mc_state.cpp @@ -69,7 +69,7 @@ RecordTraceElement State::getRecordElement() const } static inline smx_simcall_t MC_state_get_request_for_process( - simgrid::mc::State* state, int*value, smx_process_t process) + simgrid::mc::State* state, smx_process_t process) { simgrid::mc::ProcessState* procstate = &state->processStates[process->pid]; @@ -81,13 +81,13 @@ static inline smx_simcall_t MC_state_get_request_for_process( smx_simcall_t req = nullptr; switch (process->simcall.call) { case SIMCALL_COMM_WAITANY: - *value = -1; + state->req_num = -1; while (procstate->interleave_count < read_length(mc_model_checker->process(), remote(simcall_comm_waitany__get__comms(&process->simcall)))) { if (simgrid::mc::request_is_enabled_by_idx(&process->simcall, procstate->interleave_count++)) { - *value = procstate->interleave_count - 1; + state->req_num = procstate->interleave_count - 1; break; } } @@ -96,19 +96,19 @@ 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->setDone(); - if (*value != -1) + if (state->req_num != -1) req = &process->simcall; break; case SIMCALL_COMM_TESTANY: { unsigned start_count = procstate->interleave_count; - *value = -1; + state->req_num = -1; while (procstate->interleave_count < read_length(mc_model_checker->process(), remote(simcall_comm_testany__get__comms(&process->simcall)))) if (simgrid::mc::request_is_enabled_by_idx(&process->simcall, procstate->interleave_count++)) { - *value = procstate->interleave_count - 1; + state->req_num = procstate->interleave_count - 1; break; } @@ -117,7 +117,7 @@ static inline smx_simcall_t MC_state_get_request_for_process( remote(simcall_comm_testany__get__comms(&process->simcall)))) procstate->setDone(); - if (*value != -1 || start_count == 0) + if (state->req_num != -1 || start_count == 0) req = &process->simcall; break; @@ -129,12 +129,12 @@ static inline smx_simcall_t MC_state_get_request_for_process( mc_model_checker->process().read_bytes( &act, sizeof(act), remote(remote_act)); if (act.comm.src_proc && act.comm.dst_proc) - *value = 0; + state->req_num = 0; else if (act.comm.src_proc == nullptr && act.comm.type == SIMIX_COMM_READY && act.comm.detached == 1) - *value = 0; + state->req_num = 0; else - *value = -1; + state->req_num = -1; procstate->setDone(); req = &process->simcall; break; @@ -142,9 +142,9 @@ static inline smx_simcall_t MC_state_get_request_for_process( case SIMCALL_MC_RANDOM: { int min_value = simcall_mc_random__get__min(&process->simcall); - *value = procstate->interleave_count + min_value; + state->req_num = procstate->interleave_count + min_value; procstate->interleave_count++; - if (*value == simcall_mc_random__get__max(&process->simcall)) + if (state->req_num == simcall_mc_random__get__max(&process->simcall)) procstate->setDone(); req = &process->simcall; break; @@ -152,7 +152,7 @@ static inline smx_simcall_t MC_state_get_request_for_process( default: procstate->setDone(); - *value = 0; + state->req_num = 0; req = &process->simcall; break; } @@ -162,7 +162,6 @@ static inline smx_simcall_t MC_state_get_request_for_process( // 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 @@ -174,7 +173,7 @@ static inline smx_simcall_t MC_state_get_request_for_process( smx_synchro_t remote_comm; read_element(mc_model_checker->process(), &remote_comm, remote(simcall_comm_waitany__get__comms(req)), - *value, sizeof(remote_comm)); + state->req_num, 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); @@ -185,16 +184,16 @@ static inline smx_simcall_t MC_state_get_request_for_process( state->internal_req.call = SIMCALL_COMM_TEST; state->internal_req.issuer = req->issuer; - if (*value > 0) { + if (state->req_num > 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)); + state->req_num, 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); + simcall_comm_test__set__result(&state->internal_req, state->req_num); break; case SIMCALL_COMM_WAIT: @@ -221,10 +220,10 @@ static inline smx_simcall_t MC_state_get_request_for_process( return req; } -smx_simcall_t MC_state_get_request(simgrid::mc::State* state, int *value) +smx_simcall_t MC_state_get_request(simgrid::mc::State* state) { for (auto& p : mc_model_checker->process().simix_processes()) { - smx_simcall_t res = MC_state_get_request_for_process(state, value, &p.copy); + smx_simcall_t res = MC_state_get_request_for_process(state, &p.copy); if (res) return res; } diff --git a/src/mc/mc_state.h b/src/mc/mc_state.h index 957a08004b..9681d03630 100644 --- a/src/mc/mc_state.h +++ b/src/mc/mc_state.h @@ -166,6 +166,6 @@ XBT_PRIVATE void replay(std::list> const& st } XBT_PRIVATE simgrid::mc::State* MC_state_new(void); -XBT_PRIVATE smx_simcall_t MC_state_get_request(simgrid::mc::State* state, int *value); +XBT_PRIVATE smx_simcall_t MC_state_get_request(simgrid::mc::State* state); #endif