These changes are a raw update to a vanilla kernel 4.1.10, with the
[kvmfornfv.git] / qemu / docs / aio_notify.promela
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
28 bool notify_me;
29 bool event;
30
31 int req;
32 int done;
33
34 active 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
61 active 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
88 never { /* [] done < FINAL */
89 accept_init:
90         do
91         :: done < FINAL -> skip;
92         od;
93 }