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
70mutex_t mutex;
71cond_t exclusive_cond;
72cond_t exclusive_resume;
73byte pending_cpus;
74
75byte running[N_CPUS];
76byte 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
180byte done_cpu;
181byte in_cpu;
182active[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
201byte done_exclusive;
202byte in_exclusive;
203active[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
218never {    /* ! ([] 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}
226