From 939c3e18d1214e60cfc680244f8ab3e9bd5404af Mon Sep 17 00:00:00 2001
From: Brian Norris <banorris@uci.edu>
Date: Mon, 1 Oct 2012 13:29:00 -0700
Subject: [PATCH] model: add "bad synchronization" flag
Can be used for aborting a trace when an incorrectly-ordered
synchronization occurs.
---
model.cc | 8 ++++++--
model.h | 7 +++++++
2 files changed, 13 insertions(+), 2 deletions(-)
diff --git a/model.cc b/model.cc
index 1711e1a..9d2dbb6 100644
--- a/model.cc
+++ b/model.cc
@@ -38,7 +38,8 @@ ModelChecker::ModelChecker(struct model_params params) :
mo_graph(new CycleGraph()),
failed_promise(false),
too_many_reads(false),
- asserted(false)
+ asserted(false),
+ bad_synchronization(false)
{
/* Allocate this "size" on the snapshotting heap */
priv = (struct model_snapshot_members *)calloc(1, sizeof(*priv));
@@ -80,6 +81,7 @@ void ModelChecker::reset_to_initial_state()
node_stack->reset_execution();
failed_promise = false;
too_many_reads = false;
+ bad_synchronization = false;
reset_asserted();
snapshotObject->backTrackBeforeStep(0);
}
@@ -740,10 +742,12 @@ bool ModelChecker::isfeasibleotherthanRMW() {
DEBUG("Infeasible: failed promise\n");
if (too_many_reads)
DEBUG("Infeasible: too many reads\n");
+ if (bad_synchronization)
+ DEBUG("Infeasible: bad synchronization ordering\n");
if (promises_expired())
DEBUG("Infeasible: promises expired\n");
}
- return !mo_graph->checkForCycles() && !failed_promise && !too_many_reads && !promises_expired();
+ return !mo_graph->checkForCycles() && !failed_promise && !too_many_reads && !bad_synchronization && !promises_expired();
}
/** Returns whether the current completed trace is feasible. */
diff --git a/model.h b/model.h
index 4a1fcf4..4b9e3ff 100644
--- a/model.h
+++ b/model.h
@@ -91,6 +91,11 @@ public:
void finish_execution();
bool isfeasibleprefix();
void set_assert() {asserted=true;}
+
+ /** @brief Alert the model-checker that an incorrectly-ordered
+ * synchronization was made */
+ void set_bad_synchronization() { bad_synchronization = true; }
+
const model_params params;
MEMALLOC
@@ -196,6 +201,8 @@ private:
bool failed_promise;
bool too_many_reads;
bool asserted;
+ /** @brief Incorrectly-ordered synchronization was made */
+ bool bad_synchronization;
};
extern ModelChecker *model;
--
2.34.1