From: Brian Norris <banorris@uci.edu>
Date: Thu, 12 Jul 2012 18:18:00 +0000 (-0700)
Subject: Merge branch 'master' into brian
X-Git-Tag: pldi2013~363
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=8548c711d71b6474802af83f5a4800eb4ac30718;hp=ddc42efe21d50de5a6a70f82d0e45d5eea29f5fd;p=model-checker.git

Merge branch 'master' into brian
---

diff --git a/action.cc b/action.cc
index d9aae2d..39b0f7f 100644
--- a/action.cc
+++ b/action.cc
@@ -10,6 +10,7 @@ ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, int
 	order(order),
 	location(loc),
 	value(value),
+	reads_from(NULL),
 	cv(NULL)
 {
 	Thread *t = thread_current();
@@ -132,6 +133,7 @@ void ModelAction::read_from(const ModelAction *act)
 	ASSERT(cv);
 	if (act->is_release() && this->is_acquire())
 		cv->merge(act->cv);
+	reads_from = act;
 	value = act->value;
 }
 
@@ -178,8 +180,10 @@ void ModelAction::print(void) const
 		type_str = "unknown type";
 	}
 
-	printf("(%3d) Thread: %-2d    Action: %-13s    MO: %d    Loc: %14p    Value: %d",
+	printf("(%3d) Thread: %-2d    Action: %-13s    MO: %d    Loc: %14p    Value: %-4d",
 			seq_number, id_to_int(tid), type_str, order, location, value);
+	if (reads_from)
+		printf(" Rf: %d", reads_from->get_seq_number());
 	if (cv) {
 		printf("\t");
 		cv->print();
diff --git a/action.h b/action.h
index 3e44804..30c8a35 100644
--- a/action.h
+++ b/action.h
@@ -48,10 +48,10 @@ public:
 	void * get_location() const { return location; }
 	modelclock_t get_seq_number() const { return seq_number; }
 	int get_value() const { return value; }
+	const ModelAction * get_reads_from() const { return reads_from; }
 
 	Node * get_node() const { return node; }
 	void set_node(Node *n) { node = n; }
-	void set_value(int val) { value = val; }
 
 	bool is_read() const;
 	bool is_write() const;
@@ -96,6 +96,9 @@ private:
 	 * should probably be something longer. */
 	int value;
 
+	/** The action that this action reads from. Only valid for reads */
+	const ModelAction *reads_from;
+
 	/** A back reference to a Node in NodeStack, if this ModelAction is
 	 * saved on the NodeStack. */
 	Node *node;
diff --git a/clockvector.cc b/clockvector.cc
index 162a7c2..190f921 100644
--- a/clockvector.cc
+++ b/clockvector.cc
@@ -34,11 +34,11 @@ ClockVector::~ClockVector()
 }
 
 /**
- * Merge a clock vector into this vector, using a pairwise vector. The
+ * Merge a clock vector into this vector, using a pairwise comparison. The
  * resulting vector length will be the maximum length of the two being merged.
  * @param cv is the ClockVector being merged into this vector.
  */
-void ClockVector::merge(ClockVector *cv)
+void ClockVector::merge(const ClockVector *cv)
 {
 	modelclock_t *clk = clock;
 	bool resize = false;
diff --git a/clockvector.h b/clockvector.h
index 1428886..56037eb 100644
--- a/clockvector.h
+++ b/clockvector.h
@@ -16,7 +16,7 @@ class ClockVector {
 public:
 	ClockVector(ClockVector *parent = NULL, ModelAction *act = NULL);
 	~ClockVector();
-	void merge(ClockVector *cv);
+	void merge(const ClockVector *cv);
 	bool synchronized_since(const ModelAction *act) const;
 
 	void print() const;
diff --git a/libatomic.cc b/libatomic.cc
index a076533..5317319 100644
--- a/libatomic.cc
+++ b/libatomic.cc
@@ -11,10 +11,9 @@ void atomic_store_explicit(struct atomic_object *obj, int value, memory_order or
 
 int atomic_load_explicit(struct atomic_object *obj, memory_order order)
 {
-	int value = obj->value;
 	DBG();
-	model->switch_to_master(new ModelAction(ATOMIC_READ, order, obj, value));
-	return value;
+	model->switch_to_master(new ModelAction(ATOMIC_READ, order, obj));
+	return thread_current()->get_return_value();
 }
 
 void atomic_init(struct atomic_object *obj, int value)
diff --git a/main.cc b/main.cc
index 19f12f1..c9ac1d0 100644
--- a/main.cc
+++ b/main.cc
@@ -53,7 +53,7 @@ static void thread_wait_finish(void) {
 
 /** The real_main function contains the main model checking loop. */
 
-void real_main() {
+static void real_main() {
 	thrd_t user_thread;
 	ucontext_t main_context;
 
diff --git a/model.cc b/model.cc
index cde6213..d80d1d2 100644
--- a/model.cc
+++ b/model.cc
@@ -272,6 +272,19 @@ void ModelChecker::check_current_action(void)
 	set_backtracking(curr);
 
 	add_action_to_lists(curr);
+
+	/* Assign reads_from values */
+	/* TODO: perform release/acquire synchronization here; include
+	 * reads_from as ModelAction member? */
+	Thread *th = get_thread(curr->get_tid());
+	int value = VALUE_NONE;
+	if (curr->is_read()) {
+		const ModelAction *reads_from = curr->get_node()->get_next_read_from();
+		value = reads_from->get_value();
+		/* Assign reads_from, perform release/acquire synchronization */
+		curr->read_from(reads_from);
+	}
+	th->set_return_value(value);
 }
 
 /**
diff --git a/nodestack.cc b/nodestack.cc
index 10f7a72..2416ed7 100644
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -130,6 +130,22 @@ void Node::add_read_from(const ModelAction *act)
 	may_read_from.push_back(act);
 }
 
+/**
+ * Gets the next 'may_read_from' action from this Node. Only valid for a node
+ * where this->action is a 'read'.
+ * @todo Perform reads_from backtracking/replay properly, so that this function
+ * may remove elements from may_read_from
+ * @return The first element in may_read_from
+ */
+const ModelAction * Node::get_next_read_from() {
+	const ModelAction *act;
+	ASSERT(!may_read_from.empty());
+	act = may_read_from.front();
+	/* TODO: perform reads_from replay properly */
+	/* may_read_from.pop_front(); */
+	return act;
+}
+
 void Node::explore(thread_id_t tid)
 {
 	int i = id_to_int(tid);
diff --git a/nodestack.h b/nodestack.h
index c09b628..11cbdfa 100644
--- a/nodestack.h
+++ b/nodestack.h
@@ -44,6 +44,7 @@ public:
 	Node * get_parent() const { return parent; }
 
 	void add_read_from(const ModelAction *act);
+	const ModelAction * get_next_read_from();
 
 	void print();
 	void print_may_read_from();