[Qemu-devel] [PATCH 0/2] AioContext: fix missing wakeups due to event_notifier_test_and_clear

[Paolo Bonzini <pbonzini@redhat.com>]

This series fixes the remaining case where aio_poll() could hang
I/O on the main thread due to a missing wakeup.  It consists of
a bugfix and an optimization, both of which have survived hundreds
of tests on aarch64.

Both the bugfix and the optimization come with a formal model of the
interactions between the main thread, the VCPU thread doing aio_poll,
and the worker thread doing qemu_bh_schedule.  The models can test
the code both with and without ctx->notify_me, showing that this
bug is independent from the other.

The patches apply on top of the ctx->notify_me v3.  The code changes
are really pretty small; the second patch has a good deal of comments too.

Paolo

Paolo Bonzini (2):
  AioContext: fix broken placement of event_notifier_test_and_clear
  AioContext: optimize clearing the EventNotifier

 aio-posix.c                    |   2 +
 aio-win32.c                    |   2 +
 async.c                        |  16 ++++-
 docs/aio_notify_accept.promela | 152 +++++++++++++++++++++++++++++++++++++++++
 docs/aio_notify_bug.promela    | 140 +++++++++++++++++++++++++++++++++++++
 include/block/aio.h            |  32 ++++++++-
 6 files changed, 342 insertions(+), 2 deletions(-)
 create mode 100644 docs/aio_notify_accept.promela
 create mode 100644 docs/aio_notify_bug.promela

-- 
2.4.3