formal-model/ooomem-two-writes/mem.spin

   1 /*
   2  * mem.spin: Promela code to validate memory barriers with out-of-order memory
   3  * and out-of-order instruction scheduling.
   4  *
   5  * Algorithm verified :
   6  *
   7  * alpha = 0;
   8  * beta = 0;
   9  * x = 1;
  10  * y = 1;
  11  *
  12  * Process A                  Process B
  13  * alpha = 1;                 beta = 1;
  14  * mb();                      mb();
  15  * x = beta;                  y = alpha;
  16  *
  17  * if x = 0, then y != 0
  18  * if y = 0, then x != 0
  19  *
  20  * This program is free software; you can redistribute it and/or modify
  21  * it under the terms of the GNU General Public License as published by
  22  * the Free Software Foundation; either version 2 of the License, or
  23  * (at your option) any later version.
  24  *
  25  * This program is distributed in the hope that it will be useful,
  26  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  27  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  28  * GNU General Public License for more details.
  29  *
  30  * You should have received a copy of the GNU General Public License
  31  * along with this program; if not, write to the Free Software
  32  * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
  33  *
  34  * Copyright (c) 2009 Mathieu Desnoyers
  35  */
  36
  37 /* Promela validation variables. */
  38
  39 /*
  40  * Produced process control and data flow. Updated after each instruction to
  41  * show which variables are ready. Using one-hot bit encoding per variable to
  42  * save state space. Used as triggers to execute the instructions having those
  43  * variables as input. Leaving bits active to inhibit instruction execution.
  44  * Scheme used to make instruction disabling and automatic dependency fall-back
  45  * automatic.
  46  */
  47
  48 #define CONSUME_TOKENS(state, bits, notbits)                    \
  49         ((!(state & (notbits))) && (state & (bits)) == (bits))
  50
  51 #define PRODUCE_TOKENS(state, bits)                             \
  52         state = state | (bits);
  53
  54 #define CLEAR_TOKENS(state, bits)                               \
  55         state = state & ~(bits)
  56
  57 #define NR_PROCS 2
  58
  59 #define get_pid()       (_pid)
  60
  61 /*
  62  * Each process have its own data in cache. Caches are randomly updated.
  63  * smp_wmb and smp_rmb forces cache updates (write and read), wmb_mb forces
  64  * both.
  65  */
  66
  67 #define DECLARE_CACHED_VAR(type, x, v)          \
  68         type mem_##x = v;                       \
  69         type cached_##x[NR_PROCS] = v;          \
  70         bit cache_dirty_##x[NR_PROCS] = 0;
  71
  72 #define IS_CACHE_DIRTY(x, id)   (cache_dirty_##x[id])
  73
  74 #define READ_CACHED_VAR(x)                      \
  75         (cached_##x[get_pid()])
  76
  77 #define WRITE_CACHED_VAR(x, v)                  \
  78         atomic {                                \
  79                 cached_##x[get_pid()] = v;      \
  80                 cache_dirty_##x[get_pid()] = 1; \
  81         }
  82
  83 #define CACHE_WRITE_TO_MEM(x, id)               \
  84         if                                      \
  85         :: IS_CACHE_DIRTY(x, id) ->             \
  86                 mem_##x = cached_##x[id];       \
  87                 cache_dirty_##x[id] = 0;        \
  88         :: else ->                              \
  89                 skip                            \
  90         fi;
  91
  92 #define CACHE_READ_FROM_MEM(x, id)              \
  93         if                                      \
  94         :: !IS_CACHE_DIRTY(x, id) ->            \
  95                 cached_##x[id] = mem_##x;       \
  96         :: else ->                              \
  97                 skip                            \
  98         fi;
  99
 100 /*
 101  * May update other caches if cache is dirty, or not.
 102  */
 103 #define RANDOM_CACHE_WRITE_TO_MEM(x, id)        \
 104         if                                      \
 105         :: 1 -> CACHE_WRITE_TO_MEM(x, id);      \
 106         :: 1 -> skip                            \
 107         fi;
 108
 109 #define RANDOM_CACHE_READ_FROM_MEM(x, id)\
 110         if                                      \
 111         :: 1 -> CACHE_READ_FROM_MEM(x, id);     \
 112         :: 1 -> skip                            \
 113         fi;
 114
 115 inline ooo_mem()
 116 {
 117         atomic {
 118                 RANDOM_CACHE_WRITE_TO_MEM(alpha, get_pid());
 119                 RANDOM_CACHE_WRITE_TO_MEM(beta, get_pid());
 120                 RANDOM_CACHE_READ_FROM_MEM(alpha, get_pid());
 121                 RANDOM_CACHE_READ_FROM_MEM(beta, get_pid());
 122         }
 123 }
 124
 125 /* must consume all prior read tokens */
 126 inline smp_rmb()
 127 {
 128         atomic {
 129                 /* todo : consume all read tokens .. ? */
 130                 CACHE_READ_FROM_MEM(alpha, get_pid());
 131                 CACHE_READ_FROM_MEM(beta, get_pid());
 132         }
 133 }
 134
 135 /* must consume all prior write tokens */
 136 inline smp_wmb()
 137 {
 138         atomic {
 139                 CACHE_WRITE_TO_MEM(alpha, get_pid());
 140                 CACHE_WRITE_TO_MEM(beta, get_pid());
 141         }
 142 }
 143
 144 /* sync_core() must consume all prior read and write tokens, including rmb/wmb
 145  * tokens */
 146
 147 /* must consume all prior read and write tokens */
 148 inline smp_mb()
 149 {
 150         atomic {
 151                 smp_wmb();
 152                 /* sync_core() */
 153                 smp_rmb();
 154         }
 155 }
 156
 157 /* Keep in sync manually with smp_rmb, wmp_wmb and ooo_mem */
 158 DECLARE_CACHED_VAR(byte, alpha, 0);
 159 DECLARE_CACHED_VAR(byte, beta, 0);
 160
 161 byte read_one = 1;
 162 byte read_two = 1;
 163
 164 /*
 165  * Bit encoding, proc_one_produced :
 166  */
 167
 168 #define P1_PROD_NONE    (1 << 0)
 169
 170 #define P1_WRITE        (1 << 1)
 171 #define P1_WMB          (1 << 2)
 172 #define P1_SYNC_CORE    (1 << 3)
 173 #define P1_RMB          (1 << 4)
 174 #define P1_READ         (1 << 5)
 175
 176 int proc_one_produced;
 177
 178 active proctype test_proc_one()
 179 {
 180         assert(get_pid() < NR_PROCS);
 181
 182         PRODUCE_TOKENS(proc_one_produced, P1_PROD_NONE);
 183
 184 #ifdef NO_WMB
 185         PRODUCE_TOKENS(proc_one_produced, P1_WMB);
 186 #endif
 187 #ifdef NO_RMB
 188         PRODUCE_TOKENS(proc_one_produced, P1_RMB);
 189 #endif
 190 #ifdef NO_SYNC
 191         PRODUCE_TOKENS(proc_one_produced, P1_SYNC_CORE);
 192 #endif
 193
 194         do
 195         :: CONSUME_TOKENS(proc_one_produced, P1_PROD_NONE, P1_WRITE) ->
 196                 ooo_mem();
 197                 WRITE_CACHED_VAR(alpha, 1);
 198                 ooo_mem();
 199                 PRODUCE_TOKENS(proc_one_produced, P1_WRITE);
 200         :: CONSUME_TOKENS(proc_one_produced, P1_WRITE, P1_WMB) ->
 201                 smp_wmb();
 202                 PRODUCE_TOKENS(proc_one_produced, P1_WMB);
 203         :: CONSUME_TOKENS(proc_one_produced, P1_WRITE | P1_WMB, P1_SYNC_CORE) ->
 204                 /* sync_core(); */
 205                 PRODUCE_TOKENS(proc_one_produced, P1_SYNC_CORE);
 206         :: CONSUME_TOKENS(proc_one_produced, P1_SYNC_CORE, P1_RMB) ->
 207                 smp_rmb();
 208                 PRODUCE_TOKENS(proc_one_produced, P1_RMB);
 209         :: CONSUME_TOKENS(proc_one_produced, P1_RMB | P1_SYNC_CORE, P1_READ) ->
 210                 ooo_mem();
 211                 read_one = READ_CACHED_VAR(beta);
 212                 ooo_mem();
 213                 PRODUCE_TOKENS(proc_one_produced, P1_READ);
 214         :: CONSUME_TOKENS(proc_one_produced, P1_PROD_NONE | P1_WRITE
 215                 | P1_WMB | P1_SYNC_CORE | P1_RMB | P1_READ, 0) ->
 216                 break;
 217         od;
 218
 219         //CLEAR_TOKENS(proc_one_produced,
 220         //      P1_PROD_NONE | P1_WRITE | P1_WMB | P1_SYNC_CORE | P1_RMB |
 221         //      P2_READ);
 222
 223         // test : [] (read_one == 0 -> read_two != 0)
 224         // test : [] (read_two == 0 -> read_one != 0)
 225         assert(!(read_one == 0 && read_two == 0));
 226 }
 227
 228
 229 /*
 230  * Bit encoding, proc_two_produced :
 231  */
 232
 233 #define P2_PROD_NONE    (1 << 0)
 234
 235 #define P2_WRITE        (1 << 1)
 236 #define P2_WMB          (1 << 2)
 237 #define P2_SYNC_CORE    (1 << 3)
 238 #define P2_RMB          (1 << 4)
 239 #define P2_READ         (1 << 5)
 240
 241 int proc_two_produced;
 242
 243 active proctype test_proc_two()
 244 {
 245         assert(get_pid() < NR_PROCS);
 246
 247         PRODUCE_TOKENS(proc_two_produced, P2_PROD_NONE);
 248
 249 #ifdef NO_WMB
 250         PRODUCE_TOKENS(proc_two_produced, P2_WMB);
 251 #endif
 252 #ifdef NO_RMB
 253         PRODUCE_TOKENS(proc_two_produced, P2_RMB);
 254 #endif
 255 #ifdef NO_SYNC
 256         PRODUCE_TOKENS(proc_two_produced, P2_SYNC_CORE);
 257 #endif
 258
 259         do
 260         :: CONSUME_TOKENS(proc_two_produced, P2_PROD_NONE, P2_WRITE) ->
 261                 ooo_mem();
 262                 WRITE_CACHED_VAR(beta, 1);
 263                 ooo_mem();
 264                 PRODUCE_TOKENS(proc_two_produced, P2_WRITE);
 265         :: CONSUME_TOKENS(proc_two_produced, P2_WRITE, P2_WMB) ->
 266                 smp_wmb();
 267                 PRODUCE_TOKENS(proc_two_produced, P2_WMB);
 268         :: CONSUME_TOKENS(proc_two_produced, P2_WRITE | P2_WMB, P2_SYNC_CORE) ->
 269                 /* sync_core(); */
 270                 PRODUCE_TOKENS(proc_two_produced, P2_SYNC_CORE);
 271         :: CONSUME_TOKENS(proc_two_produced, P2_SYNC_CORE, P2_RMB) ->
 272                 smp_rmb();
 273                 PRODUCE_TOKENS(proc_two_produced, P2_RMB);
 274         :: CONSUME_TOKENS(proc_two_produced, P2_SYNC_CORE | P2_RMB, P2_READ) ->
 275                 ooo_mem();
 276                 read_two = READ_CACHED_VAR(alpha);
 277                 ooo_mem();
 278                 PRODUCE_TOKENS(proc_two_produced, P2_READ);
 279         :: CONSUME_TOKENS(proc_two_produced, P2_PROD_NONE | P2_WRITE
 280                 | P2_WMB | P2_SYNC_CORE | P2_RMB | P2_READ, 0) ->
 281                 break;
 282         od;
 283
 284         //CLEAR_TOKENS(proc_two_produced,
 285         //      P2_PROD_NONE | P2_WRITE | P2_WMB | P2_SYNC_CORE | P2_RMB |
 286         //      P2_READ);
 287
 288         // test : [] (read_one == 0 -> read_two != 0)
 289         // test : [] (read_two == 0 -> read_one != 0)
 290         assert(!(read_one == 0 && read_two == 0));
 291 }