diff options
| author |   José Pekkarinen <jose.pekkarinen@nokia.com> | 2016-05-18 13:18:31 +0300 |
|---|---|---|
| committer | José Pekkarinen <jose.pekkarinen@nokia.com> | 2016-05-18 13:42:15 +0300 |
| commit | 437fd90c0250dee670290f9b714253671a990160 (patch) | |
| tree | b871786c360704244a07411c69fb58da9ead4a06 /qemu/docs/win32-qemu-event.promela | |
| parent | 5bbd6fe9b8bab2a93e548c5a53b032d1939eec05 (diff) | |
These changes are the raw update to qemu-2.6.
Collission happened in the following patches:
migration: do cleanup operation after completion(738df5b9)
Bug fix.(1750c932f86)
kvmclock: add a new function to update env->tsc.(b52baab2)
The code provided by the patches was already in the upstreamed
version.
Change-Id: I3cc11841a6a76ae20887b2e245710199e1ea7f9a
Signed-off-by: José Pekkarinen <jose.pekkarinen@nokia.com>
Diffstat (limited to 'qemu/docs/win32-qemu-event.promela')
| -rw-r--r-- | qemu/docs/win32-qemu-event.promela | 98 |
1 files changed, 98 insertions, 0 deletions
diff --git a/qemu/docs/win32-qemu-event.promela b/qemu/docs/win32-qemu-event.promela new file mode 100644 index 000000000..c446a7155 --- /dev/null +++ b/qemu/docs/win32-qemu-event.promela @@ -0,0 +1,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; +} |