------------------------------- MODULE DCAS --------------------------------- EXTENDS Naturals, Sequences, TLC, FiniteSets (***************************************************************************) (* Last and Front are like Head and Tail, except for the back (right-hand *) (* end) rather than the front (left-hand) end of the sequence/list/queue. *) (***************************************************************************) Last(q) == q[Len(q)] Front(q) == [i \in 1..(Len(q)-1) |-> q[i]] (***************************************************************************) (* Here are the constant parameters of the algorithm. *) (***************************************************************************) CONSTANTS Val, \* The set of all values that can be enqueued Address, \* The set of heap addresses Dummy, \* The address of the dummy node Procs \* The set of all processes (threads) ASSUME Dummy \in Address null == CHOOSE n: n \notin Address (*************************************************************************) (* Defines null to be an arbitrary value that is not a heap address. *) (*************************************************************************) Node == [R : Address \cup {null}, L : Address \cup {null}, V : Val] (*************************************************************************) (* This defines the set of all nodes (the Node type). It asserts that *) (* an element of Node is a record with R and L fields that are either *) (* addresses or null, and a V field that is a Val or null. *) (* *) (* This definition would be used in a type-correctness invariant, which *) (* I didn't bother to write and check. (The model checker should find *) (* any type errors during execution when it tries to evaluate a function *) (* on an element not in its domain--for example, evaluating an *) (* expression exp.c when exp is not a record with a c field.) *) (*************************************************************************) DummyNode == [R |-> Dummy, L |-> Dummy, V |-> null] (*************************************************************************) (* The dummy node (whose address is Dummy). *) (*************************************************************************) InitNode == [R |-> null, L |-> null, V |-> null] (* --algorithm Snark { (***************************************************************************) (* The global variables, and their initial values. *) (***************************************************************************) variables LeftHat = Dummy, RightHat = Dummy, (***********************************************************************) (* LeftHat and RightHat are from the original algorithm. *) (***********************************************************************) Heap = [a \in Address |-> IF a = Dummy THEN DummyNode ELSE InitNode], (***********************************************************************) (* The heap, which is an array indexed by addresses. Initially *) (* Heap[Dummy] = DummyNode and Heap[i] = InitNode for all addresses *) (* i other than Dummy. *) (***********************************************************************) freeList = Address \ {Dummy}, (***********************************************************************) (* The set of addresses of free heap elements. *) (***********************************************************************) rVal = [p \in Procs |-> "okay"], (***********************************************************************) (* rVal[p] is the last value returned by a procedure call n process *) (* p. The initial value doesn't matter, but it needs to be an array *) (* (function) indexed by (with domain) Procs. *) (***********************************************************************) queue = << >> , sVal = [p \in Procs |-> TRUE] ; (***********************************************************************) (* These are the dummy variables introduced to check the algorithm. *) (***********************************************************************) macro New(result) { (*************************************************************************) (* A macro that represents the C code "result = new Node()". I *) (* originally intended to have a garbage-collection process, but I *) (* decided it wasn't likely to help detect errors. So, I just let the *) (* system just run out of heap. *) (*************************************************************************) if (freeList # {}) { result := CHOOSE a \in freeList : TRUE ; freeList := freeList \ {result} ; } else result := null } macro DCAS(result, addr1, addr2, old1, old2, new1, new2) { if ( (addr1 = old1) /\ (addr2 = old2)) { addr1 := new1 || addr2 := new2 ; result := TRUE; } else result := FALSE; } procedure pushRight(v) variables nd, rh, rhR, lh, temp; { L2: New(nd) ; if (nd = null) { rVal[self] := "full"; L3: return } ; L4: Heap[nd].R := Dummy || Heap[nd].V := v ; L6: while (TRUE) { rh := RightHat; L8: rhR := Heap[rh].R; L9: if (rhR = rh) { Heap[nd].L := Dummy; lh := LeftHat; \* this statement should have been labeled L12: DCAS(temp, RightHat, LeftHat, rh, lh, nd, nd) ; if (temp) { queue := queue \o <> ; rVal[self] := "okay"; L13: return} } else { L15: Heap[nd].L := rh; L16: DCAS(temp, RightHat, Heap[rh].R, rh, rhR, nd, nd) ; if (temp) { queue := queue \o <> ; rVal[self] := "okay"; L17: return } } } } procedure popRight() variables rh, lh, rhL, temp, result; { M2: while (TRUE) { rh := RightHat; sVal[self] := (queue = << >>) ; M4: lh := LeftHat; M5: if (Heap[rh].R = rh) { assert sVal[self] \/ (queue = << >>) ; rVal[self] := "empty"; return ;} ; M6: if (rh = lh) { DCAS(temp, RightHat, LeftHat, rh, lh, Dummy, Dummy) ; if (temp) { sVal[self] := Last(queue) ; queue := Front(queue) ; M8: rVal[self] := Heap[rh].V ; assert rVal[self] = sVal[self]; return;} } else { M10: rhL := Heap[rh].L ; M11: DCAS(temp, RightHat, Heap[rh].L, rh, rhL, rhL, rh) ; if (temp) { sVal[self] := Last(queue) ; queue := Front(queue) ; M12: result := Heap[rh].V; assert result = sVal[self] ; M13: Heap[rh].R := Dummy || Heap[rh].V := null; rVal[self] := result ; return ; } } } } procedure pushLeft(v) variables nd, rh, lhL, lh, temp; { N2: New(nd) ; if (nd = null) {rVal[self] := "full"; N1a: return ;} ; N4: Heap[nd].L := Dummy || Heap[nd].V := v; N6: while (TRUE) { lh := LeftHat; N8: lhL := Heap[lh].L; if (lhL = lh) { N10: Heap[nd].R := Dummy; N11: rh := RightHat; N12: DCAS(temp, LeftHat, RightHat, lh, rh, nd, nd) ; if (temp) { queue := <> \o queue ; rVal[self] := "okay"; N13: return;} } else { N15: Heap[nd].R := lh; N16: DCAS(temp, LeftHat, Heap[lh].L, lh, lhL, nd, nd) ; if (temp) { queue := <> \o queue ; rVal[self] := "okay"; N17: return } } } } procedure popLeft() variables rh, lh, lhR, temp, result; { O2: while (TRUE) { lh := LeftHat; sVal[self] := (queue = << >>) ; O4: rh := RightHat; O5: if (Heap[lh].L = lh) { assert sVal[self] \/ (queue = << >>) ; rVal[self] := "empty"; return ;} ; O6: if (lh = rh) { DCAS(temp, LeftHat, RightHat, lh, rh, Dummy, Dummy) ; if (temp) { sVal[self] := Head(queue) ; queue := Tail(queue) ; O8: rVal[self] := Heap[lh].V; assert rVal[self] = sVal[self] ; return; } } else { O10: lhR := Heap[lh].R; O11: DCAS(temp, LeftHat, Heap[lh].R, lh, lhR, lhR, lh) ; if (temp) { sVal[self] := Head(queue) ; queue := Tail(queue) ; O12: result := Heap[lh].V; assert result = sVal[self] ; O13: Heap[lh].L := Dummy || Heap[lh].V := null; rVal[self] := result; return ; } } } } process (test \in Procs) (*************************************************************************) (* A process just nondeterministically calls one of the four procedures, *) (* using a nondeterministically chosen element of Val as the push *) (* procedures' arguments. *) (*************************************************************************) { T1: while(TRUE) { either \* push with (pushedVal \in Val) { either call pushLeft(pushedVal) or call pushRight(pushedVal)} ; or \* pop either call popLeft() or call popRight() ; } } } *) \* BEGIN TRANSLATION \* Procedure variable nd of procedure pushRight at line 104 col 15 changed to nd_ \* Procedure variable rh of procedure pushRight at line 104 col 19 changed to rh_ \* Procedure variable lh of procedure pushRight at line 104 col 28 changed to lh_ \* Procedure variable temp of procedure pushRight at line 104 col 32 changed to temp_ \* Procedure variable rh of procedure popRight at line 129 col 12 changed to rh_p \* Procedure variable lh of procedure popRight at line 129 col 16 changed to lh_p \* Procedure variable temp of procedure popRight at line 129 col 25 changed to temp_p \* Procedure variable result of procedure popRight at line 129 col 31 changed to result_ \* Procedure variable rh of procedure pushLeft at line 159 col 16 changed to rh_pu \* Procedure variable lh of procedure pushLeft at line 159 col 25 changed to lh_pu \* Procedure variable temp of procedure pushLeft at line 159 col 29 changed to temp_pu \* Parameter v of procedure pushRight at line 103 col 21 changed to v_ VARIABLES LeftHat, RightHat, Heap, freeList, rVal, queue, sVal, pc, stack, v_, nd_, rh_, rhR, lh_, temp_, rh_p, lh_p, rhL, temp_p, result_, v, nd, rh_pu, lhL, lh_pu, temp_pu, rh, lh, lhR, temp, result vars == << LeftHat, RightHat, Heap, freeList, rVal, queue, sVal, pc, stack, v_, nd_, rh_, rhR, lh_, temp_, rh_p, lh_p, rhL, temp_p, result_, v, nd, rh_pu, lhL, lh_pu, temp_pu, rh, lh, lhR, temp, result >> ProcSet == (Procs) Init == (* Global variables *) /\ LeftHat = Dummy /\ RightHat = Dummy /\ Heap = [a \in Address |-> IF a = Dummy THEN DummyNode ELSE InitNode] /\ freeList = Address \ {Dummy} /\ rVal = [p \in Procs |-> "okay"] /\ queue = << >> /\ sVal = [p \in Procs |-> TRUE] (* Procedure pushRight *) /\ v_ = [ self \in ProcSet |-> {}] /\ nd_ = [ self \in ProcSet |-> {}] /\ rh_ = [ self \in ProcSet |-> {}] /\ rhR = [ self \in ProcSet |-> {}] /\ lh_ = [ self \in ProcSet |-> {}] /\ temp_ = [ self \in ProcSet |-> {}] (* Procedure popRight *) /\ rh_p = [ self \in ProcSet |-> {}] /\ lh_p = [ self \in ProcSet |-> {}] /\ rhL = [ self \in ProcSet |-> {}] /\ temp_p = [ self \in ProcSet |-> {}] /\ result_ = [ self \in ProcSet |-> {}] (* Procedure pushLeft *) /\ v = [ self \in ProcSet |-> {}] /\ nd = [ self \in ProcSet |-> {}] /\ rh_pu = [ self \in ProcSet |-> {}] /\ lhL = [ self \in ProcSet |-> {}] /\ lh_pu = [ self \in ProcSet |-> {}] /\ temp_pu = [ self \in ProcSet |-> {}] (* Procedure popLeft *) /\ rh = [ self \in ProcSet |-> {}] /\ lh = [ self \in ProcSet |-> {}] /\ lhR = [ self \in ProcSet |-> {}] /\ temp = [ self \in ProcSet |-> {}] /\ result = [ self \in ProcSet |-> {}] /\ stack = [self \in ProcSet |-> << >>] /\ pc = [self \in ProcSet |-> CASE self \in Procs -> "T1"] L2(self) == /\ pc[self] = "L2" /\ IF freeList # {} THEN /\ nd_' = [nd_ EXCEPT ![self] = CHOOSE a \in freeList : TRUE] /\ freeList' = freeList \ {nd_'[self]} ELSE /\ nd_' = [nd_ EXCEPT ![self] = null] /\ UNCHANGED freeList /\ IF nd_'[self] = null THEN /\ rVal' = [rVal EXCEPT ![self] = "full"] /\ pc' = [pc EXCEPT ![self] = "L3"] ELSE /\ pc' = [pc EXCEPT ![self] = "L4"] /\ UNCHANGED rVal /\ UNCHANGED << LeftHat, RightHat, Heap, queue, sVal, stack, v_, rh_, rhR, lh_, temp_, rh_p, lh_p, rhL, temp_p, result_, v, nd, rh_pu, lhL, lh_pu, temp_pu, rh, lh, lhR, temp, result >> L3(self) == /\ pc[self] = "L3" /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc] /\ nd_' = [nd_ EXCEPT ![self] = Head(stack[self]).nd_] /\ rh_' = [rh_ EXCEPT ![self] = Head(stack[self]).rh_] /\ rhR' = [rhR EXCEPT ![self] = Head(stack[self]).rhR] /\ lh_' = [lh_ EXCEPT ![self] = Head(stack[self]).lh_] /\ temp_' = [temp_ EXCEPT ![self] = Head(stack[self]).temp_] /\ v_' = [v_ EXCEPT ![self] = Head(stack[self]).v_] /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])] /\ UNCHANGED << LeftHat, RightHat, Heap, freeList, rVal, queue, sVal, rh_p, lh_p, rhL, temp_p, result_, v, nd, rh_pu, lhL, lh_pu, temp_pu, rh, lh, lhR, temp, result >> L4(self) == /\ pc[self] = "L4" /\ Heap' = [Heap EXCEPT ![nd_[self]].R = Dummy, ![nd_[self]].V = v_[self]] /\ pc' = [pc EXCEPT ![self] = "L6"] /\ UNCHANGED << LeftHat, RightHat, freeList, rVal, queue, sVal, stack, v_, nd_, rh_, rhR, lh_, temp_, rh_p, lh_p, rhL, temp_p, result_, v, nd, rh_pu, lhL, lh_pu, temp_pu, rh, lh, lhR, temp, result >> L6(self) == /\ pc[self] = "L6" /\ rh_' = [rh_ EXCEPT ![self] = RightHat] /\ pc' = [pc EXCEPT ![self] = "L8"] /\ UNCHANGED << LeftHat, RightHat, Heap, freeList, rVal, queue, sVal, stack, v_, nd_, rhR, lh_, temp_, rh_p, lh_p, rhL, temp_p, result_, v, nd, rh_pu, lhL, lh_pu, temp_pu, rh, lh, lhR, temp, result >> L8(self) == /\ pc[self] = "L8" /\ rhR' = [rhR EXCEPT ![self] = Heap[rh_[self]].R] /\ pc' = [pc EXCEPT ![self] = "L9"] /\ UNCHANGED << LeftHat, RightHat, Heap, freeList, rVal, queue, sVal, stack, v_, nd_, rh_, lh_, temp_, rh_p, lh_p, rhL, temp_p, result_, v, nd, rh_pu, lhL, lh_pu, temp_pu, rh, lh, lhR, temp, result >> L9(self) == /\ pc[self] = "L9" /\ IF rhR[self] = rh_[self] THEN /\ Heap' = [Heap EXCEPT ![nd_[self]].L = Dummy] /\ lh_' = [lh_ EXCEPT ![self] = LeftHat] /\ pc' = [pc EXCEPT ![self] = "L12"] ELSE /\ pc' = [pc EXCEPT ![self] = "L15"] /\ UNCHANGED << Heap, lh_ >> /\ UNCHANGED << LeftHat, RightHat, freeList, rVal, queue, sVal, stack, v_, nd_, rh_, rhR, temp_, rh_p, lh_p, rhL, temp_p, result_, v, nd, rh_pu, lhL, lh_pu, temp_pu, rh, lh, lhR, temp, result >> L12(self) == /\ pc[self] = "L12" /\ IF (RightHat = rh_[self]) /\ (LeftHat = lh_[self]) THEN /\ /\ LeftHat' = nd_[self] /\ RightHat' = nd_[self] /\ temp_' = [temp_ EXCEPT ![self] = TRUE] ELSE /\ temp_' = [temp_ EXCEPT ![self] = FALSE] /\ UNCHANGED << LeftHat, RightHat >> /\ IF temp_'[self] THEN /\ queue' = queue \o <> /\ rVal' = [rVal EXCEPT ![self] = "okay"] /\ pc' = [pc EXCEPT ![self] = "L13"] ELSE /\ pc' = [pc EXCEPT ![self] = "L6"] /\ UNCHANGED << rVal, queue >> /\ UNCHANGED << Heap, freeList, sVal, stack, v_, nd_, rh_, rhR, lh_, rh_p, lh_p, rhL, temp_p, result_, v, nd, rh_pu, lhL, lh_pu, temp_pu, rh, lh, lhR, temp, result >> L13(self) == /\ pc[self] = "L13" /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc] /\ nd_' = [nd_ EXCEPT ![self] = Head(stack[self]).nd_] /\ rh_' = [rh_ EXCEPT ![self] = Head(stack[self]).rh_] /\ rhR' = [rhR EXCEPT ![self] = Head(stack[self]).rhR] /\ lh_' = [lh_ EXCEPT ![self] = Head(stack[self]).lh_] /\ temp_' = [temp_ EXCEPT ![self] = Head(stack[self]).temp_] /\ v_' = [v_ EXCEPT ![self] = Head(stack[self]).v_] /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])] /\ UNCHANGED << LeftHat, RightHat, Heap, freeList, rVal, queue, sVal, rh_p, lh_p, rhL, temp_p, result_, v, nd, rh_pu, lhL, lh_pu, temp_pu, rh, lh, lhR, temp, result >> L15(self) == /\ pc[self] = "L15" /\ Heap' = [Heap EXCEPT ![nd_[self]].L = rh_[self]] /\ pc' = [pc EXCEPT ![self] = "L16"] /\ UNCHANGED << LeftHat, RightHat, freeList, rVal, queue, sVal, stack, v_, nd_, rh_, rhR, lh_, temp_, rh_p, lh_p, rhL, temp_p, result_, v, nd, rh_pu, lhL, lh_pu, temp_pu, rh, lh, lhR, temp, result >> L16(self) == /\ pc[self] = "L16" /\ IF (RightHat = rh_[self]) /\ ((Heap[rh_[self]].R) = rhR[self]) THEN /\ /\ Heap' = [Heap EXCEPT ![rh_[self]].R = nd_[self]] /\ RightHat' = nd_[self] /\ temp_' = [temp_ EXCEPT ![self] = TRUE] ELSE /\ temp_' = [temp_ EXCEPT ![self] = FALSE] /\ UNCHANGED << RightHat, Heap >> /\ IF temp_'[self] THEN /\ queue' = queue \o <> /\ rVal' = [rVal EXCEPT ![self] = "okay"] /\ pc' = [pc EXCEPT ![self] = "L17"] ELSE /\ pc' = [pc EXCEPT ![self] = "L6"] /\ UNCHANGED << rVal, queue >> /\ UNCHANGED << LeftHat, freeList, sVal, stack, v_, nd_, rh_, rhR, lh_, rh_p, lh_p, rhL, temp_p, result_, v, nd, rh_pu, lhL, lh_pu, temp_pu, rh, lh, lhR, temp, result >> L17(self) == /\ pc[self] = "L17" /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc] /\ nd_' = [nd_ EXCEPT ![self] = Head(stack[self]).nd_] /\ rh_' = [rh_ EXCEPT ![self] = Head(stack[self]).rh_] /\ rhR' = [rhR EXCEPT ![self] = Head(stack[self]).rhR] /\ lh_' = [lh_ EXCEPT ![self] = Head(stack[self]).lh_] /\ temp_' = [temp_ EXCEPT ![self] = Head(stack[self]).temp_] /\ v_' = [v_ EXCEPT ![self] = Head(stack[self]).v_] /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])] /\ UNCHANGED << LeftHat, RightHat, Heap, freeList, rVal, queue, sVal, rh_p, lh_p, rhL, temp_p, result_, v, nd, rh_pu, lhL, lh_pu, temp_pu, rh, lh, lhR, temp, result >> pushRight(self) == L2(self) \/ L3(self) \/ L4(self) \/ L6(self) \/ L8(self) \/ L9(self) \/ L12(self) \/ L13(self) \/ L15(self) \/ L16(self) \/ L17(self) M2(self) == /\ pc[self] = "M2" /\ rh_p' = [rh_p EXCEPT ![self] = RightHat] /\ sVal' = [sVal EXCEPT ![self] = (queue = << >>)] /\ pc' = [pc EXCEPT ![self] = "M4"] /\ UNCHANGED << LeftHat, RightHat, Heap, freeList, rVal, queue, stack, v_, nd_, rh_, rhR, lh_, temp_, lh_p, rhL, temp_p, result_, v, nd, rh_pu, lhL, lh_pu, temp_pu, rh, lh, lhR, temp, result >> M4(self) == /\ pc[self] = "M4" /\ lh_p' = [lh_p EXCEPT ![self] = LeftHat] /\ pc' = [pc EXCEPT ![self] = "M5"] /\ UNCHANGED << LeftHat, RightHat, Heap, freeList, rVal, queue, sVal, stack, v_, nd_, rh_, rhR, lh_, temp_, rh_p, rhL, temp_p, result_, v, nd, rh_pu, lhL, lh_pu, temp_pu, rh, lh, lhR, temp, result >> M5(self) == /\ pc[self] = "M5" /\ IF Heap[rh_p[self]].R = rh_p[self] THEN /\ Assert(sVal[self] \/ (queue = << >>), "Failure of assertion at line line 135, column 13.") /\ rVal' = [rVal EXCEPT ![self] = "empty"] /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc] /\ rh_p' = [rh_p EXCEPT ![self] = Head(stack[self]).rh_p] /\ lh_p' = [lh_p EXCEPT ![self] = Head(stack[self]).lh_p] /\ rhL' = [rhL EXCEPT ![self] = Head(stack[self]).rhL] /\ temp_p' = [temp_p EXCEPT ![self] = Head(stack[self]).temp_p] /\ result_' = [result_ EXCEPT ![self] = Head(stack[self]).result_] /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])] ELSE /\ pc' = [pc EXCEPT ![self] = "M6"] /\ UNCHANGED << rVal, stack, rh_p, lh_p, rhL, temp_p, result_ >> /\ UNCHANGED << LeftHat, RightHat, Heap, freeList, queue, sVal, v_, nd_, rh_, rhR, lh_, temp_, v, nd, rh_pu, lhL, lh_pu, temp_pu, rh, lh, lhR, temp, result >> M6(self) == /\ pc[self] = "M6" /\ IF rh_p[self] = lh_p[self] THEN /\ IF (RightHat = rh_p[self]) /\ (LeftHat = lh_p[self]) THEN /\ /\ LeftHat' = Dummy /\ RightHat' = Dummy /\ temp_p' = [temp_p EXCEPT ![self] = TRUE] ELSE /\ temp_p' = [temp_p EXCEPT ![self] = FALSE] /\ UNCHANGED << LeftHat, RightHat >> /\ IF temp_p'[self] THEN /\ sVal' = [sVal EXCEPT ![self] = Last(queue)] /\ queue' = Front(queue) /\ pc' = [pc EXCEPT ![self] = "M8"] ELSE /\ pc' = [pc EXCEPT ![self] = "M2"] /\ UNCHANGED << queue, sVal >> ELSE /\ pc' = [pc EXCEPT ![self] = "M10"] /\ UNCHANGED << LeftHat, RightHat, queue, sVal, temp_p >> /\ UNCHANGED << Heap, freeList, rVal, stack, v_, nd_, rh_, rhR, lh_, temp_, rh_p, lh_p, rhL, result_, v, nd, rh_pu, lhL, lh_pu, temp_pu, rh, lh, lhR, temp, result >> M10(self) == /\ pc[self] = "M10" /\ rhL' = [rhL EXCEPT ![self] = Heap[rh_p[self]].L] /\ pc' = [pc EXCEPT ![self] = "M11"] /\ UNCHANGED << LeftHat, RightHat, Heap, freeList, rVal, queue, sVal, stack, v_, nd_, rh_, rhR, lh_, temp_, rh_p, lh_p, temp_p, result_, v, nd, rh_pu, lhL, lh_pu, temp_pu, rh, lh, lhR, temp, result >> M11(self) == /\ pc[self] = "M11" /\ IF (RightHat = rh_p[self]) /\ ((Heap[rh_p[self]].L) = rhL[self]) THEN /\ /\ Heap' = [Heap EXCEPT ![rh_p[self]].L = rh_p[self]] /\ RightHat' = rhL[self] /\ temp_p' = [temp_p EXCEPT ![self] = TRUE] ELSE /\ temp_p' = [temp_p EXCEPT ![self] = FALSE] /\ UNCHANGED << RightHat, Heap >> /\ IF temp_p'[self] THEN /\ sVal' = [sVal EXCEPT ![self] = Last(queue)] /\ queue' = Front(queue) /\ pc' = [pc EXCEPT ![self] = "M12"] ELSE /\ pc' = [pc EXCEPT ![self] = "M2"] /\ UNCHANGED << queue, sVal >> /\ UNCHANGED << LeftHat, freeList, rVal, stack, v_, nd_, rh_, rhR, lh_, temp_, rh_p, lh_p, rhL, result_, v, nd, rh_pu, lhL, lh_pu, temp_pu, rh, lh, lhR, temp, result >> M12(self) == /\ pc[self] = "M12" /\ result_' = [result_ EXCEPT ![self] = Heap[rh_p[self]].V] /\ Assert(result_'[self] = sVal[self], "Failure of assertion at line line 151, column 11.") /\ pc' = [pc EXCEPT ![self] = "M13"] /\ UNCHANGED << LeftHat, RightHat, Heap, freeList, rVal, queue, sVal, stack, v_, nd_, rh_, rhR, lh_, temp_, rh_p, lh_p, rhL, temp_p, v, nd, rh_pu, lhL, lh_pu, temp_pu, rh, lh, lhR, temp, result >> M13(self) == /\ pc[self] = "M13" /\ Heap' = [Heap EXCEPT ![rh_p[self]].R = Dummy, ![rh_p[self]].V = null] /\ rVal' = [rVal EXCEPT ![self] = result_[self]] /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc] /\ rh_p' = [rh_p EXCEPT ![self] = Head(stack[self]).rh_p] /\ lh_p' = [lh_p EXCEPT ![self] = Head(stack[self]).lh_p] /\ rhL' = [rhL EXCEPT ![self] = Head(stack[self]).rhL] /\ temp_p' = [temp_p EXCEPT ![self] = Head(stack[self]).temp_p] /\ result_' = [result_ EXCEPT ![self] = Head(stack[self]).result_] /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])] /\ UNCHANGED << LeftHat, RightHat, freeList, queue, sVal, v_, nd_, rh_, rhR, lh_, temp_, v, nd, rh_pu, lhL, lh_pu, temp_pu, rh, lh, lhR, temp, result >> M8(self) == /\ pc[self] = "M8" /\ rVal' = [rVal EXCEPT ![self] = Heap[rh_p[self]].V] /\ Assert(rVal'[self] = sVal[self], "Failure of assertion at line line 143, column 11.") /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc] /\ rh_p' = [rh_p EXCEPT ![self] = Head(stack[self]).rh_p] /\ lh_p' = [lh_p EXCEPT ![self] = Head(stack[self]).lh_p] /\ rhL' = [rhL EXCEPT ![self] = Head(stack[self]).rhL] /\ temp_p' = [temp_p EXCEPT ![self] = Head(stack[self]).temp_p] /\ result_' = [result_ EXCEPT ![self] = Head(stack[self]).result_] /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])] /\ UNCHANGED << LeftHat, RightHat, Heap, freeList, queue, sVal, v_, nd_, rh_, rhR, lh_, temp_, v, nd, rh_pu, lhL, lh_pu, temp_pu, rh, lh, lhR, temp, result >> popRight(self) == M2(self) \/ M4(self) \/ M5(self) \/ M6(self) \/ M10(self) \/ M11(self) \/ M12(self) \/ M13(self) \/ M8(self) N2(self) == /\ pc[self] = "N2" /\ IF freeList # {} THEN /\ nd' = [nd EXCEPT ![self] = CHOOSE a \in freeList : TRUE] /\ freeList' = freeList \ {nd'[self]} ELSE /\ nd' = [nd EXCEPT ![self] = null] /\ UNCHANGED freeList /\ IF nd'[self] = null THEN /\ rVal' = [rVal EXCEPT ![self] = "full"] /\ pc' = [pc EXCEPT ![self] = "N1a"] ELSE /\ pc' = [pc EXCEPT ![self] = "N4"] /\ UNCHANGED rVal /\ UNCHANGED << LeftHat, RightHat, Heap, queue, sVal, stack, v_, nd_, rh_, rhR, lh_, temp_, rh_p, lh_p, rhL, temp_p, result_, v, rh_pu, lhL, lh_pu, temp_pu, rh, lh, lhR, temp, result >> N1a(self) == /\ pc[self] = "N1a" /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc] /\ nd' = [nd EXCEPT ![self] = Head(stack[self]).nd] /\ rh_pu' = [rh_pu EXCEPT ![self] = Head(stack[self]).rh_pu] /\ lhL' = [lhL EXCEPT ![self] = Head(stack[self]).lhL] /\ lh_pu' = [lh_pu EXCEPT ![self] = Head(stack[self]).lh_pu] /\ temp_pu' = [temp_pu EXCEPT ![self] = Head(stack[self]).temp_pu] /\ v' = [v EXCEPT ![self] = Head(stack[self]).v] /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])] /\ UNCHANGED << LeftHat, RightHat, Heap, freeList, rVal, queue, sVal, v_, nd_, rh_, rhR, lh_, temp_, rh_p, lh_p, rhL, temp_p, result_, rh, lh, lhR, temp, result >> N4(self) == /\ pc[self] = "N4" /\ Heap' = [Heap EXCEPT ![nd[self]].L = Dummy, ![nd[self]].V = v[self]] /\ pc' = [pc EXCEPT ![self] = "N6"] /\ UNCHANGED << LeftHat, RightHat, freeList, rVal, queue, sVal, stack, v_, nd_, rh_, rhR, lh_, temp_, rh_p, lh_p, rhL, temp_p, result_, v, nd, rh_pu, lhL, lh_pu, temp_pu, rh, lh, lhR, temp, result >> N6(self) == /\ pc[self] = "N6" /\ lh_pu' = [lh_pu EXCEPT ![self] = LeftHat] /\ pc' = [pc EXCEPT ![self] = "N8"] /\ UNCHANGED << LeftHat, RightHat, Heap, freeList, rVal, queue, sVal, stack, v_, nd_, rh_, rhR, lh_, temp_, rh_p, lh_p, rhL, temp_p, result_, v, nd, rh_pu, lhL, temp_pu, rh, lh, lhR, temp, result >> N8(self) == /\ pc[self] = "N8" /\ lhL' = [lhL EXCEPT ![self] = Heap[lh_pu[self]].L] /\ IF lhL'[self] = lh_pu[self] THEN /\ pc' = [pc EXCEPT ![self] = "N10"] ELSE /\ pc' = [pc EXCEPT ![self] = "N15"] /\ UNCHANGED << LeftHat, RightHat, Heap, freeList, rVal, queue, sVal, stack, v_, nd_, rh_, rhR, lh_, temp_, rh_p, lh_p, rhL, temp_p, result_, v, nd, rh_pu, lh_pu, temp_pu, rh, lh, lhR, temp, result >> N10(self) == /\ pc[self] = "N10" /\ Heap' = [Heap EXCEPT ![nd[self]].R = Dummy] /\ pc' = [pc EXCEPT ![self] = "N11"] /\ UNCHANGED << LeftHat, RightHat, freeList, rVal, queue, sVal, stack, v_, nd_, rh_, rhR, lh_, temp_, rh_p, lh_p, rhL, temp_p, result_, v, nd, rh_pu, lhL, lh_pu, temp_pu, rh, lh, lhR, temp, result >> N11(self) == /\ pc[self] = "N11" /\ rh_pu' = [rh_pu EXCEPT ![self] = RightHat] /\ pc' = [pc EXCEPT ![self] = "N12"] /\ UNCHANGED << LeftHat, RightHat, Heap, freeList, rVal, queue, sVal, stack, v_, nd_, rh_, rhR, lh_, temp_, rh_p, lh_p, rhL, temp_p, result_, v, nd, lhL, lh_pu, temp_pu, rh, lh, lhR, temp, result >> N12(self) == /\ pc[self] = "N12" /\ IF (LeftHat = lh_pu[self]) /\ (RightHat = rh_pu[self]) THEN /\ /\ LeftHat' = nd[self] /\ RightHat' = nd[self] /\ temp_pu' = [temp_pu EXCEPT ![self] = TRUE] ELSE /\ temp_pu' = [temp_pu EXCEPT ![self] = FALSE] /\ UNCHANGED << LeftHat, RightHat >> /\ IF temp_pu'[self] THEN /\ queue' = <> \o queue /\ rVal' = [rVal EXCEPT ![self] = "okay"] /\ pc' = [pc EXCEPT ![self] = "N13"] ELSE /\ pc' = [pc EXCEPT ![self] = "N6"] /\ UNCHANGED << rVal, queue >> /\ UNCHANGED << Heap, freeList, sVal, stack, v_, nd_, rh_, rhR, lh_, temp_, rh_p, lh_p, rhL, temp_p, result_, v, nd, rh_pu, lhL, lh_pu, rh, lh, lhR, temp, result >> N13(self) == /\ pc[self] = "N13" /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc] /\ nd' = [nd EXCEPT ![self] = Head(stack[self]).nd] /\ rh_pu' = [rh_pu EXCEPT ![self] = Head(stack[self]).rh_pu] /\ lhL' = [lhL EXCEPT ![self] = Head(stack[self]).lhL] /\ lh_pu' = [lh_pu EXCEPT ![self] = Head(stack[self]).lh_pu] /\ temp_pu' = [temp_pu EXCEPT ![self] = Head(stack[self]).temp_pu] /\ v' = [v EXCEPT ![self] = Head(stack[self]).v] /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])] /\ UNCHANGED << LeftHat, RightHat, Heap, freeList, rVal, queue, sVal, v_, nd_, rh_, rhR, lh_, temp_, rh_p, lh_p, rhL, temp_p, result_, rh, lh, lhR, temp, result >> N15(self) == /\ pc[self] = "N15" /\ Heap' = [Heap EXCEPT ![nd[self]].R = lh_pu[self]] /\ pc' = [pc EXCEPT ![self] = "N16"] /\ UNCHANGED << LeftHat, RightHat, freeList, rVal, queue, sVal, stack, v_, nd_, rh_, rhR, lh_, temp_, rh_p, lh_p, rhL, temp_p, result_, v, nd, rh_pu, lhL, lh_pu, temp_pu, rh, lh, lhR, temp, result >> N16(self) == /\ pc[self] = "N16" /\ IF (LeftHat = lh_pu[self]) /\ ((Heap[lh_pu[self]].L) = lhL[self]) THEN /\ /\ Heap' = [Heap EXCEPT ![lh_pu[self]].L = nd[self]] /\ LeftHat' = nd[self] /\ temp_pu' = [temp_pu EXCEPT ![self] = TRUE] ELSE /\ temp_pu' = [temp_pu EXCEPT ![self] = FALSE] /\ UNCHANGED << LeftHat, Heap >> /\ IF temp_pu'[self] THEN /\ queue' = <> \o queue /\ rVal' = [rVal EXCEPT ![self] = "okay"] /\ pc' = [pc EXCEPT ![self] = "N17"] ELSE /\ pc' = [pc EXCEPT ![self] = "N6"] /\ UNCHANGED << rVal, queue >> /\ UNCHANGED << RightHat, freeList, sVal, stack, v_, nd_, rh_, rhR, lh_, temp_, rh_p, lh_p, rhL, temp_p, result_, v, nd, rh_pu, lhL, lh_pu, rh, lh, lhR, temp, result >> N17(self) == /\ pc[self] = "N17" /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc] /\ nd' = [nd EXCEPT ![self] = Head(stack[self]).nd] /\ rh_pu' = [rh_pu EXCEPT ![self] = Head(stack[self]).rh_pu] /\ lhL' = [lhL EXCEPT ![self] = Head(stack[self]).lhL] /\ lh_pu' = [lh_pu EXCEPT ![self] = Head(stack[self]).lh_pu] /\ temp_pu' = [temp_pu EXCEPT ![self] = Head(stack[self]).temp_pu] /\ v' = [v EXCEPT ![self] = Head(stack[self]).v] /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])] /\ UNCHANGED << LeftHat, RightHat, Heap, freeList, rVal, queue, sVal, v_, nd_, rh_, rhR, lh_, temp_, rh_p, lh_p, rhL, temp_p, result_, rh, lh, lhR, temp, result >> pushLeft(self) == N2(self) \/ N1a(self) \/ N4(self) \/ N6(self) \/ N8(self) \/ N10(self) \/ N11(self) \/ N12(self) \/ N13(self) \/ N15(self) \/ N16(self) \/ N17(self) O2(self) == /\ pc[self] = "O2" /\ lh' = [lh EXCEPT ![self] = LeftHat] /\ sVal' = [sVal EXCEPT ![self] = (queue = << >>)] /\ pc' = [pc EXCEPT ![self] = "O4"] /\ UNCHANGED << LeftHat, RightHat, Heap, freeList, rVal, queue, stack, v_, nd_, rh_, rhR, lh_, temp_, rh_p, lh_p, rhL, temp_p, result_, v, nd, rh_pu, lhL, lh_pu, temp_pu, rh, lhR, temp, result >> O4(self) == /\ pc[self] = "O4" /\ rh' = [rh EXCEPT ![self] = RightHat] /\ pc' = [pc EXCEPT ![self] = "O5"] /\ UNCHANGED << LeftHat, RightHat, Heap, freeList, rVal, queue, sVal, stack, v_, nd_, rh_, rhR, lh_, temp_, rh_p, lh_p, rhL, temp_p, result_, v, nd, rh_pu, lhL, lh_pu, temp_pu, lh, lhR, temp, result >> O5(self) == /\ pc[self] = "O5" /\ IF Heap[lh[self]].L = lh[self] THEN /\ Assert(sVal[self] \/ (queue = << >>), "Failure of assertion at line line 190, column 9.") /\ rVal' = [rVal EXCEPT ![self] = "empty"] /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc] /\ rh' = [rh EXCEPT ![self] = Head(stack[self]).rh] /\ lh' = [lh EXCEPT ![self] = Head(stack[self]).lh] /\ lhR' = [lhR EXCEPT ![self] = Head(stack[self]).lhR] /\ temp' = [temp EXCEPT ![self] = Head(stack[self]).temp] /\ result' = [result EXCEPT ![self] = Head(stack[self]).result] /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])] ELSE /\ pc' = [pc EXCEPT ![self] = "O6"] /\ UNCHANGED << rVal, stack, rh, lh, lhR, temp, result >> /\ UNCHANGED << LeftHat, RightHat, Heap, freeList, queue, sVal, v_, nd_, rh_, rhR, lh_, temp_, rh_p, lh_p, rhL, temp_p, result_, v, nd, rh_pu, lhL, lh_pu, temp_pu >> O6(self) == /\ pc[self] = "O6" /\ IF lh[self] = rh[self] THEN /\ IF (LeftHat = lh[self]) /\ (RightHat = rh[self]) THEN /\ /\ LeftHat' = Dummy /\ RightHat' = Dummy /\ temp' = [temp EXCEPT ![self] = TRUE] ELSE /\ temp' = [temp EXCEPT ![self] = FALSE] /\ UNCHANGED << LeftHat, RightHat >> /\ IF temp'[self] THEN /\ sVal' = [sVal EXCEPT ![self] = Head(queue)] /\ queue' = Tail(queue) /\ pc' = [pc EXCEPT ![self] = "O8"] ELSE /\ pc' = [pc EXCEPT ![self] = "O2"] /\ UNCHANGED << queue, sVal >> ELSE /\ pc' = [pc EXCEPT ![self] = "O10"] /\ UNCHANGED << LeftHat, RightHat, queue, sVal, temp >> /\ UNCHANGED << Heap, freeList, rVal, stack, v_, nd_, rh_, rhR, lh_, temp_, rh_p, lh_p, rhL, temp_p, result_, v, nd, rh_pu, lhL, lh_pu, temp_pu, rh, lh, lhR, result >> O10(self) == /\ pc[self] = "O10" /\ lhR' = [lhR EXCEPT ![self] = Heap[lh[self]].R] /\ pc' = [pc EXCEPT ![self] = "O11"] /\ UNCHANGED << LeftHat, RightHat, Heap, freeList, rVal, queue, sVal, stack, v_, nd_, rh_, rhR, lh_, temp_, rh_p, lh_p, rhL, temp_p, result_, v, nd, rh_pu, lhL, lh_pu, temp_pu, rh, lh, temp, result >> O11(self) == /\ pc[self] = "O11" /\ IF (LeftHat = lh[self]) /\ ((Heap[lh[self]].R) = lhR[self]) THEN /\ /\ Heap' = [Heap EXCEPT ![lh[self]].R = lh[self]] /\ LeftHat' = lhR[self] /\ temp' = [temp EXCEPT ![self] = TRUE] ELSE /\ temp' = [temp EXCEPT ![self] = FALSE] /\ UNCHANGED << LeftHat, Heap >> /\ IF temp'[self] THEN /\ sVal' = [sVal EXCEPT ![self] = Head(queue)] /\ queue' = Tail(queue) /\ pc' = [pc EXCEPT ![self] = "O12"] ELSE /\ pc' = [pc EXCEPT ![self] = "O2"] /\ UNCHANGED << queue, sVal >> /\ UNCHANGED << RightHat, freeList, rVal, stack, v_, nd_, rh_, rhR, lh_, temp_, rh_p, lh_p, rhL, temp_p, result_, v, nd, rh_pu, lhL, lh_pu, temp_pu, rh, lh, lhR, result >> O12(self) == /\ pc[self] = "O12" /\ result' = [result EXCEPT ![self] = Heap[lh[self]].V] /\ Assert(result'[self] = sVal[self], "Failure of assertion at line line 207, column 11.") /\ pc' = [pc EXCEPT ![self] = "O13"] /\ UNCHANGED << LeftHat, RightHat, Heap, freeList, rVal, queue, sVal, stack, v_, nd_, rh_, rhR, lh_, temp_, rh_p, lh_p, rhL, temp_p, result_, v, nd, rh_pu, lhL, lh_pu, temp_pu, rh, lh, lhR, temp >> O13(self) == /\ pc[self] = "O13" /\ Heap' = [Heap EXCEPT ![lh[self]].L = Dummy, ![lh[self]].V = null] /\ rVal' = [rVal EXCEPT ![self] = result[self]] /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc] /\ rh' = [rh EXCEPT ![self] = Head(stack[self]).rh] /\ lh' = [lh EXCEPT ![self] = Head(stack[self]).lh] /\ lhR' = [lhR EXCEPT ![self] = Head(stack[self]).lhR] /\ temp' = [temp EXCEPT ![self] = Head(stack[self]).temp] /\ result' = [result EXCEPT ![self] = Head(stack[self]).result] /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])] /\ UNCHANGED << LeftHat, RightHat, freeList, queue, sVal, v_, nd_, rh_, rhR, lh_, temp_, rh_p, lh_p, rhL, temp_p, result_, v, nd, rh_pu, lhL, lh_pu, temp_pu >> O8(self) == /\ pc[self] = "O8" /\ rVal' = [rVal EXCEPT ![self] = Heap[lh[self]].V] /\ Assert(rVal'[self] = sVal[self], "Failure of assertion at line line 198, column 9.") /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc] /\ rh' = [rh EXCEPT ![self] = Head(stack[self]).rh] /\ lh' = [lh EXCEPT ![self] = Head(stack[self]).lh] /\ lhR' = [lhR EXCEPT ![self] = Head(stack[self]).lhR] /\ temp' = [temp EXCEPT ![self] = Head(stack[self]).temp] /\ result' = [result EXCEPT ![self] = Head(stack[self]).result] /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])] /\ UNCHANGED << LeftHat, RightHat, Heap, freeList, queue, sVal, v_, nd_, rh_, rhR, lh_, temp_, rh_p, lh_p, rhL, temp_p, result_, v, nd, rh_pu, lhL, lh_pu, temp_pu >> popLeft(self) == O2(self) \/ O4(self) \/ O5(self) \/ O6(self) \/ O10(self) \/ O11(self) \/ O12(self) \/ O13(self) \/ O8(self) T1(self) == /\ pc[self] = "T1" /\ \/ /\ \E pushedVal \in Val: \/ /\ /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "pushLeft", pc |-> "T1", nd |-> nd[self], rh_pu |-> rh_pu[self], lhL |-> lhL[self], lh_pu |-> lh_pu[self], temp_pu |-> temp_pu[self], v |-> v[self] ] >> \o stack[self]] /\ v' = [v EXCEPT ![self] = pushedVal] /\ nd' = [nd EXCEPT ![self] = {}] /\ rh_pu' = [rh_pu EXCEPT ![self] = {}] /\ lhL' = [lhL EXCEPT ![self] = {}] /\ lh_pu' = [lh_pu EXCEPT ![self] = {}] /\ temp_pu' = [temp_pu EXCEPT ![self] = {}] /\ pc' = [pc EXCEPT ![self] = "N2"] /\ UNCHANGED <> \/ /\ /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "pushRight", pc |-> "T1", nd_ |-> nd_[self], rh_ |-> rh_[self], rhR |-> rhR[self], lh_ |-> lh_[self], temp_ |-> temp_[self], v_ |-> v_[self] ] >> \o stack[self]] /\ v_' = [v_ EXCEPT ![self] = pushedVal] /\ nd_' = [nd_ EXCEPT ![self] = {}] /\ rh_' = [rh_ EXCEPT ![self] = {}] /\ rhR' = [rhR EXCEPT ![self] = {}] /\ lh_' = [lh_ EXCEPT ![self] = {}] /\ temp_' = [temp_ EXCEPT ![self] = {}] /\ pc' = [pc EXCEPT ![self] = "L2"] /\ UNCHANGED <> /\ UNCHANGED <> \/ /\ \/ /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "popLeft", pc |-> "T1", rh |-> rh[self], lh |-> lh[self], lhR |-> lhR[self], temp |-> temp[self], result |-> result[self] ] >> \o stack[self]] /\ rh' = [rh EXCEPT ![self] = {}] /\ lh' = [lh EXCEPT ![self] = {}] /\ lhR' = [lhR EXCEPT ![self] = {}] /\ temp' = [temp EXCEPT ![self] = {}] /\ result' = [result EXCEPT ![self] = {}] /\ pc' = [pc EXCEPT ![self] = "O2"] /\ UNCHANGED <> \/ /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "popRight", pc |-> "T1", rh_p |-> rh_p[self], lh_p |-> lh_p[self], rhL |-> rhL[self], temp_p |-> temp_p[self], result_ |-> result_[self] ] >> \o stack[self]] /\ rh_p' = [rh_p EXCEPT ![self] = {}] /\ lh_p' = [lh_p EXCEPT ![self] = {}] /\ rhL' = [rhL EXCEPT ![self] = {}] /\ temp_p' = [temp_p EXCEPT ![self] = {}] /\ result_' = [result_ EXCEPT ![self] = {}] /\ pc' = [pc EXCEPT ![self] = "M2"] /\ UNCHANGED <> /\ UNCHANGED <> /\ UNCHANGED << LeftHat, RightHat, Heap, freeList, rVal, queue, sVal >> test(self) == T1(self) Next == (\E self \in ProcSet: \/ pushRight(self) \/ popRight(self) \/ pushLeft(self) \/ popLeft(self)) \/ (\E self \in Procs: test(self)) \/ (* Disjunct to prevent deadlock on termination *) (\A self \in ProcSet: pc[self] = "Done" /\ UNCHANGED vars) Spec == Init /\ [][Next]_vars Termination == <>(\A self \in ProcSet: pc[self] = "Done") \* END TRANSLATION Symmetry == Permutations(Address \ {Dummy}) \cup Permutations(Procs) (*************************************************************************) (* I originally intended to use TLC's symmetry reduction but I forgot to *) (* add the SYMMETRY statement to the configuration file. To make it *) (* work with this version of the spec, it's necessary to initialize the *) (* variables with values of the correct "type". (I initialized the *) (* variables in the original version in order to slightly reduced the *) (* state space.) *) (*************************************************************************) Liveness == \A p \in Procs : []<> (pc[p] = "T1") (*************************************************************************) (* This liveness property essentially asserts that every procedure call *) (* returns. *) (*************************************************************************) =============================================================================