diff options
| author | Paolo Bonzini <pbonzini@redhat.com> | 2017-06-06 16:46:26 +0200 |
|---|---|---|
| committer | Paolo Bonzini <pbonzini@redhat.com> | 2017-06-07 18:22:03 +0200 |
| commit | ac06724a715864942e2b5e28f92d5d5421f0a0b0 (patch) | |
| tree | 8eeb9a6aeff09669b65573b1d856426cdf87d8bd /docs/win32-qemu-event.promela | |
| parent | 90bb0c04214545beb75044a2742f711335103269 (diff) | |
docs: create config/, devel/ and spin/ subdirectories
Developer documentation should be its own manual. As a start, move all
developer-oriented files to a separate directory.
Also move non-text files to their own directories: docs/config/ for
QEMU -readconfig input, and docs/spin/ for formal models to be used
with the SPIN model checker.
Reviewed-by: Daniel P. Berrange <berrange@redhat.com>
Signed-off-by: Paolo Bonzini <pbonzini@redhat.com>
Diffstat (limited to 'docs/win32-qemu-event.promela')
| -rw-r--r-- | docs/win32-qemu-event.promela | 98 |
1 files changed, 0 insertions, 98 deletions
diff --git a/docs/win32-qemu-event.promela b/docs/win32-qemu-event.promela deleted file mode 100644 index c446a71555..0000000000 --- a/docs/win32-qemu-event.promela +++ /dev/null @@ -1,98 +0,0 @@ -/* - * 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; -} |