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