docs/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 <[email protected]>
   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, TEST_EXPENSIVE.
  17  */
  18
  19 // Define the missing parameters for the model
  20 #ifndef N_CPUS
  21 #define N_CPUS 2
  22 #warning defaulting to 2 CPU processes
  23 #endif
  24
  25 // the expensive test is not so expensive for <= 3 CPUs
  26 #if N_CPUS <= 3
  27 #define TEST_EXPENSIVE
  28 #endif
  29
  30 #ifndef N_EXCLUSIVE
  31 # if !defined N_CYCLES || N_CYCLES <= 1 || defined TEST_EXPENSIVE
  32 #  define N_EXCLUSIVE     2
  33 #  warning defaulting to 2 concurrent exclusive sections
  34 # else
  35 #  define N_EXCLUSIVE     1
  36 #  warning defaulting to 1 concurrent exclusive sections
  37 # endif
  38 #endif
  39 #ifndef N_CYCLES
  40 # if N_EXCLUSIVE <= 1 || defined TEST_EXPENSIVE
  41 #  define N_CYCLES        2
  42 #  warning defaulting to 2 CPU cycles
  43 # else
  44 #  define N_CYCLES        1
  45 #  warning defaulting to 1 CPU cycles
  46 # endif
  47 #endif
  48
  49
  50 // synchronization primitives.  condition variables require a
  51 // process-local "cond_t saved;" variable.
  52
  53 #define mutex_t              byte
  54 #define MUTEX_LOCK(m)        atomic { m == 0 -> m = 1 }
  55 #define MUTEX_UNLOCK(m)      m = 0
  56
  57 #define cond_t               int
  58 #define COND_WAIT(c, m)      {                                  \
  59                                saved = c;                       \
  60                                MUTEX_UNLOCK(m);                 \
  61                                c != saved -> MUTEX_LOCK(m);     \
  62                              }
  63 #define COND_BROADCAST(c)    c++
  64
  65 // this is the logic from cpus-common.c
  66
  67 mutex_t mutex;
  68 cond_t exclusive_cond;
  69 cond_t exclusive_resume;
  70 byte pending_cpus;
  71
  72 byte running[N_CPUS];
  73 byte has_waiter[N_CPUS];
  74
  75 #define exclusive_idle()                                          \
  76   do                                                              \
  77       :: pending_cpus -> COND_WAIT(exclusive_resume, mutex);      \
  78       :: else         -> break;                                   \
  79   od
  80
  81 #define start_exclusive()                                         \
  82     MUTEX_LOCK(mutex);                                            \
  83     exclusive_idle();                                             \
  84     pending_cpus = 1;                                             \
  85                                                                   \
  86     i = 0;                                                        \
  87     do                                                            \
  88        :: i < N_CPUS -> {                                         \
  89            if                                                     \
  90               :: running[i] -> has_waiter[i] = 1; pending_cpus++; \
  91               :: else       -> skip;                              \
  92            fi;                                                    \
  93            i++;                                                   \
  94        }                                                          \
  95        :: else -> break;                                          \
  96     od;                                                           \
  97                                                                   \
  98     do                                                            \
  99       :: pending_cpus > 1 -> COND_WAIT(exclusive_cond, mutex);    \
 100       :: else             -> break;                               \
 101     od
 102
 103 #define end_exclusive()                                           \
 104     pending_cpus = 0;                                             \
 105     COND_BROADCAST(exclusive_resume);                             \
 106     MUTEX_UNLOCK(mutex);
 107
 108 #define cpu_exec_start(id)                                                   \
 109     MUTEX_LOCK(mutex);                                                       \
 110     exclusive_idle();                                                        \
 111     running[id] = 1;                                                         \
 112     MUTEX_UNLOCK(mutex);
 113
 114 #define cpu_exec_end(id)                                                     \
 115     MUTEX_LOCK(mutex);                                                       \
 116     running[id] = 0;                                                         \
 117     if                                                                       \
 118         :: pending_cpus -> {                                                 \
 119             pending_cpus--;                                                  \
 120             if                                                               \
 121                 :: pending_cpus == 1 -> COND_BROADCAST(exclusive_cond);      \
 122                 :: else -> skip;                                             \
 123             fi;                                                              \
 124         }                                                                    \
 125         :: else -> skip;                                                     \
 126     fi;                                                                      \
 127     exclusive_idle();                                                        \
 128     MUTEX_UNLOCK(mutex);
 129
 130 // Promela processes
 131
 132 byte done_cpu;
 133 byte in_cpu;
 134 active[N_CPUS] proctype cpu()
 135 {
 136     byte id = _pid % N_CPUS;
 137     byte cycles = 0;
 138     cond_t saved;
 139
 140     do
 141        :: cycles == N_CYCLES -> break;
 142        :: else -> {
 143            cycles++;
 144            cpu_exec_start(id)
 145            in_cpu++;
 146            done_cpu++;
 147            in_cpu--;
 148            cpu_exec_end(id)
 149        }
 150     od;
 151 }
 152
 153 byte done_exclusive;
 154 byte in_exclusive;
 155 active[N_EXCLUSIVE] proctype exclusive()
 156 {
 157     cond_t saved;
 158     byte i;
 159
 160     start_exclusive();
 161     in_exclusive = 1;
 162     done_exclusive++;
 163     in_exclusive = 0;
 164     end_exclusive();
 165 }
 166
 167 #define LIVENESS   (done_cpu == N_CPUS * N_CYCLES && done_exclusive == N_EXCLUSIVE)
 168 #define SAFETY     !(in_exclusive && in_cpu)
 169
 170 never {    /* ! ([] SAFETY && <> [] LIVENESS) */
 171     do
 172     // once the liveness property is satisfied, this is not executable
 173     // and the never clause is not accepted
 174     :: ! LIVENESS -> accept_liveness: skip
 175     :: 1          -> assert(SAFETY)
 176     od;
 177 }