xref: /qemu/docs/spin/aio_notify_bug.promela (revision 7294e600) 
1/*
2 * This model describes a bug in aio_notify.  If ctx->notifier is
3 * cleared too late, a wakeup could be lost.
4 *
5 * Author: Paolo Bonzini <pbonzini@redhat.com>
6 *
7 * This file is in the public domain.  If you really want a license,
8 * the WTFPL will do.
9 *
10 * To verify the buggy version:
11 *     spin -a -DBUG docs/aio_notify_bug.promela
12 *     gcc -O2 pan.c
13 *     ./a.out -a -f
14 *
15 * To verify the fixed version:
16 *     spin -a docs/aio_notify_bug.promela
17 *     gcc -O2 pan.c
18 *     ./a.out -a -f
19 *
20 * Add -DCHECK_REQ to test an alternative invariant and the
21 * "notify_me" optimization.
22 */
23
24int notify_me;
25bool event;
26bool req;
27bool notifier_done;
28
29#ifdef CHECK_REQ
30#define USE_NOTIFY_ME 1
31#else
32#define USE_NOTIFY_ME 0
33#endif
34
35active proctype notifier()
36{
37    do
38        :: true -> {
39            req = 1;
40            if
41               :: !USE_NOTIFY_ME || notify_me -> event = 1;
42               :: else -> skip;
43            fi
44        }
45        :: true -> break;
46    od;
47    notifier_done = 1;
48}
49
50#ifdef BUG
51#define AIO_POLL                                                    \
52    notify_me++;                                                    \
53    if                                                              \
54        :: !req -> {                                                \
55            if                                                      \
56                :: event -> skip;                                   \
57            fi;                                                     \
58        }                                                           \
59        :: else -> skip;                                            \
60    fi;                                                             \
61    notify_me--;                                                    \
62                                                                    \
63    req = 0;                                                        \
64    event = 0;
65#else
66#define AIO_POLL                                                    \
67    notify_me++;                                                    \
68    if                                                              \
69        :: !req -> {                                                \
70            if                                                      \
71                :: event -> skip;                                   \
72            fi;                                                     \
73        }                                                           \
74        :: else -> skip;                                            \
75    fi;                                                             \
76    notify_me--;                                                    \
77                                                                    \
78    event = 0;                                                      \
79    req = 0;
80#endif
81
82active proctype waiter()
83{
84    do
85       :: true -> AIO_POLL;
86    od;
87}
88
89/* Same as waiter(), but disappears after a while.  */
90active proctype temporary_waiter()
91{
92    do
93       :: true -> AIO_POLL;
94       :: true -> break;
95    od;
96}
97
98#ifdef CHECK_REQ
99never {
100    do
101        :: req -> goto accept_if_req_not_eventually_false;
102        :: true -> skip;
103    od;
104
105accept_if_req_not_eventually_false:
106    if
107        :: req -> goto accept_if_req_not_eventually_false;
108    fi;
109    assert(0);
110}
111
112#else
113/* There must be infinitely many transitions of event as long
114 * as the notifier does not exit.
115 *
116 * If event stayed always true, the waiters would be busy looping.
117 * If event stayed always false, the waiters would be sleeping
118 * forever.
119 */
120never {
121    do
122        :: !event    -> goto accept_if_event_not_eventually_true;
123        :: event     -> goto accept_if_event_not_eventually_false;
124        :: true      -> skip;
125    od;
126
127accept_if_event_not_eventually_true:
128    if
129        :: !event && notifier_done  -> do :: true -> skip; od;
130        :: !event && !notifier_done -> goto accept_if_event_not_eventually_true;
131    fi;
132    assert(0);
133
134accept_if_event_not_eventually_false:
135    if
136        :: event     -> goto accept_if_event_not_eventually_false;
137    fi;
138    assert(0);
139}
140#endif
141