1*ac06724aSPaolo Bonzini/* 2*ac06724aSPaolo Bonzini * This model describes a bug in aio_notify. If ctx->notifier is 3*ac06724aSPaolo Bonzini * cleared too late, a wakeup could be lost. 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 the buggy version: 11*ac06724aSPaolo Bonzini * spin -a -DBUG docs/aio_notify_bug.promela 12*ac06724aSPaolo Bonzini * gcc -O2 pan.c 13*ac06724aSPaolo Bonzini * ./a.out -a -f 14*ac06724aSPaolo Bonzini * 15*ac06724aSPaolo Bonzini * To verify the fixed version: 16*ac06724aSPaolo Bonzini * spin -a docs/aio_notify_bug.promela 17*ac06724aSPaolo Bonzini * gcc -O2 pan.c 18*ac06724aSPaolo Bonzini * ./a.out -a -f 19*ac06724aSPaolo Bonzini * 20*ac06724aSPaolo Bonzini * Add -DCHECK_REQ to test an alternative invariant and the 21*ac06724aSPaolo Bonzini * "notify_me" optimization. 22*ac06724aSPaolo Bonzini */ 23*ac06724aSPaolo Bonzini 24*ac06724aSPaolo Bonziniint notify_me; 25*ac06724aSPaolo Bonzinibool event; 26*ac06724aSPaolo Bonzinibool req; 27*ac06724aSPaolo Bonzinibool notifier_done; 28*ac06724aSPaolo Bonzini 29*ac06724aSPaolo Bonzini#ifdef CHECK_REQ 30*ac06724aSPaolo Bonzini#define USE_NOTIFY_ME 1 31*ac06724aSPaolo Bonzini#else 32*ac06724aSPaolo Bonzini#define USE_NOTIFY_ME 0 33*ac06724aSPaolo Bonzini#endif 34*ac06724aSPaolo Bonzini 35*ac06724aSPaolo Bonziniactive proctype notifier() 36*ac06724aSPaolo Bonzini{ 37*ac06724aSPaolo Bonzini do 38*ac06724aSPaolo Bonzini :: true -> { 39*ac06724aSPaolo Bonzini req = 1; 40*ac06724aSPaolo Bonzini if 41*ac06724aSPaolo Bonzini :: !USE_NOTIFY_ME || notify_me -> event = 1; 42*ac06724aSPaolo Bonzini :: else -> skip; 43*ac06724aSPaolo Bonzini fi 44*ac06724aSPaolo Bonzini } 45*ac06724aSPaolo Bonzini :: true -> break; 46*ac06724aSPaolo Bonzini od; 47*ac06724aSPaolo Bonzini notifier_done = 1; 48*ac06724aSPaolo Bonzini} 49*ac06724aSPaolo Bonzini 50*ac06724aSPaolo Bonzini#ifdef BUG 51*ac06724aSPaolo Bonzini#define AIO_POLL \ 52*ac06724aSPaolo Bonzini notify_me++; \ 53*ac06724aSPaolo Bonzini if \ 54*ac06724aSPaolo Bonzini :: !req -> { \ 55*ac06724aSPaolo Bonzini if \ 56*ac06724aSPaolo Bonzini :: event -> skip; \ 57*ac06724aSPaolo Bonzini fi; \ 58*ac06724aSPaolo Bonzini } \ 59*ac06724aSPaolo Bonzini :: else -> skip; \ 60*ac06724aSPaolo Bonzini fi; \ 61*ac06724aSPaolo Bonzini notify_me--; \ 62*ac06724aSPaolo Bonzini \ 63*ac06724aSPaolo Bonzini req = 0; \ 64*ac06724aSPaolo Bonzini event = 0; 65*ac06724aSPaolo Bonzini#else 66*ac06724aSPaolo Bonzini#define AIO_POLL \ 67*ac06724aSPaolo Bonzini notify_me++; \ 68*ac06724aSPaolo Bonzini if \ 69*ac06724aSPaolo Bonzini :: !req -> { \ 70*ac06724aSPaolo Bonzini if \ 71*ac06724aSPaolo Bonzini :: event -> skip; \ 72*ac06724aSPaolo Bonzini fi; \ 73*ac06724aSPaolo Bonzini } \ 74*ac06724aSPaolo Bonzini :: else -> skip; \ 75*ac06724aSPaolo Bonzini fi; \ 76*ac06724aSPaolo Bonzini notify_me--; \ 77*ac06724aSPaolo Bonzini \ 78*ac06724aSPaolo Bonzini event = 0; \ 79*ac06724aSPaolo Bonzini req = 0; 80*ac06724aSPaolo Bonzini#endif 81*ac06724aSPaolo Bonzini 82*ac06724aSPaolo Bonziniactive proctype waiter() 83*ac06724aSPaolo Bonzini{ 84*ac06724aSPaolo Bonzini do 85*ac06724aSPaolo Bonzini :: true -> AIO_POLL; 86*ac06724aSPaolo Bonzini od; 87*ac06724aSPaolo Bonzini} 88*ac06724aSPaolo Bonzini 89*ac06724aSPaolo Bonzini/* Same as waiter(), but disappears after a while. */ 90*ac06724aSPaolo Bonziniactive proctype temporary_waiter() 91*ac06724aSPaolo Bonzini{ 92*ac06724aSPaolo Bonzini do 93*ac06724aSPaolo Bonzini :: true -> AIO_POLL; 94*ac06724aSPaolo Bonzini :: true -> break; 95*ac06724aSPaolo Bonzini od; 96*ac06724aSPaolo Bonzini} 97*ac06724aSPaolo Bonzini 98*ac06724aSPaolo Bonzini#ifdef CHECK_REQ 99*ac06724aSPaolo Bonzininever { 100*ac06724aSPaolo Bonzini do 101*ac06724aSPaolo Bonzini :: req -> goto accept_if_req_not_eventually_false; 102*ac06724aSPaolo Bonzini :: true -> skip; 103*ac06724aSPaolo Bonzini od; 104*ac06724aSPaolo Bonzini 105*ac06724aSPaolo Bonziniaccept_if_req_not_eventually_false: 106*ac06724aSPaolo Bonzini if 107*ac06724aSPaolo Bonzini :: req -> goto accept_if_req_not_eventually_false; 108*ac06724aSPaolo Bonzini fi; 109*ac06724aSPaolo Bonzini assert(0); 110*ac06724aSPaolo Bonzini} 111*ac06724aSPaolo Bonzini 112*ac06724aSPaolo Bonzini#else 113*ac06724aSPaolo Bonzini/* There must be infinitely many transitions of event as long 114*ac06724aSPaolo Bonzini * as the notifier does not exit. 115*ac06724aSPaolo Bonzini * 116*ac06724aSPaolo Bonzini * If event stayed always true, the waiters would be busy looping. 117*ac06724aSPaolo Bonzini * If event stayed always false, the waiters would be sleeping 118*ac06724aSPaolo Bonzini * forever. 119*ac06724aSPaolo Bonzini */ 120*ac06724aSPaolo Bonzininever { 121*ac06724aSPaolo Bonzini do 122*ac06724aSPaolo Bonzini :: !event -> goto accept_if_event_not_eventually_true; 123*ac06724aSPaolo Bonzini :: event -> goto accept_if_event_not_eventually_false; 124*ac06724aSPaolo Bonzini :: true -> skip; 125*ac06724aSPaolo Bonzini od; 126*ac06724aSPaolo Bonzini 127*ac06724aSPaolo Bonziniaccept_if_event_not_eventually_true: 128*ac06724aSPaolo Bonzini if 129*ac06724aSPaolo Bonzini :: !event && notifier_done -> do :: true -> skip; od; 130*ac06724aSPaolo Bonzini :: !event && !notifier_done -> goto accept_if_event_not_eventually_true; 131*ac06724aSPaolo Bonzini fi; 132*ac06724aSPaolo Bonzini assert(0); 133*ac06724aSPaolo Bonzini 134*ac06724aSPaolo Bonziniaccept_if_event_not_eventually_false: 135*ac06724aSPaolo Bonzini if 136*ac06724aSPaolo Bonzini :: event -> goto accept_if_event_not_eventually_false; 137*ac06724aSPaolo Bonzini fi; 138*ac06724aSPaolo Bonzini assert(0); 139*ac06724aSPaolo Bonzini} 140*ac06724aSPaolo Bonzini#endif 141