summaryrefslogtreecommitdiff
path: root/docs
diff options
context:
space:
mode:
authorPaolo Bonzini <pbonzini@redhat.com>2014-07-07 15:18:04 +0200
committerKevin Wolf <kwolf@redhat.com>2014-07-09 15:50:11 +0200
commit0ceb849bd336a5f9b6e1ed56d45cf5773d251ad8 (patch)
tree970ee4f04a48eba0894602d28d2f70d23aeb532a /docs
parentef508f427b348c7f0ef2bfe7c080fe5fcaee9f6b (diff)
downloadqemu-0ceb849bd336a5f9b6e1ed56d45cf5773d251ad8.tar.gz
AioContext: speed up aio_notify
In many cases, the call to event_notifier_set in aio_notify is unnecessary. In particular, if we are executing aio_dispatch, or if aio_poll is not blocking, we know that we will soon get to the next loop iteration (if necessary); the thread that hosts the AioContext's event loop does not need any nudging. The patch includes a Promela formal model that shows that this really works and does not need any further complication such as generation counts. It needs a memory barrier though. The generation counts are not needed because any change to ctx->dispatching after the memory barrier is okay for aio_notify. If it changes from zero to one, it is the right thing to skip event_notifier_set. If it changes from one to zero, the event_notifier_set is unnecessary but harmless. Signed-off-by: Paolo Bonzini <pbonzini@redhat.com> Signed-off-by: Kevin Wolf <kwolf@redhat.com>
Diffstat (limited to 'docs')
-rw-r--r--docs/aio_notify.promela104
1 files changed, 104 insertions, 0 deletions
diff --git a/docs/aio_notify.promela b/docs/aio_notify.promela
new file mode 100644
index 0000000000..ad3f6f08b0
--- /dev/null
+++ b/docs/aio_notify.promela
@@ -0,0 +1,104 @@
+/*
+ * This model describes the interaction between aio_set_dispatching()
+ * and aio_notify().
+ *
+ * Author: Paolo Bonzini <pbonzini@redhat.com>
+ *
+ * This file is in the public domain. If you really want a license,
+ * the WTFPL will do.
+ *
+ * To simulate it:
+ * spin -p docs/aio_notify.promela
+ *
+ * To verify it:
+ * spin -a docs/aio_notify.promela
+ * gcc -O2 pan.c
+ * ./a.out -a
+ */
+
+#define MAX 4
+#define LAST (1 << (MAX - 1))
+#define FINAL ((LAST << 1) - 1)
+
+bool dispatching;
+bool event;
+
+int req, done;
+
+active proctype waiter()
+{
+ int fetch, blocking;
+
+ do
+ :: done != FINAL -> {
+ // Computing "blocking" is separate from execution of the
+ // "bottom half"
+ blocking = (req == 0);
+
+ // This is our "bottom half"
+ atomic { fetch = req; req = 0; }
+ done = done | fetch;
+
+ // Wait for a nudge from the other side
+ do
+ :: event == 1 -> { event = 0; break; }
+ :: !blocking -> break;
+ od;
+
+ dispatching = 1;
+
+ // If you are simulating this model, you may want to add
+ // something like this here:
+ //
+ // int foo; foo++; foo++; foo++;
+ //
+ // This only wastes some time and makes it more likely
+ // that the notifier process hits the "fast path".
+
+ dispatching = 0;
+ }
+ :: else -> break;
+ od
+}
+
+active proctype notifier()
+{
+ int next = 1;
+ int sets = 0;
+
+ do
+ :: next <= LAST -> {
+ // generate a request
+ req = req | next;
+ next = next << 1;
+
+ // aio_notify
+ if
+ :: dispatching == 0 -> sets++; event = 1;
+ :: else -> skip;
+ fi;
+
+ // Test both synchronous and asynchronous delivery
+ if
+ :: 1 -> do
+ :: req == 0 -> break;
+ od;
+ :: 1 -> skip;
+ fi;
+ }
+ :: else -> break;
+ od;
+ printf("Skipped %d event_notifier_set\n", MAX - sets);
+}
+
+#define p (done == FINAL)
+
+never {
+ do
+ :: 1 // after an arbitrarily long prefix
+ :: p -> break // p becomes true
+ od;
+ do
+ :: !p -> accept: break // it then must remains true forever after
+ od
+}