LXR qemu/docs/aio_notify

   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
 141