forked from aliguori/qemu
-
Notifications
You must be signed in to change notification settings - Fork 12
/
Copy pathtcg-exclusive.promela
225 lines (202 loc) · 9.32 KB
/
tcg-exclusive.promela
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
/*
* This model describes the implementation of exclusive sections in
* cpus-common.c (start_exclusive, end_exclusive, cpu_exec_start,
* cpu_exec_end).
*
* Author: Paolo Bonzini <[email protected]>
*
* This file is in the public domain. If you really want a license,
* the WTFPL will do.
*
* To verify it:
* spin -a docs/tcg-exclusive.promela
* gcc pan.c -O2
* ./a.out -a
*
* Tunable processor macros: N_CPUS, N_EXCLUSIVE, N_CYCLES, USE_MUTEX,
* TEST_EXPENSIVE.
*/
// Define the missing parameters for the model
#ifndef N_CPUS
#define N_CPUS 2
#warning defaulting to 2 CPU processes
#endif
// the expensive test is not so expensive for <= 2 CPUs
// If the mutex is used, it's also cheap (300 MB / 4 seconds) for 3 CPUs
// For 3 CPUs and the lock-free option it needs 1.5 GB of RAM
#if N_CPUS <= 2 || (N_CPUS <= 3 && defined USE_MUTEX)
#define TEST_EXPENSIVE
#endif
#ifndef N_EXCLUSIVE
# if !defined N_CYCLES || N_CYCLES <= 1 || defined TEST_EXPENSIVE
# define N_EXCLUSIVE 2
# warning defaulting to 2 concurrent exclusive sections
# else
# define N_EXCLUSIVE 1
# warning defaulting to 1 concurrent exclusive sections
# endif
#endif
#ifndef N_CYCLES
# if N_EXCLUSIVE <= 1 || defined TEST_EXPENSIVE
# define N_CYCLES 2
# warning defaulting to 2 CPU cycles
# else
# define N_CYCLES 1
# warning defaulting to 1 CPU cycles
# endif
#endif
// synchronization primitives. condition variables require a
// process-local "cond_t saved;" variable.
#define mutex_t byte
#define MUTEX_LOCK(m) atomic { m == 0 -> m = 1 }
#define MUTEX_UNLOCK(m) m = 0
#define cond_t int
#define COND_WAIT(c, m) { \
saved = c; \
MUTEX_UNLOCK(m); \
c != saved -> MUTEX_LOCK(m); \
}
#define COND_BROADCAST(c) c++
// this is the logic from cpus-common.c
mutex_t mutex;
cond_t exclusive_cond;
cond_t exclusive_resume;
byte pending_cpus;
byte running[N_CPUS];
byte has_waiter[N_CPUS];
#define exclusive_idle() \
do \
:: pending_cpus -> COND_WAIT(exclusive_resume, mutex); \
:: else -> break; \
od
#define start_exclusive() \
MUTEX_LOCK(mutex); \
exclusive_idle(); \
pending_cpus = 1; \
\
i = 0; \
do \
:: i < N_CPUS -> { \
if \
:: running[i] -> has_waiter[i] = 1; pending_cpus++; \
:: else -> skip; \
fi; \
i++; \
} \
:: else -> break; \
od; \
\
do \
:: pending_cpus > 1 -> COND_WAIT(exclusive_cond, mutex); \
:: else -> break; \
od; \
MUTEX_UNLOCK(mutex);
#define end_exclusive() \
MUTEX_LOCK(mutex); \
pending_cpus = 0; \
COND_BROADCAST(exclusive_resume); \
MUTEX_UNLOCK(mutex);
#ifdef USE_MUTEX
// Simple version using mutexes
#define cpu_exec_start(id) \
MUTEX_LOCK(mutex); \
exclusive_idle(); \
running[id] = 1; \
MUTEX_UNLOCK(mutex);
#define cpu_exec_end(id) \
MUTEX_LOCK(mutex); \
running[id] = 0; \
if \
:: pending_cpus -> { \
pending_cpus--; \
if \
:: pending_cpus == 1 -> COND_BROADCAST(exclusive_cond); \
:: else -> skip; \
fi; \
} \
:: else -> skip; \
fi; \
MUTEX_UNLOCK(mutex);
#else
// Wait-free fast path, only needs mutex when concurrent with
// an exclusive section
#define cpu_exec_start(id) \
running[id] = 1; \
if \
:: pending_cpus -> { \
MUTEX_LOCK(mutex); \
if \
:: !has_waiter[id] -> { \
running[id] = 0; \
exclusive_idle(); \
running[id] = 1; \
} \
:: else -> skip; \
fi; \
MUTEX_UNLOCK(mutex); \
} \
:: else -> skip; \
fi;
#define cpu_exec_end(id) \
running[id] = 0; \
if \
:: pending_cpus -> { \
MUTEX_LOCK(mutex); \
if \
:: has_waiter[id] -> { \
has_waiter[id] = 0; \
pending_cpus--; \
if \
:: pending_cpus == 1 -> COND_BROADCAST(exclusive_cond); \
:: else -> skip; \
fi; \
} \
:: else -> skip; \
fi; \
MUTEX_UNLOCK(mutex); \
} \
:: else -> skip; \
fi
#endif
// Promela processes
byte done_cpu;
byte in_cpu;
active[N_CPUS] proctype cpu()
{
byte id = _pid % N_CPUS;
byte cycles = 0;
cond_t saved;
do
:: cycles == N_CYCLES -> break;
:: else -> {
cycles++;
cpu_exec_start(id)
in_cpu++;
done_cpu++;
in_cpu--;
cpu_exec_end(id)
}
od;
}
byte done_exclusive;
byte in_exclusive;
active[N_EXCLUSIVE] proctype exclusive()
{
cond_t saved;
byte i;
start_exclusive();
in_exclusive = 1;
done_exclusive++;
in_exclusive = 0;
end_exclusive();
}
#define LIVENESS (done_cpu == N_CPUS * N_CYCLES && done_exclusive == N_EXCLUSIVE)
#define SAFETY !(in_exclusive && in_cpu)
never { /* ! ([] SAFETY && <> [] LIVENESS) */
do
// once the liveness property is satisfied, this is not executable
// and the never clause is not accepted
:: ! LIVENESS -> accept_liveness: skip
:: 1 -> assert(SAFETY)
od;
}