aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--aio-posix.c2
-rw-r--r--aio-win32.c2
-rw-r--r--async.c10
-rw-r--r--docs/aio_notify_accept.promela152
-rw-r--r--include/block/aio.h32
5 files changed, 194 insertions, 4 deletions
diff --git a/aio-posix.c b/aio-posix.c
index 5c8b266c72..d4770336c5 100644
--- a/aio-posix.c
+++ b/aio-posix.c
@@ -276,7 +276,7 @@ bool aio_poll(AioContext *ctx, bool blocking)
aio_context_acquire(ctx);
}
- event_notifier_test_and_clear(&ctx->notifier);
+ aio_notify_accept(ctx);
/* if we have any readable fds, dispatch event */
if (ret > 0) {
diff --git a/aio-win32.c b/aio-win32.c
index 7afc9992d6..50a6867458 100644
--- a/aio-win32.c
+++ b/aio-win32.c
@@ -338,7 +338,7 @@ bool aio_poll(AioContext *ctx, bool blocking)
}
if (first) {
- event_notifier_test_and_clear(&ctx->notifier);
+ aio_notify_accept(ctx);
progress |= aio_bh_poll(ctx);
first = false;
}
diff --git a/async.c b/async.c
index d625e8a803..9a98a74acb 100644
--- a/async.c
+++ b/async.c
@@ -203,7 +203,7 @@ aio_ctx_check(GSource *source)
QEMUBH *bh;
atomic_and(&ctx->notify_me, ~1);
- event_notifier_test_and_clear(&ctx->notifier);
+ aio_notify_accept(ctx);
for (bh = ctx->first_bh; bh; bh = bh->next) {
if (!bh->deleted && bh->scheduled) {
@@ -267,6 +267,14 @@ void aio_notify(AioContext *ctx)
smp_mb();
if (ctx->notify_me) {
event_notifier_set(&ctx->notifier);
+ atomic_mb_set(&ctx->notified, true);
+ }
+}
+
+void aio_notify_accept(AioContext *ctx)
+{
+ if (atomic_xchg(&ctx->notified, false)) {
+ event_notifier_test_and_clear(&ctx->notifier);
}
}
diff --git a/docs/aio_notify_accept.promela b/docs/aio_notify_accept.promela
new file mode 100644
index 0000000000..9cef2c955d
--- /dev/null
+++ b/docs/aio_notify_accept.promela
@@ -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
diff --git a/include/block/aio.h b/include/block/aio.h
index be91e3f701..9dd32e0f13 100644
--- a/include/block/aio.h
+++ b/include/block/aio.h
@@ -99,7 +99,19 @@ struct AioContext {
*/
int walking_bh;
- /* Used for aio_notify. */
+ /* Used by aio_notify.
+ *
+ * "notified" is used to avoid expensive event_notifier_test_and_clear
+ * calls. When it is clear, the EventNotifier is clear, or one thread
+ * is going to clear "notified" before processing more events. False
+ * positives are possible, i.e. "notified" could be set even though the
+ * EventNotifier is clear.
+ *
+ * Note that event_notifier_set *cannot* be optimized the same way. For
+ * more information on the problem that would result, see "#ifdef BUG2"
+ * in the docs/aio_notify_accept.promela formal model.
+ */
+ bool notified;
EventNotifier notifier;
/* Thread pool for performing work and receiving completion callbacks */
@@ -174,6 +186,24 @@ QEMUBH *aio_bh_new(AioContext *ctx, QEMUBHFunc *cb, void *opaque);
void aio_notify(AioContext *ctx);
/**
+ * aio_notify_accept: Acknowledge receiving an aio_notify.
+ *
+ * aio_notify() uses an EventNotifier in order to wake up a sleeping
+ * aio_poll() or g_main_context_iteration(). Calls to aio_notify() are
+ * usually rare, but the AioContext has to clear the EventNotifier on
+ * every aio_poll() or g_main_context_iteration() in order to avoid
+ * busy waiting. This event_notifier_test_and_clear() cannot be done
+ * using the usual aio_context_set_event_notifier(), because it must
+ * be done before processing all events (file descriptors, bottom halves,
+ * timers).
+ *
+ * aio_notify_accept() is an optimized event_notifier_test_and_clear()
+ * that is specific to an AioContext's notifier; it is used internally
+ * to clear the EventNotifier only if aio_notify() had been called.
+ */
+void aio_notify_accept(AioContext *ctx);
+
+/**
* aio_bh_poll: Poll bottom halves for an AioContext.
*
* These are internal functions used by the QEMU main loop.