docs/spin/aio_notify_accept.promela

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