1*7c9b2bf6SPaolo Bonzini/* 2*7c9b2bf6SPaolo Bonzini * This model describes the implementation of QemuEvent in 3*7c9b2bf6SPaolo Bonzini * util/qemu-thread-win32.c. 4*7c9b2bf6SPaolo Bonzini * 5*7c9b2bf6SPaolo Bonzini * Author: Paolo Bonzini <pbonzini@redhat.com> 6*7c9b2bf6SPaolo Bonzini * 7*7c9b2bf6SPaolo Bonzini * This file is in the public domain. If you really want a license, 8*7c9b2bf6SPaolo Bonzini * the WTFPL will do. 9*7c9b2bf6SPaolo Bonzini * 10*7c9b2bf6SPaolo Bonzini * To verify it: 11*7c9b2bf6SPaolo Bonzini * spin -a docs/event.promela 12*7c9b2bf6SPaolo Bonzini * gcc -O2 pan.c -DSAFETY 13*7c9b2bf6SPaolo Bonzini * ./a.out 14*7c9b2bf6SPaolo Bonzini */ 15*7c9b2bf6SPaolo Bonzini 16*7c9b2bf6SPaolo Bonzinibool event; 17*7c9b2bf6SPaolo Bonziniint value; 18*7c9b2bf6SPaolo Bonzini 19*7c9b2bf6SPaolo Bonzini/* Primitives for a Win32 event */ 20*7c9b2bf6SPaolo Bonzini#define RAW_RESET event = false 21*7c9b2bf6SPaolo Bonzini#define RAW_SET event = true 22*7c9b2bf6SPaolo Bonzini#define RAW_WAIT do :: event -> break; od 23*7c9b2bf6SPaolo Bonzini 24*7c9b2bf6SPaolo Bonzini#if 0 25*7c9b2bf6SPaolo Bonzini/* Basic sanity checking: test the Win32 event primitives */ 26*7c9b2bf6SPaolo Bonzini#define RESET RAW_RESET 27*7c9b2bf6SPaolo Bonzini#define SET RAW_SET 28*7c9b2bf6SPaolo Bonzini#define WAIT RAW_WAIT 29*7c9b2bf6SPaolo Bonzini#else 30*7c9b2bf6SPaolo Bonzini/* Full model: layer a userspace-only fast path on top of the RAW_* 31*7c9b2bf6SPaolo Bonzini * primitives. SET/RESET/WAIT have exactly the same semantics as 32*7c9b2bf6SPaolo Bonzini * RAW_SET/RAW_RESET/RAW_WAIT, but try to avoid invoking them. 33*7c9b2bf6SPaolo Bonzini */ 34*7c9b2bf6SPaolo Bonzini#define EV_SET 0 35*7c9b2bf6SPaolo Bonzini#define EV_FREE 1 36*7c9b2bf6SPaolo Bonzini#define EV_BUSY -1 37*7c9b2bf6SPaolo Bonzini 38*7c9b2bf6SPaolo Bonziniint state = EV_FREE; 39*7c9b2bf6SPaolo Bonzini 40*7c9b2bf6SPaolo Bonziniint xchg_result; 41*7c9b2bf6SPaolo Bonzini#define SET if :: state != EV_SET -> \ 42*7c9b2bf6SPaolo Bonzini atomic { /* xchg_result=xchg(state, EV_SET) */ \ 43*7c9b2bf6SPaolo Bonzini xchg_result = state; \ 44*7c9b2bf6SPaolo Bonzini state = EV_SET; \ 45*7c9b2bf6SPaolo Bonzini } \ 46*7c9b2bf6SPaolo Bonzini if :: xchg_result == EV_BUSY -> RAW_SET; \ 47*7c9b2bf6SPaolo Bonzini :: else -> skip; \ 48*7c9b2bf6SPaolo Bonzini fi; \ 49*7c9b2bf6SPaolo Bonzini :: else -> skip; \ 50*7c9b2bf6SPaolo Bonzini fi 51*7c9b2bf6SPaolo Bonzini 52*7c9b2bf6SPaolo Bonzini#define RESET if :: state == EV_SET -> atomic { state = state | EV_FREE; } \ 53*7c9b2bf6SPaolo Bonzini :: else -> skip; \ 54*7c9b2bf6SPaolo Bonzini fi 55*7c9b2bf6SPaolo Bonzini 56*7c9b2bf6SPaolo Bonziniint tmp1, tmp2; 57*7c9b2bf6SPaolo Bonzini#define WAIT tmp1 = state; \ 58*7c9b2bf6SPaolo Bonzini if :: tmp1 != EV_SET -> \ 59*7c9b2bf6SPaolo Bonzini if :: tmp1 == EV_FREE -> \ 60*7c9b2bf6SPaolo Bonzini RAW_RESET; \ 61*7c9b2bf6SPaolo Bonzini atomic { /* tmp2=cas(state, EV_FREE, EV_BUSY) */ \ 62*7c9b2bf6SPaolo Bonzini tmp2 = state; \ 63*7c9b2bf6SPaolo Bonzini if :: tmp2 == EV_FREE -> state = EV_BUSY; \ 64*7c9b2bf6SPaolo Bonzini :: else -> skip; \ 65*7c9b2bf6SPaolo Bonzini fi; \ 66*7c9b2bf6SPaolo Bonzini } \ 67*7c9b2bf6SPaolo Bonzini if :: tmp2 == EV_SET -> tmp1 = EV_SET; \ 68*7c9b2bf6SPaolo Bonzini :: else -> tmp1 = EV_BUSY; \ 69*7c9b2bf6SPaolo Bonzini fi; \ 70*7c9b2bf6SPaolo Bonzini :: else -> skip; \ 71*7c9b2bf6SPaolo Bonzini fi; \ 72*7c9b2bf6SPaolo Bonzini assert(tmp1 != EV_FREE); \ 73*7c9b2bf6SPaolo Bonzini if :: tmp1 == EV_BUSY -> RAW_WAIT; \ 74*7c9b2bf6SPaolo Bonzini :: else -> skip; \ 75*7c9b2bf6SPaolo Bonzini fi; \ 76*7c9b2bf6SPaolo Bonzini :: else -> skip; \ 77*7c9b2bf6SPaolo Bonzini fi 78*7c9b2bf6SPaolo Bonzini#endif 79*7c9b2bf6SPaolo Bonzini 80*7c9b2bf6SPaolo Bonziniactive proctype waiter() 81*7c9b2bf6SPaolo Bonzini{ 82*7c9b2bf6SPaolo Bonzini if 83*7c9b2bf6SPaolo Bonzini :: !value -> 84*7c9b2bf6SPaolo Bonzini RESET; 85*7c9b2bf6SPaolo Bonzini if 86*7c9b2bf6SPaolo Bonzini :: !value -> WAIT; 87*7c9b2bf6SPaolo Bonzini :: else -> skip; 88*7c9b2bf6SPaolo Bonzini fi; 89*7c9b2bf6SPaolo Bonzini :: else -> skip; 90*7c9b2bf6SPaolo Bonzini fi; 91*7c9b2bf6SPaolo Bonzini assert(value); 92*7c9b2bf6SPaolo Bonzini} 93*7c9b2bf6SPaolo Bonzini 94*7c9b2bf6SPaolo Bonziniactive proctype notifier() 95*7c9b2bf6SPaolo Bonzini{ 96*7c9b2bf6SPaolo Bonzini value = true; 97*7c9b2bf6SPaolo Bonzini SET; 98*7c9b2bf6SPaolo Bonzini} 99