motorhead/qemu
1
0
Fork 0
mirror of https://github.com/Motorhead1991/qemu.git synced 2025-08-04 08:13:54 -06:00
Code Issues Projects Releases Packages Wiki Activity Actions

AioContext: optimize clearing the EventNotifier

Browse source 
It is pretty rare for aio_notify to actually set the EventNotifier.  It
can happen with worker threads such as thread-pool.c's, but otherwise it
should never be set thanks to the ctx->notify_me optimization.  The
previous patch, unfortunately, added an unconditional call to
event_notifier_test_and_clear; now add a userspace fast path that
avoids the call.

Note that it is not possible to do the same with event_notifier_set;
it would break, as proved (again) by the included formal model.

This patch survived over 3000 reboots on aarch64 KVM.

Signed-off-by: Paolo Bonzini <pbonzini@redhat.com>
Reviewed-by: Fam Zheng <famz@redhat.com>
Tested-by: Richard W.M. Jones <rjones@redhat.com>
Message-id: 1437487673-23740-7-git-send-email-pbonzini@redhat.com
Signed-off-by: Stefan Hajnoczi <stefanha@redhat.com>
This commit is contained in:
Paolo Bonzini 2015-07-21 16:07:53 +02:00 • committed by Stefan Hajnoczi
parent 21a03d17f2
commit 05e514b1d4
5 changed files with 194 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

152
docs/aio_notify_accept.promela Normal file
View file

@ -0,0 +1,152 @@
/*
* This model describes the interaction between ctx->notified
* and ctx->notifier.
*
* 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 -DBUG1 docs/aio_notify_bug.promela
* gcc -O2 pan.c
* ./a.out -a -f
* (or -DBUG2)
*
* 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 notified;
bool event;
bool req;
bool notifier_done;
#ifdef CHECK_REQ
#define USE_NOTIFY_ME 1
#else
#define USE_NOTIFY_ME 0
#endif
#ifdef BUG
#error Please define BUG1 or BUG2 instead.
#endif
active proctype notifier()
{
do
:: true -> {
req = 1;
if
:: !USE_NOTIFY_ME || notify_me ->
#if defined BUG1
/* CHECK_REQ does not detect this bug! */
notified = 1;
event = 1;
#elif defined BUG2
if
:: !notified -> event = 1;
:: else -> skip;
fi;
notified = 1;
#else
event = 1;
notified = 1;
#endif
:: else -> skip;
fi
}
:: true -> break;
od;
notifier_done = 1;
}
#define AIO_POLL \
notify_me++; \
if \
:: !req -> { \
if \
:: event -> skip; \
fi; \
} \
:: else -> skip; \
fi; \
notify_me--; \
\
atomic { old = notified; notified = 0; } \
if \
:: old -> event = 0; \
:: else -> skip; \
fi; \
\
req = 0;
active proctype waiter()
{
bool old;
do
:: true -> AIO_POLL;
od;
}
/* Same as waiter(), but disappears after a while. */
active proctype temporary_waiter()
{
bool old;
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