docs/aio_notify.promela

   1 /*
   2  * This model describes the interaction between ctx->notify_me
   3  * and aio_notify().
   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 simulate it:
  11  *     spin -p docs/aio_notify.promela
  12  *
  13  * To verify it:
  14  *     spin -a docs/aio_notify.promela
  15  *     gcc -O2 pan.c
  16  *     ./a.out -a
  17  *
  18  * To verify it (with a bug planted in the model):
  19  *     spin -a -DBUG docs/aio_notify.promela
  20  *     gcc -O2 pan.c
  21  *     ./a.out -a
  22  */
  23
  24 #define MAX   4
  25 #define LAST  (1 << (MAX - 1))
  26 #define FINAL ((LAST << 1) - 1)
  27
  28 bool notify_me;
  29 bool event;
  30
  31 int req;
  32 int done;
  33
  34 active proctype waiter()
  35 {
  36     int fetch;
  37
  38     do
  39         :: true -> {
  40             notify_me++;
  41
  42             if
  43 #ifndef BUG
  44                 :: (req > 0) -> skip;
  45 #endif
  46                 :: else ->
  47                     // Wait for a nudge from the other side
  48                     do
  49                         :: event == 1 -> { event = 0; break; }
  50                     od;
  51             fi;
  52
  53             notify_me--;
  54
  55             atomic { fetch = req; req = 0; }
  56             done = done | fetch;
  57         }
  58     od
  59 }
  60
  61 active proctype notifier()
  62 {
  63     int next = 1;
  64
  65     do
  66         :: next <= LAST -> {
  67             // generate a request
  68             req = req | next;
  69             next = next << 1;
  70
  71             // aio_notify
  72             if
  73                 :: notify_me == 1 -> event = 1;
  74                 :: else           -> printf("Skipped event_notifier_set\n"); skip;
  75             fi;
  76
  77             // Test both synchronous and asynchronous delivery
  78             if
  79                 :: 1 -> do
  80                             :: req == 0 -> break;
  81                         od;
  82                 :: 1 -> skip;
  83             fi;
  84         }
  85     od;
  86 }
  87
  88 never { /* [] done < FINAL */
  89 accept_init:
  90         do
  91         :: done < FINAL -> skip;
  92         od;
  93 }