bugfix: straighten out STL vector allocation (snapshotted vs. persistent)
authorBrian Norris <banorris@uci.edu>
Thu, 13 Sep 2012 22:42:21 +0000 (15:42 -0700)
committerBrian Norris <banorris@uci.edu>
Thu, 13 Sep 2012 22:46:33 +0000 (15:46 -0700)
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.

action.cc
cyclegraph.h
model.cc
model.h

index 205bedb..5d726a2 100644 (file)
--- 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]);
index 013a11a..81d7369 100644 (file)
@@ -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;
index d23e994..031f6a9 100644 (file)
--- 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 (file)
--- 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;