qemu

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
}
94