qemu/docs/aio_notify.promela
<<
>>
Prefs
   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
  28bool notify_me;
  29bool event;
  30
  31int req;
  32int done;
  33
  34active 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
  61active 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
  88never { /* [] done < FINAL */
  89accept_init:
  90        do
  91        :: done < FINAL -> skip;
  92        od;
  93}
  94