cachepc-qemu

Fork of AMDESE/qemu with changes for cachepc side-channel attack
git clone https://git.sinitax.com/sinitax/cachepc-qemu
Log | Files | Refs | Submodules | LICENSE | sfeed.txt

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
     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}