projects / userspace-rcu.git / blobdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | inline | side by side
check wait free
[userspace-rcu.git] / ticketlock-testwait / lock_progress.ltl
diff --git a/ticketlock-testwait/lock_progress.ltl b/ticketlock-testwait/lock_progress.ltl
index 87186413c9ba4e59e8b4c3814696692c1f974418..4bc3952985ae1fe36195d2202f564d40a65e03e6 100644 (file)
--- a/ticketlock-testwait/lock_progress.ltl
+++ b/ticketlock-testwait/lock_progress.ltl
@@ -1 +1 @@
-([] <> !np_)
+(([] <> !np_) || (!(<> [] is_one_enabled -> [] <> last_is_one)))
Userspace RCU (urcu) for Linux
This page took 0.022025 seconds and 4 git commands to generate.