hw/arm/virt: pass VirtMachineState instead of VirtGuestInfo
[qemu.git] / docs / aio_notify_bug.promela
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
24 int notify_me;
25 bool event;
26 bool req;
27 bool notifier_done;
28
29 #ifdef CHECK_REQ
30 #define USE_NOTIFY_ME 1
31 #else
32 #define USE_NOTIFY_ME 0
33 #endif
34
35 active 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
82 active proctype waiter()
83 {
84     do
85        :: true -> AIO_POLL;
86     od;
87 }
88
89 /* Same as waiter(), but disappears after a while.  */
90 active proctype temporary_waiter()
91 {
92     do
93        :: true -> AIO_POLL;
94        :: true -> break;
95     od;
96 }
97
98 #ifdef CHECK_REQ
99 never {
100     do
101         :: req -> goto accept_if_req_not_eventually_false;
102         :: true -> skip;
103     od;
104
105 accept_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  */
120 never {
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
127 accept_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
134 accept_if_event_not_eventually_false:
135     if
136         :: event     -> goto accept_if_event_not_eventually_false;
137     fi;
138     assert(0);
139 }
140 #endif