From: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
Date: Sat, 26 Sep 2009 12:13:20 +0000 (-0400)
Subject: Cleanup promela code for wakeup verif
X-Git-Tag: v0.1~27
X-Git-Url: https://git.lttng.org./?a=commitdiff_plain;h=9b35d5dcf52a88861328f442ee0ef6812ec9b35b;p=userspace-rcu.git

Cleanup promela code for wakeup verif

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

diff --git a/formal-model/futex-wakeup/futex.ltl b/formal-model/futex-wakeup/futex.ltl
index 8718641..3d6842e 100644
--- a/formal-model/futex-wakeup/futex.ltl
+++ b/formal-model/futex-wakeup/futex.ltl
@@ -1 +1 @@
-([] <> !np_)
+([] <> ((!np_) || (!queue_has_entry)))
diff --git a/formal-model/futex-wakeup/futex.spin b/formal-model/futex-wakeup/futex.spin
index 9f6ddd4..1cb6442 100644
--- a/formal-model/futex-wakeup/futex.spin
+++ b/formal-model/futex-wakeup/futex.spin
@@ -98,13 +98,6 @@ active proctype waiter()
 				:: 1 ->
 					if
 					:: (fut == -1) ->
-						if
-						:: (queue == 0) ->
-progress_A:
-							skip;
-						:: else
-							skip;
-						fi;
 						skip;
 					:: else ->
 						break;
@@ -114,7 +107,7 @@ progress_A:
 				skip;
 			fi;
 		fi;
-progress_B:
+progress:
 		queue = 0;
 	od;
 }