From 61aa8f8322290de8ac8c4c1eeff472cd64e9d0b0 Mon Sep 17 00:00:00 2001
From: Matthew Fernandez <matthew.fernandez@gmail.com>
Date: Sat, 8 Jun 2019 21:10:29 -0700
Subject: [PATCH] FIXME: introduce shortest trace functionality

This commit needs significant work and doesn't function correctly as-is.

Github: related to #131 "minimal trace mode"
---
 rumur/resources/header.c    | 52 ++++++++++++++++++++++++++++++++++++-
 rumur/src/generate-model.cc |  9 +++++++
 rumur/src/main.cc           | 43 ++++++++++++++++++++++++++++++
 rumur/src/options.h         |  3 +++
 rumur/src/output.cc         |  1 +
 5 files changed, 107 insertions(+), 1 deletion(-)

diff --git a/rumur/resources/header.c b/rumur/resources/header.c
index bb8d8c2c..9643a2bd 100644
--- a/rumur/resources/header.c
+++ b/rumur/resources/header.c
@@ -90,6 +90,9 @@ static enum { WARMUP, RUN } phase = WARMUP;
  */
 static unsigned long error_count;
 
+/* Depth of the last found error. */
+static size_t error_depth;
+
 /* Number of rules that have been processed. There are two representations of
  * this: a thread-local count of how many rules we have fired thus far and a
  * global array of *final* counts of fired rules per-thread that is updated and
@@ -648,10 +651,57 @@ static _Noreturn int exit_with(int status);
 static __attribute__((format(printf, 2, 3))) _Noreturn void error(
   const struct state *NONNULL s, const char *NONNULL fmt, ...) {
 
+  bool report = false;
+
+#if SHORTEST_TRACE
+  /* Compare the trace we found to the previously known shortest. */
+  size_t depth = 0;
+  size_t my_depth = state_depth(s);
+  for (;;) {
+    if (depth == 0 || my_depth < depth) {
+      /* Ours is the first error trace or shorter than the previous. Notify
+       * other threads of ours.
+       */
+      report = true;
+      if (__atomic_compare_exchange_n(&error_depth, &depth, my_depth, false,
+          __ATOMIC_SEQ_CST, __ATOMIC_SEQ_CST)) {
+        break;
+      }
+    } else {
+      /* There was a previously found trace shorter than ours. */
+      report = false;
+      break;
+    }
+  }
+
+  while (report) {
+
+    depth = __atomic_load_n(&error_depth, __ATOMIC_SEQ_CST);
+    if (depth < my_depth) {
+      report = false;
+      break;
+    }
+
+    if (__atomic_load_n(&running_count, __ATOMIC_SEQ_CST) == 1) {
+      depth = __atomic_load_n(&error_depth, __ATOMIC_SEQ_CST);
+      if (depth < my_depth) {
+        report = false;
+      }
+      break;
+    }
+
+    __asm__ volatile ("");
+  }
+#endif
+
   unsigned long prior_errors = __atomic_fetch_add(&error_count, 1,
     __ATOMIC_SEQ_CST);
 
-  if (prior_errors < MAX_ERRORS) {
+#if !SHORTEST_TRACE
+  report = prior_errors < MAX_ERRORS;
+#endif
+
+  if (report) {
 
     print_lock();
 
diff --git a/rumur/src/generate-model.cc b/rumur/src/generate-model.cc
index d712abb4..04a47f90 100644
--- a/rumur/src/generate-model.cc
+++ b/rumur/src/generate-model.cc
@@ -802,11 +802,20 @@ void generate_model(std::ostream &out, const Model &m) {
       << "      break;\n"
       << "    }\n"
       << "\n"
+      << "#if SHORTEST_TRACE\n"
+      << "    if (THREADS > 1) {\n"
+      << "      size_t depth = __atomic_load_n(&error_depth, __ATOMIC_SEQ_CST);\n"
+      << "      if (depth != 0 && depth < state_depth(s)) {\n"
+      << "        break;\n"
+      << "      }\n"
+      << "    }\n"
+      << "#else\n"
       << "    if (THREADS > 1 && __atomic_load_n(&error_count,\n"
       << "        __ATOMIC_SEQ_CST) >= MAX_ERRORS) {\n"
       << "      /* Another thread found an error. */\n"
       << "      break;\n"
       << "    }\n"
+      << "#endif\n"
       << "\n"
       << "    bool possible_deadlock = true;\n"
       << "    uint64_t rule_taken = 1;\n";
diff --git a/rumur/src/main.cc b/rumur/src/main.cc
index 1b841ab4..167bdef1 100644
--- a/rumur/src/main.cc
+++ b/rumur/src/main.cc
@@ -37,6 +37,10 @@ static bool make_ul(unsigned long &value, const std::string &s) {
 
 static void parse_args(int argc, char **argv) {
 
+  bool set_max_errors = false;
+  bool set_counterexample_trace = false;
+  bool set_shortest_trace = false;
+
   for (;;) {
     static struct option opts[] = {
       { "bound", required_argument, 0, 140 },
@@ -55,6 +59,7 @@ static void parse_args(int argc, char **argv) {
       { "sandbox", required_argument, 0, 135 },
       { "set-capacity", required_argument, 0, 's' },
       { "set-expand-threshold", required_argument, 0, 'e' },
+      { "shortest-trace", required_argument, 0, 142 },
       { "symmetry-reduction", required_argument, 0, 134 },
       { "threads", required_argument, 0, 't' },
       { "trace", required_argument, 0, 130 },
@@ -234,6 +239,7 @@ static void parse_args(int argc, char **argv) {
           std::cerr << "invalid --max-errors argument \"" << optarg << "\"\n";
           exit(EXIT_FAILURE);
         }
+        set_max_errors = true;
         break;
 
       case 137: // --counterexample-trace ...
@@ -248,6 +254,7 @@ static void parse_args(int argc, char **argv) {
             << optarg << "\"\n";
           exit(EXIT_FAILURE);
         }
+        set_counterexample_trace = true;
         break;
 
       case 138: // --output-format ...
@@ -279,6 +286,18 @@ static void parse_args(int argc, char **argv) {
         options.value_type = optarg;
         break;
 
+      case 142: // --shortest-trace ...
+        if (strcmp(optarg, "on") == 0) {
+          options.shortest_trace = true;
+        } else if (strcmp(optarg, "off") == 0) {
+          options.shortest_trace = false;
+        } else {
+          std::cerr << "invalid argument to --shortest-trace, \"" << optarg << "\"\n";
+          exit(EXIT_FAILURE);
+        }
+        set_shortest_trace = true;
+        break;
+
       default:
         std::cerr << "unexpected error\n";
         exit(EXIT_FAILURE);
@@ -286,6 +305,30 @@ static void parse_args(int argc, char **argv) {
     }
   }
 
+  if (options.shortest_trace && options.max_errors > 1) {
+    if (set_shortest_trace && set_max_errors) {
+      std::cerr << "--max-errors greater than 1 and --shortest-trace on are "
+        << "incompatible\n";
+      exit(EXIT_FAILURE);
+    } else if (set_shortest_trace) {
+      options.max_errors = 1;
+    } else if (set_max_errors) {
+      options.shortest_trace = false;
+    }
+  }
+
+  if (options.shortest_trace && options.counterexample_trace == CEX_OFF) {
+    if (set_shortest_trace && set_counterexample_trace) {
+      std::cerr << "--counterexample-trace off and --shortest-trace on are "
+        << "incompatible\n";
+      exit(EXIT_FAILURE);
+    } else if (set_shortest_trace) {
+      options.counterexample_trace = DIFF;
+    } else if (set_counterexample_trace) {
+      options.shortest_trace = false;
+    }
+  }
+
   if (optind == argc - 1) {
     struct stat buf;
     if (stat(argv[optind], &buf) < 0) {
diff --git a/rumur/src/options.h b/rumur/src/options.h
index 155bb170..7b852ff1 100644
--- a/rumur/src/options.h
+++ b/rumur/src/options.h
@@ -82,6 +82,9 @@ struct Options {
 
   // Type used for value_t in the checker
   std::string value_type = "auto";
+
+  // Generate the shortest counter-example trace possible?
+  bool shortest_trace = true;
 };
 
 extern Options options;
diff --git a/rumur/src/output.cc b/rumur/src/output.cc
index 87bc05fb..6dd7419f 100644
--- a/rumur/src/output.cc
+++ b/rumur/src/output.cc
@@ -106,6 +106,7 @@ int output_checker(const std::string &path, const Model &model,
       << " };\n\n"
     << "enum { MAX_SIMPLE_WIDTH = " << max_simple_width(model) << " };\n\n"
     << "#define BOUND " << options.bound << "\n\n"
+    << "#define SHORTEST_TRACE " << options.shortest_trace << "\n\n"
     << "typedef " << value_types.first.c_type << " value_t;\n"
     << "#define VALUE_MIN " << value_types.first.int_min << "\n"
     << "#define VALUE_MAX " << value_types.first.int_max << "\n"