qemu

1
/*
2
 * This model describes a bug in aio_notify.  If ctx->notifier is
3
 * cleared too late, a wakeup could be lost.
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 -DBUG docs/aio_notify_bug.promela
12
 *     gcc -O2 pan.c
13
 *     ./a.out -a -f
14
 *
15
 * To verify the fixed version:
16
 *     spin -a docs/aio_notify_bug.promela
17
 *     gcc -O2 pan.c
18
 *     ./a.out -a -f
19
 *
20
 * Add -DCHECK_REQ to test an alternative invariant and the
21
 * "notify_me" optimization.
22
 */
23

24
int notify_me;
25
bool event;
26
bool req;
27
bool notifier_done;
28

29
#ifdef CHECK_REQ
30
#define USE_NOTIFY_ME 1
31
#else
32
#define USE_NOTIFY_ME 0
33
#endif
34

35
active proctype notifier()
36
{
37
    do
38
        :: true -> {
39
            req = 1;
40
            if
41
               :: !USE_NOTIFY_ME || notify_me -> event = 1;
42
               :: else -> skip;
43
            fi
44
        }
45
        :: true -> break;
46
    od;
47
    notifier_done = 1;
48
}
49

50
#ifdef BUG
51
#define AIO_POLL                                                    \
52
    notify_me++;                                                    \
53
    if                                                              \
54
        :: !req -> {                                                \
55
            if                                                      \
56
                :: event -> skip;                                   \
57
            fi;                                                     \
58
        }                                                           \
59
        :: else -> skip;                                            \
60
    fi;                                                             \
61
    notify_me--;                                                    \
62
                                                                    \
63
    req = 0;                                                        \
64
    event = 0;
65
#else
66
#define AIO_POLL                                                    \
67
    notify_me++;                                                    \
68
    if                                                              \
69
        :: !req -> {                                                \
70
            if                                                      \
71
                :: event -> skip;                                   \
72
            fi;                                                     \
73
        }                                                           \
74
        :: else -> skip;                                            \
75
    fi;                                                             \
76
    notify_me--;                                                    \
77
                                                                    \
78
    event = 0;                                                      \
79
    req = 0;
80
#endif
81

82
active proctype waiter()
83
{
84
    do
85
       :: true -> AIO_POLL;
86
    od;
87
}
88

89
/* Same as waiter(), but disappears after a while.  */
90
active proctype temporary_waiter()
91
{
92
    do
93
       :: true -> AIO_POLL;
94
       :: true -> break;
95
    od;
96
}
97

98
#ifdef CHECK_REQ
99
never {
100
    do
101
        :: req -> goto accept_if_req_not_eventually_false;
102
        :: true -> skip;
103
    od;
104

105
accept_if_req_not_eventually_false:
106
    if
107
        :: req -> goto accept_if_req_not_eventually_false;
108
    fi;
109
    assert(0);
110
}
111

112
#else
113
/* There must be infinitely many transitions of event as long
114
 * as the notifier does not exit.
115
 *
116
 * If event stayed always true, the waiters would be busy looping.
117
 * If event stayed always false, the waiters would be sleeping
118
 * forever.
119
 */
120
never {
121
    do
122
        :: !event    -> goto accept_if_event_not_eventually_true;
123
        :: event     -> goto accept_if_event_not_eventually_false;
124
        :: true      -> skip;
125
    od;
126

127
accept_if_event_not_eventually_true:
128
    if
129
        :: !event && notifier_done  -> do :: true -> skip; od;
130
        :: !event && !notifier_done -> goto accept_if_event_not_eventually_true;
131
    fi;
132
    assert(0);
133

134
accept_if_event_not_eventually_false:
135
    if
136
        :: event     -> goto accept_if_event_not_eventually_false;
137
    fi;
138
    assert(0);
139
}
140
#endif
141