model: use snapshot_calloc()

[c11tester.git] / model.cc

diff --git a/model.cc b/model.cc
index e5c8a55033289bf7393094c514d9e85658489342..de3b3259d79c1b47c78c75ed7fd41e3352fa764a 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -56,7 +56,7 @@ ModelChecker::ModelChecker(struct model_params params) :
        bad_synchronization(false)
 {
        /* Allocate this "size" on the snapshotting heap */
-       priv = (struct model_snapshot_members *)calloc(1, sizeof(*priv));
+       priv = (struct model_snapshot_members *)snapshot_calloc(1, sizeof(*priv));
        /* First thread created will have id INITIAL_THREAD_ID */
        priv->next_thread_id = INITIAL_THREAD_ID;
 
@@ -88,6 +88,8 @@ ModelChecker::~ModelChecker()
        delete node_stack;
        delete scheduler;
        delete mo_graph;
+
+       snapshot_free(priv);
 }
 
 static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 4> * hash, void * ptr) {
@@ -294,6 +296,21 @@ bool ModelChecker::is_deadlocked() const
        return blocking_threads;
 }
 
+/**
+ * Check if this is a complete execution. That is, have all thread completed
+ * execution (rather than exiting because sleep sets have forced a redundant
+ * execution).
+ *
+ * @return True if the execution is complete.
+ */
+bool ModelChecker::is_complete_execution() const
+{
+       for (unsigned int i = 0; i < get_num_threads(); i++)
+               if (is_enabled(int_to_id(i)))
+                       return false;
+       return true;
+}
+
 /**
  * Queries the model-checker for more executions to explore and, if one
  * exists, resets the model-checker state to execute a new execution.
@@ -1023,7 +1040,8 @@ void ModelChecker::check_curr_backtracking(ModelAction * curr) {
        }
 }
 
-bool ModelChecker::promises_expired() {
+bool ModelChecker::promises_expired() const
+{
        for (unsigned int promise_index = 0; promise_index < promises->size(); promise_index++) {
                Promise *promise = (*promises)[promise_index];
                if (promise->get_expiration()<priv->used_sequence_numbers) {
@@ -1035,12 +1053,14 @@ bool ModelChecker::promises_expired() {
 
 /** @return whether the current partial trace must be a prefix of a
  * feasible trace. */
-bool ModelChecker::isfeasibleprefix() {
+bool ModelChecker::isfeasibleprefix() const
+{
        return promises->size() == 0 && pending_rel_seqs->size() == 0 && isfeasible();
 }
 
 /** @return whether the current partial trace is feasible. */
-bool ModelChecker::isfeasible() {
+bool ModelChecker::isfeasible() const
+{
        if (DBG_ENABLED() && mo_graph->checkForRMWViolation())
                DEBUG("Infeasible: RMW violation\n");
 
@@ -1049,7 +1069,8 @@ bool ModelChecker::isfeasible() {
 
 /** @return whether the current partial trace is feasible other than
  * multiple RMW reading from the same store. */
-bool ModelChecker::isfeasibleotherthanRMW() {
+bool ModelChecker::isfeasibleotherthanRMW() const
+{
        if (DBG_ENABLED()) {
                if (mo_graph->checkForCycles())
                        DEBUG("Infeasible: modification order cycles\n");
@@ -1066,7 +1087,8 @@ bool ModelChecker::isfeasibleotherthanRMW() {
 }
 
 /** Returns whether the current completed trace is feasible. */
-bool ModelChecker::isfinalfeasible() {
+bool ModelChecker::isfinalfeasible() const
+{
        if (DBG_ENABLED() && promises->size() != 0)
                DEBUG("Infeasible: unrevolved promises\n");