qemu

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

aio_notify_accept.promela (4052B)

      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