cachepc-qemu

Fork of AMDESE/qemu with changes for cachepc side-channel attack
git clone https://git.sinitax.com/sinitax/cachepc-qemu
Log | Files | Refs | Submodules | LICENSE | sfeed.txt

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
     24int notify_me;
     25bool event;
     26bool req;
     27bool notifier_done;
     28
     29#ifdef CHECK_REQ
     30#define USE_NOTIFY_ME 1
     31#else
     32#define USE_NOTIFY_ME 0
     33#endif
     34
     35active 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
     82active proctype waiter()
     83{
     84    do
     85       :: true -> AIO_POLL;
     86    od;
     87}
     88
     89/* Same as waiter(), but disappears after a while.  */
     90active proctype temporary_waiter()
     91{
     92    do
     93       :: true -> AIO_POLL;
     94       :: true -> break;
     95    od;
     96}
     97
     98#ifdef CHECK_REQ
     99never {
    100    do
    101        :: req -> goto accept_if_req_not_eventually_false;
    102        :: true -> skip;
    103    od;
    104
    105accept_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 */
    120never {
    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
    127accept_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
    134accept_if_event_not_eventually_false:
    135    if
    136        :: event     -> goto accept_if_event_not_eventually_false;
    137    fi;
    138    assert(0);
    139}
    140#endif