From: Brian Norris <banorris@uci.edu>
Date: Thu, 13 Sep 2012 22:42:21 +0000 (-0700)
Subject: bugfix: straighten out STL vector allocation (snapshotted vs. persistent)
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=04f478b27a93b7838f58a8480b9e3e22d41688f8;p=cdsspec-compiler.git

bugfix: straighten out STL vector allocation (snapshotted vs. persistent)

When using a STL data structure allocated on the stack, we must make sure its
elements are allocated with the same allocator as the structure. For instance,
in a model-checking context, the stack is persistent (non-snapshotting), so any
stack-allocated std::vector should use the non-snapshotting allocator (i.e.,
MyAlloc).

At the same time, clarify CycleGraph and CycleNode classes by labelling them as
SNAPSHOTALLOC.
---

diff --git a/action.cc b/action.cc
index 205bedb..5d726a2 100644
--- a/action.cc
+++ b/action.cc
@@ -168,7 +168,7 @@ void ModelAction::read_from(const ModelAction *act)
 	ASSERT(cv);
 	reads_from = act;
 	if (act != NULL && this->is_acquire()) {
-		std::vector<const ModelAction *> release_heads;
+		std::vector< const ModelAction *, MyAlloc<const ModelAction *> > release_heads;
 		model->get_release_seq_heads(this, &release_heads);
 		for (unsigned int i = 0; i < release_heads.size(); i++)
 			synchronize_with(release_heads[i]);
diff --git a/cyclegraph.h b/cyclegraph.h
index 013a11a..81d7369 100644
--- a/cyclegraph.h
+++ b/cyclegraph.h
@@ -9,6 +9,8 @@
 #include <vector>
 #include <inttypes.h>
 
+#include "mymemory.h"
+
 class CycleNode;
 class ModelAction;
 
@@ -27,6 +29,7 @@ class CycleGraph {
 	void commitChanges();
 	void rollbackChanges();
 
+	SNAPSHOTALLOC
  private:
 	CycleNode * getNode(const ModelAction *);
 
@@ -61,6 +64,7 @@ class CycleNode {
 		hasRMW=NULL;
 	}
 
+	SNAPSHOTALLOC
  private:
 	/** @brief The ModelAction that this node represents */
 	const ModelAction *action;
diff --git a/model.cc b/model.cc
index d23e994..031f6a9 100644
--- a/model.cc
+++ b/model.cc
@@ -780,7 +780,7 @@ bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, con
  * false otherwise
  */
 bool ModelChecker::release_seq_head(const ModelAction *rf,
-                std::vector<const ModelAction *> *release_heads) const
+                std::vector< const ModelAction *, MyAlloc<const ModelAction *> > *release_heads) const
 {
 	if (!rf) {
 		/* read from future: need to settle this later */
@@ -886,7 +886,7 @@ bool ModelChecker::release_seq_head(const ModelAction *rf,
  * @see ModelChecker::release_seq_head
  */
 void ModelChecker::get_release_seq_heads(ModelAction *act,
-                std::vector<const ModelAction *> *release_heads)
+                std::vector< const ModelAction *, MyAlloc<const ModelAction *> > *release_heads)
 {
 	const ModelAction *rf = act->get_reads_from();
 	bool complete;
@@ -922,7 +922,7 @@ bool ModelChecker::resolve_release_sequences(void *location)
 	while (it != list->end()) {
 		ModelAction *act = *it;
 		const ModelAction *rf = act->get_reads_from();
-		std::vector<const ModelAction *> release_heads;
+		std::vector< const ModelAction *, MyAlloc<const ModelAction *> > release_heads;
 		bool complete;
 		complete = release_seq_head(rf, &release_heads);
 		for (unsigned int i = 0; i < release_heads.size(); i++) {
diff --git a/model.h b/model.h
index cf03f09..bd87919 100644
--- a/model.h
+++ b/model.h
@@ -85,7 +85,7 @@ public:
 	bool isfinalfeasible();
 	void check_promises(ClockVector *old_cv, ClockVector * merge_cv);
 	void get_release_seq_heads(ModelAction *act,
-	                std::vector<const ModelAction *> *release_heads);
+	                std::vector< const ModelAction *, MyAlloc<const ModelAction *> > *release_heads);
 	void finish_execution();
 	bool isfeasibleprefix();
 	void set_assert() {asserted=true;}
@@ -133,7 +133,7 @@ private:
 	bool r_modification_order(ModelAction *curr, const ModelAction *rf);
 	bool w_modification_order(ModelAction *curr);
 	bool release_seq_head(const ModelAction *rf,
-	                std::vector<const ModelAction *> *release_heads) const;
+	                std::vector< const ModelAction *, MyAlloc<const ModelAction *> > *release_heads) const;
 	bool resolve_release_sequences(void *location);
 
 	ModelAction *diverge;