141 lines
4.1 KiB
Promela
141 lines
4.1 KiB
Promela
|
/*
|
||
|
|
* 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
|