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.

diff --git a/model.cc b/model.cc
index 9aaab916849f466d66578d42108e55c1567ba41f..6453d537a93fdb41b91fa995551611e61f69c2fa 100644 (file)
--- 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;
        }