docs/spin/aio_notify_bug.promela

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