assign sequence numbers after initial processing

When re-ordering the execution of JOIN and LOCK operations (e.g., when
they attempt to execute when not enabled), the sequence numbers became
out of order. Also, RMW operations would cause sequence numbers to jump
by 2 every time.

This fix arranges initialization such that a ModelAction is only
assigned a sequence number after it passes some initial checks to ensure
that it will be executed and utilized immediately. Otherwise, it will
either be discarded or held pending until it is enabled.

diff --git a/action.cc b/action.cc
index 1655d9428eb57041287c7b2bef12e3742b7058f1..383be230aaea3f4b505266688fde98ce7a6a8640 100644 (file)
--- a/action.cc
+++ b/action.cc
@@ -8,17 +8,19 @@
 #include "clockvector.h"
 #include "common.h"
 
+#define ACTION_INITIAL_CLOCK 0
+
 ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, uint64_t value) :
        type(type),
        order(order),
        location(loc),
        value(value),
        reads_from(NULL),
+       seq_number(ACTION_INITIAL_CLOCK),
        cv(NULL)
 {
        Thread *t = thread_current();
        this->tid = t->get_id();
-       this->seq_number = model->get_next_seq_num();
 }
 
 ModelAction::~ModelAction()
@@ -32,6 +34,12 @@ void ModelAction::copy_from_new(ModelAction *newaction)
        seq_number = newaction->seq_number;
 }
 
+void ModelAction::set_seq_number(modelclock_t num)
+{
+       ASSERT(seq_number == ACTION_INITIAL_CLOCK);
+       seq_number = num;
+}
+
 bool ModelAction::is_mutex_op() const
 {
        return type == ATOMIC_LOCK || type == ATOMIC_TRYLOCK || type == ATOMIC_UNLOCK;

diff --git a/action.h b/action.h
index 2bf01dce092b71d1a0fa37bc82a29802036e9d1c..f6fb06236fe0230eb942c38dcc177c081db341bd 100644 (file)
--- a/action.h
+++ b/action.h
@@ -78,6 +78,7 @@ public:
        void set_node(Node *n) { node = n; }
 
        void copy_from_new(ModelAction *newaction);
+       void set_seq_number(modelclock_t num);
        void set_try_lock(bool obtainedlock);
        bool is_mutex_op() const;
        bool is_lock() const;

diff --git a/model.cc b/model.cc
index 097da8ae9b7c66fae010db5c95d3a6245622f3cc..744fec5e17a27ef75b07a2bca068ff344e951ee8 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -534,6 +534,8 @@ ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr)
                return newcurr;
        }
 
+       curr->set_seq_number(get_next_seq_num());
+
        newcurr = node_stack->explore_action(curr, scheduler->get_enabled());
        if (newcurr) {
                /* First restore type and order in case of RMW operation */

diff --git a/model.h b/model.h
index 867ec0310670f808874aaf7aabe52528fdd2592b..d6d6f090392b788b34df5dc91bd6cfcd9cf17079 100644 (file)
--- a/model.h
+++ b/model.h
@@ -78,7 +78,6 @@ public:
 
        thread_id_t get_next_id();
        int get_num_threads();
-       modelclock_t get_next_seq_num();
 
        /** @return The currently executing Thread. */
        Thread * get_current_thread() { return scheduler->get_current_thread(); }
@@ -114,6 +113,8 @@ private:
        int num_feasible_executions;
        bool promises_expired();
 
+       modelclock_t get_next_seq_num();
+
        /**
         * Stores the ModelAction for the current thread action.  Call this
         * immediately before switching from user- to system-context to pass