model: release sequences: check last action in each thread

Previously, release_seq_head would only examine actions on a particular, given
object to determine a release sequence. However, we can get information
regarding the possibility of future disruptive writes by checking the clock
vector of the last action of each thread, regardless of object.

diff --git a/model.cc b/model.cc
index a7c99af24b7b05633183e9f96494e873e9e3a5b3..d2fc366cc77d88521d583558aa50d9680df9305e 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -1118,6 +1118,10 @@ bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *rel
                 * the release seq? */
                bool future_ordered = false;
 
                 * the release seq? */
                bool future_ordered = false;
 

+               ModelAction *last = get_last_action(int_to_id(i));
+               if (last && rf->happens_before(last))
+                       future_ordered = true;
+

                for (rit = list->rbegin(); rit != list->rend(); rit++) {
                        const ModelAction *act = *rit;
                        if (!act->is_write())
                for (rit = list->rbegin(); rit != list->rend(); rit++) {
                        const ModelAction *act = *rit;
                        if (!act->is_write())