From: Brian Norris <banorris@uci.edu>
Date: Fri, 7 Sep 2012 20:12:46 +0000 (-0700)
Subject: model: maintain a count of the pending lazy synchronizations
X-Git-Tag: pldi2013~228
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=ef196e91ff5e0b6b50f926e7dcc81a5c9dbcb846

model: maintain a count of the pending lazy synchronizations

lazy_sync_size should be the sum of the size of all the lists in
lazy_sync_with_release.
---

diff --git a/model.cc b/model.cc
index 43530fe..36b7b44 100644
--- a/model.cc
+++ b/model.cc
@@ -39,6 +39,8 @@ ModelChecker::ModelChecker(struct model_params params) :
 	priv = (struct model_snapshot_members *)calloc(1, sizeof(*priv));
 	/* First thread created will have id INITIAL_THREAD_ID */
 	priv->next_thread_id = INITIAL_THREAD_ID;
+
+	lazy_sync_size = &priv->lazy_sync_size;
 }
 
 /** @brief Destructor */
@@ -372,9 +374,8 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 
 /** @returns whether the current partial trace must be a prefix of a
  * feasible trace. */
-
 bool ModelChecker::isfeasibleprefix() {
-	return promises->size()==0;
+	return promises->size() == 0 && *lazy_sync_size == 0;
 }
 
 /** @returns whether the current partial trace is feasible. */
@@ -665,6 +666,7 @@ void ModelChecker::get_release_seq_heads(ModelAction *act,
 		std::list<ModelAction *> *list;
 		list = lazy_sync_with_release->get_safe_ptr(act->get_location());
 		list->push_back(act);
+		(*lazy_sync_size)++;
 	}
 }
 
@@ -711,9 +713,10 @@ bool ModelChecker::resolve_release_sequences(void *location)
 					propagate->synchronize_with(act);
 			}
 		}
-		if (complete)
+		if (complete) {
 			it = list->erase(it);
-		else
+			(*lazy_sync_size)--;
+		} else
 			it++;
 	}
 
diff --git a/model.h b/model.h
index 9762eb0..b2f7897 100644
--- a/model.h
+++ b/model.h
@@ -39,6 +39,9 @@ struct model_snapshot_members {
 	modelclock_t used_sequence_numbers;
 	Thread *nextThread;
 	ModelAction *next_backtrack;
+
+	/** @see ModelChecker::lazy_sync_size */
+	unsigned int lazy_sync_size;
 };
 
 /** @brief The central structure for model-checking */
@@ -142,6 +145,14 @@ private:
 	 */
 	HashTable<void *, std::list<ModelAction *>, uintptr_t, 4> *lazy_sync_with_release;
 
+	/**
+	 * Represents the total size of the
+	 * ModelChecker::lazy_sync_with_release lists. This count should be
+	 * snapshotted, so it is actually a pointer to a location within
+	 * ModelChecker::priv
+	 */
+	unsigned int *lazy_sync_size;
+
 	std::vector<ModelAction *> *thrd_last_action;
 	NodeStack *node_stack;