[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

# Bikeshedding fun with problem 7.7

I had a lot of fun with Problem 7.7 and bikeshedded a bit on the style. I submit the following for your critique. This passes checks with ISpec as temporal invariant and A!ISpec as a property, where A is "OneBitProtocol."

------------------------- MODULE OneBitTwoProcesses -------------------------
EXTENDS Integers

(******************************************************************
--algorithm OneBit
{ variable x = [i \in {0,1} |-> FALSE] ;
fair process (Proc \in {0,1})
{ ncs: while (TRUE)
\* This is the model for my non-critical processing.
{     skip ;
\* Ok, I'm done with that and I want in to the
\* critical section!
e1: x[self] := TRUE ;
e2: if (~x[1-self])
\* If the other guy isn't in, I'm in!
{ cs: skip (* Model for my critical code! *) }
else
\* Oops, the other guy is in. What do I do?
{ if (self = 0)
\* If I'm process 0, I'll keep trying.
{ goto e2 }
\* But, if I'm process 1, I'll be the nice guy;
\* I'll stop trying and spin while process 0 is in.
else
{ e3: x := FALSE ;
e4: while ( x )
{ skip (* spin *) } ;
goto e1
} } ;
\* Ok, I'm done. I don't need the critical section now.
f:  x[self] := FALSE
}  }     }
******************************************************************)
\* BEGIN TRANSLATION
\* END TRANSLATION

PC0Labels   == {"ncs", "f", "e1", "e2", "cs"}
ExtraLabels == {"e3", "e4"}
PC1Labels   == PC0Labels \cup ExtraLabels

TypeOK == /\ pc \in [{0} -> PC0Labels] \cup [{1} -> PC1Labels]
/\ x  \in [{0, 1} -> BOOLEAN]

InCS(i) == pc[i] = "cs"

MutualExclusion == ~(InCS(0) /\ InCS(1))
Fairness        == \A i \in {0,1} : WF_vars(Proc(i))
Coordination    == \A i \in {0,1} : InCS(i) \/ (pc[i] = "e2") => x[i]

Trying(i)       == pc[i] \in {"e1", "e2"}
DeadlockFreedom == (Trying(0) \/ Trying(1)) ~> (InCS(0) \/ InCS(1))

Inv == /\ Init
/\ TypeOK
/\ MutualExclusion
/\ Fairness
/\ Coordination
/\ DeadlockFreedom

ISpec == Inv /\ [][Next]_<<x, pc>>

(* This algorithm implements the OneBitProtocol under the following
refinement mapping; check "ISpec" in module "OneBitProtocol." *)

A == INSTANCE OneBitProtocol
WITH pc <- [i \in {0, 1} |->
IF pc[i] \in {"ncs", "f", "e3", "e4"} THEN "r" ELSE pc[i]]