formal-model/ooomem-no-sched/mem.spin

   1 /*
   2  * mem.spin: Promela code to validate memory barriers with OOO memory.
   3  *
   4  * This program is free software; you can redistribute it and/or modify
   5  * it under the terms of the GNU General Public License as published by
   6  * the Free Software Foundation; either version 2 of the License, or
   7  * (at your option) any later version.
   8  *
   9  * This program is distributed in the hope that it will be useful,
  10  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  11  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  12  * GNU General Public License for more details.
  13  *
  14  * You should have received a copy of the GNU General Public License
  15  * along with this program; if not, write to the Free Software
  16  * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
  17  *
  18  * Copyright (c) 2009 Mathieu Desnoyers
  19  */
  20
  21 /*
  22  * Out-of-order memory model _without_ out-of-order instruction scheduling.
  23  */
  24
  25 /* Promela validation variables. */
  26
  27 #define NR_READERS 1
  28 #define NR_WRITERS 1
  29
  30 #define NR_PROCS 2
  31
  32 #define get_pid()       (_pid)
  33
  34 /*
  35  * Each process have its own data in cache. Caches are randomly updated.
  36  * smp_wmb and smp_rmb forces cache updates (write and read), wmb_mb forces
  37  * both.
  38  */
  39
  40 #define DECLARE_CACHED_VAR(type, x, v)  \
  41         type mem_##x = v;               \
  42         type cached_##x[NR_PROCS] = v;  \
  43         bit cache_dirty_##x[NR_PROCS] = 0
  44
  45 #define IS_CACHE_DIRTY(x, id)   (cache_dirty_##x[id])
  46
  47 #define READ_CACHED_VAR(x)      (cached_##x[get_pid()])
  48
  49 #define WRITE_CACHED_VAR(x, v)          \
  50         atomic {                        \
  51                 cached_##x[get_pid()] = v;      \
  52                 cache_dirty_##x[get_pid()] = 1; \
  53         }
  54
  55 #define CACHE_WRITE_TO_MEM(x, id)               \
  56         if                                      \
  57         :: IS_CACHE_DIRTY(x, id) ->             \
  58                 mem_##x = cached_##x[id];       \
  59                 cache_dirty_##x[id] = 0;        \
  60         :: else ->                              \
  61                 skip                            \
  62         fi;
  63
  64 #define CACHE_READ_FROM_MEM(x, id)      \
  65         if                              \
  66         :: !IS_CACHE_DIRTY(x, id) ->    \
  67                 cached_##x[id] = mem_##x;\
  68         :: else ->                      \
  69                 skip                    \
  70         fi;
  71
  72 /*
  73  * May update other caches if cache is dirty, or not.
  74  */
  75 #define RANDOM_CACHE_WRITE_TO_MEM(x, id)\
  76         if                              \
  77         :: 1 -> CACHE_WRITE_TO_MEM(x, id);      \
  78         :: 1 -> skip                    \
  79         fi;
  80
  81 #define RANDOM_CACHE_READ_FROM_MEM(x, id)\
  82         if                              \
  83         :: 1 -> CACHE_READ_FROM_MEM(x, id);     \
  84         :: 1 -> skip                    \
  85         fi;
  86
  87 inline smp_rmb()
  88 {
  89         atomic {
  90                 CACHE_READ_FROM_MEM(alpha, get_pid());
  91                 CACHE_READ_FROM_MEM(beta, get_pid());
  92         }
  93 }
  94
  95 inline smp_wmb()
  96 {
  97         atomic {
  98                 CACHE_WRITE_TO_MEM(alpha, get_pid());
  99                 CACHE_WRITE_TO_MEM(beta, get_pid());
 100         }
 101 }
 102
 103 inline smp_mb()
 104 {
 105         atomic {
 106                 smp_wmb();
 107                 smp_rmb();
 108         }
 109 }
 110
 111 /* Keep in sync manually with smp_rmb, wmp_wmb and ooo_mem */
 112 DECLARE_CACHED_VAR(byte, alpha, 0);
 113 DECLARE_CACHED_VAR(byte, beta, 0);
 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 #define get_readerid()  (get_pid())
 126
 127 byte first_read[NR_READERS];
 128 byte second_read[NR_READERS];
 129
 130 active [NR_READERS] proctype test_reader()
 131 {
 132         assert(get_pid() < NR_PROCS);
 133
 134         ooo_mem();
 135         first_read[get_readerid()] = READ_CACHED_VAR(beta);
 136         ooo_mem();
 137 #ifndef NO_RMB
 138         smp_rmb();
 139         ooo_mem();
 140 #endif
 141         second_read[get_readerid()] = READ_CACHED_VAR(alpha);
 142         ooo_mem();
 143         // test : [] (first_read == 6 -> <> second_read == 4)
 144         assert(first_read[get_readerid()] != 6
 145                 || second_read[get_readerid()] == 4);
 146 }
 147
 148 #define get_writerid()  (get_readerid() + NR_READERS)
 149
 150 active [NR_WRITERS] proctype test_writer()
 151 {
 152         byte i;
 153
 154         assert(get_pid() < NR_PROCS);
 155
 156         ooo_mem();
 157         WRITE_CACHED_VAR(alpha, 4);
 158         ooo_mem();
 159 #ifndef NO_WMB
 160         smp_wmb();
 161         ooo_mem();
 162 #endif
 163         WRITE_CACHED_VAR(beta, 6);
 164         ooo_mem();
 165 }