From: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
Date: Wed, 14 Oct 2009 15:07:18 +0000 (-0400)
Subject: check wait free
X-Git-Url: http://git.liburcu.org/?p=userspace-rcu.git;a=commitdiff_plain;h=6dc4684a347695670803a70b7e50986fb75ec0ec

check wait free

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
---

diff --git a/ticketlock-testwait/DEFINES b/ticketlock-testwait/DEFINES
index 4eb5315..6997f17 100644
--- a/ticketlock-testwait/DEFINES
+++ b/ticketlock-testwait/DEFINES
@@ -1 +1,3 @@
 #define refcount_gt_one (refcount > 1)
+#define is_one_enabled	(enabled(1))
+#define last_is_one	(_last == 1)
diff --git a/ticketlock-testwait/lock_progress.ltl b/ticketlock-testwait/lock_progress.ltl
index 8718641..4bc3952 100644
--- a/ticketlock-testwait/lock_progress.ltl
+++ b/ticketlock-testwait/lock_progress.ltl
@@ -1 +1 @@
-([] <> !np_)
+(([] <> !np_) || (!(<> [] is_one_enabled -> [] <> last_is_one)))