From: Brian Demsky <bdemsky@uci.edu>
Date: Fri, 5 Oct 2012 00:37:38 +0000 (-0700)
Subject: Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker
X-Git-Tag: pldi2013~102
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=6f8de9e0f5697652fd20b2ecf149f96bfb572538;hp=-c;p=model-checker.git

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

6f8de9e0f5697652fd20b2ecf149f96bfb572538
diff --combined model.cc
index dd72fdb,e8b860c..bcc4298
--- a/model.cc
+++ b/model.cc
@@@ -34,7 -34,7 +34,7 @@@ ModelChecker::ModelChecker(struct model
  	obj_thrd_map(new HashTable<void *, std::vector<action_list_t>, uintptr_t, 4 >()),
  	promises(new std::vector<Promise *>()),
  	futurevalues(new std::vector<struct PendingFutureValue>()),
- 	pending_acq_rel_seq(new std::vector<ModelAction *>()),
+ 	pending_rel_seqs(new std::vector<struct release_seq *>()),
  	thrd_last_action(new std::vector<ModelAction *>(1)),
  	node_stack(new NodeStack()),
  	mo_graph(new CycleGraph()),
@@@ -65,7 -65,7 +65,7 @@@ ModelChecker::~ModelChecker(
  		delete (*promises)[i];
  	delete promises;
  
- 	delete pending_acq_rel_seq;
+ 	delete pending_rel_seqs;
  
  	delete thrd_last_action;
  	delete node_stack;
@@@ -208,7 -208,7 +208,7 @@@ bool ModelChecker::next_execution(
  	}
  
  	DEBUG("Number of acquires waiting on pending release sequences: %lu\n",
- 			pending_acq_rel_seq->size());
+ 			pending_rel_seqs->size());
  
  	if (isfinalfeasible() || DBG_ENABLED())
  		print_summary();
@@@ -760,7 -760,7 +760,7 @@@ bool ModelChecker::promises_expired() 
  /** @return whether the current partial trace must be a prefix of a
   * feasible trace. */
  bool ModelChecker::isfeasibleprefix() {
- 	return promises->size() == 0 && pending_acq_rel_seq->size() == 0;
+ 	return promises->size() == 0 && pending_rel_seqs->size() == 0;
  }
  
  /** @return whether the current partial trace is feasible. */
@@@ -1174,13 -1174,19 +1174,19 @@@ bool ModelChecker::thin_air_constraint_
   * @todo Finish lazy updating, when promises are fulfilled in the future
   * @param rf The action that might be part of a release sequence. Must be a
   * write.
-  * @param release_heads A pass-by-reference style return parameter.  After
+  * @param release_heads A pass-by-reference style return parameter. After
   * execution of this function, release_heads will contain the heads of all the
-  * relevant release sequences, if any exists
+  * relevant release sequences, if any exists with certainty
+  * @param pending A pass-by-reference style return parameter which is only used
+  * when returning false (i.e., uncertain). Returns most information regarding
+  * an uncertain release sequence, including any write operations that might
+  * break the sequence.
   * @return true, if the ModelChecker is certain that release_heads is complete;
   * false otherwise
   */
- bool ModelChecker::release_seq_heads(const ModelAction *rf, rel_heads_list_t *release_heads) const
+ bool ModelChecker::release_seq_heads(const ModelAction *rf,
+ 		rel_heads_list_t *release_heads,
+ 		struct release_seq *pending) const
  {
  	/* Only check for release sequences if there are no cycles */
  	if (mo_graph->checkForCycles())
@@@ -1209,6 -1215,7 +1215,7 @@@
  	};
  	if (!rf) {
  		/* read from future: need to settle this later */
+ 		pending->rf = NULL;
  		return false; /* incomplete */
  	}
  
@@@ -1238,6 -1245,8 +1245,8 @@@
  
  	ASSERT(rf->same_thread(release));
  
+ 	pending->writes.clear();
+ 
  	bool certain = true;
  	for (unsigned int i = 0; i < thrd_lists->size(); i++) {
  		if (id_to_int(rf->get_tid()) == (int)i)
@@@ -1281,14 -1290,21 +1290,21 @@@
  				/* release --mo-> act --mo--> rf */
  				return true; /* complete */
  			}
+ 			/* act may break release sequence */
+ 			pending->writes.push_back(act);
  			certain = false;
  		}
  		if (!future_ordered)
- 			return false; /* This thread is uncertain */
+ 			certain = false; /* This thread is uncertain */
  	}
  
- 	if (certain)
+ 	if (certain) {
  		release_heads->push_back(release);
+ 		pending->writes.clear();
+ 	} else {
+ 		pending->release = release;
+ 		pending->rf = rf;
+ 	}
  	return certain;
  }
  
@@@ -1307,10 -1323,14 +1323,14 @@@
  void ModelChecker::get_release_seq_heads(ModelAction *act, rel_heads_list_t *release_heads)
  {
  	const ModelAction *rf = act->get_reads_from();
+ 	struct release_seq *sequence = (struct release_seq *)snapshot_calloc(1, sizeof(struct release_seq));
+ 	sequence->acquire = act;
  
- 	if (!release_seq_heads(rf, release_heads)) {
+ 	if (!release_seq_heads(rf, release_heads, sequence)) {
  		/* add act to 'lazy checking' list */
- 		pending_acq_rel_seq->push_back(act);
+ 		pending_rel_seqs->push_back(sequence);
+ 	} else {
+ 		snapshot_free(sequence);
  	}
  }
  
@@@ -1330,9 -1350,10 +1350,10 @@@
  bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_queue)
  {
  	bool updated = false;
- 	std::vector<ModelAction *>::iterator it = pending_acq_rel_seq->begin();
- 	while (it != pending_acq_rel_seq->end()) {
- 		ModelAction *act = *it;
+ 	std::vector<struct release_seq *>::iterator it = pending_rel_seqs->begin();
+ 	while (it != pending_rel_seqs->end()) {
+ 		struct release_seq *pending = *it;
+ 		ModelAction *act = pending->acquire;
  
  		/* Only resolve sequences on the given location, if provided */
  		if (location && act->get_location() != location) {
@@@ -1343,7 -1364,7 +1364,7 @@@
  		const ModelAction *rf = act->get_reads_from();
  		rel_heads_list_t release_heads;
  		bool complete;
- 		complete = release_seq_heads(rf, &release_heads);
+ 		complete = release_seq_heads(rf, &release_heads, pending);
  		for (unsigned int i = 0; i < release_heads.size(); i++) {
  			if (!act->has_synchronized_with(release_heads[i])) {
  				if (act->synchronize_with(release_heads[i]))
@@@ -1370,10 -1391,12 +1391,12 @@@
  				}
  			}
  		}
- 		if (complete)
- 			it = pending_acq_rel_seq->erase(it);
- 		else
+ 		if (complete) {
+ 			it = pending_rel_seqs->erase(it);
+ 			snapshot_free(pending);
+ 		} else {
  			it++;
+ 		}
  	}
  
  	// If we resolved promises or data races, see if we have realized a data race.
@@@ -1516,10 -1539,6 +1539,10 @@@ bool ModelChecker::resolve_promises(Mod
  		} else
  			promise_index++;
  	}
 +
 +	//Check whether reading these writes has made threads unable to
 +	//resolve promises
 +
  	for(unsigned int i=0;i<threads_to_check.size();i++)
  		mo_check_promises(threads_to_check[i], write);
  
@@@ -1564,33 -1583,7 +1587,33 @@@ void ModelChecker::check_promises(threa
  	}
  }
  
 -/** Checks promises in response to change in ClockVector Threads. */
 +/** Checks promises in response to addition to modification order for threads.
 + * Definitions:
 + * pthread is the thread that performed the read that created the promise
 + * 
 + * pread is the read that created the promise
 + *
 + * pwrite is either the first write to same location as pread by
 + * pthread that is sequenced after pread or the value read by the
 + * first read to the same lcoation as pread by pthread that is
 + * sequenced after pread..
 + *
 + *	1. If tid=pthread, then we check what other threads are reachable
 + * through the mode order starting with pwrite.  Those threads cannot
 + * perform a write that will resolve the promise due to modification
 + * order constraints.
 + *
 + * 2. If the tid is not pthread, we check whether pwrite can reach the
 + * action write through the modification order.  If so, that thread
 + * cannot perform a future write that will resolve the promise due to
 + * modificatin order constraints.
 + *
 + *	@parem tid The thread that either read from the model action
 + *	write, or actually did the model action write.
 + *
 + *	@parem write The ModelAction representing the relevant write.
 + */
 +
  void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write) {
  	void * location = write->get_location();
  	for (unsigned int i = 0; i < promises->size(); i++) {
@@@ -1601,10 -1594,7 +1624,10 @@@
  		if ( act->get_location() != location )
  			continue;
  
 -		if ( act->get_tid()==tid) {
 +		//same thread as the promise
 +		if ( act->get_tid()==tid ) {
 +
 +			//do we have a pwrite for the promise, if not, set it
  			if (promise->get_write() == NULL ) {
  				promise->set_write(write);
  			}