libsel4sync/spin/binary-sem/binary-sem.pml

/*
 * Copyright 2017, Data61
 * Commonwealth Scientific and Industrial Research Organisation (CSIRO)
 * ABN 41 687 119 230.
 *
 * This software may be distributed and modified according to the terms of
 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
 * See "LICENSE_BSD2.txt" for details.
 *
 * @TAG(DATA61_BSD)
 */

#define send_enabled 1

/* An async endpoint is implemented by a channel of length 1 that
 * drops messages when full. Dropping of messages is done by passing
 * the -m switch to spin */
chan endpoint = [1] of {bit};

/* binary semaphore starts with value of 1 */
int sem_value = 1;

inline bin_sem_wait() {
    int oldval;

    /* Atomic decrement */
    atomic {
        oldval = sem_value;
        sem_value--;
    }

    /* Conditional wait */
    if
    :: (oldval <= 0) -> endpoint ? 1;
    :: (oldval > 0) -> skip
    fi
}

inline bin_sem_signal()
{
    int new_val;

    /* Atomic increment. */
    atomic {
        sem_value++;
        new_val = sem_value;
    }

    /* Conditional wake. */
    if
    :: (new_val <= 0) ->
        send: endpoint ! 1;
    :: (new_val > 0) ->
        skip;
    fi
}

active [4] proctype wait_thread() {
    do
    :: true ->
        /* lock */
        bin_sem_wait();

        /* critical section */
        crit:;

        /* unlock */
        bin_sem_signal();
    od
}

/* Verify that the -m option was used. If it wasn't we might
 * block on a send, this will make blocking a failure case */
ltl cansend { []((wait_thread[0]@crit)->enabled(0)) }

/* Verify mutual exclusion */
ltl mutex { []( (wait_thread[0]@crit) -> !(wait_thread[1]@crit) ) }

/* Formulate liveness as a safety property by stating we will
 * always be able to get the critical section again */
ltl liveness { []<>(wait_thread[0]@crit || wait_thread[1]@crit || wait_thread[2]@crit || wait_thread[3]@crit) }