X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=execution.cc;h=e01181af486e3b518d2bddcb7b78003f7c9b6a68;hb=13a5122212f76cf215e0d704b7b46ddfc892b26b;hp=e2b690e1b6f95fca1f88c432cfac3036ba1b28c0;hpb=c76c1859f273b58b2fb3b39c8abca2159250905c;p=model-checker.git diff --git a/execution.cc b/execution.cc index e2b690e..e01181a 100644 --- a/execution.cc +++ b/execution.cc @@ -264,6 +264,14 @@ bool ModelExecution::is_deadlocked() const return blocking_threads; } +/** + * @brief Check if we are yield-blocked + * + * A program can be "yield-blocked" if all threads are ready to execute a + * yield. + * + * @return True if the program is yield-blocked; false otherwise + */ bool ModelExecution::is_yieldblocked() const { if (!params->yieldblock) @@ -1197,9 +1205,10 @@ void ModelExecution::thread_blocking_check_promises(Thread *blocker, Thread *wai /** * @brief Check whether a model action is enabled. * - * Checks whether a lock or join operation would be successful (i.e., is the - * lock already locked, or is the joined thread already complete). If not, put - * the action in a waiter list. + * Checks whether an operation would be successful (i.e., is a lock already + * locked, or is the joined thread already complete). + * + * For yield-blocking, yields are never enabled. * * @param curr is the ModelAction to check whether it is enabled. * @return a bool that indicates whether the action is enabled.