meson: Merge trace_events_subdirs array
[qemu/ar7.git] / docs / spin / win32-qemu-event.promela
blobc446a71555339f0f79ca758b7f08cb1267ac05cd
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  */
16 bool event;
17 int value;
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
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
38 int state = EV_FREE;
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
52 #define RESET if :: state == EV_SET -> atomic { state = state | EV_FREE; }  \
53                  :: else            -> skip;                                \
54               fi
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
80 active proctype waiter()
82      if
83          :: !value ->
84              RESET;
85              if
86                  :: !value -> WAIT;
87                  :: else   -> skip;
88              fi;
89         :: else -> skip;
90     fi;
91     assert(value);
94 active proctype notifier()
96     value = true;
97     SET;