qemu

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
}
226