update

[urcu.git] / ticketlock-testwait / mem-progress.spin

diff --git a/ticketlock-testwait/mem-progress.spin b/ticketlock-testwait/mem-progress.spin
index 818f445a74872642af1cadfd92f5998ba7e62b34..8329f6b8cbfd18343672b51c02d62c5ff6d80142 100644 (file)
--- a/ticketlock-testwait/mem-progress.spin
+++ b/ticketlock-testwait/mem-progress.spin
@@ -40,6 +40,10 @@ byte refcount = 0;
 
 #define need_pause()   (_pid == 2)
 
+/*
+ * do_pause() disabled:
+ * get similar effect by disabling weak fairness.
+ */
 /*
  * Test weak fairness by either not pausing or cycling for any number of
  * steps, or forever.
@@ -54,15 +58,11 @@ inline do_pause()
 {
        if
        :: need_pause() ->
-               if
+               do
                :: 1 ->
-                       do
-                       :: 1 ->
-                               skip;
-                       od;
-               :: 1 -> skip;
-               fi;
-       :: else ->
+                       skip;
+               od;
+       :: 1 ->
                skip;
        fi;
 }
@@ -110,10 +110,11 @@ proctype proc_B()
 
        do
        :: 1 ->
-               do_pause();
+progress_B:
+               //do_pause();
                spin_lock(lock, ticket);
                refcount = refcount + 1;
-               do_pause();
+               //do_pause();
                refcount = refcount - 1;
                spin_unlock(lock);
        od;