/*
 * This model describes the interaction between aio_set_dispatching()
 * 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
 */

#define MAX   4
#define LAST  (1 << (MAX - 1))
#define FINAL ((LAST << 1) - 1)

bool dispatching;
bool event;

int req, done;

active proctype waiter()
{
     int fetch, blocking;

     do
        :: done != FINAL -> {
            // Computing "blocking" is separate from execution of the
            // "bottom half"
            blocking = (req == 0);

            // This is our "bottom half"
            atomic { fetch = req; req = 0; }
            done = done | fetch;

            // Wait for a nudge from the other side
            do
                :: event == 1 -> { event = 0; break; }
                :: !blocking  -> break;
            od;

            dispatching = 1;

            // If you are simulating this model, you may want to add
            // something like this here:
            //
            //      int foo; foo++; foo++; foo++;
            //
            // This only wastes some time and makes it more likely
            // that the notifier process hits the "fast path".

            dispatching = 0;
        }
        :: else -> break;
    od
}

active proctype notifier()
{
    int next = 1;
    int sets = 0;

    do
        :: next <= LAST -> {
            // generate a request
            req = req | next;
            next = next << 1;

            // aio_notify
            if
                :: dispatching == 0 -> sets++; event = 1;
                :: else             -> skip;
            fi;

            // Test both synchronous and asynchronous delivery
            if
                :: 1 -> do
                            :: req == 0 -> break;
                        od;
                :: 1 -> skip;
            fi;
        }
        :: else -> break;
    od;
    printf("Skipped %d event_notifier_set\n", MAX - sets);
}

#define p (done == FINAL)

never  {
    do
        :: 1                      // after an arbitrarily long prefix
        :: p -> break             // p becomes true
    od;
    do
        :: !p -> accept: break    // it then must remains true forever after
    od
}