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