diff --git a/CMakeLists.txt b/CMakeLists.txt index c2fa5fc..3df3929 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -14,11 +14,16 @@ set(CMAKE_CXX_STANDARD_REQUIRED TRUE) # Project configuration option(BUILD_TESTS OFF) option(VERBOSE_TESTING OFF) +option(MCMINI_USE_SCIP OFF) set(MCMINI_DIR "${CMAKE_SOURCE_DIR}") set(MCMINI_INCLUDE_DIR "${CMAKE_SOURCE_DIR}/include") set(MCMINI_CMAKE_MODULE_DIR "${CMAKE_SOURCE_DIR}/cmake") set(MCMINI_WITH_DMTCP OFF) +if(MCMINI_USE_SCIP) +find_package(scip) +endif() + # Project source files set(MCMINI_C_SRC src/common/exit.c @@ -49,6 +54,7 @@ set(MCMINI_CPP_SRC src/mcmini/model/transitions/process.cpp src/mcmini/model/transitions/thread.cpp src/mcmini/model/transitions/semaphore.cpp + src/mcmini/model_checking/reporter.cpp src/mcmini/model_checking/algorithms/classic_dpor.cpp src/mcmini/model_checking/algorithms/clock_vector.cpp src/mcmini/real_world/dmtcp_process_source.cpp @@ -117,6 +123,10 @@ target_compile_options(mcmini target_link_libraries(mcmini PUBLIC "${MCMINI_EXTRA_LINK_FLAGS}") +if (MCMINI_USE_SCIP) +target_link_libraries(mcmini PUBLIC scip) +target_compile_definitions(mcmini PUBLIC MCMINI_USE_SCIP) +endif() add_subdirectory(src/examples) add_subdirectory(test) diff --git a/include/mcmini/misc/ddt.hpp b/include/mcmini/misc/ddt.hpp index f8db347..e7500bb 100644 --- a/include/mcmini/misc/ddt.hpp +++ b/include/mcmini/misc/ddt.hpp @@ -155,20 +155,21 @@ struct double_dispatch_member_function_table 0) { if (internal_table.at(t1_type).count(t2_type) > 0) { - const auto& pair = internal_table.at(t1_type).at(t2_type); + const auto &pair = internal_table.at(t1_type).at(t2_type); return pair.first(t1, t2, pair.second, std::forward(args)...); } - } else if (interface_member_function_table.count(t1_type) > 0) { - const auto& pair = interface_member_function_table.at(t1_type); + } + if (interface_member_function_table.count(t1_type) > 0) { + const auto &pair = interface_member_function_table.at(t1_type); return pair.first(t1, t2, pair.second, std::forward(args)...); } else if (interface_member_function_table.count(t2_type) > 0) { - const auto& pair = interface_member_function_table.at(t2_type); + const auto &pair = interface_member_function_table.at(t2_type); // NOTE: t2 should come before t1 here since // `casting_function_interface_table` always casts its first argument return pair.first(t2, t1, pair.second, std::forward(args)...); @@ -176,12 +177,12 @@ struct double_dispatch_member_function_table 0) { if (internal_table.at(t1_type).count(t2_type) > 0) { - const auto& pair = internal_table.at(t1_type).at(t2_type); + const auto &pair = internal_table.at(t1_type).at(t2_type); return pair.first(t1, t2, pair.second, std::forward(args)...); } } diff --git a/include/mcmini/model/config.hpp b/include/mcmini/model/config.hpp index f492590..f581776 100644 --- a/include/mcmini/model/config.hpp +++ b/include/mcmini/model/config.hpp @@ -13,21 +13,94 @@ namespace model { struct config { /** * The maximum number of transitions that can be run - * by any single thread while running the model checker + * by any _single thread_ while running the model checker */ uint64_t max_thread_execution_depth; + /** + * The maximum number of transitions that can be contained in any given trace. + */ + uint64_t maximum_total_execution_depth = 1500; + /** * The trace id to stop the model checker at * to print the contents of the transition stack */ trid_t target_trace_id; + /** + * Whether or not exploration occurs using round robin scheduling (default is + * smallest tid first) + */ + bool use_round_robin_scheduling = false; + /** * Whether model checking should halt at the first encountered deadlock */ bool stop_at_first_deadlock = false; + /** + * Whether relinearization should occur before displying buggy traces. + * + * A relinearization `T'` of a trace `T` is a permutation `sigma_n` such that + * `happens_before_T(i, j) <--> happens_before_T'(sigma(i), sigma(j))`. + * Informally, it is a reordering of the transitions in the trace that + * produces the same final state (and hence the same bugs, crashes, etc). + * + * The interest in relinearization is that although round-robin exploration in + * theory should enable McMini to capture shallower bugs more readily, the + * tradeoff is less readable traces when they're produced because the user + * will frequently have to switch between different threads to analyze the + * trace. Frequent switching makes it challenging to have a global idea of the + * issue causing a bug, even for small traces. + * + * With this enabled, McMini will first reorder the transitions using a greedy + * approach as follows: + * + * 1. When given the choice, McMini will first choose transitions of the same + * thread ID as the thread ID of the last chosen transition. + * 2. When McMini is forced by the happens-before relation to order a + * transition of a different thread ID, among the possible choices it chooses + * the smallest. + */ + bool relinearize_traces = false; + + /** + * Whether or not traces are relinearized optimally. Implies + * `relinearize_traces`. + * + * By default, relinearizations are created using a greedy algorithm by + * grouping together, as long as possible, transitions of the same thread ID + * subject to the happens-before relation over them. However, a + * relinearization produced using the greedy method is not guaranteed to + * minimize the number of "context switches" a user has to make. That is, + * there may exist a better linearization obeying the same happens-before + * relation but with a fewer number of changes between thread IDs. + * + * The optimization problem can be formulated as follows: + * + * Consider a colored DAG, G, with vertices V and edges E and a coloring + * function f: V —> C (where C is a finite set of colors). A linearization L + * of the vertices of G is a sequence of vertices v_I such + * that the order of v_I obeys the dag: a node ‘u’ appears before any node + * with which a directed edge from that node to any other node (formally u < v + * in L iff (u,v) in E). + * + * A colored linearization is the sequence of colors c_1, c_2, … of a + * linearization v_1, v_2, …, where c_i = f(v_i). Let h: L —> N + * denote the number of “inversions” in a linearization L. + * A linearization L has an inversion (v_i, v_i+1) iff f(v_i) != f(v_i+1). Let + * Inv: L -> Nat denote the number of inversions in a linearization L. Then + * MinInversions is the problem + * + * min (Inv L) where L is a linearization of G. + * + * The problem can be modeled as an instance of the Sequential Ordering + * Problem. Since in general this problem is challenging to solve, linearizing + * large traces may become impractical. + */ + bool use_optimal_linearization = false; + /** * Informs McMini that the target executable should be run under DMTCP with * `libmcmini.so` configured in record mode. @@ -41,6 +114,17 @@ struct config { */ bool use_multithreaded_fork = false; + /** + * Whether to print every trace, or one those that cause a bug + */ + bool verbose = false; + + /** + * Whether the STDOUT/STDERR of the program is sent to /dev/null during + * execution + */ + bool quiet_program_output = false; + /** * The time between consecutive checkpoint images when `libmcmini.so` is * running in record mode. @@ -63,4 +147,4 @@ struct config { // file path is provided (TODO). logging::severity_level global_severity_level = logging::severity_level::info; }; -} // namespace model +} // namespace model diff --git a/include/mcmini/model/pending_transitions.hpp b/include/mcmini/model/pending_transitions.hpp index 668db87..ec65268 100644 --- a/include/mcmini/model/pending_transitions.hpp +++ b/include/mcmini/model/pending_transitions.hpp @@ -43,6 +43,7 @@ struct pending_transitions final { } auto cend() -> decltype(_contents.cend()) const { return _contents.cend(); } size_t size() const { return this->_contents.size(); } + bool empty() const { return this->_contents.empty(); } /** * @brief Returns the transition mapped to id `id`, or `nullptr` if no such * runner has been mapped to an id. diff --git a/include/mcmini/model/transitions/thread/thread_exit.hpp b/include/mcmini/model/transitions/thread/thread_exit.hpp index 7509ff2..daf8576 100644 --- a/include/mcmini/model/transitions/thread/thread_exit.hpp +++ b/include/mcmini/model/transitions/thread/thread_exit.hpp @@ -8,22 +8,23 @@ namespace model { namespace transitions { struct thread_exit : public model::transition { - public: +public: thread_exit(state::runner_id_t executor) : transition(executor) {} ~thread_exit() = default; - status modify(model::mutable_state& s) const override { + status modify(model::mutable_state &s) const override { using namespace model::objects; - auto* thread_state = s.get_state_of_runner(executor); - if (!thread_state->is_running() || executor == RID_MAIN_THREAD) { + auto *thread_state = s.get_state_of_runner(executor); + if (!thread_state->is_running()) { return status::disabled; } s.add_state_for_runner(executor, new thread(thread::exited)); return status::exists; } + bool depends(const model::transition *t) const { return false; } std::string to_string() const override { return "exits"; } }; -} // namespace transitions -} // namespace model +} // namespace transitions +} // namespace model diff --git a/include/mcmini/model/transitions/thread/thread_start.hpp b/include/mcmini/model/transitions/thread/thread_start.hpp index db9821e..ed4f1fa 100644 --- a/include/mcmini/model/transitions/thread/thread_start.hpp +++ b/include/mcmini/model/transitions/thread/thread_start.hpp @@ -7,19 +7,20 @@ namespace model { namespace transitions { struct thread_start : public model::transition { - public: +public: thread_start(state::runner_id_t executor) : transition(executor) {} ~thread_start() = default; - status modify(model::mutable_state& s) const override { + status modify(model::mutable_state &s) const override { // No modification necessary: we simply move into the next state using namespace model::objects; - auto* thread_state = s.get_state_of_runner(executor); + auto *thread_state = s.get_state_of_runner(executor); return thread_state->is_embryo() ? status::disabled : status::exists; } + bool depends(const model::transition *t) const { return false; } std::string to_string() const override { return "starts"; } }; -} // namespace transitions -} // namespace model +} // namespace transitions +} // namespace model diff --git a/include/mcmini/model_checking/algorithm.hpp b/include/mcmini/model_checking/algorithm.hpp index 5fce879..df5bc65 100644 --- a/include/mcmini/model_checking/algorithm.hpp +++ b/include/mcmini/model_checking/algorithm.hpp @@ -1,7 +1,5 @@ #pragma once -#include - #include "mcmini/coordinator/coordinator.hpp" #include "mcmini/model/exception.hpp" #include "mcmini/model/program.hpp" @@ -15,24 +13,37 @@ namespace model_checking { * the correctness of a program modeled under McMini. */ class algorithm { - public: +public: + enum class exploration_policy : uint { round_robin, smallest_first }; + + struct context { + virtual const model::program &get_model() const = 0; + virtual std::vector + linearize_lowest_first() const = 0; + virtual std::vector + linearize_optimal() const = 0; + std::vector linearize_trace(bool optimal) const { + return optimal ? linearize_optimal() : linearize_lowest_first(); + } + }; + struct callbacks { - public: - callbacks() = default; - std::function crash; - std::function deadlock; - std::function data_race; - std::function unknown_error; - std::function trace_completed; - std::function - abnormal_termination; - std::function - nonzero_exit_code; - std::function - undefined_behavior; + virtual void crash(const context &, const stats &) const {} + virtual void deadlock(const context &, const stats &) const {} + virtual void data_race(const context &, const stats &) const {} + virtual void trace_completed(const context &, const stats &) const {} + + virtual void + abnormal_termination(const context &, const stats &, + const real_world::process::termination_error &) const { + } + virtual void nonzero_exit_code( + const context &, const stats &, + const real_world::process::nonzero_exit_code_error &) const {} + + virtual void + undefined_behavior(const context &, const stats &, + const model::undefined_behavior_exception &) const {} }; /** @@ -72,4 +83,4 @@ class algorithm { } }; -}; // namespace model_checking +}; // namespace model_checking diff --git a/include/mcmini/model_checking/algorithms/classic_dpor.hpp b/include/mcmini/model_checking/algorithms/classic_dpor.hpp index 931e001..7eba8e7 100644 --- a/include/mcmini/model_checking/algorithms/classic_dpor.hpp +++ b/include/mcmini/model_checking/algorithms/classic_dpor.hpp @@ -12,7 +12,7 @@ namespace model_checking { * algorithm of Flanagan and Godefroid (2005). */ class classic_dpor final : public algorithm { - public: +public: using dependency_relation_type = double_dispatch_member_function_table; @@ -29,20 +29,33 @@ class classic_dpor final : public algorithm { static dependency_relation_type default_dependencies(); static coenabled_relation_type default_coenabledness(); - struct configuration { + struct config { + public: + config() = default; + config(const model::config &c) + : maximum_total_execution_depth(c.maximum_total_execution_depth), + stop_at_first_deadlock(c.stop_at_first_deadlock), + policy(c.use_round_robin_scheduling + ? exploration_policy::round_robin + : exploration_policy::smallest_first) {} + + public: dependency_relation_type dependency_relation = classic_dpor::default_dependencies(); coenabled_relation_type coenabled_relation = classic_dpor::default_coenabledness(); uint32_t maximum_total_execution_depth = 1500; + bool stop_at_first_deadlock = false; bool assumes_linear_program_flow = false; + exploration_policy policy = exploration_policy::smallest_first; }; classic_dpor() = default; - classic_dpor(configuration config) : config(std::move(config)) {} + classic_dpor(config config) : config(std::move(config)) {} + classic_dpor(const model::config &config) : config(config) {} - private: - configuration config; +private: + config config; bool are_dependent(const model::transition &t1, const model::transition &t2) const; @@ -59,13 +72,6 @@ class classic_dpor final : public algorithm { // the DPOR algorithm and are called at specific points in time! struct dpor_context; - - bool happens_before(const dpor_context &, size_t i, size_t j) const; - bool happens_before_thread(const dpor_context &, size_t i, - runner_id_t p) const; - bool threads_race_after(const dpor_context &context, size_t i, runner_id_t q, - runner_id_t p) const; - clock_vector accumulate_max_clock_vector_against(const model::transition &, const dpor_context &) const; @@ -79,4 +85,4 @@ class classic_dpor final : public algorithm { runner_id_t p); }; -} // namespace model_checking +} // namespace model_checking diff --git a/include/mcmini/model_checking/algorithms/classic_dpor/stack_item.hpp b/include/mcmini/model_checking/algorithms/classic_dpor/stack_item.hpp index 8e41fb5..ec3e3d0 100644 --- a/include/mcmini/model_checking/algorithms/classic_dpor/stack_item.hpp +++ b/include/mcmini/model_checking/algorithms/classic_dpor/stack_item.hpp @@ -219,9 +219,9 @@ struct stack_item final { return backtrack_thread; } - clock_vector get_clock_vector() const { return this->cv; } - const std::array - &get_per_runner_clocks() const { + const clock_vector &get_clock_vector() const { return this->cv; } + const std::array & + get_per_runner_clocks() const { return this->per_runner_clocks; } runner_id_t get_first_enabled_runner() const { @@ -231,6 +231,9 @@ struct stack_item final { } return r; } + const bool is_enabled(runner_id_t rid) { + return this->enabled_runners.count(rid) > 0; + } const std::unordered_set &get_enabled_runners() const { return this->enabled_runners; } diff --git a/include/mcmini/model_checking/reporter.hpp b/include/mcmini/model_checking/reporter.hpp new file mode 100644 index 0000000..954d850 --- /dev/null +++ b/include/mcmini/model_checking/reporter.hpp @@ -0,0 +1,40 @@ +#pragma once +#include "mcmini/model/config.hpp" +#include "mcmini/model/exception.hpp" +#include "mcmini/model_checking/algorithm.hpp" + +namespace model_checking { +class reporter : public algorithm::callbacks { +private: + const bool verbose; + const bool relinearize_traces; + const bool use_optimal_linearization; + +private: + void dump_relinearized_trace(std::ostream &, const algorithm::context &, + const stats &) const; + +public: + reporter() = default; + reporter(const model::config &c) + : verbose(c.verbose), + relinearize_traces(c.relinearize_traces || c.use_optimal_linearization), + use_optimal_linearization(c.use_optimal_linearization) {} + +public: + // void crash(const algorithm::context &, const stats &) const override; + void deadlock(const algorithm::context &, const stats &) const override; + // void data_race(const algorithm::context &, const stats &) const override; + void trace_completed(const algorithm::context &, + const stats &) const override; + void abnormal_termination( + const algorithm::context &, const stats &, + const real_world::process::termination_error &) const override; + // void nonzero_exit_code( + // const algorithm::context &, const stats &, + // const real_world::process::nonzero_exit_code_error &) const override; + void undefined_behavior( + const algorithm::context &, const stats &, + const model::undefined_behavior_exception &) const override; +}; +} // namespace model_checking \ No newline at end of file diff --git a/src/lib/template/loop.c b/src/lib/template/loop.c index c37dd55..b574322 100644 --- a/src/lib/template/loop.c +++ b/src/lib/template/loop.c @@ -75,7 +75,6 @@ int rt_sigqueueinfo(pid_t tgid, int sig, siginfo_t *info) { void mc_template_receive_sigchld(int sig, siginfo_t *info, void *) { assert(global_model_checker_pid != NO_DEFINED_MCMINI_PID); - printf("signalling!!\n"); fsync(STDOUT_FILENO); int status; bool signal_mcmini = false; @@ -92,12 +91,11 @@ void mc_template_receive_sigchld(int sig, siginfo_t *info, void *) { } else if (WIFSIGNALED(status)) { int signo = WTERMSIG(status); - printf("signaled %d", status); + // printf("signaled %d", status); fsync(STDOUT_FILENO); signal_mcmini = is_bad_signal(signo); } if (signal_mcmini) { - printf("signalling McMini!!\n"); fsync(STDOUT_FILENO); // TODO: We can use `sigqueue(3)` to pass the exit status of // the child to the McMini process diff --git a/src/mcmini/mcmini.cpp b/src/mcmini/mcmini.cpp index 025c28e..27371e2 100644 --- a/src/mcmini/mcmini.cpp +++ b/src/mcmini/mcmini.cpp @@ -11,6 +11,7 @@ #include "mcmini/model/transitions/thread/thread_exit.hpp" #include "mcmini/model_checking/algorithm.hpp" #include "mcmini/model_checking/algorithms/classic_dpor.hpp" +#include "mcmini/model_checking/reporter.hpp" #include "mcmini/real_world/fifo.hpp" #include "mcmini/real_world/process/dmtcp_process_source.hpp" #include "mcmini/real_world/process/multithreaded_fork_process_source.hpp" @@ -43,164 +44,89 @@ using namespace model_checking; using namespace objects; using namespace real_world; -visible_object_state* translate_recorded_object_to_model( - const ::visible_object& recorded_object, +logging::logger setup_logger("mcmini"); + +visible_object_state *translate_recorded_object_to_model( + const ::visible_object &recorded_object, const std::unordered_map< - void*, std::vector>> + void *, std::vector>> cv_waiting_threads) { // TODO: A function table would be slightly better, but this works perfectly // fine too. switch (recorded_object.type) { - case MUTEX: { - auto mutex_state = - static_cast(recorded_object.mut_state); - pthread_mutex_t* mutex_location = - (pthread_mutex_t*)recorded_object.location; - return new objects::mutex(mutex_state, mutex_location); - } - case CONDITION_VARIABLE: { - // Create the condition variable model object with full state information - auto cv_state = static_cast( - recorded_object.cond_state.status); - - runner_id_t interacting_thread = - recorded_object.cond_state.interacting_thread; - pthread_mutex_t* associated_mutex = - recorded_object.cond_state.associated_mutex; - int count = recorded_object.cond_state.count; - // get waiting threads from the map - auto it = cv_waiting_threads.find(recorded_object.location); - std::vector> - waiters_with_state = - (it != cv_waiting_threads.end()) - ? it->second - : std::vector< - std::pair>(); - return new objects::condition_variable(cv_state, interacting_thread, - associated_mutex, count, - waiters_with_state); - } - case SEMAPHORE: { - return new objects::semaphore(static_cast( - recorded_object.sem_state.status), - recorded_object.sem_state.count); - } - // Other objects here - // case ... { } - // ... - default: { - std::cerr << "The new object type" << recorded_object.type - << "hasn't been implemented yet\n"; - std::abort(); - } + case MUTEX: { + auto mutex_state = + static_cast(recorded_object.mut_state); + pthread_mutex_t *mutex_location = + (pthread_mutex_t *)recorded_object.location; + return new objects::mutex(mutex_state, mutex_location); } -} - -runner_state* translate_recorded_runner_to_model( - const ::visible_object& recorded_object) { - switch (recorded_object.type) { - case THREAD: { - return new objects::thread(recorded_object.thrd_state.status); - } - default: { - std::abort(); - } + case CONDITION_VARIABLE: { + // Create the condition variable model object with full state information + auto cv_state = static_cast( + recorded_object.cond_state.status); + + runner_id_t interacting_thread = + recorded_object.cond_state.interacting_thread; + pthread_mutex_t *associated_mutex = + recorded_object.cond_state.associated_mutex; + int count = recorded_object.cond_state.count; + // get waiting threads from the map + auto it = cv_waiting_threads.find(recorded_object.location); + std::vector> + waiters_with_state = + (it != cv_waiting_threads.end()) + ? it->second + : std::vector< + std::pair>(); + return new objects::condition_variable(cv_state, interacting_thread, + associated_mutex, count, + waiters_with_state); } -} - -void finished_trace_classic_dpor(const coordinator& c, const stats& stats) { - std::stringstream ss; - const auto& program_model = c.get_current_program_model(); - ss << "TRACE " << stats.trace_id << "\n"; - for (const auto& t : program_model.get_trace()) { - ss << "thread " << t->get_executor() << ": " << t->to_string() << "\n"; - } - ss << "\nNEXT THREAD OPERATIONS\n"; - for (const auto& tpair : program_model.get_pending_transitions()) { - ss << "thread " << tpair.first << ": " << tpair.second->to_string() << "\n"; + case SEMAPHORE: { + return new objects::semaphore(static_cast( + recorded_object.sem_state.status), + recorded_object.sem_state.count); } - std::cout << ss.str(); - std::cout.flush(); -} - -void found_undefined_behavior(const coordinator& c, const stats& stats, - const undefined_behavior_exception& ub) { - std::cerr << "UNDEFINED BEHAVIOR:\n" << ub.what() << std::endl; - finished_trace_classic_dpor(c, stats); -} - -void found_abnormal_termination( - const coordinator& c, const stats& stats, - const real_world::process::termination_error& ub) { - std::cerr << "Abnormally Termination (signo: " << ub.signo - << ", signal: " << sig_to_str.at(ub.signo) << "):\n" - << ub.what() << std::endl; - - std::stringstream ss; - const auto& program_model = c.get_current_program_model(); - ss << "TRACE " << stats.trace_id << "\n"; - for (const auto& t : program_model.get_trace()) { - ss << "thread " << t->get_executor() << ": " << t->to_string() << "\n"; + // Other objects here + // case ... { } + // ... + default: { + std::cerr << "The new object type" << recorded_object.type + << "hasn't been implemented yet\n"; + std::abort(); } - const transition* terminator = - program_model.get_pending_transition_for(ub.culprit); - ss << "thread " << terminator->get_executor() << ": " - << terminator->to_string() << "\n"; - - ss << "\nNEXT THREAD OPERATIONS\n"; - for (const auto& tpair : program_model.get_pending_transitions()) { - if (tpair.first == terminator->get_executor()) { - ss << "thread " << tpair.first << ": executing" - << "\n"; - } else { - ss << "thread " << tpair.first << ": " << tpair.second->to_string() - << "\n"; - } } - ss << stats.total_transitions + 1 << " total transitions executed" - << "\n"; - std::cout << ss.str(); - std::cout.flush(); } -void found_deadlock(const coordinator& c, const stats& stats) { - std::cerr << "DEADLOCK" << std::endl; - std::stringstream ss; - const auto& program_model = c.get_current_program_model(); - for (const auto& t : program_model.get_trace()) { - ss << "thread " << t->get_executor() << ": " << t->to_string() << "\n"; +runner_state * +translate_recorded_runner_to_model(const ::visible_object &recorded_object) { + switch (recorded_object.type) { + case THREAD: { + return new objects::thread(recorded_object.thrd_state.status); + } + default: { + std::abort(); } - ss << "\nNEXT THREAD OPERATIONS\n"; - for (const auto& tpair : program_model.get_pending_transitions()) { - ss << "thread " << tpair.first << ": " << tpair.second->to_string() << "\n"; } - std::cout << ss.str(); - std::cout.flush(); } -void do_model_checking(const config& config) { +void do_model_checking(const config &config) { algorithm::callbacks c; target target_program(config.target_executable, config.target_executable_args); + target_program.set_quiet(config.quiet_program_output); coordinator coordinator(program::starting_from_main(), transition_registry::default_registry(), make_unique(target_program)); - std::cerr << "\n\n**************** INTIAL STATE *********************\n\n"; - coordinator.get_current_program_model().dump_state(std::cerr); - std::cerr << "\n\n**************** INTIAL STATE *********************\n\n"; - std::cerr.flush(); - - model_checking::classic_dpor classic_dpor_checker; - c.trace_completed = &finished_trace_classic_dpor; - c.deadlock = &found_deadlock; - c.undefined_behavior = &found_undefined_behavior; - c.abnormal_termination = &found_abnormal_termination; - classic_dpor_checker.verify_using(coordinator, c); + model_checking::reporter reporter(config); + model_checking::classic_dpor classic_dpor_checker(config); + classic_dpor_checker.verify_using(coordinator, reporter); std::cout << "Model checking completed!" << std::endl; } -void do_model_checking_from_dmtcp_ckpt_file(const config& config) { - volatile mcmini_shm_file* rw_region = +void do_model_checking_from_dmtcp_ckpt_file(const config &config) { + volatile mcmini_shm_file *rw_region = xpc_resources::get_instance().get_rw_region()->as(); std::unique_ptr dmtcp_template_handle; @@ -217,7 +143,6 @@ void do_model_checking_from_dmtcp_ckpt_file(const config& config) { // Make sure that `dmtcp_restart` has executed and that the template // process is ready for execution; otherwise, the state restoration will not // work as expected. - algorithm::callbacks c; transition_registry tr = transition_registry::default_registry(); coordinator coordinator(program(), tr, std::move(dmtcp_template_handle)); { @@ -314,18 +239,15 @@ void do_model_checking_from_dmtcp_ckpt_file(const config& config) { std::cerr << "\n\n**************** INTIAL STATE *********************\n\n"; std::cerr.flush(); - model_checking::classic_dpor classic_dpor_checker; - c.trace_completed = &finished_trace_classic_dpor; - c.undefined_behavior = &found_undefined_behavior; - c.deadlock = &found_deadlock; - c.abnormal_termination = &found_abnormal_termination; - classic_dpor_checker.verify_using(coordinator, c); + model_checking::reporter reporter(config); + model_checking::classic_dpor classic_dpor_checker(config); + classic_dpor_checker.verify_using(coordinator, reporter); std::cerr << "Deep debugging completed!" << std::endl; } #include "mcmini/log/logger.hpp" -void do_recording(const config& config) { +void do_recording(const config &config) { char dir[PATH_MAX]; // FIXME: This depends on mcmini starting in root dir of git repo. std::string libmcini_dir = getcwd(dir, sizeof(dir)) ? dir : "PATH_TOO_LONG"; @@ -397,18 +319,41 @@ int main_cpp(int argc, const char** argv) { mcmini_config.max_thread_execution_depth = strtoul(cur_arg[1], nullptr, 10); - char* endptr; + char *endptr; if (strtol(cur_arg[1], &endptr, 10) == 0 || endptr[0] != '\0') { fprintf(stderr, "%s: illegal value\n", "--max-depth-per-thread"); exit(1); } cur_arg += 2; + } else if (strcmp(cur_arg[0], "--max-depth-per-trace") == 0 || + strcmp(cur_arg[0], "-M") == 0) { + mcmini_config.maximum_total_execution_depth = + strtoul(cur_arg[1], nullptr, 10); + + char *endptr; + if (strtol(cur_arg[1], &endptr, 10) == 0 || endptr[0] != '\0') { + fprintf(stderr, "%s: illegal value\n", "--max-depth-per-trace"); + exit(1); + } + cur_arg += 2; } else if (strcmp(cur_arg[0], "--interval") == 0 || strcmp(cur_arg[0], "-i") == 0) { mcmini_config.record_target_executable_only = true; mcmini_config.checkpoint_period = std::chrono::seconds(strtoul(cur_arg[1], nullptr, 10)); cur_arg += 2; + } else if ((strcmp(cur_arg[0], "--round-robin") == 0) || + strcmp(cur_arg[0], "-rr") == 0) { + mcmini_config.use_round_robin_scheduling = true; + cur_arg += 1; + } else if ((strcmp(cur_arg[0], "--optimal-relinearization") == 0) || + strcmp(cur_arg[0], "-orelin") == 0) { + mcmini_config.use_optimal_linearization = true; + cur_arg += 1; + } else if ((strcmp(cur_arg[0], "--relinearize") == 0) || + strcmp(cur_arg[0], "-relin") == 0) { + mcmini_config.relinearize_traces = true; + cur_arg += 1; } else if (strcmp(cur_arg[0], "--from-checkpoint") == 0 || strcmp(cur_arg[0], "-ckpt") == 0) { mcmini_config.checkpoint_file = cur_arg[1]; @@ -424,6 +369,14 @@ int main_cpp(int argc, const char** argv) { strcmp(cur_arg[0], "-mtf") == 0) { mcmini_config.use_multithreaded_fork = true; cur_arg++; + } else if (strcmp(cur_arg[0], "--verbose") == 0 || + strcmp(cur_arg[0], "-v") == 0) { + mcmini_config.verbose = true; + cur_arg++; + } else if (strcmp(cur_arg[0], "--quiet-program-output") == 0 || + strcmp(cur_arg[0], "-q") == 0) { + mcmini_config.quiet_program_output = true; + cur_arg++; } else if (cur_arg[0][1] == 'm' && isdigit(cur_arg[0][2])) { mcmini_config.max_thread_execution_depth = strtoul(cur_arg[1], nullptr, 10); @@ -453,8 +406,12 @@ int main_cpp(int argc, const char** argv) { " [--record|-r ] \n" " [--from-checkpoint ] [--multithreaded-fork] \n" " [--max-depth-per-thread|-m ]\n" + " [--max-depth-per-trace|-M ]\n" " [--first-deadlock|--first|-f]\n" + " [--round-robin|-rr]\n" " [--log-level|-log ]\n" + " [--verbose|-v]\n" + " [--quiet-program-output|-q]\n" " [--help|-h]\n" " target_executable\n"); exit(1); @@ -503,10 +460,10 @@ int main_cpp(int argc, const char** argv) { return EXIT_SUCCESS; } -int main(int argc, const char** argv) { +int main(int argc, const char **argv) { try { return main_cpp(argc, argv); - } catch (const std::exception& e) { + } catch (const std::exception &e) { std::cerr << "ERROR: " << e.what() << std::endl; return EXIT_FAILURE; } catch (...) { diff --git a/src/mcmini/model/program.cpp b/src/mcmini/model/program.cpp index f29563c..cab2e5b 100644 --- a/src/mcmini/model/program.cpp +++ b/src/mcmini/model/program.cpp @@ -107,8 +107,8 @@ void program::model_execution_of(runner_id_t p, const transition *npo) { trace.push(next_steps.replace_unowned(npo)); } -state::objid_t program::discover_object( - const visible_object_state *initial_state) { +state::objid_t +program::discover_object(const visible_object_state *initial_state) { return this->state_seq.add_object(initial_state); } @@ -134,7 +134,8 @@ bool program::is_in_deadlock() const { // If any transition is enabled, we are not in deadlock for (const auto &pair : this->get_pending_transitions()) { - if (pair.second->is_enabled_in(this->state_seq)) return false; + if (pair.second->is_enabled_in(this->state_seq)) + return false; } // Furthermore, if there are NO enabled transitions, we need to check if this @@ -151,12 +152,10 @@ bool program::is_in_deadlock() const { // probably still want to show a bug if other userspace threads manage to get // into a deadlock even while the main thread could exit, so we don't treat // that case specially. - bool all_exited = true; - for (const auto &pair : this->get_pending_transitions()) { + for (const auto &pair : this->get_pending_transitions()) if (!this->state_seq.get_state_of_runner(pair.first)->has_exited()) - all_exited = false; - } - return !all_exited; + return true; // All blocked and at least one hasn't exited + return false; } std::ostream &program::dump_state(std::ostream &os) const { diff --git a/src/mcmini/model_checking/algorithms/classic_dpor.cpp b/src/mcmini/model_checking/algorithms/classic_dpor.cpp index 2504f21..58ca691 100644 --- a/src/mcmini/model_checking/algorithms/classic_dpor.cpp +++ b/src/mcmini/model_checking/algorithms/classic_dpor.cpp @@ -1,21 +1,27 @@ -#include "mcmini/model_checking/algorithms/classic_dpor.hpp" - -#include - +#include #include #include #include #include #include +#include #include #include #include +#include #include #include +#ifdef MCMINI_USE_SCIP +#include "scip/scip.h" +#include "scip/scipdefplugins.h" +#include +#endif + #include "mcmini/coordinator/coordinator.hpp" #include "mcmini/defines.h" #include "mcmini/log/logger.hpp" +#include "mcmini/model/config.hpp" #include "mcmini/model/exception.hpp" #include "mcmini/model/program.hpp" #include "mcmini/model/transition.hpp" @@ -24,6 +30,7 @@ #include "mcmini/model/transitions/mutex/mutex_init.hpp" #include "mcmini/model/transitions/semaphore/callbacks.hpp" #include "mcmini/model/transitions/thread/callbacks.hpp" +#include "mcmini/model_checking/algorithms/classic_dpor.hpp" #include "mcmini/model_checking/algorithms/classic_dpor/clock_vector.hpp" #include "mcmini/model_checking/algorithms/classic_dpor/runner_item.hpp" #include "mcmini/model_checking/algorithms/classic_dpor/stack_item.hpp" @@ -35,15 +42,67 @@ using namespace model_checking; logger dpor_logger("dpor"); -struct classic_dpor::dpor_context { +struct classic_dpor::dpor_context : public algorithm::context { +public: ::coordinator &coordinator; std::vector stack; dpor_context(::coordinator &c) : coordinator(c) {} +public: + const size_t state_stack_size() const { return stack.size(); } + const size_t transition_stack_size() const { + const size_t ss = state_stack_size(); + return ss > 0 ? (ss - 1) : 0; + } + const transition *get_transition(int i) const { return stack.at(i).get_out_transition(); } + + const transition *get_transition(size_t i) const { + return stack.at(i).get_out_transition(); + } + + const runner_id_t tid(size_t i) const { + return get_transition(i)->get_executor(); + } + + const clock_vector &clock(size_t j) const { + // C(j) in the DPOR paper + // NOTE: The clock vector for the `i`th transition is stored in the state + // into which the transition points, NOT the state from which the transition + // starts (hence the j + 1) + return stack.at(j + 1).get_clock_vector(); + } + + bool happens_before(size_t i, size_t j) const { + const runner_id_t procSi = get_transition(i)->get_executor(); + return i <= clock(j).value_for(procSi); + } + + bool happens_before_thread(size_t i, runner_id_t p) const { + const runner_id_t rid = get_transition(i)->get_executor(); + const clock_vector &cv = + stack.back().get_per_runner_clocks()[p].get_clock_vector(); + return i <= cv.value_for(rid); + } + + bool threads_race_after(size_t i, runner_id_t q, runner_id_t p) const { + const size_t transition_stack_height = stack.size() - 1; + for (size_t j = i + 1; j < transition_stack_height; j++) { + if (q == get_transition(j)->get_executor() && + this->happens_before_thread(j, p)) + return true; + } + return false; + } + std::vector> transitive_reduction() const; + std::vector linearize_lowest_first() const; + std::vector linearize_optimal() const; + const program &get_model() const { + return this->coordinator.get_current_program_model(); + } }; clock_vector classic_dpor::accumulate_max_clock_vector_against( @@ -53,11 +112,10 @@ clock_vector classic_dpor::accumulate_max_clock_vector_against( // (case-sensitive) in the paper, viz. the transition between states `s_i` and // `s_{i+1}`. clock_vector result; - for (const stack_item &s_i : context.stack) { - if (s_i.get_out_transition() != nullptr && - this->are_dependent(*s_i.get_out_transition(), t)) { - result = clock_vector::max(result, s_i.get_clock_vector()); - } + for (size_t i = 0; i < context.transition_stack_size(); i++) { + const model::transition *S_i = context.get_transition(i); + if (this->are_dependent(*S_i, t)) + result = clock_vector::max(result, context.clock(i)); } return result; } @@ -74,37 +132,10 @@ bool classic_dpor::are_dependent(const model::transition &t1, this->config.dependency_relation.call_or(true, &t1, &t2); } -bool classic_dpor::happens_before(const dpor_context &context, size_t i, - size_t j) const { - const runner_id_t rid = - context.stack.at(i).get_out_transition()->get_executor(); - const clock_vector &cv = context.stack.at(j).get_clock_vector(); - return i <= cv.value_for(rid); -} - -bool classic_dpor::happens_before_thread(const dpor_context &context, size_t i, - runner_id_t p) const { - const runner_id_t rid = context.get_transition(i)->get_executor(); - const clock_vector &cv = - context.stack.back().get_per_runner_clocks()[p].get_clock_vector(); - return i <= cv.value_for(rid); -} - -bool classic_dpor::threads_race_after(const dpor_context &context, size_t i, - runner_id_t q, runner_id_t p) const { - const size_t transition_stack_height = context.stack.size() - 1; - for (size_t j = i + 1; j < transition_stack_height; j++) { - if (q == context.get_transition(j)->get_executor() && - this->happens_before_thread(context, j, p)) - return true; - } - return false; -} - void classic_dpor::verify_using(coordinator &coordinator, const callbacks &callbacks) { // The code below is an implementation of the model-checking algorithm of - // Flanagan and Godefroid from 2015. + // Flanagan and Godefroid from 2005. // 1. Data structure set up @@ -114,6 +145,9 @@ void classic_dpor::verify_using(coordinator &coordinator, /// The initial entry into the stack represents the information DPOR tracks /// for state `s_0`. log_debug(dpor_logger) << "Initializing the DPOR stack"; + bool reached_max_depth = false; + std::list round_robin_sched; + stats model_checking_stats; dpor_context context(coordinator); auto &dpor_stack = context.stack; @@ -128,21 +162,64 @@ void classic_dpor::verify_using(coordinator &coordinator, // 2. Exploration phase while (dpor_stack.back().has_enabled_runners()) { if (dpor_stack.size() >= this->config.maximum_total_execution_depth) { - throw std::runtime_error( - "*** Execution Limit Reached! ***\n\n" - "McMini ran a trace with" + - std::to_string(dpor_stack.size()) + - " transitions which is\n" - "the more than McMini was configured to handle in any one trace (" + - std::to_string(this->config.maximum_total_execution_depth) + - "). Try running mcmini with the \"--max-depth-per-thread\" flag\n" - "to limit how far into a trace McMini can go\n"); + if (!reached_max_depth) { + log_unexpected(dpor_logger) + << "*** Execution Limit Reached! ***\n\n" + << "McMini encountered a trace with " << dpor_stack.size() + << " transitions which is the most that McMini was configured" + << " to handle in any given trace (" + << this->config.maximum_total_execution_depth + << "). McMini will continue its search, but it may be " + "incomplete. Rerun McMini with the " + "\"--max-depth-per-thread\" " + << "flag for correct results."; + reached_max_depth = true; + } + break; } - // NOTE: For deterministic results, always choose the "first" enabled - // runner. A runner precedes another runner in being enabled iff it has a - // smaller id. try { - const runner_id_t rid = dpor_stack.back().get_first_enabled_runner(); + runner_id_t rid; + switch (config.policy) { + case algorithm::exploration_policy::smallest_first: { + rid = dpor_stack.back().get_first_enabled_runner(); + break; + } + case algorithm::exploration_policy::round_robin: { + auto unscheduled_runners = dpor_stack.back().get_enabled_runners(); + + // For round robin scheduling, always prefer to schedule + // threads that don't appear in `round_robin_sched` because + // these threads are necessarily unscheduled wrt the previous starting + // point. + // + // 1. Among those threads not appearing in the round robin + // schedule, always pick the smallest. + // 2. If every enabled thread has already been scheduled, then pick + // the first based on the round robin schedule and move it to the back + // of the list. NOTE: Every enabled runner is in `round_robin_sched`, + // but the converse is not necessarily true (i.e. there may be threads + // in `round_robin_sched` that aren't enabled) + for (const runner_id_t id : round_robin_sched) { + unscheduled_runners.erase(id); + } + if (!unscheduled_runners.empty()) { + rid = *std::min_element(unscheduled_runners.begin(), + unscheduled_runners.end()); + round_robin_sched.push_back(rid); + } else { + auto it = + std::find_if(round_robin_sched.begin(), round_robin_sched.end(), + [&](const runner_id_t id) { + return dpor_stack.back().is_enabled(id); + }); + assert(it != round_robin_sched.end()); + round_robin_sched.splice(round_robin_sched.end(), round_robin_sched, + it); + rid = *it; + } + } + } + this->continue_dpor_by_expanding_trace_with(rid, context); model_checking_stats.total_transitions++; @@ -165,26 +242,29 @@ void classic_dpor::verify_using(coordinator &coordinator, "The program exited abnormally"); } } catch (const model::undefined_behavior_exception &ube) { - if (callbacks.undefined_behavior) - callbacks.undefined_behavior(coordinator, model_checking_stats, ube); + callbacks.undefined_behavior(context, model_checking_stats, ube); return; } catch (const real_world::process::termination_error &te) { - if (callbacks.abnormal_termination) - callbacks.abnormal_termination(coordinator, model_checking_stats, te); + callbacks.abnormal_termination(context, model_checking_stats, te); return; } catch (const real_world::process::nonzero_exit_code_error &nzec) { - if (callbacks.nonzero_exit_code) - callbacks.nonzero_exit_code(coordinator, model_checking_stats, nzec); + callbacks.nonzero_exit_code(context, model_checking_stats, nzec); return; } } - if (callbacks.trace_completed) - callbacks.trace_completed(coordinator, model_checking_stats); + callbacks.trace_completed(context, model_checking_stats); - if (callbacks.deadlock && - coordinator.get_current_program_model().is_in_deadlock()) - callbacks.deadlock(coordinator, model_checking_stats); + if (coordinator.get_current_program_model().is_in_deadlock()) { + if (config.stop_at_first_deadlock) { + log_info(dpor_logger) + << "First deadlock found. Reporting and stopping model checking."; + callbacks.deadlock(context, model_checking_stats); + return; + } else { + callbacks.deadlock(context, model_checking_stats); + } + } // 3. Backtrack phase while (!dpor_stack.empty() && dpor_stack.back().backtrack_set_empty()) @@ -208,9 +288,25 @@ void classic_dpor::verify_using(coordinator &coordinator, try { this->continue_dpor_by_expanding_trace_with( dpor_stack.back().backtrack_set_pop_first(), context); + + // If we're doing round robin scheduling for expanding the trace, + // backtracking forces a restart of the round robin process. + // Intuitively, this makes sense: round robin only applies when + // searching _new_ traces. However, we could be a little more + // intelligent here and resume the round robin from where it _should_ + // continue, but that's a little more complicated. + // + // That is, if the trace after backtracking is e.g. + // + // 1, 2, 3, 1, 2, _2_ + // + // where _2_ was inserted as a backtrack point, then we could notice + // that _3_ was technically supposed to be next in the round robin + // scheduling. The current method would schedule 1, then 2, then 3, ... + // since we only account for scheduling that occurs during _expansion_. + round_robin_sched.clear(); } catch (const model::undefined_behavior_exception &ube) { - if (callbacks.undefined_behavior) - callbacks.undefined_behavior(coordinator, model_checking_stats, ube); + callbacks.undefined_behavior(context, model_checking_stats, ube); return; } } @@ -333,7 +429,8 @@ void classic_dpor::dynamically_update_backtrack_sets(dpor_context &context) { coordinator.get_current_program_model().get_num_runners(); std::set thread_ids; - for (runner_id_t i = 0; i < num_threads; i++) thread_ids.insert(i); + for (runner_id_t i = 0; i < num_threads; i++) + thread_ids.insert(i); const ssize_t t_stack_top = (ssize_t)(context.stack.size()) - 2; const runner_id_t last_runner_to_execute = @@ -381,7 +478,8 @@ void classic_dpor::dynamically_update_backtrack_sets(dpor_context &context) { * will be the maxmimum `i` since we're searching * backwards */ - if (should_stop) break; + if (should_stop) + break; } } } @@ -393,17 +491,18 @@ bool classic_dpor::dynamically_update_backtrack_sets_at_index( // TODO: add in co-enabled conditions const bool has_reversible_race = this->are_dependent(next_sp, S_i) && this->are_coenabled(next_sp, S_i) && - !this->happens_before_thread(context, i, p); + !context.happens_before_thread(i, p); // If there exists i such that ... if (has_reversible_race) { std::set e; for (runner_id_t const q : pre_si.get_enabled_runners()) { - const bool in_e = q == p || this->threads_race_after(context, i, q, p); + const bool in_e = q == p || context.threads_race_after(i, q, p); // If E != empty set - if (in_e && !pre_si.sleep_set_contains(q)) e.insert(q); + if (in_e && !pre_si.sleep_set_contains(q)) + e.insert(q); } if (e.empty()) { @@ -418,7 +517,8 @@ bool classic_dpor::dynamically_update_backtrack_sets_at_index( // in the set E, chose that thread to backtrack // on. This is equivalent to not having to do // anything - if (pre_si.backtrack_set_contains(q)) return true; + if (pre_si.backtrack_set_contains(q)) + return true; } // Otherwise select an arbitrary thread to backtrack upon. @@ -430,57 +530,688 @@ bool classic_dpor::dynamically_update_backtrack_sets_at_index( classic_dpor::dependency_relation_type classic_dpor::default_dependencies() { classic_dpor::dependency_relation_type dr; - dr.register_dd_entry( - &transitions::thread_create::depends); - dr.register_dd_entry( - &transitions::thread_join::depends); - dr.register_dd_entry( - &transitions::mutex_lock::depends); - dr.register_dd_entry( - &transitions::mutex_lock::depends); - dr.register_dd_entry( - &transitions::condition_variable_wait::depends); - dr.register_dd_entry( - &transitions::condition_variable_wait::depends); - dr.register_dd_entry( - &transitions::condition_variable_signal::depends); - dr.register_dd_entry( - &transitions::condition_variable_signal::depends); + using namespace transitions; + dr.register_dd_entry(&thread_create::depends); + dr.register_dd_entry(&thread_join::depends); + dr.register_dd_entry(&thread_start::depends); + dr.register_dd_entry(&thread_exit::depends); + dr.register_dd_entry( + &mutex_lock::depends); + dr.register_dd_entry( + &mutex_lock::depends); + dr.register_dd_entry( + &condition_variable_wait::depends); + dr.register_dd_entry( + &condition_variable_wait::depends); + dr.register_dd_entry( + &condition_variable_signal::depends); + dr.register_dd_entry( + &condition_variable_signal::depends); return dr; } classic_dpor::coenabled_relation_type classic_dpor::default_coenabledness() { + using namespace transitions; classic_dpor::dependency_relation_type cr; - cr.register_dd_entry( - &transitions::thread_create::coenabled_with); - cr.register_dd_entry( - &transitions::thread_join::coenabled_with); - cr.register_dd_entry( - &transitions::mutex_lock::coenabled_with); - cr.register_dd_entry( - &transitions::condition_variable_signal::coenabled_with); - cr.register_dd_entry( - &transitions::condition_variable_signal::coenabled_with); - cr.register_dd_entry( - &transitions::condition_variable_broadcast::coenabled_with); - cr.register_dd_entry( - &transitions::condition_variable_broadcast::coenabled_with); - cr.register_dd_entry( - &transitions::condition_variable_destroy::coenabled_with); - cr.register_dd_entry( - &transitions::condition_variable_destroy::coenabled_with); + cr.register_dd_entry(&thread_create::coenabled_with); + cr.register_dd_entry(&thread_join::coenabled_with); + cr.register_dd_entry( + &mutex_lock::coenabled_with); + cr.register_dd_entry( + &condition_variable_signal::coenabled_with); + cr.register_dd_entry( + &condition_variable_signal::coenabled_with); + cr.register_dd_entry( + &condition_variable_broadcast::coenabled_with); + cr.register_dd_entry( + &condition_variable_broadcast::coenabled_with); + cr.register_dd_entry( + &condition_variable_destroy::coenabled_with); + cr.register_dd_entry( + &condition_variable_destroy::coenabled_with); return cr; } + +std::vector> +classic_dpor::dpor_context::transitive_reduction() const { + // This code is heavily inspired by the code in the LEDA library + // (https://leda.uni-trier.de), specifically the + // `LEDA-7.2.2/src/graph/graph_alg/_transclosure.cpp` + // + // The transitive reduction R of a digraph G is the graph of the fewest arcs + // such that a path exists between nodes u and v in G iff a path exists + // between u and v in R. Essentially, it's the smallest graph with the same + // dependency relation of G. + // + // In our case, we're considering a trace T := t1, t2, ..., tN of `N` + // total transitions. Each transition can be thought of as a node in a digraph + // with the edges representing "happens-before" dependencies between them. The + // transitive reduction of this digraph then represents those transitions in + // an "immediate" race: ti --> tj and for all transitions tk in-between, + // either ti --/--> tk or tk --/-->tj. + if (this->stack.empty()) + return {}; + const size_t N = this->transition_stack_size(); + const size_t INF = N + 1; + + // `adj_list` holds the dependencies between every point in the trace. Nodes + // are representing using integers and correspond to the index in the + // transition stack. + // + // `e in adj_list[i] <--> happens_before(i, e)`. + // + // `redundant[i][j] <---> adj_list[i][j] can be removed in the transition + // reduction` + // + // NOTE: For each `i`, the nodes are ordered in topological order. This is + // because the transitions in the stack are already topologically ordered by + // construction, and we process nodes in order. + std::vector> adj_list(N); + std::vector> redundant(N); + + for (size_t i = 0; i < N; i++) { + for (size_t j = i + 1; j < N; j++) { + if (happens_before(i, j)) { + adj_list[i].push_back(j); + redundant[i].push_back(true); + } + } + } + + // Compute Chain Decomposition + // + // Decomposes the DAG into a minimum number of disjoint paths (chains). + // + // chain_id[v]: index of the chain containing v + // C[h]: list of nodes in chain h + // + // See Dilworth's theorem. + std::vector unmarked(N, true); + std::vector chain_id(N); + std::vector> C; + + // Iterating in increasing topological order (see note above) + for (size_t v = 0; v < N; ++v) { + if (unmarked[v]) { + C.emplace_back(); // Start a new chain + size_t current_chain_id = C.size() - 1; + size_t current_node = v; + + while (current_node != INF) { + C.back().push_back(current_node); + chain_id[current_node] = current_chain_id; + unmarked[current_node] = false; + + // Find the first unmarked neighbor 'w' (smallest topological rank) + size_t next_node = INF; + for (size_t w : adj_list[current_node]) { + if (unmarked[w]) { + next_node = w; + break; + } + } + current_node = next_node; + } + } + } + + // Compute Reachability and Redundancy + // + // reach[i][c] = min{j ; node j in C[c] and path i -> j exists} + // + // where "<" refers to topological order + // + // Intuitively, `reach[i][c]` denotes the "smallest" (topologically-speaking) + // node in chain `c` to which `i` has a path. + const int num_chains = C.size(); + std::vector> reach(N, std::vector(num_chains, INF)); + + // The key loop: iterates in DECREASING topological order + for (size_t k = 0; k <= N - 1; k++) { + size_t v = N - k - 1; + + // Process outgoing edges of v (target 'w' is in INCREASING order) + for (size_t i = 0; i < adj_list[v].size(); i++) { + const int w = adj_list[v][i]; + if (w < reach[v][chain_id[w]]) { + redundant[v][i /* INDEX of w */] = false; + + // If v can reach w via a non-redundant edge, v can reach everything j + // reaches. + for (int c = 0; c < num_chains; ++c) + reach[v][c] = std::min(reach[v][c], reach[w][c]); + } + } + reach[v][chain_id[v]] = v; + } + + // Remove redundant edges from the adjacency list + for (size_t k = 0; k < N; k++) { + auto &out_edges = adj_list[k]; + auto &redundant_edges = redundant[k]; + assert(out_edges.size() == redundant_edges.size()); + size_t j = 0; + for (size_t i = 0; i < out_edges.size(); ++i) + if (!redundant_edges[i]) + out_edges[j++] = out_edges[i]; + out_edges.resize(j); + } + +#if DEBUG + // Validation: every point in the adjacency list happens before + for (size_t i = 0; i < N; i++) + for (size_t j = i + 1; j < N; j++) + if (std::find(adj_list[i].begin(), adj_list[i].end(), j) != + adj_list[i].end()) { + assert(happens_before(i, j)); + } else { + if (happens_before(i, j)) { + + auto s = std::find_if(adj_list[i].begin(), adj_list[i].end(), + [&](int w) { return happens_before(w, j); }); + assert(s != adj_list[i].end()); + } + // Not in adj so ok in `false` case + } +#endif + return adj_list; +} + +#ifdef MCMINI_USE_SCIP +void SCIP_dump(SCIP *scip) { + SCIP_CALL_ABORT(SCIPprintOrigProblem(scip, nullptr, "lp", false)); +} +#endif + +std::vector +classic_dpor::dpor_context::linearize_optimal() const { +#ifdef MCMINI_USE_SCIP + // Given a fixed trace `T` of `N` transitions and a happens-before relation + // `happens-before_T: [1, N] x [1, N] -> {0, 1}` over the indices of `T`, the + // goal is to produce a new trace `T'` such that `happens-before_T(i, j) = + // happens-before_T'(i, j)` and such that the number of inversions is + // minimized. An inversion is a point in the trace where the thread ID of the + // `i`th transition doesn't match the thread ID of the `(i + 1)`th transition. + // + // The intuition in producing such a trace `T'` is that reasoning about this + // trace is "easier" than any other because the number of context switches + // (inversions) a user must perform to analyze a new trace is minimized. + // Moreover, since `T'` obeys the same "happens-before" relation as the + // original trace `T`, it produces the exact same bug. + // + // We can map relinearization into a graph problem. Let `Tids := {tid : exists + // i, T[i]->get_executor() = tid }`. We construct an unweighted, labeled + // digraph `K` where + // + // 1. V(K) := {1, 2, ..., N} + // 2. E(K) := {(i, j) in [1, N] x [1, N] : happens-before_T(i, j)} + // 3. tid : V -> Tids, tid(v) := T[v].get_executor() + // + // Since `happens-before_T` is transitive, we note that `K = + // Transitive-Closure(K)` since `happens-before_T` is transitive. Moreover, + // the array `[1, 2, ..., N]` is a valid topological sorting of `K` since `i > + // j --> happens-before_T(i, j) = 0`. + // + // An equivalent formulation of the problem is to find a topological sorting + // of K of minimal inversions. Computing such a minimal topological sort can + // be reduced to the sequential ordering problem (SOP) (see + // https://people.idsia.ch/~roberto/SOP.pdf for a reference). The SOP problem + // is related to the Asymmetric Traveling Salesperson Problem (ATSP). In the + // ATSP, the goal is to find a Hamiltonian Cycle in a weighted directed graph + // of minimal weight. SOP adds one more constraint and requires that certain + // nodes are visited before others based on a relation `R` over the vertices. + // + // We construct a new graph `G` from `K`. Here, we + // note that although the SOP problem and ATSP problems work with cycles, we + // can add a source and sink node to our DAG with zero weight edges between + // each other and the respective start and end nodes of the digraph (those + // with in-degree and out-degree equalt to 0 respectively) to map exactly to + // the SOP problem. + // + // Denote `H := Transitive-Reduction(K)`. Recall each node `v` in `K` and by + // proxy `H` corresponds to a transition in the transition stack `T`. Let + // `tid(v)` denote the labeling function of `K`. Then let + // + // 1. V(G) := V(H) + {source, sink} + // 2. E(G) := V(H) x V(H) + {(u, sink) : u in V(H), out-degree[u] = 0} + + // {(source, u) : u in V(H), in-degree[u] = 0}} + // 3. For all e = (u, v) in E(G), + // + // w(e) := if tid(u) == tid(v) || (u == source) || (v == sink) then 0 + // else 1 + // + // Let `C := SOP(G, E(H))` denote the Hamiltonian Cycle of minimum weight + // subjet to `E(H)`. Then `C := m_1, m_2, ..., m_N` corresponds to the minimal + // topological sorting. Clearly, `C` is a valid topological sorting since it + // contains all nodes of `H` and in an order obeying `E(H)`. By construction, + // the total weight of `C` equals the number of inversions in `C`, since an + // edge is weighted iff they are inverted and don't connect either the sink or + // source. Since `C` is of minimal weight,. it is also of minimal inversions. + // + // The SOP instance can be solved by reduction using integer constraints. + // Here, we use the Miller-Tucker-Zemlin (MTZ) formulation of the TSP problem. + // In MTZ, a variable `x_ij in {0, 1}` is added to represent whether the edge + // `(i, j)` is taken. For eache node `v_i`, a variable `u_i` is added to + // indicate the order the node is visited in the cycle. Constraints are added + // to ensure that exactly one `x_ij` goes into and exits each node and such + // that if (i, j) is taken then `u_i < u_j` We can adjust the MTZ to work on + // an SOP instance by adding precendence constraints on the variables `u_i` by + // always forcing `u_i <= u_j + 1` iff `i` happens-before `j`. + // + // Reducing the number of variables is key to making the solver efficient. + // There are two optimizations we apply in the context of our specific + // optimization problem instance: + // + // A) For each edge (u, v) in E(H), only (u, v) needs to be added to G + // since a path that includes (v, u) would not satisfy the ordering + // constraint. Moreover, any edge (u', v') in E(K) such that there exists + // a node k such that (u', k) and (k, v') in E(H) can be eliminated from + // G. This is equivalent to eliminating any edges in G that are contained + // in the `Transitive-Closure(H) = K`. In general, + // + // 1. V(G) := V(H) + {source, sink} + // 2. E(G) := E(H) + {(u, v) in V(H) x V(H) : (u, v) and (v, u) not in K} + + // {(u, sink) : u in V(H), out-degree[u] = 0} + + // {(source, u) : u in V(H), in-degree[u] = 0}} + // 3. For all e = (u, v) in E(G), + // + // w(e) := if tid(u) == tid(v) || (u == source) || (v == sink) then 0 + // else 1 + // + // B) We observe the following. Firstly, for any two nodes `(u, v) in + // H_TC`, `tid[u] = tid[v] ==> u --> v`. I.e., there is always a + // happens-before relation between two nodes of the same label. + // + // For each sequence V = v_1, v_2, ..., v_r in E(H) such that + // + // 1. For all i in [1, r) out-degree[u_i] = in-degree[u_(i + 1)] = 1 + // + // V must appear in the SOP Hamiltonian cycle C of minimal + // weight. + // + // Informally, given a contiguous "block" of transitions which must appear in + // order but are otherwise independent with other transitions except possibly + // the first and last transitions of the block, anything that doesn't + // "happen-before" the first transition in the block can be placed anywhere + // inside the block (otherwise there would be a transitive dependency + // somewhere in the block). Since the block ordering "forces" a certain + // ordering of the transitions, the number of inversions `I` in the block is + // fixed. For any `j` such that `v_1 --/--> j`, `tid[v_1] != tid[j]` and + // by transitivity `u --/--> j` and hence `tid[u] != tid[j]` for all u in V. + // `u --/--> j` further implies `(u, j) and (j, u) in G` for all `u in C`. + // Since `tid[u] != tid[j]`, `w_uj = w_ju = 1`. Since any Hamiltonian cycle + // must include all nodes in order, either the edge `(v_1, v_2)` is included + // or `(v_1, u_1), ..., (u_n, v_2)` for some `u_l` sequence such that `v_1 + // --\--> u_1`. Since w_(v_1, v_2) <= 1 but `w_(v_1, u_1) = w_(u_n, v_2)`, the + // weight of taking the interior edge instead of two exterior ones smaller + // than taking the two outer ones. We can essentially treat (v_1, v_2), ..., + // (v_(r-1), v_r) as a subgraph with all incoming and outgoing edges of + // weight 1. + // + // Consequently, we can first group together simple chains and solve the + // smaller SOP instance and still obtain the same optimal result. + // + // To compute the reduced graph, we use the Disjoint Set Union. See + // https://cp-algorithms.com/data_structures/disjoint_set_union.html + struct dsu { + std::vector parent; + std::vector sizes; + + public: + dsu(size_t n) : sizes(n, 1) { + parent.resize(n); + std::iota(parent.begin(), parent.end(), 0); + } + + size_t find(size_t i) { + if (parent[i] == i) + return i; + return parent[i] = find(parent[i]); + } + + void unite(size_t i, size_t j) { + size_t root_i = find(i); + size_t root_j = find(j); + if (root_i != root_j) { + if (sizes[root_i] < sizes[root_j]) + std::swap(root_i, root_j); + parent[root_i] = root_j; + sizes[root_i] += sizes[root_j]; + } + } + }; + + // Let `H_red` be the edge-reduced, transitive reduction graph. For each edge + // `(u, v) in E(H)`, if out(u) = in(v) = 1, then we can effectively combine + // `u` and `v` together into a single node iff they refer to transitions run + // by the same thread. `supernodes` maps nodes in the reduced graph to the + // original graph `H`. + // + // ``` + // Where `i` refers to a node ID in the reduced graph H_red + // supernodes[i] = [u_1, u_2, ..., u_(l+1)] <---> (u_j, u_{j+1}) in V(H) and + // out-degree[u_j] = in-degree[u_(j+1)] = 1 + // ``` + // Where `i` refers to a member of V(H) + // dsu.find(i) = j <---> i is a part of supernode j in the reduced graph + //``` + // The immediate transitive dependencies of `supernodes[i].back()` = u_(l+1) + // are the same as the transitive dependencies of the supernode. Moreoever, + // using the argument in the proof above, the set of edges + // {(u_i, v) in V(H) x V(H) : (u_i, v) and (v, u_i) not in K} is the same for + // any u_i. Here, we pick the first one `supernodes[i].front()` + const auto H = this->transitive_reduction(); + const size_t N = H.size(); + std::vector out_degree(N, 0); + std::vector in_degree(N, 0); + + // INVARIANT: supernodes[i] is sorted by ID (and hence sorted in topological + // order) + std::vector> supernodes; + std::unordered_map H_to_supernode; + { + dsu dsu(N); + { + std::vector tids(N, 0); + + for (size_t u = 0; u < N; ++u) { + out_degree[u] = H[u].size(); + tids[u] = tid(u); + for (size_t v : H[u]) + in_degree[v]++; + } + + for (size_t u = 0; u < N; ++u) { + if (out_degree[u] == 1) { + size_t v = H[u][0]; // The only neighbor + if (in_degree[v] == 1 && tids[u] == tids[v]) + dsu.unite(u, v); + } + } + } + { + std::map> groups; + for (size_t i = 0; i < N; ++i) + groups[dsu.find(i)].push_back(i); + + supernodes.reserve(groups.size()); + for (auto &p : groups) { + const size_t new_supernode_id = supernodes.size(); + for (size_t i : p.second) + H_to_supernode[i] = new_supernode_id; + supernodes.push_back(std::move(p.second)); + } + } + } + + // In what follows, there are implicitly two graphs: + // + // 1. The original transitive reduction `H` containing the "happens-before" + // DAG wihtout transitive dependencies with `N` nodes. + // + // 2. The reduced DAG `H_red` with `M <= N` nodes where nodes `(u, v)` in `H` + // where `out-degree[u] = in-degree[v] = 1` are combined together to reduce + // the number of variables. This graph isn't explicitly stored in memory. + // Instead, for each node in `H_red`, a list of back references in `H` + // indicating + // + // Iterations happen over nodes IDs in `H_red`. There a few important + // observations (here `i`s and `j`s are over super node indices) + // ``` + // supernode[i].front() --/--> supernode[j].front() --> i -->_S' j + // out_degree_super[i] = out_degree[supernodes[i].back()] + // in_degree_super[i] = in_degree[supernodes[i].front()] + SCIP *scip = nullptr; + SCIPcreate(&scip); + SCIPsetMessagehdlr(scip, NULL); + SCIPincludeDefaultPlugins(scip); + SCIPcreateProbBasic(scip, "Minimize_Inversions"); + SCIPsetObjsense(scip, SCIP_OBJSENSE_MINIMIZE); + + const size_t M = supernodes.size(); + std::vector u(M); + std::vector> x( + M + 1, std::vector(M + 1, nullptr)); + + // Path variables: 1 <= u_i <= M + for (size_t i = 0; i < M; i++) { + const std::string name = "u_" + std::to_string(i); + SCIPcreateVarBasic(scip, &u[i], name.c_str(), 1.0, (double)M, 0.0, + SCIP_VARTYPE_CONTINUOUS); + SCIPaddVar(scip, u[i]); + } + + // All edges in the transitive reduction, add forward edge x_ij in {0, 1} + for (size_t i = 0; i < M; ++i) { + for (size_t j : H[supernodes[i].back()]) { + assert(supernodes[H_to_supernode[j]].front() == j); + j = H_to_supernode[j]; + assert(i < j); + assert(x[i][j] == nullptr); + std::string name = "x_" + std::to_string(i) + std::to_string(j); + SCIPcreateVarBasic(scip, &x[i][j], name.c_str(), 0.0, 1.0, + tid(supernodes[i].back()) != + tid(supernodes[j].front()), + SCIP_VARTYPE_BINARY); + SCIPaddVar(scip, x[i][j]); + } + } + + // All edges not contained in the transitive closure + // Add forward _and_ backward edges x_ij and x_ji + for (size_t i = 0; i < M; ++i) + for (size_t j = i + 1; j < M; j++) + if (!happens_before(supernodes[i].front(), supernodes[j].front())) { + assert(x[i][j] == nullptr); + assert(x[j][i] == nullptr); + const double w_e = + tid(supernodes[i].back()) != tid(supernodes[j].front()); + { + const std::string name = "x_" + std::to_string(i) + std::to_string(j); + SCIPcreateVarBasic(scip, &x[i][j], name.c_str(), 0.0, 1.0, w_e, + SCIP_VARTYPE_BINARY); + SCIPaddVar(scip, x[i][j]); + } + { + const std::string name = "x_" + std::to_string(j) + std::to_string(i); + SCIPcreateVarBasic(scip, &x[j][i], name.c_str(), 0.0, 1.0, w_e, + SCIP_VARTYPE_BINARY); + SCIPaddVar(scip, x[j][i]); + } + } + + // Source/sink variables --> only added to DAG's entrances + exits + for (size_t i = 0; i < M; ++i) { + if (out_degree[supernodes[i].back()] == 0) { + const std::string name = "x_" + std::to_string(i) + std::to_string(M); + SCIPcreateVarBasic(scip, &x[i][M], name.c_str(), 0.0, 1.0, 0.0, + SCIP_VARTYPE_BINARY); + SCIPaddVar(scip, x[i][M]); + } + + if (in_degree[supernodes[i].front()] == 0) { + const std::string name = "x_" + std::to_string(M) + std::to_string(i); + SCIPcreateVarBasic(scip, &x[M][i], name.c_str(), 0.0, 1.0, 0.0, + SCIP_VARTYPE_BINARY); + SCIPaddVar(scip, x[M][i]); + } + } + + // MTZ Constraints + // A. Exactly one exit and one entrance per node (including source/sink) + for (size_t i = 0; i < M + 1; ++i) { + SCIP_CONS *enter_cons = nullptr; + SCIP_CONS *leave_cons = nullptr; + const std::string enter = "enter_" + std::to_string(i); + const std::string leave = "leave_" + std::to_string(i); + SCIPcreateConsBasicLinear(scip, &enter_cons, enter.c_str(), 0, nullptr, + nullptr, 1.0, 1.0); + SCIPcreateConsBasicLinear(scip, &leave_cons, leave.c_str(), 0, nullptr, + nullptr, 1.0, 1.0); + for (size_t j = 0; j < M + 1; ++j) { + if (x[i][j]) + SCIPaddCoefLinear(scip, leave_cons, x[i][j], 1.0); + if (x[j][i]) + SCIPaddCoefLinear(scip, enter_cons, x[j][i], 1.0); + } + SCIPaddCons(scip, enter_cons); + SCIPaddCons(scip, leave_cons); + SCIPreleaseCons(scip, &enter_cons); + SCIPreleaseCons(scip, &leave_cons); + } + + // B. MTZ Subtour Elimination: + // -INF <= u_i - u_j + M*x_ij <= (M - 1) for i, j in [1, M], i != j + for (size_t i = 0; i < M; ++i) { + for (size_t j = 0; j < M; ++j) { + if (!x[i][j]) + continue; + SCIP_CONS *cons = nullptr; + const std::string name = + "subtour_" + std::to_string(i) + "_" + std::to_string(j); + SCIPcreateConsBasicLinear(scip, &cons, name.c_str(), 0, nullptr, nullptr, + -SCIPinfinity(scip), (double)(M - 1)); + SCIPaddCoefLinear(scip, cons, u[i], 1.0); + SCIPaddCoefLinear(scip, cons, u[j], -1.0); + SCIPaddCoefLinear(scip, cons, x[i][j], (double)M); + SCIPaddCons(scip, cons); + SCIPreleaseCons(scip, &cons); + } + } + + // C. Precedence Constraints: INF >= u_target - u_i >= 1 + for (size_t i = 0; i < M; ++i) { + for (size_t target : H[supernodes[i].back()]) { + target = H_to_supernode[target]; + SCIP_CONS *cons = nullptr; + const std::string name = + "precedence_" + std::to_string(i) + "_" + std::to_string(target); + SCIPcreateConsBasicLinear(scip, &cons, name.c_str(), 0, nullptr, nullptr, + 1.0, SCIPinfinity(scip)); + SCIPaddCoefLinear(scip, cons, u[target], 1.0); + SCIPaddCoefLinear(scip, cons, u[i], -1.0); + SCIPaddCons(scip, cons); + SCIPreleaseCons(scip, &cons); + } + } + SCIPsolve(scip); + SCIP_SOL *sol = SCIPgetBestSol(scip); + + std::vector linearization; + struct NodePosition { + size_t id; + double u_value; + }; + + if (sol != nullptr) { + std::vector sequence; + sequence.reserve(M); + for (size_t i = 0; i < M; ++i) { + double val = SCIPgetSolVal(scip, sol, u[i]); + sequence.push_back({i, val}); + } + std::sort(sequence.begin(), sequence.end(), + [](const NodePosition &a, const NodePosition &b) { + return a.u_value < b.u_value; + }); + for (const auto &item : sequence) + std::move(supernodes[item.id].begin(), supernodes[item.id].end(), + std::back_inserter(linearization)); + } else { + std::cerr << "No solution found!" << std::endl; + return {}; + } + { + for (size_t i = 0; i < M + 1; ++i) { + if (i < M) + SCIPreleaseVar(scip, &u[i]); + for (size_t j = 0; j < M + 1; ++j) { + if (x[i][j]) + SCIPreleaseVar(scip, &x[i][j]); + } + } + SCIPfree(&scip); + } + + std::vector linearized_trace(N, nullptr); + for (size_t i = 0; i < N; i++) + linearized_trace[i] = get_transition(linearization[i]); + return linearized_trace; +#else + // Fallback to greedy if SCIP isn't available + return linearize_lowest_first(); +#endif +} + +std::vector +classic_dpor::dpor_context::linearize_lowest_first() const { + const auto adj_list = this->transitive_reduction(); + const size_t N = adj_list.size(); + const size_t INF = N + 1; + std::vector linearization; + std::vector ready_set; + std::vector in_degree(N, 0); + for (size_t u = 0; u < N; ++u) + for (size_t v : adj_list[u]) + in_degree[v]++; + + for (size_t i = 0; i < N; ++i) + if (in_degree[i] == 0) + ready_set.push_back(i); + + runner_id_t last_rid = RUNNER_ID_MAX; + while (!ready_set.empty()) { + size_t next_vertex = INF; + size_t selected_index = INF; + if (last_rid != RUNNER_ID_MAX) { + for (size_t i = 0; i < ready_set.size(); ++i) { + const runner_id_t r = get_transition(ready_set[i])->get_executor(); + if (r == last_rid) { + next_vertex = ready_set[i]; + selected_index = i; + break; // Found the best greedy match that avoids inversion + } + } + } + + // If no ID match, or at the start, pick the thread with the lowest id + if (next_vertex == INF) { + runner_id_t min_rid = RID_INVALID; + for (size_t i = 0; i < ready_set.size(); ++i) { + const runner_id_t r = get_transition(ready_set[i])->get_executor(); + if (r < min_rid) { + next_vertex = ready_set[i]; + selected_index = i; + min_rid = r; + } + } + } + + linearization.push_back(next_vertex); + last_rid = get_transition(next_vertex)->get_executor(); + + // Remove the selected vertex from the ready set + // Swap with the back and pop for O(1) removal from vector (since order in S + // doesn't matter) + std::swap(ready_set[selected_index], ready_set.back()); + ready_set.pop_back(); + + for (int v : adj_list[next_vertex]) { + in_degree[v]--; + if (in_degree[v] == 0) { + ready_set.push_back(v); + } + } + } + + std::vector linearized_trace(N, nullptr); + for (size_t i = 0; i < N; i++) + linearized_trace[i] = get_transition(linearization[i]); + return linearized_trace; +} \ No newline at end of file diff --git a/src/mcmini/model_checking/reporter.cpp b/src/mcmini/model_checking/reporter.cpp new file mode 100644 index 0000000..806959a --- /dev/null +++ b/src/mcmini/model_checking/reporter.cpp @@ -0,0 +1,99 @@ +#include "mcmini/model_checking/reporter.hpp" +#include "mcmini/signal.hpp" + +using namespace model; +using namespace model_checking; + +void reporter::dump_relinearized_trace(std::ostream &os, + const algorithm::context &c, + const stats &) const { + if (relinearize_traces) { + os << "\nRELINEARIZED TRACE\n"; + for (const auto &t : c.linearize_trace(use_optimal_linearization)) { + os << "thread " << t->get_executor() << ": " << t->to_string() << "\n"; + } + } +} + +void reporter::trace_completed(const algorithm::context &c, + const stats &stats) const { + if (!verbose) + return; + std::cout << "TRACE " << stats.trace_id << "\n"; + for (const auto &t : c.get_model().get_trace()) { + std::cout << "thread " << t->get_executor() << ": " << t->to_string() + << "\n"; + } + dump_relinearized_trace(std::cout, c, stats); + std::cout << "\nNEXT THREAD OPERATIONS\n"; + for (const auto &tpair : c.get_model().get_pending_transitions()) { + std::cout << "thread " << tpair.first << ": " << tpair.second->to_string() + << "\n"; + } + std::cout.flush(); +} + +void reporter::deadlock(const algorithm::context &c, const stats &stats) const { + std::cout << "DEADLOCK (trace ID: " << stats.trace_id << ")" << std::endl; + for (const auto &t : c.get_model().get_trace()) { + std::cout << "thread " << t->get_executor() << ": " << t->to_string() + << "\n"; + } + dump_relinearized_trace(std::cout, c, stats); + std::cout << "\nNEXT THREAD OPERATIONS\n"; + for (const auto &tpair : c.get_model().get_pending_transitions()) { + std::cout << "thread " << tpair.first << ": " << tpair.second->to_string() + << "\n"; + } + std::cout.flush(); +} + +void reporter::undefined_behavior( + const algorithm::context &c, const stats &stats, + const undefined_behavior_exception &ub) const { + std::cout << "UNDEFINED BEHAVIOR:\n" << ub.what() << std::endl; + std::cout << "TRACE " << stats.trace_id << "\n"; + for (const auto &t : c.get_model().get_trace()) { + std::cout << "thread " << t->get_executor() << ": " << t->to_string() + << "\n"; + } + dump_relinearized_trace(std::cout, c, stats); + std::cout << "\nNEXT THREAD OPERATIONS\n"; + for (const auto &tpair : c.get_model().get_pending_transitions()) { + std::cout << "thread " << tpair.first << ": " << tpair.second->to_string() + << "\n"; + } + std::cout.flush(); +} + +void reporter::abnormal_termination( + const algorithm::context &c, const stats &stats, + const real_world::process::termination_error &ub) const { + std::cout << "Abnormally Termination (signo: " << ub.signo + << ", signal: " << sig_to_str.at(ub.signo) << "):\n" + << ub.what() << std::endl; + + std::cout << "TRACE " << stats.trace_id << "\n"; + for (const auto &t : c.get_model().get_trace()) { + std::cout << "thread " << t->get_executor() << ": " << t->to_string() + << "\n"; + } + dump_relinearized_trace(std::cout, c, stats); + const transition *terminator = + c.get_model().get_pending_transition_for(ub.culprit); + std::cout << "thread " << terminator->get_executor() << ": " + << terminator->to_string() << "\n"; + + std::cout << "\nNEXT THREAD OPERATIONS\n"; + for (const auto &tpair : c.get_model().get_pending_transitions()) { + if (tpair.first == terminator->get_executor()) { + std::cout << "thread " << tpair.first << ": executing" + << "\n"; + } else { + std::cout << "thread " << tpair.first << ": " << tpair.second->to_string() + << "\n"; + } + } + std::cout << stats.total_transitions + 1 << " total transitions executed" + << std::endl; +} \ No newline at end of file