hw/arm/virt: pass VirtMachineState instead of VirtGuestInfo
[qemu.git] / docs / aio_notify_accept.promela
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
25 int notify_me;
26 bool notified;
27 bool event;
28 bool req;
29 bool 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
41 active 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
90 active 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.  */
100 active 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
111 never {
112     do
113         :: req -> goto accept_if_req_not_eventually_false;
114         :: true -> skip;
115     od;
116
117 accept_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  */
132 never {
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
139 accept_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
146 accept_if_event_not_eventually_false:
147     if
148         :: event     -> goto accept_if_event_not_eventually_false;
149     fi;
150     assert(0);
151 }
152 #endif