model: bugfix get_last_seq_action()

The action lists may include the current action, which we don't want to
consider for 'get_last_seq_action()'.

Also, rewrite some of the comments for this function.

Bugfix thanks to Brian D.

diff --git a/model.cc b/model.cc
index acd20790f00eb20bf6675bba550a326a52ae3353..96ee3de6325156a75f1952df6cbba0415232ed80 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -758,7 +758,7 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
        if (curr->is_seqcst()) {
                /* We have to at least see the last sequentially consistent write,
                         so we are initialized. */
-               ModelAction *last_seq_cst = get_last_seq_cst(curr->get_location());
+               ModelAction *last_seq_cst = get_last_seq_cst(curr);
                if (last_seq_cst != NULL) {
                        mo_graph->addEdge(last_seq_cst, curr);
                        added = true;
@@ -1079,18 +1079,21 @@ ModelAction * ModelChecker::get_last_action(thread_id_t tid)
 }
 
 /**
- * Gets the last memory_order_seq_cst action (in the total global sequence)
- * performed on a particular object (i.e., memory location).
- * @param location The object location to check
- * @return The last seq_cst action performed
+ * Gets the last memory_order_seq_cst write (in the total global sequence)
+ * performed on a particular object (i.e., memory location), not including the
+ * current action.
+ * @param curr The current ModelAction; also denotes the object location to
+ * check
+ * @return The last seq_cst write
  */
-ModelAction * ModelChecker::get_last_seq_cst(const void *location)
+ModelAction * ModelChecker::get_last_seq_cst(ModelAction *curr)
 {
+       void *location = curr->get_location();
        action_list_t *list = obj_map->get_safe_ptr(location);
        /* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */
        action_list_t::reverse_iterator rit;
        for (rit = list->rbegin(); rit != list->rend(); rit++)
-               if ((*rit)->is_write() && (*rit)->is_seqcst())
+               if ((*rit)->is_write() && (*rit)->is_seqcst() && (*rit) != curr)
                        return *rit;
        return NULL;
 }
@@ -1204,7 +1207,7 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
        bool initialized = false;
 
        if (curr->is_seqcst()) {
-               last_seq_cst = get_last_seq_cst(curr->get_location());
+               last_seq_cst = get_last_seq_cst(curr);
                /* We have to at least see the last sequentially consistent write,
                         so we are initialized. */
                if (last_seq_cst != NULL)

diff --git a/model.h b/model.h
index 4fc32c6db6c2800d2bdf705d7a8b256683968bab..9c8fa87f2076a5f7c369c231d3bba89c0b93ca3b 100644 (file)
--- a/model.h
+++ b/model.h
@@ -129,7 +129,7 @@ private:
        void check_curr_backtracking(ModelAction * curr);
        void add_action_to_lists(ModelAction *act);
        ModelAction * get_last_action(thread_id_t tid);
-       ModelAction * get_last_seq_cst(const void *location);
+       ModelAction * get_last_seq_cst(ModelAction *curr);
        void build_reads_from_past(ModelAction *curr);
        ModelAction * process_rmw(ModelAction *curr);
        void post_r_modification_order(ModelAction *curr, const ModelAction *rf);