+/** Checks promises in response to change in ClockVector Threads. */
+void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write) {
+ void * location = write->get_location();
+ for (unsigned int i = 0; i < promises->size(); i++) {
+ Promise *promise = (*promises)[i];
+ const ModelAction *act = promise->get_action();
+
+ //Is this promise on the same location?
+ if ( act->get_location() != location )
+ continue;
+
+ if ( act->get_tid()==tid) {
+ if (promise->get_write() == NULL ) {
+ promise->set_write(write);
+ }
+ if (mo_graph->checkPromise(write, promise)) {
+ failed_promise = true;
+ return;
+ }
+ }
+
+ //Don't do any lookups twice for the same thread
+ if (promise->has_sync_thread(tid))
+ continue;
+
+ if (mo_graph->checkReachable(promise->get_write(), write)) {
+ if (promise->increment_threads(tid)) {
+ failed_promise = true;
+ return;
+ }
+ }
+ }
+}
+