be even more aggressive about sleep sets...

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 4f2719f338c8afa9ba05d2f0835fd565bd6dfbd2..f8482cbf7b9db9eb9689a213c5de18cf3b583ad9 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),
@@ -179,7 +179,6 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr)
                        scheduler->add_sleep(thread_map->get(id_to_int(next->get_tid())));
                        tid = prevnode->get_next_backtrack();
                        /* Make sure the backtracked thread isn't sleeping. */
-                       scheduler->remove_sleep(thread_map->get(id_to_int(tid)));
                        node_stack->pop_restofstack(1);
                        if (diverge==earliest_diverge) {
                                earliest_diverge=prevnode->get_action();
@@ -213,6 +212,7 @@ void ModelChecker::execute_sleep_set() {
                        thr->set_state(THREAD_RUNNING);
                        scheduler->next_thread(thr);
                        Thread::swap(&system_context, thr);
+                       priv->current_action->set_sleep_flag();
                        thr->set_pending(priv->current_action);
                }
        }
@@ -346,7 +346,8 @@ void ModelChecker::set_backtracking(ModelAction *act)
        for(int i = low_tid; i < high_tid; i++) {
                thread_id_t tid = int_to_id(i);
 
-               if (!node->is_enabled(tid))
+               /* Don't backtrack into a point where the thread is disabled or sleeping. */
+               if (node->get_enabled_array()[i]!=THREAD_ENABLED)
                        continue;
        
                /* Check if this has been explored already */
@@ -1296,7 +1297,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 +1479,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 +1641,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];
@@ -1847,7 +1847,12 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
                                        act->print();
                                        curr->print();
                                }
-                               curr->get_node()->add_read_from(act);
+
+                               if (curr->get_sleep_flag()) {
+                                       if (sleep_can_read_from(curr, act))
+                                               curr->get_node()->add_read_from(act);
+                               } else
+                                       curr->get_node()->add_read_from(act);
                        }
 
                        /* Include at most one act per-thread that "happens before" curr */
@@ -1874,6 +1879,20 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
        ASSERT(initialized);
 }
 
+bool ModelChecker::sleep_can_read_from(ModelAction * curr, const ModelAction *write) {
+       while(true) {
+               Node *prevnode=write->get_node()->get_parent();
+               bool thread_sleep=prevnode->get_enabled_array()[id_to_int(curr->get_tid())]==THREAD_SLEEP_SET;
+               if (write->is_release()&&thread_sleep)
+                       return true;
+               if (!write->is_rmw())
+                       return false;
+               if (write->get_reads_from()==NULL)
+                       return true;
+               write=write->get_reads_from();
+       }
+}
+
 static void print_list(action_list_t *list)
 {
        action_list_t::iterator it;