+/**
+ * @brief Synchronizes two actions
+ *
+ * When A synchronizes with B (or A --sw-> B), B inherits A's clock vector.
+ * This function performs the synchronization as well as providing other hooks
+ * for other checks along with synchronization.
+ *
+ * @param first The left-hand side of the synchronizes-with relation
+ * @param second The right-hand side of the synchronizes-with relation
+ * @return True if the synchronization was successful (i.e., was consistent
+ * with the execution order); false otherwise
+ */
+bool ModelChecker::synchronize(const ModelAction *first, ModelAction *second)
+{
+ if (*second < *first) {
+ set_bad_synchronization();
+ return false;
+ }
+ check_promises(first->get_tid(), second->get_cv(), first->get_cv());
+ return second->synchronize_with(first);
+}
+
+/**
+ * Check promises and eliminate potentially-satisfying threads when a thread is
+ * blocked (e.g., join, lock). A thread which is waiting on another thread can
+ * no longer satisfy a promise generated from that thread.
+ *
+ * @param blocker The thread on which a thread is waiting
+ * @param waiting The waiting thread
+ */
+void ModelChecker::thread_blocking_check_promises(Thread *blocker, Thread *waiting)
+{
+ for (unsigned int i = 0; i < promises->size(); i++) {
+ Promise *promise = (*promises)[i];
+ if (!promise->thread_is_available(waiting->get_id()))
+ continue;
+ for (unsigned int j = 0; j < promise->get_num_readers(); j++) {
+ ModelAction *reader = promise->get_reader(j);
+ if (reader->get_tid() != blocker->get_id())
+ continue;
+ if (promise->eliminate_thread(waiting->get_id())) {
+ /* Promise has failed */
+ priv->failed_promise = true;
+ } else {
+ /* Only eliminate the 'waiting' thread once */
+ return;
+ }
+ }
+ }
+}
+