libsel4sync/spin/sem/sem.promela

/*
 * 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 MAX_SEM_VAL 1

/* Semaphore value. */
int sem_value = MAX_SEM_VAL;

/* Endpoint. */
chan endpoint = [0] of {bit};

/* Users in critical section. */
byte users = 0;

inline do_wait(procnum)
{
    int oldval;

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

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

inline do_try_wait(procnum)
{
    int observed_val;

    do
    :: true;
       observed_val = sem_value;
       if
       :: (observed_val <= 0) ->
           return 0;
           break;
       :: (observed_val > 0) ->
               /* Atomic compare and set: compare observed value, set
                * (observed_value - 1). */
               atomic {
                  if
                  :: (sem_value == observed_val) ->
                         sem_value = observed_val - 1;
                         return 1;
                         break;
                  :: (sem_value != observed_val) -> skip;
                  fi;
               };
       fi
    od
}

inline do_signal(procnum)
{
    int new_val;

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

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

proctype wait_cpu(byte procnum)
{
    do
    :: true;
progress_wait:;
        /* Lock. */
        printf("%d getting the lock.\n", procnum);
        do_wait(procnum);
        printf("%d got the lock.\n", procnum);

        /* Use a common resource. */
        users++;
        assert(users <= MAX_SEM_VAL);
        users--;

        /* Release. */
        printf("%d releasing the lock\n", procnum);
        do_signal(procnum);
        printf("%d released the lock.\n", procnum);
    od
}

proctype trywait_cpu(byte procnum)
{
    byte x;
    do
    :: true;
progress_trywait:;
        /* Lock. */
        printf("%d trying to get the lock.\n", procnum);
        x = do_try_wait(procnum);
        if
        :: (x == 0) ->
            printf("%d failed to get the lock.\n", procnum);
        :: (x == 1) ->
            printf("%d got the lock.\n", procnum);

            /* Use a common resource. */
            users++;
            assert(users <= MAX_SEM_VAL);
            users--;

            /* Release. */
            printf("%d releasing the lock\n", procnum);
            do_signal(procnum);
            printf("%d released the lock.\n", procnum);
        fi
    od
}

init {
    atomic {
        run wait_cpu(1);
        run trywait_cpu(2);
        run trywait_cpu(3);
        run wait_cpu(4);
    }
}