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 205bedbf6f12806835a503975e95709162630070..5d726a2a0514f1c63c66fc3604ec8409fe0ba8cb 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]);

diff --git a/cyclegraph.h b/cyclegraph.h
index 013a11a793bd9f20971a881af2c104a59e3085ec..81d736962dcb6893c8ef213b9571454c24ac5ea6 100644 (file)
--- 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 d23e9946d8c32628f36c1a2685d07a7c9ea93b8e..031f6a935ec5701bdf72fdf2bdfe321e70712a28 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 cf03f0913c80db12e55fef5d3f91c7e75318c603..bd8791964baee4982c058c05c42d3678a7f621da 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;