From 7e9dd8b8493a9dcad8eb24e4ffc883d5b46faf80 Mon Sep 17 00:00:00 2001
From: Matthew Fernandez <matthew.fernandez@gmail.com>
Date: Sat, 15 Jun 2019 19:33:45 -0700
Subject: [PATCH] move rendezvous opt out out of exit_with

The purpose of this seemingly irrelevant change is to ensure we opt out of the
rendezvous protocol as soon as error() is called when MAX_ERRORS == 1. In
upcoming changes to ensure we get the shortest resulting trace, we're going to
loop indefinitely in error(). This is only possible without livelocking if we're
no longer part of the thread rendezvous protocol.

Github: related to #131 "minimal trace mode"
---
 rumur/resources/header.c    | 19 +++++++++++++++++--
 rumur/src/generate-model.cc |  1 +
 2 files changed, 18 insertions(+), 2 deletions(-)

diff --git a/rumur/resources/header.c b/rumur/resources/header.c
index aed2895a..eb64019e 100644
--- a/rumur/resources/header.c
+++ b/rumur/resources/header.c
@@ -636,6 +636,11 @@ static __attribute__((unused)) size_t state_depth(
 static void print_counterexample(
   const struct state *NONNULL s __attribute__((unused)));
 
+/* Opt out the thread rendezvous protocol and return any held reference to the
+ * global seen set.
+ */
+static void resign(void);
+
 /* "Exit" the current thread. This takes into account which thread we are. I.e.
  * the correct way to exit the checker is for every thread to eventually call
  * this function.
@@ -645,6 +650,10 @@ 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, ...) {
 
+  if (MAX_ERRORS == 1) {
+    resign();
+  }
+
   unsigned long prior_errors = __atomic_fetch_add(&error_count, 1,
     __ATOMIC_SEQ_CST);
 
@@ -727,6 +736,10 @@ static __attribute__((format(printf, 2, 3))) _Noreturn void error(
     siglongjmp(checkpoint, 1);
   }
 
+  if (MAX_ERRORS != 1) {
+    resign();
+  }
+
   exit_with(EXIT_FAILURE);
 }
 
@@ -3006,11 +3019,13 @@ static _Noreturn void explore(void);
 static void check_liveness_final(void);
 static unsigned long check_liveness_summarise(void);
 
-static int exit_with(int status) {
-
+static void resign(void) {
   /* Opt out of the thread-wide rendezvous protocol. */
   refcounted_ptr_put(&global_seen, local_seen);
   rendezvous_opt_out();
+}
+
+static int exit_with(int status) {
 
   /* Make fired rule count visible globally. */
   rules_fired[thread_id] = rules_fired_local;
diff --git a/rumur/src/generate-model.cc b/rumur/src/generate-model.cc
index 8b2ef91a..0be16ad5 100644
--- a/rumur/src/generate-model.cc
+++ b/rumur/src/generate-model.cc
@@ -934,6 +934,7 @@ void generate_model(std::ostream &out, const Model &m) {
       << "    }\n"
       << "\n"
       << "  }\n"
+      << "  resign();\n"
       << "  exit_with(EXIT_SUCCESS);\n"
       << "}\n\n";
   }