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 <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, 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     MUTEX_UNLOCK(mutex);
 103
 104 #define end_exclusive()                                           \
 105     MUTEX_LOCK(mutex);                                            \
 106     pending_cpus = 0;                                             \
 107     COND_BROADCAST(exclusive_resume);                             \
 108     MUTEX_UNLOCK(mutex);
 109
 110 #define cpu_exec_start(id)                                                   \
 111     MUTEX_LOCK(mutex);                                                       \
 112     exclusive_idle();                                                        \
 113     running[id] = 1;                                                         \
 114     MUTEX_UNLOCK(mutex);
 115
 116 #define cpu_exec_end(id)                                                     \
 117     MUTEX_LOCK(mutex);                                                       \
 118     running[id] = 0;                                                         \
 119     if                                                                       \
 120         :: pending_cpus -> {                                                 \
 121             pending_cpus--;                                                  \
 122             if                                                               \
 123                 :: pending_cpus == 1 -> COND_BROADCAST(exclusive_cond);      \
 124                 :: else -> skip;                                             \
 125             fi;                                                              \
 126         }                                                                    \
 127         :: else -> skip;                                                     \
 128     fi;                                                                      \
 129     MUTEX_UNLOCK(mutex);
 130
 131 // Promela processes
 132
 133 byte done_cpu;
 134 byte in_cpu;
 135 active[N_CPUS] proctype cpu()
 136 {
 137     byte id = _pid % N_CPUS;
 138     byte cycles = 0;
 139     cond_t saved;
 140
 141     do
 142        :: cycles == N_CYCLES -> break;
 143        :: else -> {
 144            cycles++;
 145            cpu_exec_start(id)
 146            in_cpu++;
 147            done_cpu++;
 148            in_cpu--;
 149            cpu_exec_end(id)
 150        }
 151     od;
 152 }
 153
 154 byte done_exclusive;
 155 byte in_exclusive;
 156 active[N_EXCLUSIVE] proctype exclusive()
 157 {
 158     cond_t saved;
 159     byte i;
 160
 161     start_exclusive();
 162     in_exclusive = 1;
 163     done_exclusive++;
 164     in_exclusive = 0;
 165     end_exclusive();
 166 }
 167
 168 #define LIVENESS   (done_cpu == N_CPUS * N_CYCLES && done_exclusive == N_EXCLUSIVE)
 169 #define SAFETY     !(in_exclusive && in_cpu)
 170
 171 never {    /* ! ([] SAFETY && <> [] LIVENESS) */
 172     do
 173     // once the liveness property is satisfied, this is not executable
 174     // and the never clause is not accepted
 175     :: ! LIVENESS -> accept_liveness: skip
 176     :: 1          -> assert(SAFETY)
 177     od;
 178 }