docs/spin/win32-qemu-event.promela


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98

/*
 * This model describes the implementation of QemuEvent in
 * util/qemu-thread-win32.c.
 *
 * Author: Paolo Bonzini <pbonzini@redhat.com>
 *
 * This file is in the public domain.  If you really want a license,
 * the WTFPL will do.
 *
 * To verify it:
 *     spin -a docs/event.promela
 *     gcc -O2 pan.c -DSAFETY
 *     ./a.out
 */

bool event;
int value;

/* Primitives for a Win32 event */
#define RAW_RESET event = false
#define RAW_SET   event = true
#define RAW_WAIT  do :: event -> break; od

#if 0
/* Basic sanity checking: test the Win32 event primitives */
#define RESET     RAW_RESET
#define SET       RAW_SET
#define WAIT      RAW_WAIT
#else
/* Full model: layer a userspace-only fast path on top of the RAW_*
 * primitives.  SET/RESET/WAIT have exactly the same semantics as
 * RAW_SET/RAW_RESET/RAW_WAIT, but try to avoid invoking them.
 */
#define EV_SET 0
#define EV_FREE 1
#define EV_BUSY -1

int state = EV_FREE;

int xchg_result;
#define SET   if :: state != EV_SET ->                                      \
                    atomic { /* xchg_result=xchg(state, EV_SET) */          \
                        xchg_result = state;                                \
                        state = EV_SET;                                     \
                    }                                                       \
                    if :: xchg_result == EV_BUSY -> RAW_SET;                \
                       :: else -> skip;                                     \
                    fi;                                                     \
                 :: else -> skip;                                           \
              fi

#define RESET if :: state == EV_SET -> atomic { state = state | EV_FREE; }  \
                 :: else            -> skip;                                \
              fi

int tmp1, tmp2;
#define WAIT  tmp1 = state;                                                 \
              if :: tmp1 != EV_SET ->                                       \
                    if :: tmp1 == EV_FREE ->                                \
                          RAW_RESET;                                        \
                          atomic { /* tmp2=cas(state, EV_FREE, EV_BUSY) */  \
                              tmp2 = state;                                 \
                              if :: tmp2 == EV_FREE -> state = EV_BUSY;     \
                                 :: else            -> skip;                \
                              fi;                                           \
                          }                                                 \
                          if :: tmp2 == EV_SET -> tmp1 = EV_SET;            \
                             :: else           -> tmp1 = EV_BUSY;           \
                          fi;                                               \
                       :: else -> skip;                                     \
                    fi;                                                     \
                    assert(tmp1 != EV_FREE);                                \
                    if :: tmp1 == EV_BUSY -> RAW_WAIT;                      \
                       :: else -> skip;                                     \
                    fi;                                                     \
                 :: else -> skip;                                           \
              fi
#endif

active proctype waiter()
{
     if
         :: !value ->
             RESET;
             if
                 :: !value -> WAIT;
                 :: else   -> skip;
             fi;
        :: else -> skip;
    fi;
    assert(value);
}

active proctype notifier()
{
    value = true;
    SET;
}