hw/arm/virt: pass VirtMachineState instead of VirtGuestInfo
[qemu.git] / 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, 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 }