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 = 2;
  10  * y = 2;
  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 /* value 2 is uninitialized */
 162 byte read_one = 2;
 163 byte read_two = 2;
 164
 165 /*
 166  * Bit encoding, proc_one_produced :
 167  */
 168
 169 #define P1_PROD_NONE    (1 << 0)
 170
 171 #define P1_WRITE        (1 << 1)
 172 #define P1_WMB          (1 << 2)
 173 #define P1_SYNC_CORE    (1 << 3)
 174 #define P1_RMB          (1 << 4)
 175 #define P1_READ         (1 << 5)
 176
 177 int proc_one_produced;
 178
 179 active proctype test_proc_one()
 180 {
 181         assert(get_pid() < NR_PROCS);
 182
 183         PRODUCE_TOKENS(proc_one_produced, P1_PROD_NONE);
 184
 185 #ifdef NO_WMB
 186         PRODUCE_TOKENS(proc_one_produced, P1_WMB);
 187 #endif
 188 #ifdef NO_RMB
 189         PRODUCE_TOKENS(proc_one_produced, P1_RMB);
 190 #endif
 191 #ifdef NO_SYNC
 192         PRODUCE_TOKENS(proc_one_produced, P1_SYNC_CORE);
 193 #endif
 194
 195         do
 196         :: CONSUME_TOKENS(proc_one_produced, P1_PROD_NONE, P1_WRITE) ->
 197                 ooo_mem();
 198                 WRITE_CACHED_VAR(alpha, 1);
 199                 ooo_mem();
 200                 PRODUCE_TOKENS(proc_one_produced, P1_WRITE);
 201         :: CONSUME_TOKENS(proc_one_produced, P1_WRITE, P1_WMB) ->
 202                 smp_wmb();
 203                 PRODUCE_TOKENS(proc_one_produced, P1_WMB);
 204         :: CONSUME_TOKENS(proc_one_produced, P1_WRITE | P1_WMB, P1_SYNC_CORE) ->
 205                 /* sync_core(); */
 206                 PRODUCE_TOKENS(proc_one_produced, P1_SYNC_CORE);
 207         :: CONSUME_TOKENS(proc_one_produced, P1_SYNC_CORE, P1_RMB) ->
 208                 smp_rmb();
 209                 PRODUCE_TOKENS(proc_one_produced, P1_RMB);
 210         :: CONSUME_TOKENS(proc_one_produced, P1_RMB | P1_SYNC_CORE, P1_READ) ->
 211                 ooo_mem();
 212                 read_one = READ_CACHED_VAR(beta);
 213                 ooo_mem();
 214                 PRODUCE_TOKENS(proc_one_produced, P1_READ);
 215         :: CONSUME_TOKENS(proc_one_produced, P1_PROD_NONE | P1_WRITE
 216                 | P1_WMB | P1_SYNC_CORE | P1_RMB | P1_READ, 0) ->
 217                 break;
 218         od;
 219
 220         //CLEAR_TOKENS(proc_one_produced,
 221         //      P1_PROD_NONE | P1_WRITE | P1_WMB | P1_SYNC_CORE | P1_RMB |
 222         //      P2_READ);
 223
 224         // test : [] (read_one == 0 -> read_two != 0)
 225         // test : [] (read_two == 0 -> read_one != 0)
 226         assert(!(read_one == 0 && read_two == 0));
 227 }
 228
 229
 230 /*
 231  * Bit encoding, proc_two_produced :
 232  */
 233
 234 #define P2_PROD_NONE    (1 << 0)
 235
 236 #define P2_WRITE        (1 << 1)
 237 #define P2_WMB          (1 << 2)
 238 #define P2_SYNC_CORE    (1 << 3)
 239 #define P2_RMB          (1 << 4)
 240 #define P2_READ         (1 << 5)
 241
 242 int proc_two_produced;
 243
 244 active proctype test_proc_two()
 245 {
 246         assert(get_pid() < NR_PROCS);
 247
 248         PRODUCE_TOKENS(proc_two_produced, P2_PROD_NONE);
 249
 250 #ifdef NO_WMB
 251         PRODUCE_TOKENS(proc_two_produced, P2_WMB);
 252 #endif
 253 #ifdef NO_RMB
 254         PRODUCE_TOKENS(proc_two_produced, P2_RMB);
 255 #endif
 256 #ifdef NO_SYNC
 257         PRODUCE_TOKENS(proc_two_produced, P2_SYNC_CORE);
 258 #endif
 259
 260         do
 261         :: CONSUME_TOKENS(proc_two_produced, P2_PROD_NONE, P2_WRITE) ->
 262                 ooo_mem();
 263                 WRITE_CACHED_VAR(beta, 1);
 264                 ooo_mem();
 265                 PRODUCE_TOKENS(proc_two_produced, P2_WRITE);
 266         :: CONSUME_TOKENS(proc_two_produced, P2_WRITE, P2_WMB) ->
 267                 smp_wmb();
 268                 PRODUCE_TOKENS(proc_two_produced, P2_WMB);
 269         :: CONSUME_TOKENS(proc_two_produced, P2_WRITE | P2_WMB, P2_SYNC_CORE) ->
 270                 /* sync_core(); */
 271                 PRODUCE_TOKENS(proc_two_produced, P2_SYNC_CORE);
 272         :: CONSUME_TOKENS(proc_two_produced, P2_SYNC_CORE, P2_RMB) ->
 273                 smp_rmb();
 274                 PRODUCE_TOKENS(proc_two_produced, P2_RMB);
 275         :: CONSUME_TOKENS(proc_two_produced, P2_SYNC_CORE | P2_RMB, P2_READ) ->
 276                 ooo_mem();
 277                 read_two = READ_CACHED_VAR(alpha);
 278                 ooo_mem();
 279                 PRODUCE_TOKENS(proc_two_produced, P2_READ);
 280         :: CONSUME_TOKENS(proc_two_produced, P2_PROD_NONE | P2_WRITE
 281                 | P2_WMB | P2_SYNC_CORE | P2_RMB | P2_READ, 0) ->
 282                 break;
 283         od;
 284
 285         //CLEAR_TOKENS(proc_two_produced,
 286         //      P2_PROD_NONE | P2_WRITE | P2_WMB | P2_SYNC_CORE | P2_RMB |
 287         //      P2_READ);
 288
 289         // test : [] (read_one == 0 -> read_two != 0)
 290         // test : [] (read_two == 0 -> read_one != 0)
 291         assert(!(read_one == 0 && read_two == 0));
 292 }