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