blob: 1d20ece1d66071998bf7418b41003ec585042f47 [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 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);
}
}