ticketlock model: state-space simplication

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>

diff --git a/ticketlock/mem-progress.spin b/ticketlock/mem-progress.spin
index dad43a45062a90e307b9b00c44d0eafe66bc49d3..b7395413dea110b4006e50313168579b9eebcbea 100644 (file)
--- a/ticketlock/mem-progress.spin
+++ b/ticketlock/mem-progress.spin
@@ -45,15 +45,8 @@ inline spin_lock(lock, ticket)
                lock = lock + HIGH_HALF_INC;    /* overflow expected */
        }
 
-       do
-       :: 1 ->
-               if
-               :: (LOW_HALF(lock) == ticket) ->
-                       break;
-               :: else ->
-                       skip;
-               fi;
-       od;
+       /* busy-wait */
+       LOW_HALF(lock) == ticket -> 1;
 }
 
 inline spin_unlock(lock)
@@ -66,9 +59,9 @@ proctype proc_A()
        byte ticket;
 
        do
-       :: 1 ->
-progress_A:
+       :: 
                spin_lock(lock, ticket);
+progress_A:
                refcount = refcount + 1;
                refcount = refcount - 1;
                spin_unlock(lock);
@@ -80,8 +73,7 @@ proctype proc_B()
        byte ticket;
 
        do
-       :: 1 ->
-               spin_lock(lock, ticket);
+       ::      spin_lock(lock, ticket);
                refcount = refcount + 1;
                refcount = refcount - 1;
                spin_unlock(lock);

diff --git a/ticketlock/mem.spin b/ticketlock/mem.spin
index 445ee9a6d4193da200ebbf810d2aeb91088b871a..59acfcf054dbb5ac1ae7ad556a315c9b31da88ce 100644 (file)
--- a/ticketlock/mem.spin
+++ b/ticketlock/mem.spin
@@ -44,15 +44,8 @@ inline spin_lock(lock, ticket)
                lock = lock + HIGH_HALF_INC;    /* overflow expected */
        }
 
-       do
-       :: 1 ->
-               if
-               :: (LOW_HALF(lock) == ticket) ->
-                       break;
-               :: else ->
-                       skip;
-               fi;
-       od;
+       /* busy-wait */
+       LOW_HALF(lock) == ticket -> 1;
 }
 
 inline spin_unlock(lock)
@@ -65,8 +58,7 @@ proctype proc_X()
        byte ticket;
 
        do
-       :: 1->
-               spin_lock(lock, ticket);
+       ::      spin_lock(lock, ticket);
                refcount = refcount + 1;
                refcount = refcount - 1;
                spin_unlock(lock);