Introduce Round-Robin Exploration and Relinearization Schemes

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)

include/mcmini/misc/ddt.hpp

@@ -155,33 +155,34 @@ struct double_dispatch_member_function_table<InterfaceType,
                        unspecified_callback_handle);
   }
 
-  ReturnType call_or(ReturnType fallback, InterfaceType* t1, InterfaceType* t2,
+  ReturnType call_or(ReturnType fallback, InterfaceType *t1, InterfaceType *t2,
                      Args... args) const {
     const auto t1_type = std::type_index(typeid(*t1));
     const auto t2_type = std::type_index(typeid(*t2));
     if (internal_table.count(t1_type) > 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>(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>(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>(args)...);
     }
     return fallback;
   }
 
-  ReturnType call(InterfaceType* t1, InterfaceType* t2, Args... args) const {
+  ReturnType call(InterfaceType *t1, InterfaceType *t2, Args... args) const {
     const auto t1_type = std::type_index(typeid(*t1));
     const auto t2_type = std::type_index(typeid(*t2));
     if (internal_table.count(t1_type) > 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)...);
       }
     }

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

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.

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<thread>(executor);
-    if (!thread_state->is_running() || executor == RID_MAIN_THREAD) {
+    auto *thread_state = s.get_state_of_runner<thread>(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

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<thread>(executor);
+    auto *thread_state = s.get_state_of_runner<thread>(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

include/mcmini/model_checking/algorithm.hpp

@@ -1,7 +1,5 @@
 #pragma once
 
-#include <functional>
-
 #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<const model::transition *>
+    linearize_lowest_first() const = 0;
+    virtual std::vector<const model::transition *>
+    linearize_optimal() const = 0;
+    std::vector<const model::transition *> linearize_trace(bool optimal) const {
+      return optimal ? linearize_optimal() : linearize_lowest_first();
+    }
+  };
+
   struct callbacks {
-   public:
-    callbacks() = default;
-    std::function<void(const coordinator &, const stats &)> crash;
-    std::function<void(const coordinator &, const stats &)> deadlock;
-    std::function<void(const coordinator &, const stats &)> data_race;
-    std::function<void(const coordinator &, const stats &)> unknown_error;
-    std::function<void(const coordinator &, const stats &)> trace_completed;
-    std::function<void(const coordinator &, const stats &,
-                       const real_world::process::termination_error &)>
-        abnormal_termination;
-    std::function<void(const coordinator &, const stats &,
-                       const real_world::process::nonzero_exit_code_error &)>
-        nonzero_exit_code;
-    std::function<void(const coordinator &, const stats &,
-                       const model::undefined_behavior_exception &)>
-        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

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<const model::transition,
                                             bool(void)>;
@@ -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