docs/spin/win32-qemu-event.promela

   1 /*
   2  * This model describes the implementation of QemuEvent in
   3  * util/qemu-thread-win32.c.
   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 it:
  11  *     spin -a docs/event.promela
  12  *     gcc -O2 pan.c -DSAFETY
  13  *     ./a.out
  14  */
  15
  16 bool event;
  17 int value;
  18
  19 /* Primitives for a Win32 event */
  20 #define RAW_RESET event = false
  21 #define RAW_SET   event = true
  22 #define RAW_WAIT  do :: event -> break; od
  23
  24 #if 0
  25 /* Basic sanity checking: test the Win32 event primitives */
  26 #define RESET     RAW_RESET
  27 #define SET       RAW_SET
  28 #define WAIT      RAW_WAIT
  29 #else
  30 /* Full model: layer a userspace-only fast path on top of the RAW_*
  31  * primitives.  SET/RESET/WAIT have exactly the same semantics as
  32  * RAW_SET/RAW_RESET/RAW_WAIT, but try to avoid invoking them.
  33  */
  34 #define EV_SET 0
  35 #define EV_FREE 1
  36 #define EV_BUSY -1
  37
  38 int state = EV_FREE;
  39
  40 int xchg_result;
  41 #define SET   if :: state != EV_SET ->                                      \
  42                     atomic { /* xchg_result=xchg(state, EV_SET) */          \
  43                         xchg_result = state;                                \
  44                         state = EV_SET;                                     \
  45                     }                                                       \
  46                     if :: xchg_result == EV_BUSY -> RAW_SET;                \
  47                        :: else -> skip;                                     \
  48                     fi;                                                     \
  49                  :: else -> skip;                                           \
  50               fi
  51
  52 #define RESET if :: state == EV_SET -> atomic { state = state | EV_FREE; }  \
  53                  :: else            -> skip;                                \
  54               fi
  55
  56 int tmp1, tmp2;
  57 #define WAIT  tmp1 = state;                                                 \
  58               if :: tmp1 != EV_SET ->                                       \
  59                     if :: tmp1 == EV_FREE ->                                \
  60                           RAW_RESET;                                        \
  61                           atomic { /* tmp2=cas(state, EV_FREE, EV_BUSY) */  \
  62                               tmp2 = state;                                 \
  63                               if :: tmp2 == EV_FREE -> state = EV_BUSY;     \
  64                                  :: else            -> skip;                \
  65                               fi;                                           \
  66                           }                                                 \
  67                           if :: tmp2 == EV_SET -> tmp1 = EV_SET;            \
  68                              :: else           -> tmp1 = EV_BUSY;           \
  69                           fi;                                               \
  70                        :: else -> skip;                                     \
  71                     fi;                                                     \
  72                     assert(tmp1 != EV_FREE);                                \
  73                     if :: tmp1 == EV_BUSY -> RAW_WAIT;                      \
  74                        :: else -> skip;                                     \
  75                     fi;                                                     \
  76                  :: else -> skip;                                           \
  77               fi
  78 #endif
  79
  80 active proctype waiter()
  81 {
  82      if
  83          :: !value ->
  84              RESET;
  85              if
  86                  :: !value -> WAIT;
  87                  :: else   -> skip;
  88              fi;
  89         :: else -> skip;
  90     fi;
  91     assert(value);
  92 }
  93
  94 active proctype notifier()
  95 {
  96     value = true;
  97     SET;
  98 }