qemu

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
153