blob: 5889b40638832f8dd2e2e8203b42b2eaa0c4d7f7 (
plain)
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
|
/*
* 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 <pbonzini@redhat.com>
*
* 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, 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 <= 3 CPUs
#if N_CPUS <= 3
#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
#define end_exclusive() \
pending_cpus = 0; \
COND_BROADCAST(exclusive_resume); \
MUTEX_UNLOCK(mutex);
#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; \
exclusive_idle(); \
MUTEX_UNLOCK(mutex);
// 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;
}
|
