From 58d95ccaa27bb984b83885dc0bd37d945d946944 Mon Sep 17 00:00:00 2001 From: Gabriel Corona Date: Fri, 25 Mar 2016 10:55:04 +0100 Subject: [PATCH] [mc] Let the Checker give us the current record trace This could probably be infered from the interaction with the Session at some point in the future but we're not there yet. --- src/mc/Checker.cpp | 17 +++ src/mc/Checker.hpp | 12 +- src/mc/CommunicationDeterminismChecker.cpp | 21 +++ src/mc/CommunicationDeterminismChecker.hpp | 1 + src/mc/LivenessChecker.cpp | 23 +++- src/mc/LivenessChecker.hpp | 1 + src/mc/ModelChecker.hpp | 4 + src/mc/SafetyChecker.cpp | 20 +++ src/mc/SafetyChecker.hpp | 1 + src/mc/Session.hpp | 2 +- src/mc/mc_global.cpp | 4 +- src/mc/mc_record.cpp | 142 ++++++--------------- src/mc/mc_record.h | 69 +++++----- src/simgrid/sg_config.c | 1 - src/simix/smx_global.cpp | 2 +- 15 files changed, 177 insertions(+), 143 deletions(-) diff --git a/src/mc/Checker.cpp b/src/mc/Checker.cpp index cfa6563f3c..89065a1c40 100644 --- a/src/mc/Checker.cpp +++ b/src/mc/Checker.cpp @@ -4,14 +4,31 @@ /* 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. */ +#include + +#include + #include "src/mc/Checker.hpp" +#include "src/mc/ModelChecker.hpp" namespace simgrid { namespace mc { +Checker::Checker(Session& session) : session_(&session) +{ + xbt_assert(mc_model_checker); + xbt_assert(mc_model_checker->getChecker() == nullptr); + mc_model_checker->setChecker(this); +} + Checker::~Checker() { } +RecordTrace Checker::getRecordTrace() +{ + return {}; +} + } } diff --git a/src/mc/Checker.hpp b/src/mc/Checker.hpp index cf3e37af66..db9c2aeb48 100644 --- a/src/mc/Checker.hpp +++ b/src/mc/Checker.hpp @@ -9,8 +9,10 @@ #include #include +#include #include "src/mc/mc_forward.hpp" +#include "src/mc/mc_record.h" namespace simgrid { namespace mc { @@ -28,7 +30,7 @@ namespace mc { class Checker { Session* session_; public: - Checker(Session& session) : session_(&session) {} + Checker(Session& session); // No copy: Checker(Checker const&) = delete; @@ -37,6 +39,14 @@ public: virtual ~Checker(); virtual int run() = 0; + // Give me your internal state: + + /** Show the current trace/stack + * + * Could this be handled in the Session/ModelChecker instead? + */ + virtual RecordTrace getRecordTrace(); + protected: Session& getSession() { return *session_; } }; diff --git a/src/mc/CommunicationDeterminismChecker.cpp b/src/mc/CommunicationDeterminismChecker.cpp index 5262982bce..968d60aff9 100644 --- a/src/mc/CommunicationDeterminismChecker.cpp +++ b/src/mc/CommunicationDeterminismChecker.cpp @@ -309,6 +309,27 @@ CommunicationDeterminismChecker::~CommunicationDeterminismChecker() } +// TODO, deduplicate with SafetyChecker +RecordTrace CommunicationDeterminismChecker::getRecordTrace() // override +{ + RecordTrace res; + + xbt_fifo_item_t start = xbt_fifo_get_last_item(mc_stack); + for (xbt_fifo_item_t item = start; item; item = xbt_fifo_get_prev_item(item)) { + + // Find (pid, value): + mc_state_t state = (mc_state_t) xbt_fifo_get_item_content(item); + int value = 0; + smx_simcall_t saved_req = MC_state_get_executed_request(state, &value); + const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req); + const int pid = issuer->pid; + + res.push_back(RecordTraceElement(pid, value)); + } + + return std::move(res); +} + void CommunicationDeterminismChecker::prepare() { mc_state_t initial_state = nullptr; diff --git a/src/mc/CommunicationDeterminismChecker.hpp b/src/mc/CommunicationDeterminismChecker.hpp index d23c95c42f..062348da67 100644 --- a/src/mc/CommunicationDeterminismChecker.hpp +++ b/src/mc/CommunicationDeterminismChecker.hpp @@ -18,6 +18,7 @@ public: CommunicationDeterminismChecker(Session& session); ~CommunicationDeterminismChecker(); int run() override; + RecordTrace getRecordTrace() override; private: void prepare(); int main(); diff --git a/src/mc/LivenessChecker.cpp b/src/mc/LivenessChecker.cpp index c1dcd91da0..6a0a1c7597 100644 --- a/src/mc/LivenessChecker.cpp +++ b/src/mc/LivenessChecker.cpp @@ -426,13 +426,34 @@ LivenessChecker::~LivenessChecker() { } +RecordTrace LivenessChecker::getRecordTrace() // override +{ + RecordTrace res; + + xbt_fifo_item_t start = xbt_fifo_get_last_item(mc_stack); + for (xbt_fifo_item_t item = start; item; item = xbt_fifo_get_prev_item(item)) { + simgrid::mc::Pair* pair = (simgrid::mc::Pair*) xbt_fifo_get_item_content(item); + int value; + smx_simcall_t req = MC_state_get_executed_request(pair->graph_state, &value); + if (req && req->call != SIMCALL_NONE) { + smx_process_t issuer = MC_smx_simcall_get_issuer(req); + const int pid = issuer->pid; + + // Serialization the (pid, value) pair: + res.push_back(RecordTraceElement(pid, value)); + } + } + + return std::move(res); +} + void LivenessChecker::showAcceptanceCycle(std::size_t depth) { XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); XBT_INFO("| ACCEPTANCE CYCLE |"); XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); XBT_INFO("Counter-example that violates formula :"); - MC_record_dump_path(mc_stack); + simgrid::mc::dumpRecordPath(); this->showStack(mc_stack); this->dumpStack(mc_stack); MC_print_statistics(mc_stats); diff --git a/src/mc/LivenessChecker.hpp b/src/mc/LivenessChecker.hpp index 918c855ded..2811f93056 100644 --- a/src/mc/LivenessChecker.hpp +++ b/src/mc/LivenessChecker.hpp @@ -66,6 +66,7 @@ public: LivenessChecker(Session& session); ~LivenessChecker(); int run() override; + RecordTrace getRecordTrace() override; private: int main(); void prepare(); diff --git a/src/mc/ModelChecker.hpp b/src/mc/ModelChecker.hpp index 9bde129c7d..a53e99a86a 100644 --- a/src/mc/ModelChecker.hpp +++ b/src/mc/ModelChecker.hpp @@ -35,6 +35,7 @@ class ModelChecker { // This is the parent snapshot of the current state: PageStore page_store_; std::unique_ptr process_; + Checker* checker_ = nullptr; public: simgrid::mc::Snapshot* parent_snapshot_; @@ -74,6 +75,9 @@ public: bool checkDeadlock(); + Checker* getChecker() const { return checker_; } + void setChecker(Checker* checker) { checker_ = checker; } + private: void setup_ignore(); bool handle_message(char* buffer, ssize_t size); diff --git a/src/mc/SafetyChecker.cpp b/src/mc/SafetyChecker.cpp index e1b87d3076..c8caba1cdf 100644 --- a/src/mc/SafetyChecker.cpp +++ b/src/mc/SafetyChecker.cpp @@ -66,6 +66,26 @@ static int is_exploration_stack_state(mc_state_t current_state){ return 0; } +RecordTrace SafetyChecker::getRecordTrace() // override +{ + RecordTrace res; + + xbt_fifo_item_t start = xbt_fifo_get_last_item(mc_stack); + for (xbt_fifo_item_t item = start; item; item = xbt_fifo_get_prev_item(item)) { + + // Find (pid, value): + mc_state_t state = (mc_state_t) xbt_fifo_get_item_content(item); + int value = 0; + smx_simcall_t saved_req = MC_state_get_executed_request(state, &value); + const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req); + const int pid = issuer->pid; + + res.push_back(RecordTraceElement(pid, value)); + } + + return std::move(res); +} + int SafetyChecker::run() { this->init(); diff --git a/src/mc/SafetyChecker.hpp b/src/mc/SafetyChecker.hpp index d7fe099f5d..084ce89135 100644 --- a/src/mc/SafetyChecker.hpp +++ b/src/mc/SafetyChecker.hpp @@ -19,6 +19,7 @@ public: SafetyChecker(Session& session); ~SafetyChecker(); int run() override; + RecordTrace getRecordTrace() override; private: // Temp void init(); diff --git a/src/mc/Session.hpp b/src/mc/Session.hpp index f53d94816f..9b7d857c13 100644 --- a/src/mc/Session.hpp +++ b/src/mc/Session.hpp @@ -38,7 +38,7 @@ class Session { private: std::unique_ptr modelChecker_; -private: // +private: Session(pid_t pid, int socket); // No copy: diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp index 93defaf036..9f8e1a1fd8 100644 --- a/src/mc/mc_global.cpp +++ b/src/mc/mc_global.cpp @@ -354,7 +354,7 @@ void MC_report_assertion_error(void) XBT_INFO("*** PROPERTY NOT VALID ***"); XBT_INFO("**************************"); XBT_INFO("Counter-example execution trace:"); - MC_record_dump_path(mc_stack); + simgrid::mc::dumpRecordPath(); MC_dump_stack_safety(mc_stack); MC_print_statistics(mc_stats); } @@ -373,7 +373,7 @@ void MC_report_crash(int status) else XBT_INFO("No core dump was generated by the system."); XBT_INFO("Counter-example execution trace:"); - MC_record_dump_path(mc_stack); + simgrid::mc::dumpRecordPath(); MC_dump_stack_safety(mc_stack); MC_print_statistics(mc_stats); } diff --git a/src/mc/mc_record.cpp b/src/mc/mc_record.cpp index 32702eb70c..49f111f258 100644 --- a/src/mc/mc_record.cpp +++ b/src/mc/mc_record.cpp @@ -8,6 +8,10 @@ #include #include +#include +#include +#include + #include #include #include @@ -33,25 +37,21 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_record, mc, " Logging specific to MC record/replay facility"); extern "C" { - char* MC_record_path = nullptr; +} + +namespace simgrid { +namespace mc { -void MC_record_replay(mc_record_item_t start, std::size_t len) +void replay(RecordTrace const& trace) { simgrid::mc::wait_for_requests(); - mc_record_item_t end = start + len; - // Choose the recorded simcall and execute it: - for (mc_record_item_t item=start;item!=end; ++item) { - - XBT_DEBUG("Executing %i$%i", item->pid, item->value); -/* - if (xbt_dynar_is_empty(simix_global->process_to_run)) - xbt_die("Unexpected end of application."); -*/ + for (auto& item : trace) { + XBT_DEBUG("Executing %i$%i", item.pid, item.value); // Choose a request: - smx_process_t process = SIMIX_process_from_PID(item->pid); + smx_process_t process = SIMIX_process_from_PID(item.pid); if (!process) xbt_die("Unexpected process."); smx_simcall_t simcall = &(process->simcall); @@ -62,27 +62,34 @@ void MC_record_replay(mc_record_item_t start, std::size_t len) xbt_die("Unexpected simcall."); // Execute the request: - SIMIX_simcall_handle(simcall, item->value); + SIMIX_simcall_handle(simcall, item.value); simgrid::mc::wait_for_requests(); } } -xbt_dynar_t MC_record_from_string(const char* data) +void replay(const char* path_string) { + simgrid::mc::processes_time.resize(simix_process_maxpid); + simgrid::mc::RecordTrace trace = simgrid::mc::parseRecordTrace(path_string); + simgrid::mc::replay(trace); + simgrid::mc::processes_time.clear(); +} + +RecordTrace parseRecordTrace(const char* data) +{ + RecordTrace res; XBT_INFO("path=%s", data); if (!data || !data[0]) - return nullptr; - - xbt_dynar_t dynar = xbt_dynar_new(sizeof(s_mc_record_item_t), nullptr); + throw std::runtime_error("Could not parse record path"); const char* current = data; while (*current) { - s_mc_record_item_t item = { 0, 0 }; + simgrid::mc::RecordTraceElement item; int count = sscanf(current, "%u/%u", &item.pid, &item.value); if(count != 2 && count != 1) - goto fail; - xbt_dynar_push(dynar, &item); + throw std::runtime_error("Could not parse record path"); + res.push_back(item); // Find next chunk: const char* end = std::strchr(current, ';'); @@ -92,100 +99,33 @@ xbt_dynar_t MC_record_from_string(const char* data) current = end + 1; } - return dynar; - -fail: - xbt_dynar_free(&dynar); - return nullptr; + return std::move(res); } #if HAVE_MC -static char* MC_record_stack_to_string_liveness(xbt_fifo_t stack) -{ - char* buffer; - std::size_t size; - std::FILE* file = open_memstream(&buffer, &size); - - xbt_fifo_item_t item; - xbt_fifo_item_t start = xbt_fifo_get_last_item(stack); - for (item = start; item; item = xbt_fifo_get_prev_item(item)) { - simgrid::mc::Pair* pair = (simgrid::mc::Pair*) xbt_fifo_get_item_content(item); - int value; - smx_simcall_t req = MC_state_get_executed_request(pair->graph_state, &value); - if (req && req->call != SIMCALL_NONE) { - smx_process_t issuer = MC_smx_simcall_get_issuer(req); - const int pid = issuer->pid; - - // Serialization the (pid, value) pair: - const char* sep = (item!=start) ? ";" : ""; - if (value) - std::fprintf(file, "%s%u/%u", sep, pid, value); - else - std::fprintf(file, "%s%u", sep, pid); - } - } - - std::fclose(file); - return buffer; -} -char* MC_record_stack_to_string(xbt_fifo_t stack) +std::string traceToString(simgrid::mc::RecordTrace const& trace) { - if (_sg_mc_liveness) - return MC_record_stack_to_string_liveness(stack); - - xbt_fifo_item_t start = xbt_fifo_get_last_item(stack); - - if (!start) { - char* res = (char*) malloc(1 * sizeof(char)); - res[0] = '\0'; - return res; + std::ostringstream stream; + for (auto i = trace.begin(); i != trace.end(); ++i) { + if (i != trace.begin()) + stream << ';'; + stream << i->pid; + if (i->value) + stream << '/' << i->value; } - - char* buffer; - std::size_t size; - std::FILE* file = open_memstream(&buffer, &size); - - xbt_fifo_item_t item; - for (item = start; item; item = xbt_fifo_get_prev_item(item)) { - - // Find (pid, value): - mc_state_t state = (mc_state_t) xbt_fifo_get_item_content(item); - int value = 0; - smx_simcall_t saved_req = MC_state_get_executed_request(state, &value); - const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req); - const int pid = issuer->pid; - - // Serialization the (pid, value) pair: - const char* sep = (item!=start) ? ";" : ""; - if (value) - std::fprintf(file, "%s%u/%u", sep, pid, value); - else - std::fprintf(file, "%s%u", sep, pid); - } - - std::fclose(file); - return buffer; + return stream.str(); } -void MC_record_dump_path(xbt_fifo_t stack) +void dumpRecordPath() { if (MC_record_is_active()) { - char* path = MC_record_stack_to_string(stack); - XBT_INFO("Path = %s", path); - std::free(path); + RecordTrace trace = mc_model_checker->getChecker()->getRecordTrace(); + XBT_INFO("Path = %s", traceToString(trace).c_str()); } } + #endif -void MC_record_replay_from_string(const char* path_string) -{ - simgrid::mc::processes_time.resize(simix_process_maxpid); - xbt_dynar_t path = MC_record_from_string(path_string); - mc_record_item_t start = &xbt_dynar_get_as(path, 0, s_mc_record_item_t); - MC_record_replay(start, xbt_dynar_length(path)); - xbt_dynar_free(&path); - simgrid::mc::processes_time.clear(); } - } diff --git a/src/mc/mc_record.h b/src/mc/mc_record.h index 88911c00c7..2c55598a85 100644 --- a/src/mc/mc_record.h +++ b/src/mc/mc_record.h @@ -17,20 +17,15 @@ #ifndef SIMGRID_MC_RECORD_H #define SIMGRID_MC_RECORD_H +#include +#include + #include #include #include -SG_BEGIN_DECL() - -/** Whether the MC record mode is enabled - * - * The behaviour is not changed. The only real difference is that - * the path is writtent in the log when an interesting path is found. - */ -#define MC_record_is_active() _sg_do_model_check_record - -// **** Data conversion +namespace simgrid { +namespace mc { /** An element in the recorded path * @@ -40,14 +35,37 @@ SG_BEGIN_DECL() * in things like waitany and for associating a given value of MC_random() * calls. */ -typedef struct s_mc_record_item { - int pid; - int value; -} s_mc_record_item_t, *mc_record_item_t; +struct RecordTraceElement { + int pid = 0; + int value = 0; + RecordTraceElement() {} + RecordTraceElement(int pid, int value) : pid(pid), value(value) {} +}; + +typedef std::vector RecordTrace; + +/** Convert a string representation of the path into a array of `simgrid::mc::RecordTraceElement` + */ +XBT_PRIVATE RecordTrace parseRecordTrace(const char* data); +XBT_PRIVATE std::string traceToString(simgrid::mc::RecordTrace const& trace); +XBT_PRIVATE void dumpRecordPath(); + +XBT_PRIVATE void replay(RecordTrace const& trace); +XBT_PRIVATE void replay(const char* trace); + +} +} + +SG_BEGIN_DECL() -/** Convert a string representation of the path into a array of `s_mc_record_item_t` +/** Whether the MC record mode is enabled + * + * The behaviour is not changed. The only real difference is that + * the path is writtent in the log when an interesting path is found. */ -XBT_PRIVATE xbt_dynar_t MC_record_from_string(const char* data); +#define MC_record_is_active() _sg_do_model_check_record + +// **** Data conversion /** Generate a string representation * @@ -57,25 +75,6 @@ XBT_PRIVATE xbt_dynar_t MC_record_from_string(const char* data); */ XBT_PRIVATE char* MC_record_stack_to_string(xbt_fifo_t stack); -/** Dump the path represented by a given stack in the log - */ -XBT_PRIVATE void MC_record_dump_path(xbt_fifo_t stack); - -// ***** Replay - -/** Replay a path represented by the record items - * - * \param start Array of record item - * \item count Number of record items - */ -XBT_PRIVATE void MC_record_replay(mc_record_item_t start, size_t count); - -/** Replay a path represented by a string - * - * \param data String representation of the path - */ -XBT_PRIVATE void MC_record_replay_from_string(const char* data); - SG_END_DECL() #endif diff --git a/src/simgrid/sg_config.c b/src/simgrid/sg_config.c index 054272ae94..62cb97dd81 100644 --- a/src/simgrid/sg_config.c +++ b/src/simgrid/sg_config.c @@ -23,7 +23,6 @@ #include "smpi/smpi_interface.h" #endif #include "mc/mc.h" -#include "src/mc/mc_record.h" #include "simgrid/instr.h" #include "src/mc/mc_replay.h" diff --git a/src/simix/smx_global.cpp b/src/simix/smx_global.cpp index f783f8be9d..d84905a738 100644 --- a/src/simix/smx_global.cpp +++ b/src/simix/smx_global.cpp @@ -381,7 +381,7 @@ static int process_syscall_color(void *p) void SIMIX_run(void) { if (MC_record_path) { - MC_record_replay_from_string(MC_record_path); + simgrid::mc::replay(MC_record_path); return; } -- 2.20.1