qemu

FORK: QEMU emulator
git clone https://git.neptards.moe/neptards/qemu.git
Log | Files | Refs | Submodules | LICENSE

aio_notify_bug.promela (4164B)

      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