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.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.promela')
-rw-r--r-- | qemu/docs/aio_notify.promela | 93 |
1 files changed, 0 insertions, 93 deletions
diff --git a/qemu/docs/aio_notify.promela b/qemu/docs/aio_notify.promela deleted file mode 100644 index fccc7ee1c..000000000 --- a/qemu/docs/aio_notify.promela +++ /dev/null @@ -1,93 +0,0 @@ -/* - * This model describes the interaction between ctx->notify_me - * 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 - * - * To verify it (with a bug planted in the model): - * spin -a -DBUG 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 notify_me; -bool event; - -int req; -int done; - -active proctype waiter() -{ - int fetch; - - do - :: true -> { - notify_me++; - - if -#ifndef BUG - :: (req > 0) -> skip; -#endif - :: else -> - // Wait for a nudge from the other side - do - :: event == 1 -> { event = 0; break; } - od; - fi; - - notify_me--; - - atomic { fetch = req; req = 0; } - done = done | fetch; - } - od -} - -active proctype notifier() -{ - int next = 1; - - do - :: next <= LAST -> { - // generate a request - req = req | next; - next = next << 1; - - // aio_notify - if - :: notify_me == 1 -> event = 1; - :: else -> printf("Skipped event_notifier_set\n"); skip; - fi; - - // Test both synchronous and asynchronous delivery - if - :: 1 -> do - :: req == 0 -> break; - od; - :: 1 -> skip; - fi; - } - od; -} - -never { /* [] done < FINAL */ -accept_init: - do - :: done < FINAL -> skip; - od; -} |