/* * This model describes a bug in aio_notify. If ctx->notifier is * cleared too late, a wakeup could be lost. * * 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 the buggy version: * spin -a -DBUG docs/aio_notify_bug.promela * gcc -O2 pan.c * ./a.out -a -f * * To verify the fixed version: * spin -a docs/aio_notify_bug.promela * gcc -O2 pan.c * ./a.out -a -f * * Add -DCHECK_REQ to test an alternative invariant and the * "notify_me" optimization. */ int notify_me; bool event; bool req; bool notifier_done; #ifdef CHECK_REQ #define USE_NOTIFY_ME 1 #else #define USE_NOTIFY_ME 0 #endif active proctype notifier() { do :: true -> { req = 1; if :: !USE_NOTIFY_ME || notify_me -> event = 1; :: else -> skip; fi } :: true -> break; od; notifier_done = 1; } #ifdef BUG #define AIO_POLL \ notify_me++; \ if \ :: !req -> { \ if \ :: event -> skip; \ fi; \ } \ :: else -> skip; \ fi; \ notify_me--; \ \ req = 0; \ event = 0; #else #define AIO_POLL \ notify_me++; \ if \ :: !req -> { \ if \ :: event -> skip; \ fi; \ } \ :: else -> skip; \ fi; \ notify_me--; \ \ event = 0; \ req = 0; #endif active proctype waiter() { do :: true -> AIO_POLL; od; } /* Same as waiter(), but disappears after a while. */ active proctype temporary_waiter() { do :: true -> AIO_POLL; :: true -> break; od; } #ifdef CHECK_REQ never { do :: req -> goto accept_if_req_not_eventually_false; :: true -> skip; od; accept_if_req_not_eventually_false: if :: req -> goto accept_if_req_not_eventually_false; fi; assert(0); } #else /* There must be infinitely many transitions of event as long * as the notifier does not exit. * * If event stayed always true, the waiters would be busy looping. * If event stayed always false, the waiters would be sleeping * forever. */ never { do :: !event -> goto accept_if_event_not_eventually_true; :: event -> goto accept_if_event_not_eventually_false; :: true -> skip; od; accept_if_event_not_eventually_true: if :: !event && notifier_done -> do :: true -> skip; od; :: !event && !notifier_done -> goto accept_if_event_not_eventually_true; fi; assert(0); accept_if_event_not_eventually_false: if :: event -> goto accept_if_event_not_eventually_false; fi; assert(0); } #endif