diff options
author | RajithaY <rajithax.yerrumsetty@intel.com> | 2017-04-25 03:31:15 -0700 |
---|---|---|
committer | Rajitha Yerrumchetty <rajithax.yerrumsetty@intel.com> | 2017-05-22 06:48:08 +0000 |
commit | bb756eebdac6fd24e8919e2c43f7d2c8c4091f59 (patch) | |
tree | ca11e03542edf2d8f631efeca5e1626d211107e3 /qemu/docs/aio_notify_bug.promela | |
parent | a14b48d18a9ed03ec191cf16b162206998a895ce (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.promela | 140 |
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 |