Fix standard (no remote barrier) parity flip bug

[urcu.git] / formal-model / urcu-controldataflow / urcu.spin

diff --git a/formal-model/urcu-controldataflow/urcu.spin b/formal-model/urcu-controldataflow/urcu.spin
index 484205a1dd999a9fd6c97f214e964b9aa2a884ff..44bbe523e153abfe52c39ee3eac957a4b7f22f46 100644 (file)
--- a/formal-model/urcu-controldataflow/urcu.spin
+++ b/formal-model/urcu-controldataflow/urcu.spin
@@ -243,7 +243,6 @@ inline smp_mb(i, j)
        }
 }
 
-
 #ifdef REMOTE_BARRIERS
 
 bit reader_barrier[NR_READERS];
@@ -269,32 +268,53 @@ inline smp_mb_recv(i, j)
        :: (reader_barrier[get_readerid()] == 1) ->
                smp_mb(i, j);
                reader_barrier[get_readerid()] = 0;
-       :: 1 -> skip;
+       :: 1 ->
+       /*
+        * Busy-looping waiting for other barrier requests are not considered as
+        * non-progress.
+        */
+#ifdef READER_PROGRESS
+progress_reader2:
+#endif
+               skip;
        :: 1 -> break;
        od;
 }
 
-inline smp_mb_send(i, j)
-{
-       smp_mb(i, j);
-       i = 0;
-       do
-       :: i < NR_READERS ->
-               reader_barrier[i] = 1;
-               do
-               :: (reader_barrier[i] == 1) -> skip;
-               :: (reader_barrier[i] == 0) -> break;
-               od;
-               i++;
-       :: i >= NR_READERS ->
-               break
-       od;
-       smp_mb(i, j);
+#ifdef WRITER_PROGRESS
+#define PROGRESS_LABEL(progressid)     progress_writer_progid_##progressid:
+#else
+#define PROGRESS_LABEL(progressid)
+#endif
+
+#define smp_mb_send(i, j, progressid)                                          \
+{                                                                              \
+       smp_mb(i, j);                                                           \
+       i = 0;                                                                  \
+       do                                                                      \
+       :: i < NR_READERS ->                                                    \
+               reader_barrier[i] = 1;                                          \
+               do                                                              \
+               :: (reader_barrier[i] == 1) ->                                  \
+               /*                                                              \
+                * Busy-looping waiting for reader barrier handling is of little\
+                * interest, given the reader has the ability to totally ignore \
+                * barrier requests.                                            \
+                */                                                             \
+PROGRESS_LABEL(progressid)                                                     \
+                       skip;                                                   \
+               :: (reader_barrier[i] == 0) -> break;                           \
+               od;                                                             \
+               i++;                                                            \
+       :: i >= NR_READERS ->                                                   \
+               break                                                           \
+       od;                                                                     \
+       smp_mb(i, j);                                                           \
 }
 
 #else
 
-#define smp_mb_send    smp_mb
+#define smp_mb_send(i, j, progressid)  smp_mb(i, j)
 #define smp_mb_reader  smp_mb
 #define smp_mb_recv(i, j)
 
@@ -592,7 +612,7 @@ non_atomic3_end:
 
                goto non_atomic3_skip;
 non_atomic3:
-               smp_mb_recv(i, j);      
+               smp_mb_recv(i, j);
                goto non_atomic3_end;
 non_atomic3_skip:
 
@@ -841,6 +861,11 @@ active proctype urcu_writer()
        byte i, j;
        byte tmp, tmp2, tmpa;
        byte old_gen;
+       byte cur_gp_val = 0;    /*
+                                * Keep a local trace of the current parity so
+                                * we don't add non-existing dependencies on the global
+                                * GP update. Needed to test single flip case.
+                                */
 
        wait_init_done();
 
@@ -882,13 +907,18 @@ progress_writer1:
                PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_READ_GP);
                PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_WRITE_GP);
                PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_WAIT);
+               /* For single flip, we need to know the current parity */
+               cur_gp_val = cur_gp_val ^ RCU_GP_CTR_BIT;
 #endif
 
-               do
+               do :: 1 ->
+               atomic {
+               if
                :: CONSUME_TOKENS(proc_urcu_writer,
                                  WRITE_PROD_NONE,
                                  WRITE_PROC_FIRST_MB) ->
-                       smp_mb_send(i, j);
+                       goto smp_mb_send1;
+smp_mb_send1_end:
                        PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_FIRST_MB);
 
                /* first flip */
@@ -911,9 +941,15 @@ progress_writer1:
                        ooo_mem(i);
                        /* ONLY WAITING FOR READER 0 */
                        tmp2 = READ_CACHED_VAR(urcu_active_readers[0]);
+#ifndef SINGLE_FLIP
+                       /* In normal execution, we are always starting by
+                        * waiting for the even parity.
+                        */
+                       cur_gp_val = RCU_GP_CTR_BIT;
+#endif
                        if
                        :: (tmp2 & RCU_GP_CTR_NEST_MASK)
-                                       && ((tmp2 ^ RCU_GP_CTR_BIT) & RCU_GP_CTR_BIT) ->
+                                       && ((tmp2 ^ cur_gp_val) & RCU_GP_CTR_BIT) ->
                                PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_FIRST_WAIT_LOOP);
                        :: else ->
                                PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_FIRST_WAIT);
@@ -927,7 +963,8 @@ progress_writer1:
                                  | WRITE_PROC_FIRST_MB,        /* can be reordered before/after flips */
                                  0) ->
 #ifndef GEN_ERROR_WRITER_PROGRESS
-                       smp_mb_send(i, j);
+                       goto smp_mb_send2;
+smp_mb_send2_end:
 #else
                        ooo_mem(i);
 #endif
@@ -942,7 +979,6 @@ progress_writer1:
                                  | WRITE_PROC_FIRST_READ_GP
                                  | WRITE_PROC_FIRST_MB,
                                  WRITE_PROC_SECOND_READ_GP) ->
-                       //smp_mb_send(i, j);            //TEST
                        ooo_mem(i);
                        tmpa = READ_CACHED_VAR(urcu_gp_ctr);
                        PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_READ_GP);
@@ -982,7 +1018,8 @@ progress_writer1:
                                  | WRITE_PROC_FIRST_MB,        /* can be reordered before/after flips */
                                  0) ->
 #ifndef GEN_ERROR_WRITER_PROGRESS
-                       smp_mb_send(i, j);
+                       goto smp_mb_send3;
+smp_mb_send3_end:
 #else
                        ooo_mem(i);
 #endif
@@ -999,12 +1036,15 @@ progress_writer1:
                                  | WRITE_PROC_SECOND_WRITE_GP
                                  | WRITE_PROC_FIRST_MB,
                                  WRITE_PROC_SECOND_MB) ->
-                       smp_mb_send(i, j);
+                       goto smp_mb_send4;
+smp_mb_send4_end:
                        PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_MB);
 
                :: CONSUME_TOKENS(proc_urcu_writer, WRITE_PROC_ALL_TOKENS, 0) ->
                        CLEAR_TOKENS(proc_urcu_writer, WRITE_PROC_ALL_TOKENS_CLEAR);
                        break;
+               fi;
+               }
                od;
 
                write_lock = 0;
@@ -1028,6 +1068,25 @@ progress_writer2:
 #endif
                skip;
        od;
+
+       /* Non-atomic parts of the loop */
+       goto end;
+smp_mb_send1:
+       smp_mb_send(i, j, 1);
+       goto smp_mb_send1_end;
+#ifndef GEN_ERROR_WRITER_PROGRESS
+smp_mb_send2:
+       smp_mb_send(i, j, 2);
+       goto smp_mb_send2_end;
+smp_mb_send3:
+       smp_mb_send(i, j, 3);
+       goto smp_mb_send3_end;
+#endif
+smp_mb_send4:
+       smp_mb_send(i, j, 4);
+       goto smp_mb_send4_end;
+end:
+       skip;
 }
 
 /* no name clash please */