#include "src/mc/CommunicationDeterminismChecker.hpp"
#include "src/mc/mc_exit.h"
#include "src/mc/VisitedState.hpp"
+#include "src/mc/Transition.hpp"
using simgrid::mc::remote;
smx_simcall_t req = &state->executed_req;
if (req)
trace.push_back(simgrid::mc::request_to_string(
- req, state->req_num, simgrid::mc::RequestType::executed));
+ req, state->transition.argument, simgrid::mc::RequestType::executed));
}
return trace;
}
&& (req = MC_state_get_request(state)) != nullptr
&& (visited_state == nullptr)) {
- int req_num = state->req_num;
+ int req_num = state->transition.argument;
XBT_DEBUG("Execute: %s",
simgrid::mc::request_to_string(
call = MC_get_call_type(req);
/* Answer the request */
- simgrid::mc::handle_simcall(req, req_num); /* After this call req is no longer useful */
+ mc_model_checker->handle_simcall(state->transition);
+ /* After this call req is no longer useful */
if(!initial_global_state->initial_communications_pattern_done)
MC_handle_comm_pattern(call, req, req_num, initial_communications_pattern, 0);
#include "src/mc/mc_replay.h"
#include "src/mc/mc_safety.h"
#include "src/mc/mc_exit.h"
+#include "src/mc/Transition.hpp"
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
"Logging specific to algorithms for liveness properties verification");
if (pair->exploration_started) {
- int req_num = state->req_num;
+ int req_num = state->transition.argument;
smx_simcall_t saved_req = &state->executed_req;
smx_simcall_t req = nullptr;
state.get());
}
- simgrid::mc::handle_simcall(req, req_num);
+ mc_model_checker->handle_simcall(state->transition);
mc_model_checker->wait_for_requests();
}
{
std::vector<std::string> trace;
for (std::shared_ptr<Pair> const& pair : explorationStack_) {
- int req_num = pair->graph_state->req_num;
+ int req_num = pair->graph_state->transition.argument;
smx_simcall_t req = &pair->graph_state->executed_req;
if (req && req->call != SIMCALL_NONE)
trace.push_back(simgrid::mc::request_to_string(
}
smx_simcall_t req = MC_state_get_request(current_pair->graph_state.get());
- int req_num = current_pair->graph_state->req_num;
+ int req_num = current_pair->graph_state->transition.argument;
if (dot_output != nullptr) {
if (initial_global_state->prev_pair != 0 && initial_global_state->prev_pair != current_pair->num) {
mc_stats->visited_pairs++;
/* Answer the request */
- simgrid::mc::handle_simcall(req, req_num);
+ mc_model_checker->handle_simcall(current_pair->graph_state->transition);
/* Wait for requests (schedules processes) */
mc_model_checker->wait_for_requests();
#include "src/mc/mc_private.h"
#include "src/mc/mc_ignore.h"
#include "src/mc/mc_exit.h"
+#include "src/mc/Transition.hpp"
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_ModelChecker, mc, "ModelChecker");
return;
}
-void ModelChecker::simcall_handle(simgrid::mc::Process& process, unsigned long pid, int value)
+void ModelChecker::handle_simcall(Transition const& transition)
{
s_mc_simcall_handle_message m;
memset(&m, 0, sizeof(m));
m.type = MC_MESSAGE_SIMCALL_HANDLE;
- m.pid = pid;
- m.value = value;
- process.getChannel().send(m);
- process.clear_cache();
- while (process.running())
+ m.pid = transition.pid;
+ m.value = transition.argument;
+ this->process_->getChannel().send(m);
+ this->process_->clear_cache();
+ while (this->process_->running())
if (!this->handle_events())
return;
}
#include "src/mc/Process.hpp"
#include "src/mc/PageStore.hpp"
#include "src/mc/mc_protocol.h"
+#include "src/mc/Transition.hpp"
namespace simgrid {
namespace mc {
void loop();
bool handle_events();
void wait_client(simgrid::mc::Process& process);
- void simcall_handle(simgrid::mc::Process& process, unsigned long pid, int value);
+ void handle_simcall(Transition const& transition);
void wait_for_requests()
{
mc_model_checker->wait_client(mc_model_checker->process());
#include "src/mc/Checker.hpp"
#include "src/mc/SafetyChecker.hpp"
#include "src/mc/VisitedState.hpp"
+#include "src/mc/Transition.hpp"
#include "src/xbt/mmalloc/mmprivate.h"
{
std::vector<std::string> trace;
for (auto const& state : stack_) {
- int value = state->req_num;
+ int value = state->transition.argument;
smx_simcall_t req = &state->executed_req;
if (req)
trace.push_back(simgrid::mc::request_to_string(
continue;
}
- int req_num = state->req_num;
+ int req_num = state->transition.argument;
// If there are processes to interleave and the maximum depth has not been
// reached then perform one step of the exploration algorithm.
// MC_execute_transition(req, req_num)
/* Answer the request */
- simgrid::mc::handle_simcall(req, req_num);
+ mc_model_checker->handle_simcall(state->transition);
mc_model_checker->wait_for_requests();
/* Create the new expanded state */
&& simgrid::mc::request_depend(req, &prev_state->internal_req)) {
if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
XBT_DEBUG("Dependent Transitions:");
- int value = prev_state->req_num;
+ int value = prev_state->transition.argument;
smx_simcall_t prev_req = &prev_state->executed_req;
XBT_DEBUG("%s (state=%d)",
simgrid::mc::request_to_string(
prev_req, value, simgrid::mc::RequestType::internal).c_str(),
prev_state->num);
- value = state->req_num;
+ value = state->transition.argument;
prev_req = &state->executed_req;
XBT_DEBUG("%s (state=%d)",
simgrid::mc::request_to_string(
--- /dev/null
+/* Copyright (c) 2015-2016. The SimGrid Team.
+ * All rights reserved. */
+
+/* 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. */
+
+#ifndef SIMGRID_MC_TRANSITION_HPP
+#define SIMGRID_MC_TRANSITION_HPP
+
+namespace simgrid {
+namespace mc {
+
+/** An element in the recorded path
+ *
+ * At each decision point, we need to record which process transition
+ * is trigerred and potentially which value is associated with this
+ * transition. The value is used to find which communication is triggerred
+ * in things like waitany and for associating a given value of MC_random()
+ * calls.
+ */
+struct Transition {
+ int pid = 0;
+
+ /* Which transition was executed for this simcall
+ *
+ * Some simcalls can lead to different transitions:
+ *
+ * * waitany/testany can trigger on different messages;
+ *
+ * * random can produce different values.
+ */
+ int argument = 0;
+};
+
+}
+}
+
+#endif
#include "src/mc/mc_record.h"
#include "src/mc/mc_protocol.h"
#include "src/mc/Client.hpp"
+#include "src/mc/Transition.hpp"
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc, "Logging specific to MC (global)");
namespace simgrid {
namespace mc {
-void handle_simcall(smx_simcall_t req, int req_num)
-{
- for (auto& pi : mc_model_checker->process().smx_process_infos)
- if (req == &pi.copy.simcall) {
- mc_model_checker->simcall_handle(
- mc_model_checker->process(), pi.copy.pid, req_num);
- return;
- }
- xbt_die("Could not find the request");
-}
-
/**
* \brief Re-executes from the state at position start all the transitions indicated by
* a given model-checker stack.
if (state == stack.back())
break;
- int req_num = state->req_num;
+ int req_num = state->transition.argument;
smx_simcall_t saved_req = &state->executed_req;
if (saved_req) {
if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
call = MC_get_call_type(req);
- simgrid::mc::handle_simcall(req, req_num);
+ mc_model_checker->handle_simcall(state->transition);
if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
MC_handle_comm_pattern(call, req, req_num, nullptr, 1);
mc_model_checker->wait_for_requests();
#include "src/mc/mc_replay.h"
#include "src/mc/mc_record.h"
#include "src/mc/mc_base.h"
+#include "src/mc/Transition.hpp"
#if HAVE_MC
#include "src/mc/mc_request.h"
{
simgrid::mc::wait_for_requests();
- for (auto& item : trace) {
- XBT_DEBUG("Executing %i$%i", item.pid, item.value);
+ for (simgrid::mc::Transition const& transition : trace) {
+ XBT_DEBUG("Executing %i$%i", transition.pid, transition.argument);
// Choose a request:
- smx_process_t process = SIMIX_process_from_PID(item.pid);
+ smx_process_t process = SIMIX_process_from_PID(transition.pid);
if (!process)
xbt_die("Unexpected process.");
smx_simcall_t simcall = &(process->simcall);
xbt_die("Unexpected simcall.");
// Execute the request:
- SIMIX_simcall_handle(simcall, item.value);
+ SIMIX_simcall_handle(simcall, transition.argument);
simgrid::mc::wait_for_requests();
}
}
const char* current = data;
while (*current) {
- simgrid::mc::RecordTraceElement item;
- int count = sscanf(current, "%u/%u", &item.pid, &item.value);
+ simgrid::mc::Transition item;
+ int count = sscanf(current, "%u/%u", &item.pid, &item.argument);
if(count != 2 && count != 1)
throw std::runtime_error("Could not parse record path");
res.push_back(item);
if (i != trace.begin())
stream << ';';
stream << i->pid;
- if (i->value)
- stream << '/' << i->value;
+ if (i->argument)
+ stream << '/' << i->argument;
}
return stream.str();
}
#include <xbt/base.h>
+#include "src/mc/Transition.hpp"
+
namespace simgrid {
namespace mc {
-/** An element in the recorded path
- *
- * At each decision point, we need to record which process transition
- * is trigerred and potentially which value is associated with this
- * transition. The value is used to find which communication is triggerred
- * in things like waitany and for associating a given value of MC_random()
- * calls.
- */
-struct RecordTraceElement {
- int pid = 0;
- int value = 0;
- RecordTraceElement() {}
- RecordTraceElement(int pid, int value) : pid(pid), value(value) {}
-};
-
-typedef std::vector<RecordTraceElement> RecordTrace;
+typedef std::vector<Transition> RecordTrace;
-/** Convert a string representation of the path into a array of `simgrid::mc::RecordTraceElement`
+/** Convert a string representation of the path into a array of `simgrid::mc::Transition`
*/
XBT_PRIVATE RecordTrace parseRecordTrace(const char* data);
XBT_PRIVATE std::string traceToString(simgrid::mc::RecordTrace const& trace);
#include "src/mc/mc_comm_pattern.h"
#include "src/mc/mc_smx.h"
#include "src/mc/mc_xbt.hpp"
+#include "src/mc/Transition.hpp"
using simgrid::mc::remote;
[](simgrid::mc::ProcessState const& state) { return state.isToInterleave(); });
}
-RecordTraceElement State::getRecordElement() const
+Transition State::getRecordElement() const
{
- smx_process_t issuer = MC_smx_simcall_get_issuer(&this->executed_req);
- return RecordTraceElement(issuer->pid, this->req_num);
+ return this->transition;
}
}
simgrid::mc::State* state, smx_process_t process)
{
simgrid::mc::ProcessState* procstate = &state->processStates[process->pid];
+ state->transition.pid = -1;
+ state->transition.argument = -1;
if (!procstate->isToInterleave())
return nullptr;
smx_simcall_t req = nullptr;
switch (process->simcall.call) {
case SIMCALL_COMM_WAITANY:
- state->req_num = -1;
+ state->transition.argument = -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++)) {
- state->req_num = procstate->interleave_count - 1;
+ state->transition.argument = procstate->interleave_count - 1;
break;
}
}
simgrid::mc::read_length(mc_model_checker->process(),
simgrid::mc::remote(simcall_comm_waitany__get__comms(&process->simcall))))
procstate->setDone();
- if (state->req_num != -1)
+ if (state->transition.argument != -1)
req = &process->simcall;
break;
case SIMCALL_COMM_TESTANY: {
unsigned start_count = procstate->interleave_count;
- state->req_num = -1;
+ state->transition.argument = -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++)) {
- state->req_num = procstate->interleave_count - 1;
+ state->transition.argument = procstate->interleave_count - 1;
break;
}
remote(simcall_comm_testany__get__comms(&process->simcall))))
procstate->setDone();
- if (state->req_num != -1 || start_count == 0)
+ if (state->transition.argument != -1 || start_count == 0)
req = &process->simcall;
break;
mc_model_checker->process().read_bytes(
&act, sizeof(act), remote(remote_act));
if (act.comm.src_proc && act.comm.dst_proc)
- state->req_num = 0;
+ state->transition.argument = 0;
else if (act.comm.src_proc == nullptr && act.comm.type == SIMIX_COMM_READY
&& act.comm.detached == 1)
- state->req_num = 0;
+ state->transition.argument = 0;
else
- state->req_num = -1;
+ state->transition.argument = -1;
procstate->setDone();
req = &process->simcall;
break;
case SIMCALL_MC_RANDOM: {
int min_value = simcall_mc_random__get__min(&process->simcall);
- state->req_num = procstate->interleave_count + min_value;
+ state->transition.argument = procstate->interleave_count + min_value;
procstate->interleave_count++;
- if (state->req_num == simcall_mc_random__get__max(&process->simcall))
+ if (state->transition.argument == simcall_mc_random__get__max(&process->simcall))
procstate->setDone();
req = &process->simcall;
break;
default:
procstate->setDone();
- state->req_num = 0;
+ state->transition.argument = 0;
req = &process->simcall;
break;
}
// Fetch the data of the request and translate it:
+ state->transition.pid = process->pid;
+
state->executed_req = *req;
/* The waitany and testany request are transformed into a wait or test request
smx_synchro_t remote_comm;
read_element(mc_model_checker->process(),
&remote_comm, remote(simcall_comm_waitany__get__comms(req)),
- state->req_num, sizeof(remote_comm));
+ state->transition.argument, 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);
state->internal_req.call = SIMCALL_COMM_TEST;
state->internal_req.issuer = req->issuer;
- if (state->req_num > 0) {
+ if (state->transition.argument > 0) {
smx_synchro_t remote_comm;
read_element(mc_model_checker->process(),
&remote_comm, remote(simcall_comm_testany__get__comms(req)),
- state->req_num, sizeof(remote_comm));
+ state->transition.argument, 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, state->req_num);
+ simcall_comm_test__set__result(&state->internal_req, state->transition.argument);
break;
case SIMCALL_COMM_WAIT:
#include "src/simix/smx_private.h"
#include "src/mc/mc_snapshot.h"
#include "src/mc/mc_record.h"
+#include "src/mc/Transition.hpp"
namespace simgrid {
namespace mc {
/** Sequential state number (used for debugging) */
int num = 0;
- /* Which transition was executed for this simcall
- *
- * Some simcalls can lead to different transitions:
- *
- * * waitany/testany can trigger on different messages;
- *
- * * random can produce different values.
- */
- int req_num = 0;
-
/** State's exploration status by process */
std::vector<ProcessState> processStates;
+ Transition transition;
+
/** The simcall which was executed */
s_smx_simcall_t executed_req;
{
this->processStates[process->pid].interleave();
}
- RecordTraceElement getRecordElement() const;
+ Transition getRecordElement() const;
};
XBT_PRIVATE void replay(std::list<std::unique_ptr<simgrid::mc::State>> const& stack);
src/mc/mc_xbt.hpp
src/mc/mc_xbt.cpp
src/mc/mc_exit.h
+ src/mc/Transition.hpp
)
set(MC_SIMGRID_MC_SRC
