[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[1] := FALSE ;
                     e4: while ( x[0] ) 
                         { 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]]