From: Brian Norris <banorris@uci.edu>
Date: Wed, 3 Oct 2012 20:54:22 +0000 (-0700)
Subject: Merge remote-tracking branch 'origin/master'
X-Git-Tag: pldi2013~107^2~8
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=81ea453e58cbb85fddff3aa8919dfbc59c3140eb;hp=-c;p=model-checker.git

Merge remote-tracking branch 'origin/master'
---

81ea453e58cbb85fddff3aa8919dfbc59c3140eb
diff --combined model.cc
index 73d212d,c9353db..39a7c21
--- a/model.cc
+++ b/model.cc
@@@ -12,7 -12,6 +12,7 @@@
  #include "promise.h"
  #include "datarace.h"
  #include "mutex.h"
 +#include "threads.h"
  
  #define INITIAL_THREAD_ID	0
  
@@@ -100,12 -99,6 +100,12 @@@ int ModelChecker::get_num_threads(
  	return priv->next_thread_id;
  }
  
 +/** @return The currently executing Thread. */
 +Thread * ModelChecker::get_current_thread()
 +{
 +	return scheduler->get_current_thread();
 +}
 +
  /** @return a sequence number for a new ModelAction */
  modelclock_t ModelChecker::get_next_seq_num()
  {
@@@ -941,7 -934,11 +941,11 @@@ bool ModelChecker::r_modification_order
  					}
  				} else {
  					const ModelAction *prevreadfrom = act->get_reads_from();
- 					if (prevreadfrom != NULL && rf != prevreadfrom) {
+ 					//if the previous read is unresolved, keep going...
+ 					if (prevreadfrom == NULL)
+ 						continue;
+ 
+ 					if (rf != prevreadfrom) {
  						mo_graph->addEdge(prevreadfrom, rf);
  						added = true;
  					}
@@@ -1066,14 -1063,22 +1070,22 @@@ bool ModelChecker::w_modification_order
  			ModelAction *act = *rit;
  			if (act == curr) {
  				/*
- 				 * If RMW, we already have all relevant edges,
- 				 * so just skip to next thread.
- 				 * If normal write, we need to look at earlier
- 				 * actions, so continue processing list.
+ 				 * 1) If RMW and it actually read from something, then we
+ 				 * already have all relevant edges, so just skip to next
+ 				 * thread.
+ 				 * 
+ 				 * 2) If RMW and it didn't read from anything, we should
+ 				 * whatever edge we can get to speed up convergence.
+ 				 *
+ 				 * 3) If normal write, we need to look at earlier actions, so
+ 				 * continue processing list.
  				 */
- 				if (curr->is_rmw())
- 					break;
- 				else
+ 				if (curr->is_rmw()) {
+ 					if (curr->get_reads_from()!=NULL)
+ 						break;
+ 					else 
+ 						continue;
+ 				} else
  					continue;
  			}
  
@@@ -1090,8 -1095,12 +1102,12 @@@
  				 */
  				if (act->is_write())
  					mo_graph->addEdge(act, curr);
- 				else if (act->is_read() && act->get_reads_from() != NULL)
+ 				else if (act->is_read()) { 
+ 					//if previous read accessed a null, just keep going
+ 					if (act->get_reads_from() == NULL)
+ 						continue;
  					mo_graph->addEdge(act->get_reads_from(), curr);
+ 				}
  				added = true;
  				break;
  			} else if (act->is_read() && !act->is_synchronizing(curr) &&
@@@ -1635,7 -1644,8 +1651,8 @@@ void ModelChecker::dumpGraph(char *file
  		ModelAction *action=*it;
  		if (action->is_read()) {
  			fprintf(file, "N%u [label=\"%u, T%u\"];\n", action->get_seq_number(),action->get_seq_number(), action->get_tid());
- 			fprintf(file, "N%u -> N%u[label=\"rf\", color=red];\n", action->get_seq_number(), action->get_reads_from()->get_seq_number());
+ 			if (action->get_reads_from()!=NULL)
+ 				fprintf(file, "N%u -> N%u[label=\"rf\", color=red];\n", action->get_seq_number(), action->get_reads_from()->get_seq_number());
  		}
  		if (thread_array[action->get_tid()] != NULL) {
  			fprintf(file, "N%u -> N%u[label=\"sb\", color=blue];\n", thread_array[action->get_tid()]->get_seq_number(), action->get_seq_number());
@@@ -1691,35 -1701,12 +1708,35 @@@ void ModelChecker::remove_thread(Threa
  	scheduler->remove_thread(t);
  }
  
 +/**
 + * @brief Get a Thread reference by its ID
 + * @param tid The Thread's ID
 + * @return A Thread reference
 + */
 +Thread * ModelChecker::get_thread(thread_id_t tid)
 +{
 +	return thread_map->get(id_to_int(tid));
 +}
 +
 +/**
 + * @brief Get a reference to the Thread in which a ModelAction was executed
 + * @param act The ModelAction
 + * @return A Thread reference
 + */
 +Thread * ModelChecker::get_thread(ModelAction *act)
 +{
 +	return get_thread(act->get_tid());
 +}
 +
  /**
   * Switch from a user-context to the "master thread" context (a.k.a. system
   * context). This switch is made with the intention of exploring a particular
   * model-checking action (described by a ModelAction object). Must be called
   * from a user-thread context.
 - * @param act The current action that will be explored. Must not be NULL.
 + *
 + * @param act The current action that will be explored. May be NULL only if
 + * trace is exiting via an assertion (see ModelChecker::set_assert and
 + * ModelChecker::has_asserted).
   * @return Return status from the 'swap' call (i.e., success/fail, 0/-1)
   */
  int ModelChecker::switch_to_master(ModelAction *act)