---- MODULE Monitor ---- EXTENDS Naturals, Sequences, TLC, FiniteSets, TLAPS ---- \* Auxiliary definitions \* General definitions PositiveInteger == Nat \ {0} \* Operations on Last(q) == q[Len(q)] Front(q) == [i \in 1..(Len(q)-1) |-> q[i]] \* not used: Insert_as_2nd(q,x) == <> \o q Member(q,e) == \E i \in 1 .. Len(q) : q[i] = e ---- \* Process identifiers \* PlusCal requires process identifiers of different processes to be different: CONSTANTS N_Lockers, N_Waiters, N_Signalers ASSUME AtLeastOne == /\ N_Lockers \in PositiveInteger /\ N_Waiters \in PositiveInteger /\ N_Signalers \in PositiveInteger Locker_First_PId == 1 Locker_Last_PId == Locker_First_PId + N_Lockers - 1 Waiter_First_PId == Locker_Last_PId + 1 Waiter_Last_PId == Waiter_First_PId + N_Waiters - 1 Signaler_First_PId == Waiter_Last_PId + 1 Signaler_Last_PId == Signaler_First_PId + N_Signalers - 1 Locker_PId == Locker_First_PId .. Locker_Last_PId Waiter_PId == Waiter_First_PId .. Waiter_Last_PId Signaler_PId == Signaler_First_PId .. Signaler_Last_PId ---- \* Condition identifiers (condition number 0 will be implemented as purgatory) CONSTANT N_Conditions ASSUME N_Conditions \in PositiveInteger CId == 0 .. N_Conditions ---- (* --algorithm TestMonitor { (***************************************************************************) (* The global variables, and their initial values. *) (***************************************************************************) variables \* Problem variables cq = [cid \in CId |-> <<>>]; lq = <<>>; pendingSignals = 0; inPurgatory = 0; waiting = [cid \in CId |-> 0]; \* Instrumentation lastSignal = <<0,0>>; \* from-to \********************************************************************* \* Specification of the Java implementations of Lock and Conditions procedure java_lock() { java_lock_begin: lq := Append(lq,self); java_lock_blocked: await self = Head(lq); java_lock_end: return; } procedure java_unlock() { java_unlock_begin: lq := Tail(lq); java_unlock_end: return; } procedure java_await(wcid) { java_await_begin: cq[wcid] := Append(cq[wcid],self); java_await_unlocking: lq := Tail(lq); java_await_blocked: await Len(lq) > 0 /\ self = Head(lq); java_await_end: return; } procedure java_signal(scid) { java_signal_begin: if (Len(cq[scid]) > 0) { lq := Append(lq,Head(cq[scid])); cq[scid] := Tail(cq[scid]); }; java_signal_end: return; } \********************************************************************* \* Specification of the CCLib implementations of Monitors procedure cclib_enter() { cclib_enter_begin: call java_lock(); cclib_enter_check_priority: if (pendingSignals > 0 \/ inPurgatory > 0) { inPurgatory := inPurgatory + 1; call java_await(0); cclib_enter_toheaven: inPurgatory := inPurgatory - 1; }; cclib_enter_end: return; } procedure cclib_leave() { cclib_leave_begin: if (pendingSignals = 0 /\ inPurgatory > 0) { call java_signal(0); }; cclib_leave_resetlastsignal: if (lastSignal[1] # self) { lastSignal := <<0,0>>; }; cclib_leave_unlocking: call java_unlock(); cclib_leave_end: return; } procedure cclib_await(cclwcid) { cclib_await_begin: waiting[cclwcid] := waiting[cclwcid] + 1; if (pendingSignals = 0 /\ inPurgatory > 0 ) { call java_signal(0); }; cclib_await_actualawait: call java_await(cclwcid); cclib_await_reentering: pendingSignals := pendingSignals - 1; cclib_await_end: return; } procedure cclib_signal(cclscid) { cclib_signal_begin: if (waiting[cclscid] > 0) { cclib_signal_actualsignal: pendingSignals := pendingSignals + 1; waiting[cclscid] := waiting[cclscid] - 1; cclib_signal_setlastsignal: lastSignal := <>; call java_signal(cclscid); }; cclib_signal_end: return; } \********************************************************************* \* Process in the system process (locker \in Locker_PId) { locker_begin: call cclib_enter(); locker_in: skip; call cclib_leave(); } process (waiter \in Waiter_PId) { waiter_begin: call cclib_enter(); waiter_before_await: call cclib_await(1 + ((self - Waiter_First_PId) % N_Conditions)); waiter_after_await: call cclib_leave(); } process (signaler \in Signaler_PId) { signaler_begin: call cclib_enter(); signaler_before_signal: call cclib_signal(1 + ((self - Signaler_First_PId) % N_Conditions)); signaler_after_signal: call cclib_leave(); } } *) \* BEGIN TRANSLATION CONSTANT defaultInitValue VARIABLES cq, lq, pendingSignals, inPurgatory, waiting, lastSignal, pc, stack, wcid, scid, cclwcid, cclscid vars == << cq, lq, pendingSignals, inPurgatory, waiting, lastSignal, pc, stack, wcid, scid, cclwcid, cclscid >> ProcSet == (Locker_PId) \cup (Waiter_PId) \cup (Signaler_PId) Init == (* Global variables *) /\ cq = [cid \in CId |-> <<>>] /\ lq = <<>> /\ pendingSignals = 0 /\ inPurgatory = 0 /\ waiting = [cid \in CId |-> 0] /\ lastSignal = <<0,0>> (* Procedure java_await *) /\ wcid = [ self \in ProcSet |-> defaultInitValue] (* Procedure java_signal *) /\ scid = [ self \in ProcSet |-> defaultInitValue] (* Procedure cclib_await *) /\ cclwcid = [ self \in ProcSet |-> defaultInitValue] (* Procedure cclib_signal *) /\ cclscid = [ self \in ProcSet |-> defaultInitValue] /\ stack = [self \in ProcSet |-> << >>] /\ pc = [self \in ProcSet |-> CASE self \in Locker_PId -> "locker_begin" [] self \in Waiter_PId -> "waiter_begin" [] self \in Signaler_PId -> "signaler_begin"] java_lock_begin(self) == /\ pc[self] = "java_lock_begin" /\ lq' = Append(lq,self) /\ pc' = [pc EXCEPT ![self] = "java_lock_blocked"] /\ UNCHANGED << cq, pendingSignals, inPurgatory, waiting, lastSignal, stack, wcid, scid, cclwcid, cclscid >> java_lock_blocked(self) == /\ pc[self] = "java_lock_blocked" /\ self = Head(lq) /\ pc' = [pc EXCEPT ![self] = "java_lock_end"] /\ UNCHANGED << cq, lq, pendingSignals, inPurgatory, waiting, lastSignal, stack, wcid, scid, cclwcid, cclscid >> java_lock_end(self) == /\ pc[self] = "java_lock_end" /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc] /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])] /\ UNCHANGED << cq, lq, pendingSignals, inPurgatory, waiting, lastSignal, wcid, scid, cclwcid, cclscid >> java_lock(self) == java_lock_begin(self) \/ java_lock_blocked(self) \/ java_lock_end(self) java_unlock_begin(self) == /\ pc[self] = "java_unlock_begin" /\ lq' = Tail(lq) /\ pc' = [pc EXCEPT ![self] = "java_unlock_end"] /\ UNCHANGED << cq, pendingSignals, inPurgatory, waiting, lastSignal, stack, wcid, scid, cclwcid, cclscid >> java_unlock_end(self) == /\ pc[self] = "java_unlock_end" /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc] /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])] /\ UNCHANGED << cq, lq, pendingSignals, inPurgatory, waiting, lastSignal, wcid, scid, cclwcid, cclscid >> java_unlock(self) == java_unlock_begin(self) \/ java_unlock_end(self) java_await_begin(self) == /\ pc[self] = "java_await_begin" /\ cq' = [cq EXCEPT ![wcid[self]] = Append(cq[wcid[self]],self)] /\ pc' = [pc EXCEPT ![self] = "java_await_unlocking"] /\ UNCHANGED << lq, pendingSignals, inPurgatory, waiting, lastSignal, stack, wcid, scid, cclwcid, cclscid >> java_await_unlocking(self) == /\ pc[self] = "java_await_unlocking" /\ lq' = Tail(lq) /\ pc' = [pc EXCEPT ![self] = "java_await_blocked"] /\ UNCHANGED << cq, pendingSignals, inPurgatory, waiting, lastSignal, stack, wcid, scid, cclwcid, cclscid >> java_await_blocked(self) == /\ pc[self] = "java_await_blocked" /\ Len(lq) > 0 /\ self = Head(lq) /\ pc' = [pc EXCEPT ![self] = "java_await_end"] /\ UNCHANGED << cq, lq, pendingSignals, inPurgatory, waiting, lastSignal, stack, wcid, scid, cclwcid, cclscid >> java_await_end(self) == /\ pc[self] = "java_await_end" /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc] /\ wcid' = [wcid EXCEPT ![self] = Head(stack[self]).wcid] /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])] /\ UNCHANGED << cq, lq, pendingSignals, inPurgatory, waiting, lastSignal, scid, cclwcid, cclscid >> java_await(self) == java_await_begin(self) \/ java_await_unlocking(self) \/ java_await_blocked(self) \/ java_await_end(self) java_signal_begin(self) == /\ pc[self] = "java_signal_begin" /\ IF Len(cq[scid[self]]) > 0 THEN /\ lq' = Append(lq,Head(cq[scid[self]])) /\ cq' = [cq EXCEPT ![scid[self]] = Tail(cq[scid[self]])] ELSE /\ TRUE /\ UNCHANGED << cq, lq >> /\ pc' = [pc EXCEPT ![self] = "java_signal_end"] /\ UNCHANGED << pendingSignals, inPurgatory, waiting, lastSignal, stack, wcid, scid, cclwcid, cclscid >> java_signal_end(self) == /\ pc[self] = "java_signal_end" /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc] /\ scid' = [scid EXCEPT ![self] = Head(stack[self]).scid] /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])] /\ UNCHANGED << cq, lq, pendingSignals, inPurgatory, waiting, lastSignal, wcid, cclwcid, cclscid >> java_signal(self) == java_signal_begin(self) \/ java_signal_end(self) cclib_enter_begin(self) == /\ pc[self] = "cclib_enter_begin" /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "java_lock", pc |-> "cclib_enter_check_priority" ] >> \o stack[self]] /\ pc' = [pc EXCEPT ![self] = "java_lock_begin"] /\ UNCHANGED << cq, lq, pendingSignals, inPurgatory, waiting, lastSignal, wcid, scid, cclwcid, cclscid >> cclib_enter_check_priority(self) == /\ pc[self] = "cclib_enter_check_priority" /\ IF pendingSignals > 0 \/ inPurgatory > 0 THEN /\ inPurgatory' = inPurgatory + 1 /\ /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "java_await", pc |-> "cclib_enter_toheaven", wcid |-> wcid[self] ] >> \o stack[self]] /\ wcid' = [wcid EXCEPT ![self] = 0] /\ pc' = [pc EXCEPT ![self] = "java_await_begin"] ELSE /\ pc' = [pc EXCEPT ![self] = "cclib_enter_end"] /\ UNCHANGED << inPurgatory, stack, wcid >> /\ UNCHANGED << cq, lq, pendingSignals, waiting, lastSignal, scid, cclwcid, cclscid >> cclib_enter_toheaven(self) == /\ pc[self] = "cclib_enter_toheaven" /\ inPurgatory' = inPurgatory - 1 /\ pc' = [pc EXCEPT ![self] = "cclib_enter_end"] /\ UNCHANGED << cq, lq, pendingSignals, waiting, lastSignal, stack, wcid, scid, cclwcid, cclscid >> cclib_enter_end(self) == /\ pc[self] = "cclib_enter_end" /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc] /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])] /\ UNCHANGED << cq, lq, pendingSignals, inPurgatory, waiting, lastSignal, wcid, scid, cclwcid, cclscid >> cclib_enter(self) == cclib_enter_begin(self) \/ cclib_enter_check_priority(self) \/ cclib_enter_toheaven(self) \/ cclib_enter_end(self) cclib_leave_begin(self) == /\ pc[self] = "cclib_leave_begin" /\ IF pendingSignals = 0 /\ inPurgatory > 0 THEN /\ /\ scid' = [scid EXCEPT ![self] = 0] /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "java_signal", pc |-> "cclib_leave_resetlastsignal", scid |-> scid[self] ] >> \o stack[self]] /\ pc' = [pc EXCEPT ![self] = "java_signal_begin"] ELSE /\ pc' = [pc EXCEPT ![self] = "cclib_leave_resetlastsignal"] /\ UNCHANGED << stack, scid >> /\ UNCHANGED << cq, lq, pendingSignals, inPurgatory, waiting, lastSignal, wcid, cclwcid, cclscid >> cclib_leave_resetlastsignal(self) == /\ pc[self] = "cclib_leave_resetlastsignal" /\ IF lastSignal[1] # self THEN /\ lastSignal' = <<0,0>> ELSE /\ TRUE /\ UNCHANGED lastSignal /\ pc' = [pc EXCEPT ![self] = "cclib_leave_unlocking"] /\ UNCHANGED << cq, lq, pendingSignals, inPurgatory, waiting, stack, wcid, scid, cclwcid, cclscid >> cclib_leave_unlocking(self) == /\ pc[self] = "cclib_leave_unlocking" /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "java_unlock", pc |-> "cclib_leave_end" ] >> \o stack[self]] /\ pc' = [pc EXCEPT ![self] = "java_unlock_begin"] /\ UNCHANGED << cq, lq, pendingSignals, inPurgatory, waiting, lastSignal, wcid, scid, cclwcid, cclscid >> cclib_leave_end(self) == /\ pc[self] = "cclib_leave_end" /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc] /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])] /\ UNCHANGED << cq, lq, pendingSignals, inPurgatory, waiting, lastSignal, wcid, scid, cclwcid, cclscid >> cclib_leave(self) == cclib_leave_begin(self) \/ cclib_leave_resetlastsignal(self) \/ cclib_leave_unlocking(self) \/ cclib_leave_end(self) cclib_await_begin(self) == /\ pc[self] = "cclib_await_begin" /\ waiting' = [waiting EXCEPT ![cclwcid[self]] = waiting[cclwcid[self]] + 1] /\ IF pendingSignals = 0 /\ inPurgatory > 0 THEN /\ /\ scid' = [scid EXCEPT ![self] = 0] /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "java_signal", pc |-> "cclib_await_actualawait", scid |-> scid[self] ] >> \o stack[self]] /\ pc' = [pc EXCEPT ![self] = "java_signal_begin"] ELSE /\ pc' = [pc EXCEPT ![self] = "cclib_await_actualawait"] /\ UNCHANGED << stack, scid >> /\ UNCHANGED << cq, lq, pendingSignals, inPurgatory, lastSignal, wcid, cclwcid, cclscid >> cclib_await_actualawait(self) == /\ pc[self] = "cclib_await_actualawait" /\ /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "java_await", pc |-> "cclib_await_reentering", wcid |-> wcid[self] ] >> \o stack[self]] /\ wcid' = [wcid EXCEPT ![self] = cclwcid[self]] /\ pc' = [pc EXCEPT ![self] = "java_await_begin"] /\ UNCHANGED << cq, lq, pendingSignals, inPurgatory, waiting, lastSignal, scid, cclwcid, cclscid >> cclib_await_reentering(self) == /\ pc[self] = "cclib_await_reentering" /\ pendingSignals' = pendingSignals - 1 /\ pc' = [pc EXCEPT ![self] = "cclib_await_end"] /\ UNCHANGED << cq, lq, inPurgatory, waiting, lastSignal, stack, wcid, scid, cclwcid, cclscid >> cclib_await_end(self) == /\ pc[self] = "cclib_await_end" /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc] /\ cclwcid' = [cclwcid EXCEPT ![self] = Head(stack[self]).cclwcid] /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])] /\ UNCHANGED << cq, lq, pendingSignals, inPurgatory, waiting, lastSignal, wcid, scid, cclscid >> cclib_await(self) == cclib_await_begin(self) \/ cclib_await_actualawait(self) \/ cclib_await_reentering(self) \/ cclib_await_end(self) cclib_signal_begin(self) == /\ pc[self] = "cclib_signal_begin" /\ IF waiting[cclscid[self]] > 0 THEN /\ pc' = [pc EXCEPT ![self] = "cclib_signal_actualsignal"] ELSE /\ pc' = [pc EXCEPT ![self] = "cclib_signal_end"] /\ UNCHANGED << cq, lq, pendingSignals, inPurgatory, waiting, lastSignal, stack, wcid, scid, cclwcid, cclscid >> cclib_signal_actualsignal(self) == /\ pc[self] = "cclib_signal_actualsignal" /\ pendingSignals' = pendingSignals + 1 /\ waiting' = [waiting EXCEPT ![cclscid[self]] = waiting[cclscid[self]] - 1] /\ pc' = [pc EXCEPT ![self] = "cclib_signal_setlastsignal"] /\ UNCHANGED << cq, lq, inPurgatory, lastSignal, stack, wcid, scid, cclwcid, cclscid >> cclib_signal_setlastsignal(self) == /\ pc[self] = "cclib_signal_setlastsignal" /\ lastSignal' = <> /\ /\ scid' = [scid EXCEPT ![self] = cclscid[self]] /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "java_signal", pc |-> "cclib_signal_end", scid |-> scid[self] ] >> \o stack[self]] /\ pc' = [pc EXCEPT ![self] = "java_signal_begin"] /\ UNCHANGED << cq, lq, pendingSignals, inPurgatory, waiting, wcid, cclwcid, cclscid >> cclib_signal_end(self) == /\ pc[self] = "cclib_signal_end" /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc] /\ cclscid' = [cclscid EXCEPT ![self] = Head(stack[self]).cclscid] /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])] /\ UNCHANGED << cq, lq, pendingSignals, inPurgatory, waiting, lastSignal, wcid, scid, cclwcid >> cclib_signal(self) == cclib_signal_begin(self) \/ cclib_signal_actualsignal(self) \/ cclib_signal_setlastsignal(self) \/ cclib_signal_end(self) locker_begin(self) == /\ pc[self] = "locker_begin" /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "cclib_enter", pc |-> "locker_in" ] >> \o stack[self]] /\ pc' = [pc EXCEPT ![self] = "cclib_enter_begin"] /\ UNCHANGED << cq, lq, pendingSignals, inPurgatory, waiting, lastSignal, wcid, scid, cclwcid, cclscid >> locker_in(self) == /\ pc[self] = "locker_in" /\ TRUE /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "cclib_leave", pc |-> "Done" ] >> \o stack[self]] /\ pc' = [pc EXCEPT ![self] = "cclib_leave_begin"] /\ UNCHANGED << cq, lq, pendingSignals, inPurgatory, waiting, lastSignal, wcid, scid, cclwcid, cclscid >> locker(self) == locker_begin(self) \/ locker_in(self) waiter_begin(self) == /\ pc[self] = "waiter_begin" /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "cclib_enter", pc |-> "waiter_before_await" ] >> \o stack[self]] /\ pc' = [pc EXCEPT ![self] = "cclib_enter_begin"] /\ UNCHANGED << cq, lq, pendingSignals, inPurgatory, waiting, lastSignal, wcid, scid, cclwcid, cclscid >> waiter_before_await(self) == /\ pc[self] = "waiter_before_await" /\ /\ cclwcid' = [cclwcid EXCEPT ![self] = 1 + ((self - Waiter_First_PId) % N_Conditions)] /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "cclib_await", pc |-> "waiter_after_await", cclwcid |-> cclwcid[self] ] >> \o stack[self]] /\ pc' = [pc EXCEPT ![self] = "cclib_await_begin"] /\ UNCHANGED << cq, lq, pendingSignals, inPurgatory, waiting, lastSignal, wcid, scid, cclscid >> waiter_after_await(self) == /\ pc[self] = "waiter_after_await" /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "cclib_leave", pc |-> "Done" ] >> \o stack[self]] /\ pc' = [pc EXCEPT ![self] = "cclib_leave_begin"] /\ UNCHANGED << cq, lq, pendingSignals, inPurgatory, waiting, lastSignal, wcid, scid, cclwcid, cclscid >> waiter(self) == waiter_begin(self) \/ waiter_before_await(self) \/ waiter_after_await(self) signaler_begin(self) == /\ pc[self] = "signaler_begin" /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "cclib_enter", pc |-> "signaler_before_signal" ] >> \o stack[self]] /\ pc' = [pc EXCEPT ![self] = "cclib_enter_begin"] /\ UNCHANGED << cq, lq, pendingSignals, inPurgatory, waiting, lastSignal, wcid, scid, cclwcid, cclscid >> signaler_before_signal(self) == /\ pc[self] = "signaler_before_signal" /\ /\ cclscid' = [cclscid EXCEPT ![self] = 1 + ((self - Signaler_First_PId) % N_Conditions)] /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "cclib_signal", pc |-> "signaler_after_signal", cclscid |-> cclscid[self] ] >> \o stack[self]] /\ pc' = [pc EXCEPT ![self] = "cclib_signal_begin"] /\ UNCHANGED << cq, lq, pendingSignals, inPurgatory, waiting, lastSignal, wcid, scid, cclwcid >> signaler_after_signal(self) == /\ pc[self] = "signaler_after_signal" /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "cclib_leave", pc |-> "Done" ] >> \o stack[self]] /\ pc' = [pc EXCEPT ![self] = "cclib_leave_begin"] /\ UNCHANGED << cq, lq, pendingSignals, inPurgatory, waiting, lastSignal, wcid, scid, cclwcid, cclscid >> signaler(self) == signaler_begin(self) \/ signaler_before_signal(self) \/ signaler_after_signal(self) Next == (\E self \in ProcSet: \/ java_lock(self) \/ java_unlock(self) \/ java_await(self) \/ java_signal(self) \/ cclib_enter(self) \/ cclib_leave(self) \/ cclib_await(self) \/ cclib_signal(self)) \/ (\E self \in Locker_PId: locker(self)) \/ (\E self \in Waiter_PId: waiter(self)) \/ (\E self \in Signaler_PId: signaler(self)) \/ (* Disjunct to prevent deadlock on termination *) ((\A self \in ProcSet: pc[self] = "Done") /\ UNCHANGED vars) Spec == /\ Init /\ [][Next]_vars /\ WF_vars(Next) Termination == <>(\A self \in ProcSet: pc[self] = "Done") \* END TRANSLATION ---- ---- \* Invariants and temporal properties (theorems) Types == (* Global variables *) /\ cq \in [CId -> Seq(ProcSet)] /\ lq \in Seq(ProcSet) /\ pendingSignals \in Nat /\ inPurgatory \in Nat /\ waiting \in [CId -> Nat] /\ lastSignal \in (ProcSet \union {0}) \X (ProcSet \union {0}) (* Procedure java_await *) /\ wcid \in [ProcSet -> CId \union {defaultInitValue}] (* Procedure java_signal *) /\ scid \in [ProcSet -> CId \union {defaultInitValue}] (* Procedure cclib_await *) /\ cclwcid \in [ProcSet -> CId \union {defaultInitValue}] (* Procedure cclib_signal *) /\ cclscid \in [ProcSet -> CId \union {defaultInitValue}] THEOREM TypePreservation == []Types ---- (* 1.- Characteristic property: La que hemos chequeado con UPPAAL, que si un "signaller" hace un signal sobre una condition no vacĂ­a, el siguiente thread en tomar acceso del monitor es el primer "waiter" de dicha condition, y no ninguno de los "lockers" que estaban en la cola del lock mutex. *) \* As an invariant with the instrumentation: CharacteristicAsInv == \/ lastSignal = <<0,0>> \/ (\A pid \in ProcSet : (\/ pc[pid] = "locker_in" \/ pc[pid] = "waiter_after_await" \/ pc[pid] = "signaler_after_signal") => (\/ lastSignal[1] = pid \/ lastSignal[2] = pid)) Signaling(from,cid,to) == /\ pc[from] = "cclib_signal_actualsignal" /\ cclscid[from] = cid /\ pc[to] = "java_await_blocked" /\ Head(cq[cid]) = to THEOREM CharacteristicThm == \A cid \in CId \ {0} : \A from \in Signaler_PId : \A to \in Waiter_PId : Signaling(from,cid,to) ~> TRUE ---- (* 2.- ToHeaven: Que se acaba saliendo del purgatorio, es decir, que todo "locker" que es enviado al purgatorio acaba terminando de ejecutar el enter(). *) InPurgatory(pid) == Member(cq[0],pid) LockedByLocker(pid) == pc[pid] = "locker_in" ToHeaven == \A pid \in Locker_PId : (InPurgatory(pid) ~> LockedByLocker(pid)) \* BY Auto THEOREM ToHeavenThm == InPurgatory(1) ~> LockedByLocker(1) <1>1. ASSUME InPurgatory(1) /\ [Next]_vars => (InPurgatory(1)' \/ LockedByLocker(1)'), InPurgatory(1) /\ <>_vars => LockedByLocker(1)', InPurgatory(1) => ENABLED <>_vars PROVE [][Next]_vars /\ WF_vars(Next) => (InPurgatory(1) ~> LockedByLocker(1)) BY RuleWF1 <1>. QED ---- (* 3.- OrderPreservation: among lockers *) ====