Makefile: fixup Mac dependencies

[c11tester.git] / model.cc

diff --git a/model.cc b/model.cc
index c3a8c8415a71ed684e18b19fc2e9284e6bc6fac1..2a2d7760f24512ac11072ac48f646481476f4f0a 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -28,14 +28,14 @@ ModelChecker::ModelChecker(struct model_params params) :
        obj_map(new HashTable<const void *, action_list_t, uintptr_t, 4>()),
        obj_thrd_map(new HashTable<void *, std::vector<action_list_t>, uintptr_t, 4 >()),
        promises(new std::vector<Promise *>()),
+       futurevalues(new std::vector<struct PendingFutureValue>()),
        lazy_sync_with_release(new HashTable<void *, std::list<ModelAction *>, uintptr_t, 4>()),
        thrd_last_action(new std::vector<ModelAction *>(1)),
        node_stack(new NodeStack()),
        mo_graph(new CycleGraph()),
        failed_promise(false),
        too_many_reads(false),
-       asserted(false),
-       rmw_cycle(false)
+       asserted(false)
 {
        /* Allocate this "size" on the snapshotting heap */
        priv = (struct model_snapshot_members *)calloc(1, sizeof(*priv));
@@ -78,7 +78,6 @@ void ModelChecker::reset_to_initial_state()
        node_stack->reset_execution();
        failed_promise = false;
        too_many_reads = false;
-       rmw_cycle=false;
        reset_asserted();
        snapshotObject->backTrackBeforeStep(0);
 }
@@ -260,30 +259,6 @@ ModelAction * ModelChecker::get_next_backtrack()
        return next;
 }
 
-
-/** Checks whether making the ModelAction read read_from the
-               ModelAction write will introduce a cycle in the reads_from
-               relation.
-
-@return true if making it read from will be fine, false otherwise.
-
-*/
-
-bool ModelChecker::ensure_rmw_acyclic(const ModelAction * read, const ModelAction *write) {
-       if (!read->is_rmw())
-               return true;
-       if (!write->is_rmw())
-               return true;
-       while(write!=NULL) {
-               if (write==read) {
-                       rmw_cycle=true;
-                       return false;
-               }
-               write=write->get_reads_from();
-       }
-       return true;
-}
-
 /**
  * Processes a read or rmw model action.
  * @param curr is the read model action to process.
@@ -291,7 +266,6 @@ bool ModelChecker::ensure_rmw_acyclic(const ModelAction * read, const ModelActio
  * @param second_part_of_rmw is boolean that is true is this is the second action of a rmw.
  * @return True if processing this read updates the mo_graph.
  */
-
 bool ModelChecker::process_read(ModelAction *curr, Thread * th, bool second_part_of_rmw) {
        uint64_t value;
        bool updated=false;
@@ -301,9 +275,7 @@ bool ModelChecker::process_read(ModelAction *curr, Thread * th, bool second_part
                        mo_graph->startChanges();
 
                        value = reads_from->get_value();
-                               /* Assign reads_from, perform release/acquire synchronization */
-                       if (ensure_rmw_acyclic(curr, reads_from))
-                               curr->read_from(reads_from);
+
                        if (!second_part_of_rmw) {
                                check_recency(curr,false);
                        }
@@ -316,6 +288,7 @@ bool ModelChecker::process_read(ModelAction *curr, Thread * th, bool second_part
                                continue;
                        }
 
+                       curr->read_from(reads_from);
                        mo_graph->commitChanges();
                        updated |= r_status;
                } else if (!second_part_of_rmw) {
@@ -430,6 +403,16 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
                bool updated_promises=resolve_promises(curr);
                updated=updated_mod_order|updated_promises;
 
+               if (promises->size()==0) {
+                       for(unsigned int i=0;i<futurevalues->size();i++) {
+                               struct PendingFutureValue pfv=(*futurevalues)[i];
+                               if (pfv.act->get_node()->add_future_value(pfv.value, pfv.expiration) &&
+                                               (!priv->next_backtrack || *pfv.act > *priv->next_backtrack))
+                                       priv->next_backtrack = pfv.act;
+                       }
+                       futurevalues->resize(0);
+               }
+
                mo_graph->commitChanges();
                th->set_return_value(VALUE_NONE);
        }
@@ -442,7 +425,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
                add_action_to_lists(curr);
 
        check_curr_backtracking(curr);
-       
+
        set_backtracking(curr);
 
        return get_next_thread(curr);
@@ -451,7 +434,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 void ModelChecker::check_curr_backtracking(ModelAction * curr) {
        Node *currnode = curr->get_node();
        Node *parnode = currnode->get_parent();
-       
+
        if ((!parnode->backtrack_empty() ||
                         !currnode->read_from_empty() ||
                         !currnode->future_value_empty() ||
@@ -462,7 +445,6 @@ void ModelChecker::check_curr_backtracking(ModelAction * curr) {
        }
 }
 
-
 bool ModelChecker::promises_expired() {
        for (unsigned int promise_index = 0; promise_index < promises->size(); promise_index++) {
                Promise *promise = (*promises)[promise_index];
@@ -487,7 +469,7 @@ bool ModelChecker::isfeasible() {
 /** @returns whether the current partial trace is feasible other than
  * multiple RMW reading from the same store. */
 bool ModelChecker::isfeasibleotherthanRMW() {
-       return !mo_graph->checkForCycles() && !failed_promise && !too_many_reads && !rmw_cycle && !promises_expired();
+       return !mo_graph->checkForCycles() && !failed_promise && !too_many_reads && !promises_expired();
 }
 
 /** Returns whether the current completed trace is feasible. */
@@ -740,9 +722,8 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
                                if (thin_air_constraint_may_allow(curr, act)) {
                                        if (isfeasible() ||
                                                        (curr->is_rmw() && act->is_rmw() && curr->get_reads_from()==act->get_reads_from() && isfeasibleotherthanRMW())) {
-                                               if (act->get_node()->add_future_value(curr->get_value(), curr->get_seq_number()+params.maxfuturedelay) &&
-                                                               (!priv->next_backtrack || *act > *priv->next_backtrack))
-                                                       priv->next_backtrack = act;
+                                               struct PendingFutureValue pfv={curr->get_value(),curr->get_seq_number()+params.maxfuturedelay,act};
+                                               futurevalues->push_back(pfv);
                                        }
                                }
                        }
@@ -774,7 +755,6 @@ bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, con
        return true;
 }
 
-
 /**
  * Finds the head(s) of the release sequence(s) containing a given ModelAction.
  * The ModelAction under consideration is expected to be taking part in
@@ -1054,8 +1034,7 @@ bool ModelChecker::resolve_promises(ModelAction *write)
                Promise *promise = (*promises)[promise_index];
                if (write->get_node()->get_promise(i)) {
                        ModelAction *read = promise->get_action();
-                       if (ensure_rmw_acyclic(read, write))
-                               read->read_from(write);
+                       read->read_from(write);
                        if (read->is_rmw()) {
                                mo_graph->addRMWEdge(write, read);
                        }
@@ -1069,8 +1048,6 @@ bool ModelChecker::resolve_promises(ModelAction *write)
        return resolved;
 }
 
-
-
 /**
  * Compute the set of promises that could potentially be satisfied by this
  * action. Note that the set computation actually appears in the Node, not in