This should be quite straightforward:
active proctype P() {
bit sema = 0;
do
:: atomic {
sema == 0 -> sema = 1
}
// critical section
sema = 0
od
}
Possibly you do not need the do
loop, if in your code you only needed it for some active waiting. The atomic block is only executable if sema
is set to 0, and then it executes at once. Spin has a built-in passive waiting semantics.