blob: b3bfca1ca4f52f73365c413af97c0bd739be922d (
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
|
/*
* This model describes a bug in aio_notify. If ctx->notifier is
* cleared too late, a wakeup could be lost.
*
* 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 -DBUG docs/aio_notify_bug.promela
* gcc -O2 pan.c
* ./a.out -a -f
*
* 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 event;
bool req;
bool notifier_done;
#ifdef CHECK_REQ
#define USE_NOTIFY_ME 1
#else
#define USE_NOTIFY_ME 0
#endif
active proctype notifier()
{
do
:: true -> {
req = 1;
if
:: !USE_NOTIFY_ME || notify_me -> event = 1;
:: else -> skip;
fi
}
:: true -> break;
od;
notifier_done = 1;
}
#ifdef BUG
#define AIO_POLL \
notify_me++; \
if \
:: !req -> { \
if \
:: event -> skip; \
fi; \
} \
:: else -> skip; \
fi; \
notify_me--; \
\
req = 0; \
event = 0;
#else
#define AIO_POLL \
notify_me++; \
if \
:: !req -> { \
if \
:: event -> skip; \
fi; \
} \
:: else -> skip; \
fi; \
notify_me--; \
\
event = 0; \
req = 0;
#endif
active proctype waiter()
{
do
:: true -> AIO_POLL;
od;
}
/* Same as waiter(), but disappears after a while. */
active proctype temporary_waiter()
{
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
|
