xref: /qemu/docs/spin/aio_notify_accept.promela (revision 6402cbbb) 
1/*
2 * This model describes the interaction between ctx->notified
3 * and ctx->notifier.
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 -DBUG1 docs/aio_notify_bug.promela
12 *     gcc -O2 pan.c
13 *     ./a.out -a -f
14 * (or -DBUG2)
15 *
16 * To verify the fixed version:
17 *     spin -a docs/aio_notify_bug.promela
18 *     gcc -O2 pan.c
19 *     ./a.out -a -f
20 *
21 * Add -DCHECK_REQ to test an alternative invariant and the
22 * "notify_me" optimization.
23 */
24
25int notify_me;
26bool notified;
27bool event;
28bool req;
29bool notifier_done;
30
31#ifdef CHECK_REQ
32#define USE_NOTIFY_ME 1
33#else
34#define USE_NOTIFY_ME 0
35#endif
36
37#ifdef BUG
38#error Please define BUG1 or BUG2 instead.
39#endif
40
41active proctype notifier()
42{
43    do
44        :: true -> {
45            req = 1;
46            if
47               :: !USE_NOTIFY_ME || notify_me ->
48#if defined BUG1
49                   /* CHECK_REQ does not detect this bug! */
50                   notified = 1;
51                   event = 1;
52#elif defined BUG2
53                   if
54                      :: !notified -> event = 1;
55                      :: else -> skip;
56                   fi;
57                   notified = 1;
58#else
59                   event = 1;
60                   notified = 1;
61#endif
62               :: else -> skip;
63            fi
64        }
65        :: true -> break;
66    od;
67    notifier_done = 1;
68}
69
70#define AIO_POLL                                                    \
71    notify_me++;                                                    \
72    if                                                              \
73        :: !req -> {                                                \
74            if                                                      \
75                :: event -> skip;                                   \
76            fi;                                                     \
77        }                                                           \
78        :: else -> skip;                                            \
79    fi;                                                             \
80    notify_me--;                                                    \
81                                                                    \
82    atomic { old = notified; notified = 0; }                        \
83    if                                                              \
84       :: old -> event = 0;                                         \
85       :: else -> skip;                                             \
86    fi;                                                             \
87                                                                    \
88    req = 0;
89
90active proctype waiter()
91{
92    bool old;
93
94    do
95       :: true -> AIO_POLL;
96    od;
97}
98
99/* Same as waiter(), but disappears after a while.  */
100active proctype temporary_waiter()
101{
102    bool old;
103
104    do
105       :: true -> AIO_POLL;
106       :: true -> break;
107    od;
108}
109
110#ifdef CHECK_REQ
111never {
112    do
113        :: req -> goto accept_if_req_not_eventually_false;
114        :: true -> skip;
115    od;
116
117accept_if_req_not_eventually_false:
118    if
119        :: req -> goto accept_if_req_not_eventually_false;
120    fi;
121    assert(0);
122}
123
124#else
125/* There must be infinitely many transitions of event as long
126 * as the notifier does not exit.
127 *
128 * If event stayed always true, the waiters would be busy looping.
129 * If event stayed always false, the waiters would be sleeping
130 * forever.
131 */
132never {
133    do
134        :: !event    -> goto accept_if_event_not_eventually_true;
135        :: event     -> goto accept_if_event_not_eventually_false;
136        :: true      -> skip;
137    od;
138
139accept_if_event_not_eventually_true:
140    if
141        :: !event && notifier_done  -> do :: true -> skip; od;
142        :: !event && !notifier_done -> goto accept_if_event_not_eventually_true;
143    fi;
144    assert(0);
145
146accept_if_event_not_eventually_false:
147    if
148        :: event     -> goto accept_if_event_not_eventually_false;
149    fi;
150    assert(0);
151}
152#endif
153