qemu

FORK: QEMU emulator
git clone https://git.neptards.moe/neptards/qemu.git
Log | Files | Refs | Submodules | LICENSE

win32-qemu-event.promela (3744B)

      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 }