@samitouri / QOSamiQemu
Code Commits Issues Pulls Sessions CI/CD
master
master
promela 225 lines 9.32 KB
Raw
1 /*
2 * This model describes the implementation of exclusive sections in
3 * cpu-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 cpu-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 }