Skip to content

Commit

Permalink
move rendezvous opt out out of exit_with
Browse files Browse the repository at this point in the history
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"
  • Loading branch information
Smattr committed Jun 16, 2019
1 parent 825d434 commit 7e9dd8b
Show file tree
Hide file tree
Showing 2 changed files with 18 additions and 2 deletions.
19 changes: 17 additions & 2 deletions rumur/resources/header.c
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -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);

Expand Down Expand Up @@ -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);
}

Expand Down Expand Up @@ -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;
Expand Down
1 change: 1 addition & 0 deletions rumur/src/generate-model.cc
Original file line number Diff line number Diff line change
Expand Up @@ -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";
}
Expand Down

0 comments on commit 7e9dd8b

Please sign in to comment.