blob: 7cede0ff6e730181c3e370b0b0bcc18299209642 [file] [log] [blame]
/*
* 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) }