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