From: Brian Demsky <bdemsky@uci.edu>
Date: Mon, 8 Oct 2012 08:21:35 +0000 (-0700)
Subject: merge massive speedup with release sequence support...
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=b8b39c87557325a384faa45d0cae56a6f71f52b1

merge massive speedup with release sequence support...

Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker

Conflicts:
	schedule.cc
	schedule.h
---

b8b39c87557325a384faa45d0cae56a6f71f52b1
diff --cc model.cc
index 2c275679,8267377f..4f2719f3
--- a/model.cc
+++ b/model.cc
@@@ -166,20 -167,19 +170,24 @@@ Thread * ModelChecker::get_next_thread(
  			/* The next node will try to read from a different future value. */
  			tid = next->get_tid();
  			node_stack->pop_restofstack(2);
+ 		} else if (nextnode->increment_relseq_break()) {
+ 			/* The next node will try to resolve a release sequence differently */
+ 			tid = next->get_tid();
+ 			node_stack->pop_restofstack(2);
  		} else {
  			/* Make a different thread execute for next step */
 -			Node *node = nextnode->get_parent();
 -			tid = node->get_next_backtrack();
 +			scheduler->add_sleep(thread_map->get(id_to_int(next->get_tid())));
 +			tid = prevnode->get_next_backtrack();
 +			/* Make sure the backtracked thread isn't sleeping. */
 +			scheduler->remove_sleep(thread_map->get(id_to_int(tid)));
  			node_stack->pop_restofstack(1);
  			if (diverge==earliest_diverge) {
 -				earliest_diverge=node->get_action();
 +				earliest_diverge=prevnode->get_action();
  			}
  		}
 +		/* The correct sleep set is in the parent node. */
 +		execute_sleep_set();
 +
  		DEBUG("*** Divergence point ***\n");
  
  		diverge = NULL;
diff --cc nodestack.h
index 147b0048,cb281cad..803d2b8e
--- a/nodestack.h
+++ b/nodestack.h
@@@ -90,8 -90,12 +90,13 @@@ public
  	bool get_promise(unsigned int i);
  	bool increment_promise();
  	bool promise_empty();
 +	enabled_type_t *get_enabled_array() {return enabled_array;}
  
+ 	void add_relseq_break(const ModelAction *write);
+ 	const ModelAction * get_relseq_break();
+ 	bool increment_relseq_break();
+ 	bool relseq_break_empty();
+ 
  	void print();
  	void print_may_read_from();
  
diff --cc schedule.cc
index c5e58fe6,dd35237b..ea1d5820
--- a/schedule.cc
+++ b/schedule.cc
@@@ -21,47 -20,25 +21,58 @@@ void Scheduler::set_enabled(Thread *t, 
  	if (threadid>=enabled_len) {
  		enabled_type_t *new_enabled = (enabled_type_t *)snapshot_malloc(sizeof(enabled_type_t) * (threadid + 1));
  		memset(&new_enabled[enabled_len], 0, (threadid+1-enabled_len)*sizeof(enabled_type_t));
- 		if (is_enabled != NULL) {
- 			memcpy(new_enabled, is_enabled, enabled_len*sizeof(enabled_type_t));
- 			snapshot_free(is_enabled);
+ 		if (enabled != NULL) {
+ 			memcpy(new_enabled, enabled, enabled_len*sizeof(enabled_type_t));
+ 			snapshot_free(enabled);
  		}
- 		is_enabled=new_enabled;
+ 		enabled=new_enabled;
  		enabled_len=threadid+1;
  	}
- 	is_enabled[threadid]=enabled_status;
+ 	enabled[threadid]=enabled_status;
+ }
+ 
+ /**
+  * @brief Check if a Thread is currently enabled
+  * @param t The Thread to check
+  * @return True if the Thread is currently enabled
+  */
+ bool Scheduler::is_enabled(Thread *t) const
+ {
+ 	int id = id_to_int(t->get_id());
 -	return (id >= enabled_len) ? false : (enabled[id] == THREAD_ENABLED);
++	return (id >= enabled_len) ? false : (enabled[id] != THREAD_DISABLED);
 +}
 +
 +enabled_type_t Scheduler::get_enabled(Thread *t) {
- 	return is_enabled[id_to_int(t->get_id())];
++	return enabled[id_to_int(t->get_id())];
 +}
 +
 +void Scheduler::update_sleep_set(Node *n) {
 +	enabled_type_t *enabled_array=n->get_enabled_array();
 +	for(int i=0;i<enabled_len;i++) {
 +		if (enabled_array[i]==THREAD_SLEEP_SET) {
- 			is_enabled[i]=THREAD_SLEEP_SET;
++			enabled[i]=THREAD_SLEEP_SET;
 +		}
 +	}
 +}
 +
 +/**
 + * Add a Thread to the sleep set.
 + * @param t The Thread to add
 + */
 +void Scheduler::add_sleep(Thread *t)
 +{
 +	DEBUG("thread %d\n", id_to_int(t->get_id()));
 +	set_enabled(t, THREAD_SLEEP_SET);
 +}
 +
 +/**
 + * Remove a Thread from the sleep set.
 + * @param t The Thread to remove
 + */
 +void Scheduler::remove_sleep(Thread *t)
 +{
 +	DEBUG("thread %d\n", id_to_int(t->get_id()));
 +	set_enabled(t, THREAD_ENABLED);
  }
  
  /**
@@@ -120,7 -99,7 +133,7 @@@ Thread * Scheduler::next_thread(Thread 
  		int old_curr_thread = curr_thread_index;
  		while(true) {
  			curr_thread_index = (curr_thread_index+1) % enabled_len;
- 			if (is_enabled[curr_thread_index]==THREAD_ENABLED) {
 -			if (enabled[curr_thread_index]) {
++			if (enabled[curr_thread_index]==THREAD_ENABLED) {
  				t = model->get_thread(int_to_id(curr_thread_index));
  				break;
  			}
diff --cc schedule.h
index 3a54e8cf,3feddd90..72670590
--- a/schedule.h
+++ b/schedule.h
@@@ -30,11 -29,9 +30,13 @@@ public
  	Thread * next_thread(Thread *t);
  	Thread * get_current_thread() const;
  	void print() const;
- 	enabled_type_t * get_enabled() { return is_enabled; };
+ 	enabled_type_t * get_enabled() { return enabled; };
 +	void remove_sleep(Thread *t);
 +	void add_sleep(Thread *t);
 +	enabled_type_t get_enabled(Thread *t);
 +	void update_sleep_set(Node *n);
+ 	bool is_enabled(Thread *t) const;
+ 
  	SNAPSHOTALLOC
  private:
  	/** The list of available Threads that are not currently running */