| * This model describes the interaction between ctx->notify_me |
| * Author: Paolo Bonzini <pbonzini@redhat.com> |
| * This file is in the public domain. If you really want a license, |
| * spin -p docs/aio_notify.promela |
| * spin -a docs/aio_notify.promela |
| * To verify it (with a bug planted in the model): |
| * spin -a -DBUG docs/aio_notify.promela |
| #define LAST (1 << (MAX - 1)) |
| #define FINAL ((LAST << 1) - 1) |
| // Wait for a nudge from the other side |
| :: event == 1 -> { event = 0; break; } |
| atomic { fetch = req; req = 0; } |
| active proctype notifier() |
| :: notify_me == 1 -> event = 1; |
| :: else -> printf("Skipped event_notifier_set\n"); skip; |
| // Test both synchronous and asynchronous delivery |
| never { /* [] done < FINAL */ |