From: Brian Norris <banorris@uci.edu>
Date: Wed, 3 Oct 2012 00:54:26 +0000 (-0700)
Subject: assign sequence numbers after initial processing
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=f8bac60ca108ab3d7729c0254ff80819e6d8c121

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 1655d942..383be230 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 2bf01dce..f6fb0623 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 097da8ae..744fec5e 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 867ec031..d6d6f090 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