docs/aio_notify.promela

   1 /*
   2  * This model describes the interaction between aio_set_dispatching()
   3  * and aio_notify().
   4  *
   5  * Author: Paolo Bonzini <[email protected]>
   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
  19 #define MAX   4
  20 #define LAST  (1 << (MAX - 1))
  21 #define FINAL ((LAST << 1) - 1)
  22
  23 bool dispatching;
  24 bool event;
  25
  26 int req, done;
  27
  28 active proctype waiter()
  29 {
  30      int fetch, blocking;
  31
  32      do
  33         :: done != FINAL -> {
  34             // Computing "blocking" is separate from execution of the
  35             // "bottom half"
  36             blocking = (req == 0);
  37
  38             // This is our "bottom half"
  39             atomic { fetch = req; req = 0; }
  40             done = done | fetch;
  41
  42             // Wait for a nudge from the other side
  43             do
  44                 :: event == 1 -> { event = 0; break; }
  45                 :: !blocking  -> break;
  46             od;
  47
  48             dispatching = 1;
  49
  50             // If you are simulating this model, you may want to add
  51             // something like this here:
  52             //
  53             //      int foo; foo++; foo++; foo++;
  54             //
  55             // This only wastes some time and makes it more likely
  56             // that the notifier process hits the "fast path".
  57
  58             dispatching = 0;
  59         }
  60         :: else -> break;
  61     od
  62 }
  63
  64 active proctype notifier()
  65 {
  66     int next = 1;
  67     int sets = 0;
  68
  69     do
  70         :: next <= LAST -> {
  71             // generate a request
  72             req = req | next;
  73             next = next << 1;
  74
  75             // aio_notify
  76             if
  77                 :: dispatching == 0 -> sets++; event = 1;
  78                 :: else             -> skip;
  79             fi;
  80
  81             // Test both synchronous and asynchronous delivery
  82             if
  83                 :: 1 -> do
  84                             :: req == 0 -> break;
  85                         od;
  86                 :: 1 -> skip;
  87             fi;
  88         }
  89         :: else -> break;
  90     od;
  91     printf("Skipped %d event_notifier_set\n", MAX - sets);
  92 }
  93
  94 #define p (done == FINAL)
  95
  96 never  {
  97     do
  98         :: 1                      // after an arbitrarily long prefix
  99         :: p -> break             // p becomes true
 100     od;
 101     do
 102         :: !p -> accept: break    // it then must remains true forever after
 103     od
 104 }