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_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
     25int notify_me;
     26bool notified;
     27bool event;
     28bool req;
     29bool 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
     41active 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
     90active 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.  */
    100active 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
    111never {
    112    do
    113        :: req -> goto accept_if_req_not_eventually_false;
    114        :: true -> skip;
    115    od;
    116
    117accept_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 */
    132never {
    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
    139accept_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
    146accept_if_event_not_eventually_false:
    147    if
    148        :: event     -> goto accept_if_event_not_eventually_false;
    149    fi;
    150    assert(0);
    151}
    152#endif