mymemory: re-indent

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 4f2719f338c8afa9ba05d2f0835fd565bd6dfbd2..d77ba4bdb7982b11757642d7ddb253703ecf7109 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -32,10 +32,10 @@ ModelChecker::ModelChecker(struct model_params params) :
        obj_map(new HashTable<const void *, action_list_t, uintptr_t, 4>()),
        lock_waiters_map(new HashTable<const void *, action_list_t, uintptr_t, 4>()),
        obj_thrd_map(new HashTable<void *, std::vector<action_list_t>, uintptr_t, 4 >()),
-       promises(new std::vector<Promise *>()),
-       futurevalues(new std::vector<struct PendingFutureValue>()),
-       pending_rel_seqs(new std::vector<struct release_seq *>()),
-       thrd_last_action(new std::vector<ModelAction *>(1)),
+       promises(new std::vector< Promise *, SnapshotAlloc<Promise *> >()),
+       futurevalues(new std::vector< struct PendingFutureValue, SnapshotAlloc<struct PendingFutureValue> >()),
+       pending_rel_seqs(new std::vector< struct release_seq *, SnapshotAlloc<struct release_seq *> >()),
+       thrd_last_action(new std::vector< ModelAction *, SnapshotAlloc<ModelAction *> >(1)),
        node_stack(new NodeStack()),
        mo_graph(new CycleGraph()),
        failed_promise(false),
@@ -1296,7 +1296,6 @@ bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, con
  * "returns" two pieces of data: a pass-by-reference vector of @a release_heads
  * and a boolean representing certainty.
  *
- * @todo Finish lazy updating, when promises are fulfilled in the future
  * @param rf The action that might be part of a release sequence. Must be a
  * write.
  * @param release_heads A pass-by-reference style return parameter. After
@@ -1479,7 +1478,7 @@ void ModelChecker::get_release_seq_heads(ModelAction *act, rel_heads_list_t *rel
 bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_queue)
 {
        bool updated = false;
-       std::vector<struct release_seq *>::iterator it = pending_rel_seqs->begin();
+       std::vector< struct release_seq *, SnapshotAlloc<struct release_seq *> >::iterator it = pending_rel_seqs->begin();
        while (it != pending_rel_seqs->end()) {
                struct release_seq *pending = *it;
                ModelAction *act = pending->acquire;
@@ -1641,7 +1640,7 @@ ClockVector * ModelChecker::get_cv(thread_id_t tid)
 bool ModelChecker::resolve_promises(ModelAction *write)
 {
        bool resolved = false;
-  std::vector<thread_id_t> threads_to_check;
+       std::vector< thread_id_t, ModelAlloc<thread_id_t> > threads_to_check;
 
        for (unsigned int i = 0, promise_index = 0; promise_index < promises->size(); i++) {
                Promise *promise = (*promises)[promise_index];