docs/spin/tcg-exclusive.promela

   1 /*
   2  * This model describes the implementation of exclusive sections in
   3  * cpus-common.c (start_exclusive, end_exclusive, cpu_exec_start,
   4  * cpu_exec_end).
   5  *
   6  * Author: Paolo Bonzini <pbonzini@redhat.com>
   7  *
   8  * This file is in the public domain.  If you really want a license,
   9  * the WTFPL will do.
  10  *
  11  * To verify it:
  12  *     spin -a docs/tcg-exclusive.promela
  13  *     gcc pan.c -O2
  14  *     ./a.out -a
  15  *
  16  * Tunable processor macros: N_CPUS, N_EXCLUSIVE, N_CYCLES, USE_MUTEX,
  17  *                           TEST_EXPENSIVE.
  18  */
  19
  20 // Define the missing parameters for the model
  21 #ifndef N_CPUS
  22 #define N_CPUS 2
  23 #warning defaulting to 2 CPU processes
  24 #endif
  25
  26 // the expensive test is not so expensive for <= 2 CPUs
  27 // If the mutex is used, it's also cheap (300 MB / 4 seconds) for 3 CPUs
  28 // For 3 CPUs and the lock-free option it needs 1.5 GB of RAM
  29 #if N_CPUS <= 2 || (N_CPUS <= 3 && defined USE_MUTEX)
  30 #define TEST_EXPENSIVE
  31 #endif
  32
  33 #ifndef N_EXCLUSIVE
  34 # if !defined N_CYCLES || N_CYCLES <= 1 || defined TEST_EXPENSIVE
  35 #  define N_EXCLUSIVE     2
  36 #  warning defaulting to 2 concurrent exclusive sections
  37 # else
  38 #  define N_EXCLUSIVE     1
  39 #  warning defaulting to 1 concurrent exclusive sections
  40 # endif
  41 #endif
  42 #ifndef N_CYCLES
  43 # if N_EXCLUSIVE <= 1 || defined TEST_EXPENSIVE
  44 #  define N_CYCLES        2
  45 #  warning defaulting to 2 CPU cycles
  46 # else
  47 #  define N_CYCLES        1
  48 #  warning defaulting to 1 CPU cycles
  49 # endif
  50 #endif
  51
  52
  53 // synchronization primitives.  condition variables require a
  54 // process-local "cond_t saved;" variable.
  55
  56 #define mutex_t              byte
  57 #define MUTEX_LOCK(m)        atomic { m == 0 -> m = 1 }
  58 #define MUTEX_UNLOCK(m)      m = 0
  59
  60 #define cond_t               int
  61 #define COND_WAIT(c, m)      {                                  \
  62                                saved = c;                       \
  63                                MUTEX_UNLOCK(m);                 \
  64                                c != saved -> MUTEX_LOCK(m);     \
  65                              }
  66 #define COND_BROADCAST(c)    c++
  67
  68 // this is the logic from cpus-common.c
  69
  70 mutex_t mutex;
  71 cond_t exclusive_cond;
  72 cond_t exclusive_resume;
  73 byte pending_cpus;
  74
  75 byte running[N_CPUS];
  76 byte has_waiter[N_CPUS];
  77
  78 #define exclusive_idle()                                          \
  79   do                                                              \
  80       :: pending_cpus -> COND_WAIT(exclusive_resume, mutex);      \
  81       :: else         -> break;                                   \
  82   od
  83
  84 #define start_exclusive()                                         \
  85     MUTEX_LOCK(mutex);                                            \
  86     exclusive_idle();                                             \
  87     pending_cpus = 1;                                             \
  88                                                                   \
  89     i = 0;                                                        \
  90     do                                                            \
  91        :: i < N_CPUS -> {                                         \
  92            if                                                     \
  93               :: running[i] -> has_waiter[i] = 1; pending_cpus++; \
  94               :: else       -> skip;                              \
  95            fi;                                                    \
  96            i++;                                                   \
  97        }                                                          \
  98        :: else -> break;                                          \
  99     od;                                                           \
 100                                                                   \
 101     do                                                            \
 102       :: pending_cpus > 1 -> COND_WAIT(exclusive_cond, mutex);    \
 103       :: else             -> break;                               \
 104     od;                                                           \
 105     MUTEX_UNLOCK(mutex);
 106
 107 #define end_exclusive()                                           \
 108     MUTEX_LOCK(mutex);                                            \
 109     pending_cpus = 0;                                             \
 110     COND_BROADCAST(exclusive_resume);                             \
 111     MUTEX_UNLOCK(mutex);
 112
 113 #ifdef USE_MUTEX
 114 // Simple version using mutexes
 115 #define cpu_exec_start(id)                                                   \
 116     MUTEX_LOCK(mutex);                                                       \
 117     exclusive_idle();                                                        \
 118     running[id] = 1;                                                         \
 119     MUTEX_UNLOCK(mutex);
 120
 121 #define cpu_exec_end(id)                                                     \
 122     MUTEX_LOCK(mutex);                                                       \
 123     running[id] = 0;                                                         \
 124     if                                                                       \
 125         :: pending_cpus -> {                                                 \
 126             pending_cpus--;                                                  \
 127             if                                                               \
 128                 :: pending_cpus == 1 -> COND_BROADCAST(exclusive_cond);      \
 129                 :: else -> skip;                                             \
 130             fi;                                                              \
 131         }                                                                    \
 132         :: else -> skip;                                                     \
 133     fi;                                                                      \
 134     MUTEX_UNLOCK(mutex);
 135 #else
 136 // Wait-free fast path, only needs mutex when concurrent with
 137 // an exclusive section
 138 #define cpu_exec_start(id)                                                   \
 139     running[id] = 1;                                                         \
 140     if                                                                       \
 141         :: pending_cpus -> {                                                 \
 142             MUTEX_LOCK(mutex);                                               \
 143             if                                                               \
 144                 :: !has_waiter[id] -> {                                      \
 145                     running[id] = 0;                                         \
 146                     exclusive_idle();                                        \
 147                     running[id] = 1;                                         \
 148                 }                                                            \
 149                 :: else -> skip;                                             \
 150             fi;                                                              \
 151             MUTEX_UNLOCK(mutex);                                             \
 152         }                                                                    \
 153         :: else -> skip;                                                     \
 154     fi;
 155
 156 #define cpu_exec_end(id)                                                     \
 157     running[id] = 0;                                                         \
 158     if                                                                       \
 159         :: pending_cpus -> {                                                 \
 160             MUTEX_LOCK(mutex);                                               \
 161             if                                                               \
 162                 :: has_waiter[id] -> {                                       \
 163                     has_waiter[id] = 0;                                      \
 164                     pending_cpus--;                                          \
 165                     if                                                       \
 166                         :: pending_cpus == 1 -> COND_BROADCAST(exclusive_cond); \
 167                         :: else -> skip;                                     \
 168                     fi;                                                      \
 169                 }                                                            \
 170                 :: else -> skip;                                             \
 171             fi;                                                              \
 172             MUTEX_UNLOCK(mutex);                                             \
 173         }                                                                    \
 174         :: else -> skip;                                                     \
 175     fi
 176 #endif
 177
 178 // Promela processes
 179
 180 byte done_cpu;
 181 byte in_cpu;
 182 active[N_CPUS] proctype cpu()
 183 {
 184     byte id = _pid % N_CPUS;
 185     byte cycles = 0;
 186     cond_t saved;
 187
 188     do
 189        :: cycles == N_CYCLES -> break;
 190        :: else -> {
 191            cycles++;
 192            cpu_exec_start(id)
 193            in_cpu++;
 194            done_cpu++;
 195            in_cpu--;
 196            cpu_exec_end(id)
 197        }
 198     od;
 199 }
 200
 201 byte done_exclusive;
 202 byte in_exclusive;
 203 active[N_EXCLUSIVE] proctype exclusive()
 204 {
 205     cond_t saved;
 206     byte i;
 207
 208     start_exclusive();
 209     in_exclusive = 1;
 210     done_exclusive++;
 211     in_exclusive = 0;
 212     end_exclusive();
 213 }
 214
 215 #define LIVENESS   (done_cpu == N_CPUS * N_CYCLES && done_exclusive == N_EXCLUSIVE)
 216 #define SAFETY     !(in_exclusive && in_cpu)
 217
 218 never {    /* ! ([] SAFETY && <> [] LIVENESS) */
 219     do
 220     // once the liveness property is satisfied, this is not executable
 221     // and the never clause is not accepted
 222     :: ! LIVENESS -> accept_liveness: skip
 223     :: 1          -> assert(SAFETY)
 224     od;
 225 }