From: Brian Demsky <bdemsky@uci.edu>
Date: Fri, 18 May 2012 23:32:38 +0000 (-0700)
Subject: merging stuff...made need to clean up some stuff...but need to push it somewhere... 
X-Git-Tag: pldi2013~435
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=810306cb85accaaace9a50f174264f105991230b;hp=8c24abefd5f4c7528a245ec786309f96601b5c58;p=model-checker.git

merging stuff...made need to clean up some stuff...but need to push it somewhere else for now
Merge branch 'subramanian'

Conflicts:
	.gitignore
	Makefile
	action.h
	userprog.c
---

diff --git a/.gitignore b/.gitignore
index 6223e7e..f9a2676 100644
--- a/.gitignore
+++ b/.gitignore
@@ -3,7 +3,10 @@
 .*.swp
 *.so
 *~
+<<<<<<< HEAD
+=======
 *.*~
+>>>>>>> subramanian
 
 # files in this directory
 /model
diff --git a/Makefile b/Makefile
index 8344eff..b67d994 100644
--- a/Makefile
+++ b/Makefile
@@ -10,9 +10,9 @@ LIB_MEM_SO=lib$(LIB_MEM).so
 USER_O=userprog.o
 USER_H=libthreads.h libatomic.h
 
-MODEL_CC=libthreads.cc schedule.cc libatomic.cc model.cc threads.cc tree.cc librace.cc action.cc main.cc snapshot-interface.cc
-MODEL_O=libthreads.o schedule.o libatomic.o model.o threads.o tree.o librace.o action.o main.o snapshot-interface.o
-MODEL_H=libthreads.h schedule.h common.h libatomic.h model.h threads.h tree.h librace.h action.h snapshot-interface.h
+MODEL_CC=libthreads.cc schedule.cc libatomic.cc model.cc malloc.c threads.cc tree.cc librace.cc action.cc nodestack.cc clockvector.cc main.cc snapshot-interface.cc
+MODEL_O=libthreads.o schedule.o libatomic.o model.o malloc.o threads.o tree.o librace.o action.o nodestack.o clockvector.o main.o snapshot-interface.o
+MODEL_H=libthreads.h schedule.h common.h libatomic.h model.h threads.h tree.h librace.h action.h nodestack.h clockvector.h snapshot-interface.h
 
 SHMEM_CC=snapshot.cc malloc.c mymemory.cc
 SHMEM_O=snapshot.o malloc.o mymemory.o
diff --git a/action.h b/action.h
index c069cab..2f856e9 100644
--- a/action.h
+++ b/action.h
@@ -17,6 +17,7 @@ typedef enum action_type {
 
 /* Forward declaration */
 class TreeNode;
+class Node;
 
 class ModelAction {
 public:
@@ -27,10 +28,12 @@ public:
 	action_type get_type() { return type; }
 	memory_order get_mo() { return order; }
 	void * get_location() { return location; }
-	int get_seq_number() { return seq_number; }
+	int get_seq_number() const { return seq_number; }
 
-	TreeNode * get_node() { return node; }
-	void set_node(TreeNode *n) { node = n; }
+	TreeNode * get_treenode() { return treenode; }
+	void set_node(TreeNode *n) { treenode = n; }
+	Node * get_node() { return node; }
+	void set_node(Node *n) { node = n; }
 
 	bool is_read();
 	bool is_write();
@@ -39,6 +42,13 @@ public:
 	bool same_var(ModelAction *act);
 	bool same_thread(ModelAction *act);
 	bool is_dependent(ModelAction *act);
+
+	inline bool operator <(const ModelAction& act) const {
+		return get_seq_number() < act.get_seq_number();
+	}
+	inline bool operator >(const ModelAction& act) const {
+		return get_seq_number() > act.get_seq_number();
+	}
   MEMALLOC
 private:
 	action_type type;
@@ -46,7 +56,8 @@ private:
 	void *location;
 	thread_id_t tid;
 	int value;
-	TreeNode *node;
+	TreeNode *treenode;
+	Node *node;
 	int seq_number;
 };
 
diff --git a/clockvector.cc b/clockvector.cc
new file mode 100644
index 0000000..15e6590
--- /dev/null
+++ b/clockvector.cc
@@ -0,0 +1,61 @@
+#include <algorithm>
+#include <cstring>
+
+#include "model.h"
+#include "action.h"
+#include "clockvector.h"
+#include "common.h"
+
+ClockVector::ClockVector(ClockVector *parent, ModelAction *act)
+{
+	num_threads = parent ? parent->num_threads : 1;
+	if (act && act->get_type() == THREAD_CREATE)
+		num_threads++;
+	clock = (int *)myMalloc(num_threads * sizeof(int));
+	if (parent)
+		std::memcpy(clock, parent->clock, parent->num_threads * sizeof(int));
+	else
+		clock[0] = 0;
+
+	if (act)
+		clock[id_to_int(act->get_tid())] = act->get_seq_number();
+}
+
+ClockVector::~ClockVector()
+{
+	myFree(clock);
+}
+
+void ClockVector::merge(ClockVector *cv)
+{
+	int *clk = clock;
+	bool resize = false;
+
+	ASSERT(cv != NULL);
+
+	if (cv->num_threads > num_threads) {
+		resize = true;
+		clk = (int *)myMalloc(cv->num_threads * sizeof(int));
+	}
+
+	/* Element-wise maximum */
+	for (int i = 0; i < num_threads; i++)
+		clk[i] = std::max(clock[i], cv->clock[i]);
+
+	if (resize) {
+		for (int i = num_threads; i < cv->num_threads; i++)
+			clk[i] = cv->clock[i];
+		num_threads = cv->num_threads;
+		myFree(clock);
+	}
+	clock = clk;
+}
+
+bool ClockVector::happens_before(ModelAction *act, thread_id_t id)
+{
+	int i = id_to_int(id);
+
+	if (i < num_threads)
+		return act->get_seq_number() < clock[i];
+	return false;
+}
diff --git a/clockvector.h b/clockvector.h
new file mode 100644
index 0000000..615dfeb
--- /dev/null
+++ b/clockvector.h
@@ -0,0 +1,20 @@
+#ifndef __CLOCKVECTOR_H__
+#define __CLOCKVECTOR_H__
+
+#include "threads.h"
+
+/* Forward declaration */
+class ModelAction;
+
+class ClockVector {
+public:
+	ClockVector(ClockVector *parent = NULL, ModelAction *act = NULL);
+	~ClockVector();
+	void merge(ClockVector *cv);
+	bool happens_before(ModelAction *act, thread_id_t id);
+private:
+	int *clock;
+	int num_threads;
+};
+
+#endif /* __CLOCKVECTOR_H__ */
diff --git a/libatomic.cc b/libatomic.cc
index f552d93..88d7fbf 100644
--- a/libatomic.cc
+++ b/libatomic.cc
@@ -11,9 +11,10 @@ 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_NONE));
-	return obj->value;
+	model->switch_to_master(new ModelAction(ATOMIC_READ, order, obj, value));
+	return value;
 }
 
 void atomic_init(struct atomic_object *obj, int value)
diff --git a/librace.cc b/librace.cc
index 42ed9c1..fa9a110 100644
--- a/librace.cc
+++ b/librace.cc
@@ -7,43 +7,47 @@
 void store_8(void *addr, uint8_t val)
 {
 	DEBUG("addr = %p, val = %" PRIu8 "\n", addr, val);
+	(*(uint8_t *)addr) = val;
 }
 
 void store_16(void *addr, uint16_t val)
 {
 	DEBUG("addr = %p, val = %" PRIu16 "\n", addr, val);
+	(*(uint16_t *)addr) = val;
 }
 
 void store_32(void *addr, uint32_t val)
 {
 	DEBUG("addr = %p, val = %" PRIu32 "\n", addr, val);
+	(*(uint32_t *)addr) = val;
 }
 
 void store_64(void *addr, uint64_t val)
 {
 	DEBUG("addr = %p, val = %" PRIu64 "\n", addr, val);
+	(*(uint64_t *)addr) = val;
 }
 
 uint8_t load_8(void *addr)
 {
 	DEBUG("addr = %p\n", addr);
-	return 0;
+	return *((uint8_t *)addr);
 }
 
 uint16_t load_16(void *addr)
 {
 	DEBUG("addr = %p\n", addr);
-	return 0;
+	return *((uint16_t *)addr);
 }
 
 uint32_t load_32(void *addr)
 {
 	DEBUG("addr = %p\n", addr);
-	return 0;
+	return *((uint32_t *)addr);
 }
 
 uint64_t load_64(void *addr)
 {
 	DEBUG("addr = %p\n", addr);
-	return 0;
+	return *((uint64_t *)addr);
 }
diff --git a/main.cc b/main.cc
index 9af745d..e456ac6 100644
--- a/main.cc
+++ b/main.cc
@@ -1,7 +1,4 @@
-#include <stdlib.h>
-
 #include "libthreads.h"
-#include "schedule.h"
 #include "common.h"
 #include "threads.h"
 
diff --git a/model.cc b/model.cc
index 51715d2..e068a08 100644
--- a/model.cc
+++ b/model.cc
@@ -41,21 +41,21 @@ void free_action_list(action_list_t *list)
 }
 
 ModelChecker::ModelChecker()
-{
-	/* First thread created will have id INITIAL_THREAD_ID */
-	this->next_thread_id = INITIAL_THREAD_ID;
-	used_sequence_numbers = 0;
+	:
 	/* Initialize default scheduler */
-	this->scheduler = new Scheduler();
-
-	num_executions = 0;
-	this->current_action = NULL;
-	this->exploring = NULL;
-	this->nextThread = THREAD_ID_T_NONE;
-
-	rootNode = new TreeNode();
-	currentNode = rootNode;
-	action_trace = new action_list_t();
+	scheduler(new Scheduler()),
+	/* First thread created will have id INITIAL_THREAD_ID */
+	next_thread_id(INITIAL_THREAD_ID),
+	used_sequence_numbers(0),
+
+	num_executions(0),
+	current_action(NULL),
+	exploring(NULL),
+	nextThread(THREAD_ID_T_NONE),
+	action_trace(new action_list_t()),
+	rootNode(new TreeNode()),
+	currentNode(rootNode)
+{
 }
 
 ModelChecker::~ModelChecker()
@@ -67,7 +67,7 @@ ModelChecker::~ModelChecker()
 
 	free_action_list(action_trace);
 
-	delete this->scheduler;
+	delete scheduler;
 	delete rootNode;
 }
 
@@ -83,6 +83,7 @@ void ModelChecker::reset_to_initial_state()
 	current_action = NULL;
 	next_thread_id = INITIAL_THREAD_ID;
 	used_sequence_numbers = 0;
+	nextThread = 0;
 	/* scheduler reset ? */
 }
 
@@ -120,10 +121,19 @@ thread_id_t ModelChecker::get_next_replay_thread()
 	ModelAction *next;
 	thread_id_t tid;
 
+	/* Have we completed exploring the preselected path? */
+	if (exploring == NULL)
+		return THREAD_ID_T_NONE;
+
+	/* Else, we are trying to replay an execution */
+	exploring->advance_state();
+
+	ASSERT(exploring->get_state() != NULL);
+
 	next = exploring->get_state();
 
 	if (next == exploring->get_diverge()) {
-		TreeNode *node = next->get_node();
+		TreeNode *node = next->get_treenode();
 
 		/* Reached divergence point; discard our current 'exploring' */
 		DEBUG("*** Discard 'Backtrack' object ***\n");
@@ -137,20 +147,6 @@ thread_id_t ModelChecker::get_next_replay_thread()
 	return tid;
 }
 
-thread_id_t ModelChecker::advance_backtracking_state()
-{
-	/* Have we completed exploring the preselected path? */
-	if (exploring == NULL)
-		return THREAD_ID_T_NONE;
-
-	/* Else, we are trying to replay an execution */
-	exploring->advance_state();
-
-	ASSERT(exploring->get_state() != NULL);
-
-	return get_next_replay_thread();
-}
-
 bool ModelChecker::next_execution()
 {
 	DBG();
@@ -167,7 +163,6 @@ bool ModelChecker::next_execution()
 	}
 
 	model->reset_to_initial_state();
-	nextThread = get_next_replay_thread();
 	return true;
 }
 
@@ -205,7 +200,7 @@ void ModelChecker::set_backtracking(ModelAction *act)
 	if (prev == NULL)
 		return;
 
-	node = prev->get_node();
+	node = prev->get_treenode();
 
 	while (t && !node->is_enabled(t))
 		t = t->get_parent();
@@ -240,18 +235,18 @@ Backtrack * ModelChecker::get_next_backtrack()
 
 void ModelChecker::check_current_action(void)
 {
-	ModelAction *next = this->current_action;
-
-	if (!next) {
+	ModelAction *curr = this->current_action;
+	current_action = NULL;
+	if (!curr) {
 		DEBUG("trying to push NULL action...\n");
 		return;
 	}
-	current_action = NULL;
-	nextThread = advance_backtracking_state();
-	next->set_node(currentNode);
-	set_backtracking(next);
-	currentNode = currentNode->explore_child(next);
-	this->action_trace->push_back(next);
+
+	nextThread = get_next_replay_thread();
+	curr->set_node(currentNode);
+	set_backtracking(curr);
+	currentNode = currentNode->explore_child(curr);
+	this->action_trace->push_back(curr);
 }
 
 void ModelChecker::print_summary(void)
diff --git a/model.h b/model.h
index d3b4205..1dc6a15 100644
--- a/model.h
+++ b/model.h
@@ -51,7 +51,6 @@ private:
 
 	ModelAction * get_last_conflict(ModelAction *act);
 	void set_backtracking(ModelAction *act);
-	thread_id_t advance_backtracking_state();
 	thread_id_t get_next_replay_thread();
 	Backtrack * get_next_backtrack();
 	void reset_to_initial_state();
diff --git a/nodestack.cc b/nodestack.cc
new file mode 100644
index 0000000..379fb3b
--- /dev/null
+++ b/nodestack.cc
@@ -0,0 +1,173 @@
+#include "nodestack.h"
+#include "action.h"
+#include "common.h"
+
+int Node::total_nodes = 0;
+
+Node::Node(ModelAction *act, Node *parent)
+	: action(act),
+	num_threads(parent ? parent->num_threads : 1),
+	explored_children(num_threads),
+	backtrack(num_threads)
+{
+	total_nodes++;
+	if (act && act->get_type() == THREAD_CREATE) {
+		num_threads++;
+		explored_children.resize(num_threads);
+		backtrack.resize(num_threads);
+	}
+}
+
+Node::~Node()
+{
+	if (action)
+		delete action;
+}
+
+void Node::print()
+{
+	if (action)
+		action->print();
+	else
+		printf("******** empty action ********\n");
+}
+
+bool Node::has_been_explored(thread_id_t tid)
+{
+	int id = id_to_int(tid);
+	return explored_children[id];
+}
+
+bool Node::backtrack_empty()
+{
+	unsigned int i;
+	for (i = 0; i < backtrack.size(); i++)
+		if (backtrack[i] == true)
+			return false;
+	return true;
+}
+
+void Node::explore_child(ModelAction *act)
+{
+	act->set_node(this);
+	explore(act->get_tid());
+}
+
+bool Node::set_backtrack(thread_id_t id)
+{
+	int i = id_to_int(id);
+	if (backtrack[i])
+		return false;
+	backtrack[i] = true;
+	return true;
+}
+
+thread_id_t Node::get_next_backtrack()
+{
+	/* TODO: find next backtrack */
+	unsigned int i;
+	for (i = 0; i < backtrack.size(); i++)
+		if (backtrack[i] == true)
+			break;
+	if (i >= backtrack.size())
+		return THREAD_ID_T_NONE;
+	backtrack[i] = false;
+	return int_to_id(i);
+}
+
+bool Node::is_enabled(Thread *t)
+{
+	return id_to_int(t->get_id()) < num_threads;
+}
+
+void Node::explore(thread_id_t tid)
+{
+	int i = id_to_int(tid);
+	backtrack[i] = false;
+	explored_children[i] = true;
+}
+
+static void clear_node_list(node_list_t *list, node_list_t::iterator start,
+					       node_list_t::iterator end)
+{
+	node_list_t::iterator it;
+
+	for (it = start; it != end; it++)
+		delete (*it);
+	list->erase(start, end);
+}
+
+NodeStack::NodeStack()
+{
+	node_list.push_back(new Node());
+	iter = node_list.begin();
+}
+
+NodeStack::~NodeStack()
+{
+	clear_node_list(&node_list, node_list.begin(), node_list.end());
+}
+
+void NodeStack::print()
+{
+	node_list_t::iterator it;
+	printf("............................................\n");
+	printf("NodeStack printing node_list:\n");
+	for (it = node_list.begin(); it != node_list.end(); it++) {
+		if (it == this->iter)
+			printf("vvv following action is the current iterator vvv\n");
+		(*it)->print();
+	}
+	printf("............................................\n");
+}
+
+ModelAction * NodeStack::explore_action(ModelAction *act)
+{
+	DBG();
+
+	ASSERT(!node_list.empty());
+
+	if (get_head()->has_been_explored(act->get_tid())) {
+		/* Discard duplicate ModelAction */
+		delete act;
+		iter++;
+	} else { /* Diverging from previous execution */
+		/* Clear out remainder of list */
+		node_list_t::iterator it = iter;
+		it++;
+		clear_node_list(&node_list, it, node_list.end());
+
+		/* Record action */
+		get_head()->explore_child(act);
+		node_list.push_back(new Node(act, get_head()));
+		iter++;
+	}
+	return (*iter)->get_action();
+}
+
+Node * NodeStack::get_head()
+{
+	if (node_list.empty())
+		return NULL;
+	return *iter;
+}
+
+Node * NodeStack::get_next()
+{
+	node_list_t::iterator it = iter;
+	if (node_list.empty()) {
+		DEBUG("Empty\n");
+		return NULL;
+	}
+	it++;
+	if (it == node_list.end()) {
+		DEBUG("At end\n");
+		return NULL;
+	}
+	return *it;
+}
+
+void NodeStack::reset_execution()
+{
+	iter = node_list.begin();
+}
diff --git a/nodestack.h b/nodestack.h
new file mode 100644
index 0000000..2fd84dd
--- /dev/null
+++ b/nodestack.h
@@ -0,0 +1,56 @@
+#ifndef __NODESTACK_H__
+#define __NODESTACK_H__
+
+#include <list>
+#include <vector>
+#include <cstddef>
+#include "threads.h"
+
+class ModelAction;
+
+class Node {
+public:
+	Node(ModelAction *act = NULL, Node *parent = NULL);
+	~Node();
+	/* return true = thread choice has already been explored */
+	bool has_been_explored(thread_id_t tid);
+	/* return true = backtrack set is empty */
+	bool backtrack_empty();
+	void explore_child(ModelAction *act);
+	/* return false = thread was already in backtrack */
+	bool set_backtrack(thread_id_t id);
+	thread_id_t get_next_backtrack();
+	bool is_enabled(Thread *t);
+	ModelAction * get_action() { return action; }
+
+	void print();
+
+	static int get_total_nodes() { return total_nodes; }
+private:
+	void explore(thread_id_t tid);
+
+	static int total_nodes;
+	ModelAction *action;
+	int num_threads;
+	std::vector<bool> explored_children;
+	std::vector<bool> backtrack;
+};
+
+typedef std::list<class Node *> node_list_t;
+
+class NodeStack {
+public:
+	NodeStack();
+	~NodeStack();
+	ModelAction * explore_action(ModelAction *act);
+	Node * get_head();
+	Node * get_next();
+	void reset_execution();
+
+	void print();
+private:
+	node_list_t node_list;
+	node_list_t::iterator iter;
+};
+
+#endif /* __NODESTACK_H__ */
diff --git a/threads.cc b/threads.cc
index 10ff3c5..9929774 100644
--- a/threads.cc
+++ b/threads.cc
@@ -1,7 +1,4 @@
-#include <stdlib.h>
-
 #include "libthreads.h"
-#include "schedule.h"
 #include "common.h"
 #include "threads.h"
 
diff --git a/userprog.c b/userprog.c
index 5598bfb..0948f0b 100644
--- a/userprog.c
+++ b/userprog.c
@@ -2,13 +2,17 @@
 
 #include "libthreads.h"
 #include "libatomic.h"
+#include "librace.h"
 
 static void a(atomic_int *obj)
 {
 	int i;
 	int ret;
 
-	for (i = 0; i < 7; i++) {
+	store_32(&i, 10);
+	printf("load 32 yields: %d\n", load_32(&i));
+
+	for (i = 0; i < 2; i++) {
 		printf("Thread %d, loop %d\n", thrd_current(), i);
 		switch (i  ) {
 		case 1:
@@ -16,8 +20,8 @@ static void a(atomic_int *obj)
 			printf("Read value: %d\n", ret);
 			break;
 		case 0:
-			atomic_store(obj, i);
-			printf("Write value: %d\n", i);
+			atomic_store(obj, i + 1);
+			printf("Write value: %d\n", i + 1);
 			break;
 		}
 	}