From d2985e8129a69c7fb28c080272988485830c2bd9 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Wed, 23 Jan 2013 18:47:53 -0800 Subject: [PATCH] model: modify promises on THREAD_{CREATE,FINISH} When a thread is created it *must* pass its promise satisfiability to its children. When a thread finishes, we should remove it from all promises. This can help prune a search early, if some read was depending only on the finishing thread: we can then declare an unresolved promise. --- model.cc | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/model.cc b/model.cc index 9aaab91..6453d53 100644 --- a/model.cc +++ b/model.cc @@ -968,6 +968,12 @@ bool ModelChecker::process_thread_action(ModelAction *curr) case THREAD_CREATE: { Thread *th = curr->get_thread_operand(); th->set_creation(curr); + /* Promises can be satisfied by children */ + for (unsigned int i = 0; i < promises->size(); i++) { + Promise *promise = (*promises)[i]; + if (promise->thread_is_available(curr->get_tid())) + promise->add_thread(th->get_id()); + } break; } case THREAD_JOIN: { @@ -984,6 +990,13 @@ bool ModelChecker::process_thread_action(ModelAction *curr) scheduler->wake(get_thread(act)); } th->complete(); + /* Completed thread can't satisfy promises */ + for (unsigned int i = 0; i < promises->size(); i++) { + Promise *promise = (*promises)[i]; + if (promise->thread_is_available(th->get_id())) + if (promise->eliminate_thread(th->get_id())) + priv->failed_promise = true; + } updated = true; /* trigger rel-seq checks */ break; } -- 2.34.1