summaryrefslogtreecommitdiffstats
path: root/qemu/docs/aio_notify_bug.promela
diff options
context:
space:
mode:
authorRajithaY <rajithax.yerrumsetty@intel.com>2017-04-25 03:31:15 -0700
committerRajitha Yerrumchetty <rajithax.yerrumsetty@intel.com>2017-05-22 06:48:08 +0000
commitbb756eebdac6fd24e8919e2c43f7d2c8c4091f59 (patch)
treeca11e03542edf2d8f631efeca5e1626d211107e3 /qemu/docs/aio_notify_bug.promela
parenta14b48d18a9ed03ec191cf16b162206998a895ce (diff)
Adding qemu as a submodule of KVMFORNFV
This Patch includes the changes to add qemu as a submodule to kvmfornfv repo and make use of the updated latest qemu for the execution of all testcase Change-Id: I1280af507a857675c7f81d30c95255635667bdd7 Signed-off-by:RajithaY<rajithax.yerrumsetty@intel.com>
Diffstat (limited to 'qemu/docs/aio_notify_bug.promela')
-rw-r--r--qemu/docs/aio_notify_bug.promela140
1 files changed, 0 insertions, 140 deletions
diff --git a/qemu/docs/aio_notify_bug.promela b/qemu/docs/aio_notify_bug.promela
deleted file mode 100644
index b3bfca1ca..000000000
--- a/qemu/docs/aio_notify_bug.promela
+++ /dev/null
@@ -1,140 +0,0 @@
-/*
- * 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