xref: /qemu/docs/spin/aio_notify.promela (revision 417296c8) 
1/*
2 * This model describes the interaction between ctx->notify_me
3 * and aio_notify().
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 simulate it:
11 *     spin -p docs/aio_notify.promela
12 *
13 * To verify it:
14 *     spin -a docs/aio_notify.promela
15 *     gcc -O2 pan.c
16 *     ./a.out -a
17 *
18 * To verify it (with a bug planted in the model):
19 *     spin -a -DBUG docs/aio_notify.promela
20 *     gcc -O2 pan.c
21 *     ./a.out -a
22 */
23
24#define MAX   4
25#define LAST  (1 << (MAX - 1))
26#define FINAL ((LAST << 1) - 1)
27
28bool notify_me;
29bool event;
30
31int req;
32int done;
33
34active proctype waiter()
35{
36    int fetch;
37
38    do
39        :: true -> {
40            notify_me++;
41
42            if
43#ifndef BUG
44                :: (req > 0) -> skip;
45#endif
46                :: else ->
47                    // Wait for a nudge from the other side
48                    do
49                        :: event == 1 -> { event = 0; break; }
50                    od;
51            fi;
52
53            notify_me--;
54
55            atomic { fetch = req; req = 0; }
56            done = done | fetch;
57        }
58    od
59}
60
61active proctype notifier()
62{
63    int next = 1;
64
65    do
66        :: next <= LAST -> {
67            // generate a request
68            req = req | next;
69            next = next << 1;
70
71            // aio_notify
72            if
73                :: notify_me == 1 -> event = 1;
74                :: else           -> printf("Skipped event_notifier_set\n"); skip;
75            fi;
76
77            // Test both synchronous and asynchronous delivery
78            if
79                :: 1 -> do
80                            :: req == 0 -> break;
81                        od;
82                :: 1 -> skip;
83            fi;
84        }
85    od;
86}
87
88never { /* [] done < FINAL */
89accept_init:
90        do
91        :: done < FINAL -> skip;
92        od;
93}
94