Update formal model from local copy
[urcu.git] / formal-model / urcu-controldataflow / urcu.spin
index 948f3dd0f5fec3e8ae84f0fd4b5dfb6d55a148eb..8075506ec66c4cb21dca6dbb9efa8a5e8a8c9f9e 100644 (file)
  * output exchanged. Therefore, i post-dominating j ensures that every path
  * passing by j will pass by i before reaching the output.
  *
+ * Prefetch and speculative execution
+ *
+ * If an instruction depends on the result of a previous branch, but it does not
+ * have side-effects, it can be executed before the branch result is known.
+ * however, it must be restarted if a core-synchronizing instruction is issued.
+ * Note that instructions which depend on the speculative instruction result
+ * but that have side-effects must depend on the branch completion in addition
+ * to the speculatively executed instruction.
+ *
  * Other considerations
  *
  * Note about "volatile" keyword dependency : The compiler will order volatile
  * Nested calls are not supported.
  */
 
+/*
+ * Only Alpha has out-of-order cache bank loads. Other architectures (intel,
+ * powerpc, arm) ensure that dependent reads won't be reordered. c.f.
+ * http://www.linuxjournal.com/article/8212)
+ */
+#ifdef ARCH_ALPHA
+#define HAVE_OOO_CACHE_READ
+#endif
+
 /*
  * Each process have its own data in cache. Caches are randomly updated.
  * smp_wmb and smp_rmb forces cache updates (write and read), smp_mb forces
@@ -146,38 +164,34 @@ typedef per_proc_bitfield {
 };
 
 #define DECLARE_CACHED_VAR(type, x)    \
-       type mem_##x;                   \
-       per_proc_##type cached_##x;     \
-       per_proc_bitfield cache_dirty_##x;
-
-#define INIT_CACHED_VAR(x, v, j)       \
-       mem_##x = v;                    \
-       cache_dirty_##x.bitfield = 0;   \
-       j = 0;                          \
-       do                              \
-       :: j < NR_PROCS ->              \
-               cached_##x.val[j] = v;  \
-               j++                     \
-       :: j >= NR_PROCS -> break       \
-       od;
+       type mem_##x;
+
+#define DECLARE_PROC_CACHED_VAR(type, x)\
+       type cached_##x;                \
+       bit cache_dirty_##x;
 
-#define IS_CACHE_DIRTY(x, id)  (cache_dirty_##x.bitfield & (1 << id))
+#define INIT_CACHED_VAR(x, v)          \
+       mem_##x = v;
 
-#define READ_CACHED_VAR(x)     (cached_##x.val[get_pid()])
+#define INIT_PROC_CACHED_VAR(x, v)     \
+       cache_dirty_##x = 0;            \
+       cached_##x = v;
+
+#define IS_CACHE_DIRTY(x, id)  (cache_dirty_##x)
+
+#define READ_CACHED_VAR(x)     (cached_##x)
 
 #define WRITE_CACHED_VAR(x, v)                         \
        atomic {                                        \
-               cached_##x.val[get_pid()] = v;          \
-               cache_dirty_##x.bitfield =              \
-                       cache_dirty_##x.bitfield | (1 << get_pid());    \
+               cached_##x = v;                         \
+               cache_dirty_##x = 1;                    \
        }
 
 #define CACHE_WRITE_TO_MEM(x, id)                      \
        if                                              \
        :: IS_CACHE_DIRTY(x, id) ->                     \
-               mem_##x = cached_##x.val[id];           \
-               cache_dirty_##x.bitfield =              \
-                       cache_dirty_##x.bitfield & (~(1 << id));        \
+               mem_##x = cached_##x;                   \
+               cache_dirty_##x = 0;                    \
        :: else ->                                      \
                skip                                    \
        fi;
@@ -185,7 +199,7 @@ typedef per_proc_bitfield {
 #define CACHE_READ_FROM_MEM(x, id)     \
        if                              \
        :: !IS_CACHE_DIRTY(x, id) ->    \
-               cached_##x.val[id] = mem_##x;\
+               cached_##x = mem_##x;   \
        :: else ->                      \
                skip                    \
        fi;
@@ -206,7 +220,7 @@ typedef per_proc_bitfield {
        fi;
 
 /* Must consume all prior read tokens. All subsequent reads depend on it. */
-inline smp_rmb(i, j)
+inline smp_rmb(i)
 {
        atomic {
                CACHE_READ_FROM_MEM(urcu_gp_ctr, get_pid());
@@ -229,7 +243,7 @@ inline smp_rmb(i, j)
 }
 
 /* Must consume all prior write tokens. All subsequent writes depend on it. */
-inline smp_wmb(i, j)
+inline smp_wmb(i)
 {
        atomic {
                CACHE_WRITE_TO_MEM(urcu_gp_ctr, get_pid());
@@ -253,11 +267,11 @@ inline smp_wmb(i, j)
 
 /* Synchronization point. Must consume all prior read and write tokens. All
  * subsequent reads and writes depend on it. */
-inline smp_mb(i, j)
+inline smp_mb(i)
 {
        atomic {
-               smp_wmb(i, j);
-               smp_rmb(i, j);
+               smp_wmb(i);
+               smp_rmb(i);
        }
 }
 
@@ -290,7 +304,7 @@ inline smp_mb_recv(i, j)
                 * reader always services them without continuing execution.
                 */
 progress_ignoring_mb1:
-               smp_mb(i, j);
+               smp_mb(i);
                reader_barrier[get_readerid()] = 0;
        :: 1 ->
                /*
@@ -306,7 +320,7 @@ progress_ignoring_mb2:
 
 #define smp_mb_send(i, j, progressid)                                          \
 {                                                                              \
-       smp_mb(i, j);                                                           \
+       smp_mb(i);                                                              \
        i = 0;                                                                  \
        do                                                                      \
        :: i < NR_READERS ->                                                    \
@@ -326,13 +340,13 @@ PROGRESS_LABEL(progressid)                                                        \
        :: i >= NR_READERS ->                                                   \
                break                                                           \
        od;                                                                     \
-       smp_mb(i, j);                                                           \
+       smp_mb(i);                                                              \
 }
 
 #else
 
-#define smp_mb_send(i, j, progressid)  smp_mb(i, j)
-#define smp_mb_reader  smp_mb
+#define smp_mb_send(i, j, progressid)  smp_mb(i)
+#define smp_mb_reader(i, j)            smp_mb(i)
 #define smp_mb_recv(i, j)
 
 #endif
@@ -388,6 +402,7 @@ inline ooo_mem(i)
                        i++
                :: i >= SLAB_SIZE -> break
                od;
+#ifdef HAVE_OOO_CACHE_READ
                RANDOM_CACHE_READ_FROM_MEM(urcu_gp_ctr, get_pid());
                i = 0;
                do
@@ -405,6 +420,9 @@ inline ooo_mem(i)
                        i++
                :: i >= SLAB_SIZE -> break
                od;
+#else
+               smp_rmb(i);
+#endif /* HAVE_OOO_CACHE_READ */
        }
 }
 
@@ -421,8 +439,8 @@ int _proc_urcu_reader;
 #define READ_PROD_B_IF_FALSE           (1 << 2)
 #define READ_PROD_C_IF_TRUE_READ       (1 << 3)
 
-#define PROCEDURE_READ_LOCK(base, consumetoken, producetoken)                          \
-       :: CONSUME_TOKENS(proc_urcu_reader, consumetoken, READ_PROD_A_READ << base) ->  \
+#define PROCEDURE_READ_LOCK(base, consumetoken, consumetoken2, producetoken)           \
+       :: CONSUME_TOKENS(proc_urcu_reader, (consumetoken | consumetoken2), READ_PROD_A_READ << base) ->        \
                ooo_mem(i);                                                             \
                tmp = READ_CACHED_VAR(urcu_active_readers[get_readerid()]);             \
                PRODUCE_TOKENS(proc_urcu_reader, READ_PROD_A_READ << base);             \
@@ -436,13 +454,14 @@ int _proc_urcu_reader;
                        PRODUCE_TOKENS(proc_urcu_reader, READ_PROD_B_IF_FALSE << base); \
                fi;                                                                     \
        /* IF TRUE */                                                                   \
-       :: CONSUME_TOKENS(proc_urcu_reader, READ_PROD_B_IF_TRUE << base,                \
+       :: CONSUME_TOKENS(proc_urcu_reader, consumetoken, /* prefetch */                \
                          READ_PROD_C_IF_TRUE_READ << base) ->                          \
                ooo_mem(i);                                                             \
                tmp2 = READ_CACHED_VAR(urcu_gp_ctr);                                    \
                PRODUCE_TOKENS(proc_urcu_reader, READ_PROD_C_IF_TRUE_READ << base);     \
        :: CONSUME_TOKENS(proc_urcu_reader,                                             \
-                         (READ_PROD_C_IF_TRUE_READ     /* pre-dominant */              \
+                         (READ_PROD_B_IF_TRUE                                          \
+                         | READ_PROD_C_IF_TRUE_READ    /* pre-dominant */              \
                          | READ_PROD_A_READ) << base,          /* WAR */               \
                          producetoken) ->                                              \
                ooo_mem(i);                                                             \
@@ -472,14 +491,14 @@ int _proc_urcu_reader;
                          consumetoken,                                                 \
                          READ_PROC_READ_UNLOCK << base) ->                             \
                ooo_mem(i);                                                             \
-               tmp2 = READ_CACHED_VAR(urcu_active_readers[get_readerid()]);            \
+               tmp = READ_CACHED_VAR(urcu_active_readers[get_readerid()]);             \
                PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_READ_UNLOCK << base);        \
        :: CONSUME_TOKENS(proc_urcu_reader,                                             \
                          consumetoken                                                  \
                          | (READ_PROC_READ_UNLOCK << base),    /* WAR */               \
                          producetoken) ->                                              \
                ooo_mem(i);                                                             \
-               WRITE_CACHED_VAR(urcu_active_readers[get_readerid()], tmp2 - 1);        \
+               WRITE_CACHED_VAR(urcu_active_readers[get_readerid()], tmp - 1);         \
                PRODUCE_TOKENS(proc_urcu_reader, producetoken);                         \
        skip
 
@@ -655,7 +674,7 @@ non_atomic3_skip:
 
                atomic {
                        if
-                       PROCEDURE_READ_LOCK(READ_LOCK_BASE, READ_PROD_NONE, READ_LOCK_OUT);
+                       PROCEDURE_READ_LOCK(READ_LOCK_BASE, READ_PROD_NONE, 0, READ_LOCK_OUT);
 
                        :: CONSUME_TOKENS(proc_urcu_reader,
                                          READ_LOCK_OUT,                /* post-dominant */
@@ -663,7 +682,7 @@ non_atomic3_skip:
                                smp_mb_reader(i, j);
                                PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_FIRST_MB);
 
-                       PROCEDURE_READ_LOCK(READ_LOCK_NESTED_BASE, READ_PROC_FIRST_MB | READ_LOCK_OUT,
+                       PROCEDURE_READ_LOCK(READ_LOCK_NESTED_BASE, READ_PROC_FIRST_MB, READ_LOCK_OUT,
                                            READ_LOCK_NESTED_OUT);
 
                        :: CONSUME_TOKENS(proc_urcu_reader,
@@ -721,12 +740,12 @@ rmb1_end:
                        /* reading urcu_active_readers, which have been written by
                         * READ_UNLOCK_OUT : RAW */
                        PROCEDURE_READ_LOCK(READ_LOCK_UNROLL_BASE,
-                                           READ_UNLOCK_OUT             /* RAW */
-                                           | READ_PROC_SECOND_MB       /* mb() orders reads */
-                                           | READ_PROC_FIRST_MB        /* mb() orders reads */
-                                           | READ_LOCK_NESTED_OUT      /* RAW */
+                                           READ_PROC_SECOND_MB         /* mb() orders reads */
+                                           | READ_PROC_FIRST_MB,       /* mb() orders reads */
+                                           READ_LOCK_NESTED_OUT        /* RAW */
                                            | READ_LOCK_OUT             /* RAW */
-                                           | READ_UNLOCK_NESTED_OUT,   /* RAW */
+                                           | READ_UNLOCK_NESTED_OUT    /* RAW */
+                                           | READ_UNLOCK_OUT,          /* RAW */
                                            READ_LOCK_OUT_UNROLL);
 
 
@@ -811,14 +830,14 @@ rmb2_end:
        goto end;
 rmb1:
 #ifndef NO_RMB
-       smp_rmb(i, j);
+       smp_rmb(i);
 #else
        ooo_mem(i);
 #endif
        goto rmb1_end;
 rmb2:
 #ifndef NO_RMB
-       smp_rmb(i, j);
+       smp_rmb(i);
 #else
        ooo_mem(i);
 #endif
@@ -834,6 +853,41 @@ active proctype urcu_reader()
        byte i, j, nest_i;
        byte tmp, tmp2;
 
+       /* Keep in sync manually with smp_rmb, smp_wmb, ooo_mem and init() */
+       DECLARE_PROC_CACHED_VAR(byte, urcu_gp_ctr);
+       /* Note ! currently only one reader */
+       DECLARE_PROC_CACHED_VAR(byte, urcu_active_readers[NR_READERS]);
+       /* RCU data */
+       DECLARE_PROC_CACHED_VAR(bit, rcu_data[SLAB_SIZE]);
+
+       /* RCU pointer */
+#if (SLAB_SIZE == 2)
+       DECLARE_PROC_CACHED_VAR(bit, rcu_ptr);
+#else
+       DECLARE_PROC_CACHED_VAR(byte, rcu_ptr);
+#endif
+
+       atomic {
+               INIT_PROC_CACHED_VAR(urcu_gp_ctr, 1);
+               INIT_PROC_CACHED_VAR(rcu_ptr, 0);
+
+               i = 0;
+               do
+               :: i < NR_READERS ->
+                       INIT_PROC_CACHED_VAR(urcu_active_readers[i], 0);
+                       i++;
+               :: i >= NR_READERS -> break
+               od;
+               INIT_PROC_CACHED_VAR(rcu_data[0], WINE);
+               i = 1;
+               do
+               :: i < SLAB_SIZE ->
+                       INIT_PROC_CACHED_VAR(rcu_data[i], POISON);
+                       i++
+               :: i >= SLAB_SIZE -> break
+               od;
+       }
+
        wait_init_done();
 
        assert(get_pid() < NR_PROCS);
@@ -923,6 +977,42 @@ active proctype urcu_writer()
                                 * GP update. Needed to test single flip case.
                                 */
 
+       /* Keep in sync manually with smp_rmb, smp_wmb, ooo_mem and init() */
+       DECLARE_PROC_CACHED_VAR(byte, urcu_gp_ctr);
+       /* Note ! currently only one reader */
+       DECLARE_PROC_CACHED_VAR(byte, urcu_active_readers[NR_READERS]);
+       /* RCU data */
+       DECLARE_PROC_CACHED_VAR(bit, rcu_data[SLAB_SIZE]);
+
+       /* RCU pointer */
+#if (SLAB_SIZE == 2)
+       DECLARE_PROC_CACHED_VAR(bit, rcu_ptr);
+#else
+       DECLARE_PROC_CACHED_VAR(byte, rcu_ptr);
+#endif
+
+       atomic {
+               INIT_PROC_CACHED_VAR(urcu_gp_ctr, 1);
+               INIT_PROC_CACHED_VAR(rcu_ptr, 0);
+
+               i = 0;
+               do
+               :: i < NR_READERS ->
+                       INIT_PROC_CACHED_VAR(urcu_active_readers[i], 0);
+                       i++;
+               :: i >= NR_READERS -> break
+               od;
+               INIT_PROC_CACHED_VAR(rcu_data[0], WINE);
+               i = 1;
+               do
+               :: i < SLAB_SIZE ->
+                       INIT_PROC_CACHED_VAR(rcu_data[i], POISON);
+                       i++
+               :: i >= SLAB_SIZE -> break
+               od;
+       }
+
+
        wait_init_done();
 
        assert(get_pid() < NR_PROCS);
@@ -969,7 +1059,7 @@ progress_writer1:
                :: CONSUME_TOKENS(proc_urcu_writer,
                                  WRITE_DATA,
                                  WRITE_PROC_WMB) ->
-                       smp_wmb(i, j);
+                       smp_wmb(i);
                        PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_WMB);
 
                :: CONSUME_TOKENS(proc_urcu_writer,
@@ -1004,10 +1094,11 @@ smp_mb_send1_end:
                        PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_FIRST_WRITE_GP);
 
                :: CONSUME_TOKENS(proc_urcu_writer,
-                                 //WRITE_PROC_FIRST_WRITE_GP   /* TEST ADDING SYNC CORE */
+                                 //WRITE_PROC_FIRST_WRITE_GP | /* TEST ADDING SYNC CORE */
                                  WRITE_PROC_FIRST_MB,  /* can be reordered before/after flips */
                                  WRITE_PROC_FIRST_WAIT | WRITE_PROC_FIRST_WAIT_LOOP) ->
                        ooo_mem(i);
+                       //smp_mb(i);    /* TEST */
                        /* ONLY WAITING FOR READER 0 */
                        tmp2 = READ_CACHED_VAR(urcu_active_readers[0]);
 #ifndef SINGLE_FLIP
@@ -1035,6 +1126,12 @@ smp_mb_send1_end:
 #ifndef GEN_ERROR_WRITER_PROGRESS
                        goto smp_mb_send2;
 smp_mb_send2_end:
+                       /* The memory barrier will invalidate the
+                        * second read done as prefetching. Note that all
+                        * instructions with side-effects depending on
+                        * WRITE_PROC_SECOND_READ_GP should also depend on
+                        * completion of this busy-waiting loop. */
+                       CLEAR_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_READ_GP);
 #else
                        ooo_mem(i);
 #endif
@@ -1043,17 +1140,21 @@ smp_mb_send2_end:
 
                /* second flip */
                :: CONSUME_TOKENS(proc_urcu_writer,
-                                 WRITE_PROC_FIRST_WAIT         /* Control dependency : need to branch out of
-                                                                * the loop to execute the next flip (CHECK) */
-                                 | WRITE_PROC_FIRST_WRITE_GP
+                                 //WRITE_PROC_FIRST_WAIT |     //test  /* no dependency. Could pre-fetch, no side-effect. */
+                                 WRITE_PROC_FIRST_WRITE_GP
                                  | WRITE_PROC_FIRST_READ_GP
                                  | WRITE_PROC_FIRST_MB,
                                  WRITE_PROC_SECOND_READ_GP) ->
                        ooo_mem(i);
+                       //smp_mb(i);    /* TEST */
                        tmpa = READ_CACHED_VAR(urcu_gp_ctr);
                        PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_READ_GP);
                :: CONSUME_TOKENS(proc_urcu_writer,
-                                 WRITE_PROC_FIRST_MB
+                                 WRITE_PROC_FIRST_WAIT                 /* dependency on first wait, because this
+                                                                        * instruction has globally observable
+                                                                        * side-effects.
+                                                                        */
+                                 | WRITE_PROC_FIRST_MB
                                  | WRITE_PROC_WMB
                                  | WRITE_PROC_FIRST_READ_GP
                                  | WRITE_PROC_FIRST_WRITE_GP
@@ -1064,11 +1165,12 @@ smp_mb_send2_end:
                        PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_WRITE_GP);
 
                :: CONSUME_TOKENS(proc_urcu_writer,
-                                 //WRITE_PROC_FIRST_WRITE_GP   /* TEST ADDING SYNC CORE */
+                                 //WRITE_PROC_FIRST_WRITE_GP | /* TEST ADDING SYNC CORE */
                                  WRITE_PROC_FIRST_WAIT
                                  | WRITE_PROC_FIRST_MB,        /* can be reordered before/after flips */
                                  WRITE_PROC_SECOND_WAIT | WRITE_PROC_SECOND_WAIT_LOOP) ->
                        ooo_mem(i);
+                       //smp_mb(i);    /* TEST */
                        /* ONLY WAITING FOR READER 0 */
                        tmp2 = READ_CACHED_VAR(urcu_active_readers[0]);
                        if
@@ -1080,7 +1182,7 @@ smp_mb_send2_end:
                        fi;
 
                :: CONSUME_TOKENS(proc_urcu_writer,
-                                 //WRITE_PROC_FIRST_WRITE_GP   /* TEST ADDING SYNC CORE */
+                                 //WRITE_PROC_FIRST_WRITE_GP | /* TEST ADDING SYNC CORE */
                                  WRITE_PROC_SECOND_WRITE_GP
                                  | WRITE_PROC_FIRST_WRITE_GP
                                  | WRITE_PROC_SECOND_READ_GP
@@ -1191,13 +1293,13 @@ init {
        byte i, j;
 
        atomic {
-               INIT_CACHED_VAR(urcu_gp_ctr, 1, j);
-               INIT_CACHED_VAR(rcu_ptr, 0, j);
+               INIT_CACHED_VAR(urcu_gp_ctr, 1);
+               INIT_CACHED_VAR(rcu_ptr, 0);
 
                i = 0;
                do
                :: i < NR_READERS ->
-                       INIT_CACHED_VAR(urcu_active_readers[i], 0, j);
+                       INIT_CACHED_VAR(urcu_active_readers[i], 0);
                        ptr_read_first[i] = 1;
                        ptr_read_second[i] = 1;
                        data_read_first[i] = WINE;
@@ -1205,11 +1307,11 @@ init {
                        i++;
                :: i >= NR_READERS -> break
                od;
-               INIT_CACHED_VAR(rcu_data[0], WINE, j);
+               INIT_CACHED_VAR(rcu_data[0], WINE);
                i = 1;
                do
                :: i < SLAB_SIZE ->
-                       INIT_CACHED_VAR(rcu_data[i], POISON, j);
+                       INIT_CACHED_VAR(rcu_data[i], POISON);
                        i++
                :: i >= SLAB_SIZE -> break
                od;
This page took 0.029095 seconds and 4 git commands to generate.