blob: 9cef2c955dd0059270c14289d121f6c3cf7d1ce8 (
plain) (
blame)
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
|
/*
* This model describes the interaction between ctx->notified
* and ctx->notifier.
*
* 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 the buggy version:
* spin -a -DBUG1 docs/aio_notify_bug.promela
* gcc -O2 pan.c
* ./a.out -a -f
* (or -DBUG2)
*
* To verify the fixed version:
* spin -a docs/aio_notify_bug.promela
* gcc -O2 pan.c
* ./a.out -a -f
*
* Add -DCHECK_REQ to test an alternative invariant and the
* "notify_me" optimization.
*/
int notify_me;
bool notified;
bool event;
bool req;
bool notifier_done;
#ifdef CHECK_REQ
#define USE_NOTIFY_ME 1
#else
#define USE_NOTIFY_ME 0
#endif
#ifdef BUG
#error Please define BUG1 or BUG2 instead.
#endif
active proctype notifier()
{
do
:: true -> {
req = 1;
if
:: !USE_NOTIFY_ME || notify_me ->
#if defined BUG1
/* CHECK_REQ does not detect this bug! */
notified = 1;
event = 1;
#elif defined BUG2
if
:: !notified -> event = 1;
:: else -> skip;
fi;
notified = 1;
#else
event = 1;
notified = 1;
#endif
:: else -> skip;
fi
}
:: true -> break;
od;
notifier_done = 1;
}
#define AIO_POLL \
notify_me++; \
if \
:: !req -> { \
if \
:: event -> skip; \
fi; \
} \
:: else -> skip; \
fi; \
notify_me--; \
\
atomic { old = notified; notified = 0; } \
if \
:: old -> event = 0; \
:: else -> skip; \
fi; \
\
req = 0;
active proctype waiter()
{
bool old;
do
:: true -> AIO_POLL;
od;
}
/* Same as waiter(), but disappears after a while. */
active proctype temporary_waiter()
{
bool old;
do
:: true -> AIO_POLL;
:: true -> break;
od;
}
#ifdef CHECK_REQ
never {
do
:: req -> goto accept_if_req_not_eventually_false;
:: true -> skip;
od;
accept_if_req_not_eventually_false:
if
:: req -> goto accept_if_req_not_eventually_false;
fi;
assert(0);
}
#else
/* There must be infinitely many transitions of event as long
* as the notifier does not exit.
*
* If event stayed always true, the waiters would be busy looping.
* If event stayed always false, the waiters would be sleeping
* forever.
*/
never {
do
:: !event -> goto accept_if_event_not_eventually_true;
:: event -> goto accept_if_event_not_eventually_false;
:: true -> skip;
od;
accept_if_event_not_eventually_true:
if
:: !event && notifier_done -> do :: true -> skip; od;
:: !event && !notifier_done -> goto accept_if_event_not_eventually_true;
fi;
assert(0);
accept_if_event_not_eventually_false:
if
:: event -> goto accept_if_event_not_eventually_false;
fi;
assert(0);
}
#endif
|
