From: Brian Norris <banorris@uci.edu>
Date: Wed, 12 Sep 2012 00:52:02 +0000 (-0700)
Subject: Merge branch 'demsky'
X-Git-Tag: pldi2013~223
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=50b95c3747f4fe79b2ab1a1a6fc303224e16e418

Merge branch 'demsky'

Branch cleaned up by Brian Norris
---

50b95c3747f4fe79b2ab1a1a6fc303224e16e418
diff --cc model.cc
index ba239b9,6f144ab..3e54a00
--- a/model.cc
+++ b/model.cc
@@@ -329,40 -356,26 +374,30 @@@ Thread * ModelChecker::check_current_ac
  			scheduler->wake(wake);
  		}
  		th->complete();
 +		break;
  	}
 -
 -	/* Deal with new thread */
 -	if (curr->get_type() == THREAD_START)
 +	case THREAD_START: {
  		check_promises(NULL, curr->get_cv());
 +		break;
 +	}
 +	default:
 +		break;
 +	}
  
- 	/* Assign reads_from values */
  	Thread *th = get_thread(curr->get_tid());
- 	uint64_t value = VALUE_NONE;
+ 
  	bool updated = false;
  	if (curr->is_read()) {
- 		const ModelAction *reads_from = curr->get_node()->get_read_from();
- 		if (reads_from != NULL) {
- 			value = reads_from->get_value();
- 			/* Assign reads_from, perform release/acquire synchronization */
- 			curr->read_from(reads_from);
- 			if (r_modification_order(curr,reads_from))
- 				updated = true;
- 		} else {
- 			/* Read from future value */
- 			value = curr->get_node()->get_future_value();
- 			curr->read_from(NULL);
- 			Promise *valuepromise = new Promise(curr, value);
- 			promises->push_back(valuepromise);
- 		}
- 	} else if (curr->is_write()) {
- 		if (w_modification_order(curr))
- 			updated = true;
- 		if (resolve_promises(curr))
- 			updated = true;
+ 		updated=process_read(curr, th, second_part_of_rmw);
+ 	}
+ 
+ 	if (curr->is_write()) {
+ 		bool updated_mod_order=w_modification_order(curr);
+ 		bool updated_promises=resolve_promises(curr);
+ 		updated=updated_mod_order|updated_promises;
+ 
+ 		mo_graph->commitChanges();
+ 		th->set_return_value(VALUE_NONE);
  	}
  
  	if (updated)
diff --cc model.h
index 1b6bb10,d73e457..c3e5830
--- a/model.h
+++ b/model.h
@@@ -103,9 -105,10 +105,10 @@@ private
  
  	bool take_step();
  
+ 	void check_recency(ModelAction *curr, bool already_added);
  	ModelAction * get_last_conflict(ModelAction *act);
  	void set_backtracking(ModelAction *act);
 -	Thread * get_next_replay_thread();
 +	Thread * get_next_thread(ModelAction *curr);
  	ModelAction * get_next_backtrack();
  	void reset_to_initial_state();
  	bool resolve_promises(ModelAction *curr);