docs/aio_notify.promela


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93

/*
 * This model describes the interaction between ctx->notify_me
 * and aio_notify().
 *
 * Author: Paolo Bonzini <pbonzini@redhat.com>
 *
 * This file is in the public domain.  If you really want a license,
 * the WTFPL will do.
 *
 * To simulate it:
 *     spin -p docs/aio_notify.promela
 *
 * To verify it:
 *     spin -a docs/aio_notify.promela
 *     gcc -O2 pan.c
 *     ./a.out -a
 *
 * To verify it (with a bug planted in the model):
 *     spin -a -DBUG docs/aio_notify.promela
 *     gcc -O2 pan.c
 *     ./a.out -a
 */

#define MAX   4
#define LAST  (1 << (MAX - 1))
#define FINAL ((LAST << 1) - 1)

bool notify_me;
bool event;

int req;
int done;

active proctype waiter()
{
    int fetch;

    do
        :: true -> {
            notify_me++;

            if
#ifndef BUG
                :: (req > 0) -> skip;
#endif
                :: else ->
                    // Wait for a nudge from the other side
                    do
                        :: event == 1 -> { event = 0; break; }
                    od;
            fi;

            notify_me--;

            atomic { fetch = req; req = 0; }
            done = done | fetch;
        }
    od
}

active proctype notifier()
{
    int next = 1;

    do
        :: next <= LAST -> {
            // generate a request
            req = req | next;
            next = next << 1;

            // aio_notify
            if
                :: notify_me == 1 -> event = 1;
                :: else           -> printf("Skipped event_notifier_set\n"); skip;
            fi;

            // Test both synchronous and asynchronous delivery
            if
                :: 1 -> do
                            :: req == 0 -> break;
                        od;
                :: 1 -> skip;
            fi;
        }
    od;
}

never { /* [] done < FINAL */
accept_init:
        do
        :: done < FINAL -> skip;
        od;
}