[mc] Let the Checker give us the current trace

[simgrid.git] / src / mc / SafetyChecker.cpp

diff --git a/src/mc/SafetyChecker.cpp b/src/mc/SafetyChecker.cpp
index 442b871..2c9ca22 100644 (file)
--- a/src/mc/SafetyChecker.cpp
+++ b/src/mc/SafetyChecker.cpp
@@ -33,6 +33,26 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
 namespace simgrid {
 namespace mc {
 
+static void MC_show_non_termination(void)
+{
+  XBT_INFO("******************************************");
+  XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
+  XBT_INFO("******************************************");
+  XBT_INFO("Counter-example execution trace:");
+  for (auto& s : mc_model_checker->getChecker()->getTextualTrace())
+    XBT_INFO("%s", s.c_str());
+  MC_print_statistics(mc_stats);
+}
+
+static int snapshot_compare(mc_state_t state1, mc_state_t state2)
+{
+  simgrid::mc::Snapshot* s1 = state1->system_state;
+  simgrid::mc::Snapshot* s2 = state2->system_state;
+  int num1 = state1->num;
+  int num2 = state2->num;
+  return snapshot_compare(num1, s1, num2, s2);
+}
+
 static int is_exploration_stack_state(mc_state_t current_state){
 
   xbt_fifo_item_t item;
@@ -47,30 +67,42 @@ static int is_exploration_stack_state(mc_state_t current_state){
   return 0;
 }
 
-/**
- *  \brief Initialize the DPOR exploration algorithm
- */
-void SafetyChecker::pre()
+RecordTrace SafetyChecker::getRecordTrace() // override
 {
-  simgrid::mc::visited_states.clear();
+  RecordTrace res;
 
-  mc_state_t initial_state = MC_state_new();
+  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)) {
 
-  XBT_DEBUG("**************************************************");
-  XBT_DEBUG("Initial state");
+    // 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;
 
-  /* Wait for requests (schedules processes) */
-  mc_model_checker->wait_for_requests();
+    res.push_back(RecordTraceElement(pid, value));
+  }
 
-  /* Get an enabled process and insert it in the interleave set of the initial state */
-  for (auto& p : mc_model_checker->process().simix_processes())
-    if (simgrid::mc::process_is_enabled(&p.copy)) {
-      MC_state_interleave_process(initial_state, &p.copy);
-      if (reductionMode_ != simgrid::mc::ReductionMode::none)
-        break;
-    }
+  return std::move(res);
+}
 
-  xbt_fifo_unshift(mc_stack, initial_state);
+std::vector<std::string> SafetyChecker::getTextualTrace() // override
+{
+  std::vector<std::string> trace;
+  for (xbt_fifo_item_t item = xbt_fifo_get_last_item(mc_stack);
+       item; item = xbt_fifo_get_prev_item(item)) {
+    mc_state_t state = (mc_state_t)xbt_fifo_get_item_content(item);
+    int value;
+    smx_simcall_t req = MC_state_get_executed_request(state, &value);
+    if (req) {
+      char* req_str = simgrid::mc::request_to_string(
+        req, value, simgrid::mc::RequestType::executed);
+      trace.push_back(req_str);
+      xbt_free(req_str);
+    }
+  }
+  return std::move(trace);
 }
 
 int SafetyChecker::run()
@@ -176,7 +208,7 @@ int SafetyChecker::run()
 
       /* Check for deadlocks */
       if (mc_model_checker->checkDeadlock()) {
-        MC_show_deadlock(nullptr);
+        MC_show_deadlock();
         return SIMGRID_MC_EXIT_DEADLOCK;
       }
 
@@ -273,7 +305,25 @@ void SafetyChecker::init()
   /* Create exploration stack */
   mc_stack = xbt_fifo_new();
 
-  this->pre();
+  simgrid::mc::visited_states.clear();
+
+  mc_state_t initial_state = MC_state_new();
+
+  XBT_DEBUG("**************************************************");
+  XBT_DEBUG("Initial state");
+
+  /* Wait for requests (schedules processes) */
+  mc_model_checker->wait_for_requests();
+
+  /* Get an enabled process and insert it in the interleave set of the initial state */
+  for (auto& p : mc_model_checker->process().simix_processes())
+    if (simgrid::mc::process_is_enabled(&p.copy)) {
+      MC_state_interleave_process(initial_state, &p.copy);
+      if (reductionMode_ != simgrid::mc::ReductionMode::none)
+        break;
+    }
+
+  xbt_fifo_unshift(mc_stack, initial_state);
 
   /* Save the initial state */
   initial_global_state = xbt_new0(s_mc_global_t, 1);