LXR qemu/docs/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
  16bool event;
  17int 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
  38int state = EV_FREE;
  39
  40int 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
  56int 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
  80active 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
  94active proctype notifier()
  95{
  96    value = true;
  97    SET;
  98}
  99