action: switch from "libatomic" to C++-spec "memory_order_*" macros

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 3262f5e55caf992397d9134f24f2bba325cc4e87..c86a6f676718d3fab6122282483786dd85589cb0 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -304,8 +304,6 @@ void ModelChecker::check_current_action(void)
        set_backtracking(curr);
 
        /* Assign reads_from values */
-       /* TODO: perform release/acquire synchronization here; include
-        * reads_from as ModelAction member? */
        Thread *th = get_thread(curr->get_tid());
        uint64_t value = VALUE_NONE;
        if (curr->is_read()) {
@@ -332,10 +330,9 @@ bool ModelChecker::isfeasible() {
 /** Process a RMW by converting previous read into a RMW. */
 void ModelChecker::process_rmw(ModelAction * act) {
        int tid = id_to_int(act->get_tid());
-       std::vector<action_list_t> *vec = &(*obj_thrd_map)[act->get_location()];
-       ASSERT(tid < (int) vec->size());
-       ModelAction *lastread=(*vec)[tid].back();
+       ModelAction *lastread=get_last_action(tid);
        lastread->upgrade_rmw(act);
+       cyclegraph->addRMWEdge(lastread->get_reads_from(),lastread);
 }
 
 /**