From f8bac60ca108ab3d7729c0254ff80819e6d8c121 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Tue, 2 Oct 2012 17:54:26 -0700 Subject: [PATCH] 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. --- action.cc | 10 +++++++++- action.h | 1 + model.cc | 2 ++ model.h | 3 ++- 4 files changed, 14 insertions(+), 2 deletions(-) diff --git a/action.cc b/action.cc index 1655d94..383be23 100644 --- 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 2bf01dc..f6fb062 100644 --- 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 097da8a..744fec5 100644 --- 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 867ec03..d6d6f09 100644 --- 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 -- 2.34.1