From: Brian Demsky <bdemsky@uci.edu>
Date: Wed, 18 Jul 2012 05:03:01 +0000 (-0700)
Subject: model: add support for modification orders
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=21c976cef707ef9ccd33ec72f07a297b4cec057d;p=cdsspec-compiler.git

model: add support for modification orders

This update adds support for modification orders and kills the bogus executions
seen before...

[Updated, split by Brian Norris]
---

diff --git a/main.cc b/main.cc
index 339b85e..cbf93b6 100644
--- a/main.cc
+++ b/main.cc
@@ -31,6 +31,8 @@ static int thread_system_next(void) {
 			ASSERT(false);
 	}
 	next = model->scheduler->next_thread();
+	if (!model->isfeasible())
+		return 1;
 	if (next)
 		next->set_state(THREAD_RUNNING);
 	DEBUG("(%d, %d)\n", curr ? curr->get_id() : -1, next ? next->get_id() : -1);
diff --git a/model.cc b/model.cc
index e9d1f1d..3180991 100644
--- a/model.cc
+++ b/model.cc
@@ -7,6 +7,7 @@
 #include "snapshot-interface.h"
 #include "common.h"
 #include "clockvector.h"
+#include "cyclegraph.h"
 
 #define INITIAL_THREAD_ID	0
 
@@ -31,7 +32,8 @@ ModelChecker::ModelChecker()
 	obj_thrd_map(new std::map<void *, std::vector<action_list_t> >()),
 	thrd_last_action(new std::vector<ModelAction *>(1)),
 	node_stack(new NodeStack()),
-	next_backtrack(NULL)
+	next_backtrack(NULL),
+	cyclegraph(new CycleGraph())
 {
 }
 
@@ -49,6 +51,7 @@ ModelChecker::~ModelChecker()
 	delete thrd_last_action;
 	delete node_stack;
 	delete scheduler;
+	delete cyclegraph;
 }
 
 /**
@@ -279,8 +282,6 @@ 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? */
@@ -291,8 +292,80 @@ void ModelChecker::check_current_action(void)
 		value = reads_from->get_value();
 		/* Assign reads_from, perform release/acquire synchronization */
 		curr->read_from(reads_from);
+		r_modification_order(curr,reads_from);
+	} else if (curr->is_write()) {
+		w_modification_order(curr);
 	}
+
 	th->set_return_value(value);
+
+	/* Add action to list last.  */
+	add_action_to_lists(curr);
+}
+
+bool ModelChecker::isfeasible() {
+	return !cyclegraph->checkForCycles();
+}
+
+void ModelChecker::r_modification_order(ModelAction * curr, const ModelAction *rf) {
+	std::vector<action_list_t> *thrd_lists = &(*obj_thrd_map)[curr->get_location()];
+	unsigned int i;
+	ASSERT(curr->is_read());
+
+	/* Iterate over all threads */
+	for (i = 0; i < thrd_lists->size(); i++) {
+		/* Iterate over actions in thread, starting from most recent */
+		action_list_t *list = &(*thrd_lists)[i];
+		action_list_t::reverse_iterator rit;
+		for (rit = list->rbegin(); rit != list->rend(); rit++) {
+			ModelAction *act = *rit;
+
+			/* Include at most one act per-thread that "happens before" curr */
+			if (act->happens_before(curr)) {
+				if (act->is_read()) {
+					const ModelAction * prevreadfrom=act->get_reads_from();
+					if (rf!=prevreadfrom)
+						cyclegraph->addEdge(rf, prevreadfrom);
+				} else if (rf!=act) {
+					cyclegraph->addEdge(rf, act);
+				}
+				break;
+			}
+		}
+	}
+}
+
+void ModelChecker::w_modification_order(ModelAction * curr) {
+	std::vector<action_list_t> *thrd_lists = &(*obj_thrd_map)[curr->get_location()];
+	unsigned int i;
+	ASSERT(curr->is_write());
+
+	if (curr->is_seqcst()) {
+		/* We have to at least see the last sequentially consistent write,
+			 so we are initialized. */
+		ModelAction * last_seq_cst=get_last_seq_cst(curr->get_location());
+		if (last_seq_cst!=NULL)
+			cyclegraph->addEdge(curr, last_seq_cst);
+	}
+
+	/* Iterate over all threads */
+	for (i = 0; i < thrd_lists->size(); i++) {
+		/* Iterate over actions in thread, starting from most recent */
+		action_list_t *list = &(*thrd_lists)[i];
+		action_list_t::reverse_iterator rit;
+		for (rit = list->rbegin(); rit != list->rend(); rit++) {
+			ModelAction *act = *rit;
+
+			/* Include at most one act per-thread that "happens before" curr */
+			if (act->happens_before(curr)) {
+				if (act->is_read()) {
+					cyclegraph->addEdge(curr, act->get_reads_from());
+				} else
+					cyclegraph->addEdge(curr, act);
+				break;
+			}
+		}
+	}
 }
 
 /**
@@ -446,6 +519,8 @@ void ModelChecker::print_summary(void)
 	printf("\n");
 	printf("Number of executions: %d\n", num_executions);
 	printf("Total nodes created: %d\n", node_stack->get_total_nodes());
+	if (!isfeasible())
+		printf("INFEASIBLE EXECUTION!\n");
 
 	scheduler->print();
 
diff --git a/model.h b/model.h
index 2093bf4..4c0af0a 100644
--- a/model.h
+++ b/model.h
@@ -21,6 +21,7 @@
 
 /* Forward declaration */
 class NodeStack;
+class CycleGraph;
 
 /** @brief The central structure for model-checking */
 class ModelChecker {
@@ -55,6 +56,7 @@ public:
 	int switch_to_master(ModelAction *act);
 	ClockVector * get_cv(thread_id_t tid);
 	bool next_execution();
+	bool isfeasible();
 
 	MEMALLOC
 private:
@@ -81,6 +83,9 @@ private:
 	ModelAction * get_parent_action(thread_id_t tid);
 	ModelAction * get_last_seq_cst(const void *location);
 	void build_reads_from_past(ModelAction *curr);
+	void r_modification_order(ModelAction * curr, const ModelAction *rf);
+	void w_modification_order(ModelAction * curr);
+
 
 	ModelAction *current_action;
 	ModelAction *diverge;
@@ -98,6 +103,7 @@ private:
 	std::vector<ModelAction *> *thrd_last_action;
 	NodeStack *node_stack;
 	ModelAction *next_backtrack;
+	CycleGraph * cyclegraph;
 };
 
 extern ModelChecker *model;