]>
Commit | Line | Data |
---|---|---|
a200f2fb PB |
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 | * | |
c265e976 PB |
16 | * Tunable processor macros: N_CPUS, N_EXCLUSIVE, N_CYCLES, USE_MUTEX, |
17 | * TEST_EXPENSIVE. | |
a200f2fb PB |
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 | ||
c265e976 PB |
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) | |
a200f2fb PB |
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; \ | |
758e1b2b PB |
104 | od; \ |
105 | MUTEX_UNLOCK(mutex); | |
a200f2fb PB |
106 | |
107 | #define end_exclusive() \ | |
758e1b2b | 108 | MUTEX_LOCK(mutex); \ |
a200f2fb PB |
109 | pending_cpus = 0; \ |
110 | COND_BROADCAST(exclusive_resume); \ | |
111 | MUTEX_UNLOCK(mutex); | |
112 | ||
c265e976 PB |
113 | #ifdef USE_MUTEX |
114 | // Simple version using mutexes | |
a200f2fb PB |
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; \ | |
a200f2fb | 134 | MUTEX_UNLOCK(mutex); |
c265e976 PB |
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 | |
a200f2fb PB |
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 | } |