commit untested condvar code

[model-checker.git] / action.cc

diff --git a/action.cc b/action.cc
index 44a6d9ad6948c116e3305bd955e204825f01bc96..57058921d95726fb5c8f305b5316e34a80e6d39d 100644 (file)
--- a/action.cc
+++ b/action.cc
@@ -76,7 +76,7 @@ bool ModelAction::is_relseq_fixup() const
 
 bool ModelAction::is_mutex_op() const
 {
-       return type == ATOMIC_LOCK || type == ATOMIC_TRYLOCK || type == ATOMIC_UNLOCK;
+       return type == ATOMIC_LOCK || type == ATOMIC_TRYLOCK || type == ATOMIC_UNLOCK || type == ATOMIC_WAIT || type == ATOMIC_NOTIFY_ONE || type == ATOMIC_NOTIFY_ALL;
 }
 
 bool ModelAction::is_lock() const
@@ -84,6 +84,18 @@ bool ModelAction::is_lock() const
        return type == ATOMIC_LOCK;
 }
 
+bool ModelAction::is_wait() const {
+       return type == ATOMIC_WAIT;
+}
+
+bool ModelAction::is_notify() const {
+       return type==ATOMIC_NOTIFY_ONE || type==ATOMIC_NOTIFY_ALL;
+}
+
+bool ModelAction::is_notify_one() const {
+       return type==ATOMIC_NOTIFY_ONE;
+}
+
 bool ModelAction::is_unlock() const
 {
        return type == ATOMIC_UNLOCK;
@@ -250,6 +262,10 @@ bool ModelAction::is_conflicting_lock(const ModelAction *act) const
        if (act->is_unlock() && is_trylock() && value == VALUE_TRYSUCCESS)
                return true;
 
+       //Try to push a successful trylock past a wait
+       if (act->is_wait() && is_trylock() && value == VALUE_TRYSUCCESS)
+               return true;
+
        return false;
 }