diff options
author | fishsoupisgood <github@madingley.org> | 2019-04-29 01:17:54 +0100 |
---|---|---|
committer | fishsoupisgood <github@madingley.org> | 2019-05-27 03:43:43 +0100 |
commit | 3f2546b2ef55b661fd8dd69682b38992225e86f6 (patch) | |
tree | 65ca85f13617aee1dce474596800950f266a456c /docs/aio_notify.promela | |
download | qemu-master.tar.gz qemu-master.tar.bz2 qemu-master.zip |
Diffstat (limited to 'docs/aio_notify.promela')
-rw-r--r-- | docs/aio_notify.promela | 93 |
1 files changed, 93 insertions, 0 deletions
diff --git a/docs/aio_notify.promela b/docs/aio_notify.promela new file mode 100644 index 00000000..fccc7ee1 --- /dev/null +++ b/docs/aio_notify.promela @@ -0,0 +1,93 @@ +/* + * 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; +} |