LXR qemu/docs/aio_notify

   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
 153