From b6b20d6755a457dbbda4220164f45fe3d68a6ea5 Mon Sep 17 00:00:00 2001 From: Federico Ponzi Date: Sat, 27 Jan 2024 13:01:49 +0000 Subject: [PATCH 1/3] Revert "Remove the spec to allow pr creation" This reverts commit 43a70ebc2bb751d8fcd0e3e978c0895964b1c291. --- logical-clocks-and-mutual-exclusion/README.md | 18 ++ .../lamport_clock.cfg | 18 ++ .../lamport_clock.tla | 302 ++++++++++++++++++ 3 files changed, 338 insertions(+) create mode 100644 logical-clocks-and-mutual-exclusion/README.md create mode 100644 logical-clocks-and-mutual-exclusion/lamport_clock.cfg create mode 100644 logical-clocks-and-mutual-exclusion/lamport_clock.tla diff --git a/logical-clocks-and-mutual-exclusion/README.md b/logical-clocks-and-mutual-exclusion/README.md new file mode 100644 index 0000000..41cf7e1 --- /dev/null +++ b/logical-clocks-and-mutual-exclusion/README.md @@ -0,0 +1,18 @@ +# Lamport clocks +Lamport clocks used to solve the mutual exclusion problem, as seen in Lamport's paper: [Time, Clocks, and the Ordering of Events in a Distributed System](https://lamport.azurewebsites.net/pubs/time-clocks.pdf). + +Mutual exclusion rules: +1. A process which has been granted the resource must release it before it can be granted to another process. +2. Different requests for the resource must be granted in the order in which they are made. +3. If every process which is granted the resource eventually releases it, then every request is eventually granted. + +Safety: + * Only a single process can access the resource at a time. Checked via assert. + +Liveness: + * All processes that requested access to the resource, eventually get it. + +As we're just trying to show a way to use lamport clocks to solve a synchronization problem, the algorithm presented in the paper above and modeled here doesn't deal with crashes. + +When the `ProcessCanFail` constant in the config to TRUE, the smallest process ("0") will never send an AckRequestResource back (akin to a crash). +This breaks the liveness property. diff --git a/logical-clocks-and-mutual-exclusion/lamport_clock.cfg b/logical-clocks-and-mutual-exclusion/lamport_clock.cfg new file mode 100644 index 0000000..3af88f9 --- /dev/null +++ b/logical-clocks-and-mutual-exclusion/lamport_clock.cfg @@ -0,0 +1,18 @@ +\* Add statements after this line. +SPECIFICATION Spec + +CONSTANTS + Processes = {0, 1} + ProcessCanFail = FALSE + MaxTimestamp = 15 + +INVARIANT + Inv + TypeOk + +PROPERTIES + ResourceAcquisition + +CHECK_DEADLOCK + FALSE \* needed due to MaxTimestamp + diff --git a/logical-clocks-and-mutual-exclusion/lamport_clock.tla b/logical-clocks-and-mutual-exclusion/lamport_clock.tla new file mode 100644 index 0000000..8dc0501 --- /dev/null +++ b/logical-clocks-and-mutual-exclusion/lamport_clock.tla @@ -0,0 +1,302 @@ +Lamport clocks: https://lamport.azurewebsites.net/pubs/time-clocks.pdf + +Mutual exclusion rules: +(I) A process which has been granted the resource must release it before it +can be granted to another process. +(II) Different requests for the resource must be granted in the order in which +they are made. +(III) If every process which is granted the resource eventually releases it, then every request is eventually granted. + +Safety: + * Only a single process can access the resource at a time. Checked via assert. +Liveness: + * All processes that requested access to the resource, eventually get it. + +As we're just trying to show a way to use lamport clocks to solve a synchronization problem, +the algorithm presented in the paper above and modeled here doesn't deal with crashes. +When the `ProcessCanFail` constant in the config to TRUE, the smallest process ("0") will never send an AckRequestResource back. +This breaks the liveness property. + +---- MODULE lamport_clock ---- +LOCAL INSTANCE Sequences +LOCAL INSTANCE Naturals +LOCAL INSTANCE FiniteSets +LOCAL INSTANCE Functions +LOCAL INSTANCE Folds +LOCAL INSTANCE TLC +LOCAL INSTANCE Integers + +CONSTANT Processes, ProcessCanFail, MaxTimestamp +ASSUME IsFiniteSet(Processes) +ASSUME \A p \in Processes : p \in Nat + +AckRequestResource == "AckRequestResource" +RequestResource == "RequestResource" +ReleaseResource == "ReleaseResource" +Commands == {RequestResource, AckRequestResource, ReleaseResource} +EmptyMailbox == <<"Empty">> + +(* --fair algorithm mutual_exclusion{ + + variables resource_owner = {}, + mailbox = [p \in Processes |-> EmptyMailbox]; + + define { + \* Some util definitions: + Max(x, y) == IF x > y THEN x ELSE y + Min(x, y) == IF x > y THEN y ELSE x + SetToSeq(S) == CHOOSE f \in [1..Cardinality(S) -> S] : IsInjective(f) + SetToSortSeq(S, op(_,_)) == SortSeq(SetToSeq(S), op) + SeqToSet(S) == {S[d]: d \in DOMAIN S} + + CanSendMessage(myself) == \A p \in Processes : mailbox[p] = EmptyMailbox + + \* Sort function for a RequestResource message with shape <> + SortFunction(seq1, seq2) == + IF seq1[3] > seq2[3] + THEN FALSE + ELSE IF seq1[3] < seq2[3] + THEN TRUE + ELSE IF seq1[2] > seq2[2] + THEN FALSE + ELSE IF seq1[2] < seq2[2] + THEN TRUE + ELSE FALSE + + TypeLamportTimestamp(t) == t \in Nat /\ t <= MaxTimestamp + + \* Has the shape: <<"EmptyMailbox"> | <> + TypeMailbox == \/ \A m \in DOMAIN mailbox : \/ mailbox[m] = EmptyMailbox + \/ /\ mailbox[m][1] \in Commands + /\ mailbox[m][2] \in Processes + /\ TypeLamportTimestamp(mailbox[m][3]) + TypeResourceOwner == \A ro \in resource_owner: ro \in Processes + + \* SAFETY: Only one process is allowed in the critical section + Inv == Cardinality(resource_owner) <= 1 + } + \* Used for the message sending event + macro BumpTimestamp() { + local_timestamp := Min(local_timestamp + 1, MaxTimestamp); + } + \* Used for the message reciving event. We need to take max of local_timestamp and other and bump the result. + macro BumpTimestampO(other) { + local_timestamp := Min(Max(local_timestamp, other) + 1, MaxTimestamp); + } + + fair process (p \in Processes) + variables local_timestamp = 0, + ack_request_resource = {}, + requests_queue = {}; + { + S: + while (TRUE) { + either { + \* send a request resource message + await /\ Cardinality(resource_owner) = 0 + /\ CanSendMessage(self) + /\ Cardinality(ack_request_resource) = 0; + BumpTimestamp(); + \* append to the local requests queue + requests_queue := requests_queue \union {<>}; + mailbox := [p \in Processes |-> IF p = self THEN EmptyMailbox ELSE <>]; + ack_request_resource := {<>}; + } or { + \* Handle a request resource message by 1. adding it to the local requests_queue and 2. sending a timestampated ack back + \* message being <> + await mailbox[self][1] = RequestResource; + \* Add it to the local requests queue + requests_queue := requests_queue \union {mailbox[self]}; + \* Bump the timestamp + BumpTimestampO(mailbox[self][3]); + \* Respond with an Ack. + + \* buffer has space only for a message at a time + \* so to send the ack back, we need to wait for the other process to free up their queue + await mailbox[mailbox[self][2]] = EmptyMailbox; + mailbox[mailbox[self][2]] := IF ProcessCanFail /\ \A proc \in Processes \ {self}: proc > self \* if process can fail and this is the smallest + THEN EmptyMailbox + ELSE <>; +EMPTY_MAILBOX: + \* handle of the message is completed, release the message queue + mailbox[self] := EmptyMailbox; + BumpTimestamp(); + } or { \* Handle a release resource message + \* When process Pj receives a Pi releases resource + \* message, it removes any Tm:P~ requests resource message + \* from its request queue. + await mailbox[self][1] = ReleaseResource; + requests_queue := {req \in requests_queue : req[2] # mailbox[self][2]}; + BumpTimestampO(mailbox[self][3]); + mailbox[self] := EmptyMailbox; + } or { \* Handle a Release Resource Ownership + \* To release the resource, process P~ removes any + \* Tm:Pi requests resource message from its request queue + \* and sends a (timestamped) Pi releases resource message + \* to every other process. + await self \in resource_owner /\ CanSendMessage(self); + \* If we're the resource owner it means we're at the top of the local queue, so it should work + requests_queue := SeqToSet(Tail(SetToSortSeq(requests_queue, SortFunction))); + BumpTimestamp(); + mailbox := [p \in Processes |-> IF p = self THEN EmptyMailbox ELSE <>]; + resource_owner := resource_owner \ {self}; + ack_request_resource := {}; + } or { \* take owenrship if possible + await /\ Cardinality(requests_queue) > 0 + /\ Head(SetToSortSeq(requests_queue, SortFunction))[2] = self + /\ Cardinality(ack_request_resource) = Cardinality(Processes) + \* doesn't make sense to take ownership again of this resource if we already own it + /\ self \notin resource_owner; + + resource_owner := resource_owner \union {self}; + } or { \* handle an AckRequestResource message + await mailbox[self][1] = AckRequestResource; + ack_request_resource := IF /\ \E el \in ack_request_resource : mailbox[self][3] > el[3] + /\ mailbox[self][2] \notin {m[2] : m \in ack_request_resource} + THEN ack_request_resource \union {mailbox[self]} + ELSE ack_request_resource; + BumpTimestampO(mailbox[self][3]); + mailbox[self] := EmptyMailbox; + } + } + } + +} + +*) +\* BEGIN TRANSLATION (chksum(pcal) = "7c28162a" /\ chksum(tla) = "4d664f9f") +VARIABLES resource_owner, mailbox, pc + +(* define statement *) +Max(x, y) == IF x > y THEN x ELSE y +Min(x, y) == IF x > y THEN y ELSE x +SetToSeq(S) == CHOOSE f \in [1..Cardinality(S) -> S] : IsInjective(f) +SetToSortSeq(S, op(_,_)) == SortSeq(SetToSeq(S), op) +SeqToSet(S) == {S[d]: d \in DOMAIN S} + +CanSendMessage(myself) == \A p \in Processes : mailbox[p] = EmptyMailbox + + +SortFunction(seq1, seq2) == + IF seq1[3] > seq2[3] + THEN FALSE + ELSE IF seq1[3] < seq2[3] + THEN TRUE + ELSE IF seq1[2] > seq2[2] + THEN FALSE + ELSE IF seq1[2] < seq2[2] + THEN TRUE + ELSE FALSE + +TypeLamportTimestamp(t) == t \in Nat /\ t <= MaxTimestamp + + +TypeMailbox == \/ \A m \in DOMAIN mailbox : \/ mailbox[m] = EmptyMailbox + \/ /\ mailbox[m][1] \in Commands + /\ mailbox[m][2] \in Processes + /\ TypeLamportTimestamp(mailbox[m][3]) +TypeResourceOwner == \A ro \in resource_owner: ro \in Processes + + +Inv == Cardinality(resource_owner) <= 1 + +VARIABLES local_timestamp, ack_request_resource, requests_queue + +vars == << resource_owner, mailbox, pc, local_timestamp, ack_request_resource, + requests_queue >> + +ProcSet == (Processes) + +Init == (* Global variables *) + /\ resource_owner = {} + /\ mailbox = [p \in Processes |-> EmptyMailbox] + (* Process p *) + /\ local_timestamp = [self \in Processes |-> 0] + /\ ack_request_resource = [self \in Processes |-> {}] + /\ requests_queue = [self \in Processes |-> {}] + /\ pc = [self \in ProcSet |-> "S"] + +S(self) == /\ pc[self] = "S" + /\ \/ /\ /\ Cardinality(resource_owner) = 0 + /\ CanSendMessage(self) + /\ Cardinality(ack_request_resource[self]) = 0 + /\ local_timestamp' = [local_timestamp EXCEPT ![self] = Min(local_timestamp[self] + 1, MaxTimestamp)] + /\ requests_queue' = [requests_queue EXCEPT ![self] = requests_queue[self] \union {<>}] + /\ mailbox' = [p \in Processes |-> IF p = self THEN EmptyMailbox ELSE <>] + /\ ack_request_resource' = [ack_request_resource EXCEPT ![self] = {<>}] + /\ pc' = [pc EXCEPT ![self] = "S"] + /\ UNCHANGED resource_owner + \/ /\ mailbox[self][1] = RequestResource + /\ requests_queue' = [requests_queue EXCEPT ![self] = requests_queue[self] \union {mailbox[self]}] + /\ local_timestamp' = [local_timestamp EXCEPT ![self] = Min(Max(local_timestamp[self], (mailbox[self][3])) + 1, MaxTimestamp)] + /\ mailbox[mailbox[self][2]] = EmptyMailbox + /\ mailbox' = [mailbox EXCEPT ![mailbox[self][2]] = IF ProcessCanFail /\ \A proc \in Processes \ {self}: proc > self + THEN EmptyMailbox + ELSE <>] + /\ pc' = [pc EXCEPT ![self] = "EMPTY_MAILBOX"] + /\ UNCHANGED <> + \/ /\ mailbox[self][1] = ReleaseResource + /\ requests_queue' = [requests_queue EXCEPT ![self] = {req \in requests_queue[self] : req[2] # mailbox[self][2]}] + /\ local_timestamp' = [local_timestamp EXCEPT ![self] = Min(Max(local_timestamp[self], (mailbox[self][3])) + 1, MaxTimestamp)] + /\ mailbox' = [mailbox EXCEPT ![self] = EmptyMailbox] + /\ pc' = [pc EXCEPT ![self] = "S"] + /\ UNCHANGED <> + \/ /\ self \in resource_owner /\ CanSendMessage(self) + /\ requests_queue' = [requests_queue EXCEPT ![self] = SeqToSet(Tail(SetToSortSeq(requests_queue[self], SortFunction)))] + /\ local_timestamp' = [local_timestamp EXCEPT ![self] = Min(local_timestamp[self] + 1, MaxTimestamp)] + /\ mailbox' = [p \in Processes |-> IF p = self THEN EmptyMailbox ELSE <>] + /\ resource_owner' = resource_owner \ {self} + /\ ack_request_resource' = [ack_request_resource EXCEPT ![self] = {}] + /\ pc' = [pc EXCEPT ![self] = "S"] + \/ /\ /\ Cardinality(requests_queue[self]) > 0 + /\ Head(SetToSortSeq(requests_queue[self], SortFunction))[2] = self + /\ Cardinality(ack_request_resource[self]) = Cardinality(Processes) + + /\ self \notin resource_owner + /\ resource_owner' = (resource_owner \union {self}) + /\ pc' = [pc EXCEPT ![self] = "S"] + /\ UNCHANGED <> + \/ /\ mailbox[self][1] = AckRequestResource + /\ ack_request_resource' = [ack_request_resource EXCEPT ![self] = IF /\ \E el \in ack_request_resource[self] : mailbox[self][3] > el[3] + /\ mailbox[self][2] \notin {m[2] : m \in ack_request_resource[self]} + THEN ack_request_resource[self] \union {mailbox[self]} + ELSE ack_request_resource[self]] + /\ local_timestamp' = [local_timestamp EXCEPT ![self] = Min(Max(local_timestamp[self], (mailbox[self][3])) + 1, MaxTimestamp)] + /\ mailbox' = [mailbox EXCEPT ![self] = EmptyMailbox] + /\ pc' = [pc EXCEPT ![self] = "S"] + /\ UNCHANGED <> + +EMPTY_MAILBOX(self) == /\ pc[self] = "EMPTY_MAILBOX" + /\ mailbox' = [mailbox EXCEPT ![self] = EmptyMailbox] + /\ local_timestamp' = [local_timestamp EXCEPT ![self] = Min(local_timestamp[self] + 1, MaxTimestamp)] + /\ pc' = [pc EXCEPT ![self] = "S"] + /\ UNCHANGED << resource_owner, ack_request_resource, + requests_queue >> + +p(self) == S(self) \/ EMPTY_MAILBOX(self) + +Next == (\E self \in Processes: p(self)) + +Spec == /\ Init /\ [][Next]_vars + /\ WF_vars(Next) + /\ \A self \in Processes : WF_vars(p(self)) + +\* END TRANSLATION + +TypeLocalTimestamp == \A proc \in Processes: /\ local_timestamp[proc] \in Nat + /\ local_timestamp[proc] <= MaxTimestamp + +TypeAckRequestResource == \A proc \in Processes: \A message \in ack_request_resource[proc]: /\ message[1] = AckRequestResource + /\ message[2] \in Processes + /\ TypeLamportTimestamp(message[3]) + +TypeOk == /\ TypeMailbox + /\ TypeResourceOwner + /\ TypeLocalTimestamp + /\ TypeAckRequestResource + +\* LIVENESS: either we eventually get ownership, or we're at the edge of the timestamp boundary. +ResourceAcquisition == \A proc \in Processes : Cardinality(ack_request_resource[proc]) > 0 ~> \/ proc \in resource_owner + \/ local_timestamp[proc] = MaxTimestamp + +==== From 48afda378f9d2c68db4fd3d4da7e76c47ccfda1f Mon Sep 17 00:00:00 2001 From: Federico Ponzi Date: Tue, 30 Jan 2024 23:14:31 +0000 Subject: [PATCH 2/3] Lamport clocks: docs, and use records instead of seq for messages --- .../lamport_clock.tla | 194 ++++++++++-------- 1 file changed, 103 insertions(+), 91 deletions(-) diff --git a/logical-clocks-and-mutual-exclusion/lamport_clock.tla b/logical-clocks-and-mutual-exclusion/lamport_clock.tla index 8dc0501..3fb625f 100644 --- a/logical-clocks-and-mutual-exclusion/lamport_clock.tla +++ b/logical-clocks-and-mutual-exclusion/lamport_clock.tla @@ -28,15 +28,19 @@ LOCAL INSTANCE Integers CONSTANT Processes, ProcessCanFail, MaxTimestamp ASSUME IsFiniteSet(Processes) +ASSUME Cardinality(Processes) > 1 ASSUME \A p \in Processes : p \in Nat +ASSUME MaxTimestamp \in Nat +ASSUME ProcessCanFail \in BOOLEAN AckRequestResource == "AckRequestResource" RequestResource == "RequestResource" ReleaseResource == "ReleaseResource" Commands == {RequestResource, AckRequestResource, ReleaseResource} -EmptyMailbox == <<"Empty">> +EmptyMailbox == [msg |-> "Empty"] +MessageType == [msg: Commands, proc: Processes, ts: Nat] \cup [msg: {"Empty"}] -(* --fair algorithm mutual_exclusion{ +(* --fair algorithm mutual_exclusion { variables resource_owner = {}, mailbox = [p \in Processes |-> EmptyMailbox]; @@ -53,23 +57,19 @@ EmptyMailbox == <<"Empty">> \* Sort function for a RequestResource message with shape <> SortFunction(seq1, seq2) == - IF seq1[3] > seq2[3] + IF seq1.ts > seq2.ts THEN FALSE - ELSE IF seq1[3] < seq2[3] + ELSE IF seq1.ts < seq2.ts THEN TRUE - ELSE IF seq1[2] > seq2[2] + ELSE IF seq1.proc > seq2.proc THEN FALSE - ELSE IF seq1[2] < seq2[2] + ELSE IF seq1.proc < seq2.proc THEN TRUE ELSE FALSE TypeLamportTimestamp(t) == t \in Nat /\ t <= MaxTimestamp - \* Has the shape: <<"EmptyMailbox"> | <> - TypeMailbox == \/ \A m \in DOMAIN mailbox : \/ mailbox[m] = EmptyMailbox - \/ /\ mailbox[m][1] \in Commands - /\ mailbox[m][2] \in Processes - /\ TypeLamportTimestamp(mailbox[m][3]) + TypeMailbox == \A m \in DOMAIN mailbox : mailbox[m] \in MessageType TypeResourceOwner == \A ro \in resource_owner: ro \in Processes \* SAFETY: Only one process is allowed in the critical section @@ -90,73 +90,90 @@ EmptyMailbox == <<"Empty">> requests_queue = {}; { S: - while (TRUE) { - either { - \* send a request resource message - await /\ Cardinality(resource_owner) = 0 - /\ CanSendMessage(self) - /\ Cardinality(ack_request_resource) = 0; + while (TRUE) { + either { + (********************* + 1. To request the resource, process Pi sends the message <> + to every other process, and puts that message on its own request queue, where Tm is the timestamp of the message. + **********************) + await /\ CanSendMessage(self) + /\ Cardinality(ack_request_resource) = 0; BumpTimestamp(); \* append to the local requests queue - requests_queue := requests_queue \union {<>}; - mailbox := [p \in Processes |-> IF p = self THEN EmptyMailbox ELSE <>]; - ack_request_resource := {<>}; + requests_queue := requests_queue \union {[ msg |-> RequestResource, proc |-> self, ts |-> local_timestamp]}; + mailbox := [p \in Processes |-> IF p = self THEN EmptyMailbox ELSE [ msg |-> RequestResource, proc |-> self, ts |-> local_timestamp]]; + ack_request_resource := {[ msg |-> AckRequestResource, proc |-> self, ts |-> local_timestamp]}; } or { - \* Handle a request resource message by 1. adding it to the local requests_queue and 2. sending a timestampated ack back - \* message being <> - await mailbox[self][1] = RequestResource; + (********************* + 2. When process Pj receives the message <> requests resource, + (i) it places it on its request queue and + (ii) sends a (timestamped) acknowledgment message to Pi. + **********************) + await mailbox[self].msg = RequestResource; \* Add it to the local requests queue requests_queue := requests_queue \union {mailbox[self]}; \* Bump the timestamp - BumpTimestampO(mailbox[self][3]); + BumpTimestampO(mailbox[self].ts); \* Respond with an Ack. \* buffer has space only for a message at a time \* so to send the ack back, we need to wait for the other process to free up their queue - await mailbox[mailbox[self][2]] = EmptyMailbox; - mailbox[mailbox[self][2]] := IF ProcessCanFail /\ \A proc \in Processes \ {self}: proc > self \* if process can fail and this is the smallest - THEN EmptyMailbox - ELSE <>; + await mailbox[mailbox[self].proc] = EmptyMailbox; + mailbox[mailbox[self].proc] := IF ProcessCanFail /\ \A proc \in Processes \ {self}: proc > self \* if process can fail and this is the smallest + THEN EmptyMailbox + ELSE [ msg |-> AckRequestResource, proc |-> self, ts |-> local_timestamp]; EMPTY_MAILBOX: - \* handle of the message is completed, release the message queue + \* handling of the message is completed, release the message queue mailbox[self] := EmptyMailbox; BumpTimestamp(); - } or { \* Handle a release resource message - \* When process Pj receives a Pi releases resource - \* message, it removes any Tm:P~ requests resource message - \* from its request queue. - await mailbox[self][1] = ReleaseResource; - requests_queue := {req \in requests_queue : req[2] # mailbox[self][2]}; - BumpTimestampO(mailbox[self][3]); + } or { + (********************* + 3. Whenever Pi receives the AckRequestResource, it appends it to its local acknowledgments set. + **********************) + await mailbox[self].msg = AckRequestResource; + ack_request_resource := IF /\ \E el \in ack_request_resource : mailbox[self].ts > el.ts + /\ mailbox[self].proc \notin {m.proc : m \in ack_request_resource} + THEN ack_request_resource \union {mailbox[self]} + ELSE ack_request_resource; + \*ack_request_resource := ack_request_resource \union {mailbox[self]}; + BumpTimestampO(mailbox[self].ts); mailbox[self] := EmptyMailbox; - } or { \* Handle a Release Resource Ownership - \* To release the resource, process P~ removes any - \* Tm:Pi requests resource message from its request queue - \* and sends a (timestamped) Pi releases resource message - \* to every other process. + } or { + (********************* + 4. To release the resource, process Pi removes any <> message from its request + queue and sends a timestamped Pi, ReleaseResource message to every other process. + **********************) + await mailbox[self].msg = ReleaseResource; + requests_queue := {req \in requests_queue : req.proc # mailbox[self].proc}; + BumpTimestampO(mailbox[self].ts); + mailbox[self] := EmptyMailbox; + } or { + (********************* + 5. When process Pj receives a Pi ReleaseResource message, it removes any <> + requests resource message from its request queue. + **********************) await self \in resource_owner /\ CanSendMessage(self); - \* If we're the resource owner it means we're at the top of the local queue, so it should work + \* If there is a resource owner, its request has to be at the top of the local queue, so this is safe requests_queue := SeqToSet(Tail(SetToSortSeq(requests_queue, SortFunction))); BumpTimestamp(); - mailbox := [p \in Processes |-> IF p = self THEN EmptyMailbox ELSE <>]; + mailbox := [p \in Processes |-> IF p = self THEN EmptyMailbox ELSE [ msg |-> ReleaseResource, proc |-> self, ts |-> local_timestamp]]; resource_owner := resource_owner \ {self}; ack_request_resource := {}; - } or { \* take owenrship if possible + } or { + (********************* + 6. Process Pi is granted the resource when the following two conditions are satisfied: + (i) There is a <> in its request queue which is ordered before any other + request in its queue by the relation ⇒. (To define the relation " ⇒ " for messages, we identify a message + with the event of sending it.). + (ii) Pi has received a message from every other process timestamped later than Tm. + **********************) await /\ Cardinality(requests_queue) > 0 - /\ Head(SetToSortSeq(requests_queue, SortFunction))[2] = self + /\ Head(SetToSortSeq(requests_queue, SortFunction)).proc = self /\ Cardinality(ack_request_resource) = Cardinality(Processes) \* doesn't make sense to take ownership again of this resource if we already own it /\ self \notin resource_owner; resource_owner := resource_owner \union {self}; - } or { \* handle an AckRequestResource message - await mailbox[self][1] = AckRequestResource; - ack_request_resource := IF /\ \E el \in ack_request_resource : mailbox[self][3] > el[3] - /\ mailbox[self][2] \notin {m[2] : m \in ack_request_resource} - THEN ack_request_resource \union {mailbox[self]} - ELSE ack_request_resource; - BumpTimestampO(mailbox[self][3]); - mailbox[self] := EmptyMailbox; } } } @@ -164,7 +181,7 @@ EMPTY_MAILBOX: } *) -\* BEGIN TRANSLATION (chksum(pcal) = "7c28162a" /\ chksum(tla) = "4d664f9f") +\* BEGIN TRANSLATION (chksum(pcal) = "7c28162a" /\ chksum(tla) = "5aee13df") VARIABLES resource_owner, mailbox, pc (* define statement *) @@ -178,23 +195,19 @@ CanSendMessage(myself) == \A p \in Processes : mailbox[p] = EmptyMailbox SortFunction(seq1, seq2) == - IF seq1[3] > seq2[3] + IF seq1.ts > seq2.ts THEN FALSE - ELSE IF seq1[3] < seq2[3] + ELSE IF seq1.ts < seq2.ts THEN TRUE - ELSE IF seq1[2] > seq2[2] + ELSE IF seq1.proc > seq2.proc THEN FALSE - ELSE IF seq1[2] < seq2[2] + ELSE IF seq1.proc < seq2.proc THEN TRUE ELSE FALSE TypeLamportTimestamp(t) == t \in Nat /\ t <= MaxTimestamp - -TypeMailbox == \/ \A m \in DOMAIN mailbox : \/ mailbox[m] = EmptyMailbox - \/ /\ mailbox[m][1] \in Commands - /\ mailbox[m][2] \in Processes - /\ TypeLamportTimestamp(mailbox[m][3]) +TypeMailbox == \A m \in DOMAIN mailbox : mailbox[m] \in MessageType TypeResourceOwner == \A ro \in resource_owner: ro \in Processes @@ -217,54 +230,53 @@ Init == (* Global variables *) /\ pc = [self \in ProcSet |-> "S"] S(self) == /\ pc[self] = "S" - /\ \/ /\ /\ Cardinality(resource_owner) = 0 - /\ CanSendMessage(self) + /\ \/ /\ /\ CanSendMessage(self) /\ Cardinality(ack_request_resource[self]) = 0 /\ local_timestamp' = [local_timestamp EXCEPT ![self] = Min(local_timestamp[self] + 1, MaxTimestamp)] - /\ requests_queue' = [requests_queue EXCEPT ![self] = requests_queue[self] \union {<>}] - /\ mailbox' = [p \in Processes |-> IF p = self THEN EmptyMailbox ELSE <>] - /\ ack_request_resource' = [ack_request_resource EXCEPT ![self] = {<>}] + /\ requests_queue' = [requests_queue EXCEPT ![self] = requests_queue[self] \union {[ msg |-> RequestResource, proc |-> self, ts |-> local_timestamp'[self]]}] + /\ mailbox' = [p \in Processes |-> IF p = self THEN EmptyMailbox ELSE [ msg |-> RequestResource, proc |-> self, ts |-> local_timestamp'[self]]] + /\ ack_request_resource' = [ack_request_resource EXCEPT ![self] = {[ msg |-> AckRequestResource, proc |-> self, ts |-> local_timestamp'[self]]}] /\ pc' = [pc EXCEPT ![self] = "S"] /\ UNCHANGED resource_owner - \/ /\ mailbox[self][1] = RequestResource + \/ /\ mailbox[self].msg = RequestResource /\ requests_queue' = [requests_queue EXCEPT ![self] = requests_queue[self] \union {mailbox[self]}] - /\ local_timestamp' = [local_timestamp EXCEPT ![self] = Min(Max(local_timestamp[self], (mailbox[self][3])) + 1, MaxTimestamp)] - /\ mailbox[mailbox[self][2]] = EmptyMailbox - /\ mailbox' = [mailbox EXCEPT ![mailbox[self][2]] = IF ProcessCanFail /\ \A proc \in Processes \ {self}: proc > self - THEN EmptyMailbox - ELSE <>] + /\ local_timestamp' = [local_timestamp EXCEPT ![self] = Min(Max(local_timestamp[self], (mailbox[self].ts)) + 1, MaxTimestamp)] + /\ mailbox[mailbox[self].proc] = EmptyMailbox + /\ mailbox' = [mailbox EXCEPT ![mailbox[self].proc] = IF ProcessCanFail /\ \A proc \in Processes \ {self}: proc > self + THEN EmptyMailbox + ELSE [ msg |-> AckRequestResource, proc |-> self, ts |-> local_timestamp'[self]]] /\ pc' = [pc EXCEPT ![self] = "EMPTY_MAILBOX"] /\ UNCHANGED <> - \/ /\ mailbox[self][1] = ReleaseResource - /\ requests_queue' = [requests_queue EXCEPT ![self] = {req \in requests_queue[self] : req[2] # mailbox[self][2]}] - /\ local_timestamp' = [local_timestamp EXCEPT ![self] = Min(Max(local_timestamp[self], (mailbox[self][3])) + 1, MaxTimestamp)] + \/ /\ mailbox[self].msg = AckRequestResource + /\ ack_request_resource' = [ack_request_resource EXCEPT ![self] = IF /\ \E el \in ack_request_resource[self] : mailbox[self].ts > el.ts + /\ mailbox[self].proc \notin {m.proc : m \in ack_request_resource[self]} + THEN ack_request_resource[self] \union {mailbox[self]} + ELSE ack_request_resource[self]] + /\ local_timestamp' = [local_timestamp EXCEPT ![self] = Min(Max(local_timestamp[self], (mailbox[self].ts)) + 1, MaxTimestamp)] + /\ mailbox' = [mailbox EXCEPT ![self] = EmptyMailbox] + /\ pc' = [pc EXCEPT ![self] = "S"] + /\ UNCHANGED <> + \/ /\ mailbox[self].msg = ReleaseResource + /\ requests_queue' = [requests_queue EXCEPT ![self] = {req \in requests_queue[self] : req.proc # mailbox[self].proc}] + /\ local_timestamp' = [local_timestamp EXCEPT ![self] = Min(Max(local_timestamp[self], (mailbox[self].ts)) + 1, MaxTimestamp)] /\ mailbox' = [mailbox EXCEPT ![self] = EmptyMailbox] /\ pc' = [pc EXCEPT ![self] = "S"] /\ UNCHANGED <> \/ /\ self \in resource_owner /\ CanSendMessage(self) /\ requests_queue' = [requests_queue EXCEPT ![self] = SeqToSet(Tail(SetToSortSeq(requests_queue[self], SortFunction)))] /\ local_timestamp' = [local_timestamp EXCEPT ![self] = Min(local_timestamp[self] + 1, MaxTimestamp)] - /\ mailbox' = [p \in Processes |-> IF p = self THEN EmptyMailbox ELSE <>] + /\ mailbox' = [p \in Processes |-> IF p = self THEN EmptyMailbox ELSE [ msg |-> ReleaseResource, proc |-> self, ts |-> local_timestamp'[self]]] /\ resource_owner' = resource_owner \ {self} /\ ack_request_resource' = [ack_request_resource EXCEPT ![self] = {}] /\ pc' = [pc EXCEPT ![self] = "S"] \/ /\ /\ Cardinality(requests_queue[self]) > 0 - /\ Head(SetToSortSeq(requests_queue[self], SortFunction))[2] = self + /\ Head(SetToSortSeq(requests_queue[self], SortFunction)).proc = self /\ Cardinality(ack_request_resource[self]) = Cardinality(Processes) /\ self \notin resource_owner /\ resource_owner' = (resource_owner \union {self}) /\ pc' = [pc EXCEPT ![self] = "S"] /\ UNCHANGED <> - \/ /\ mailbox[self][1] = AckRequestResource - /\ ack_request_resource' = [ack_request_resource EXCEPT ![self] = IF /\ \E el \in ack_request_resource[self] : mailbox[self][3] > el[3] - /\ mailbox[self][2] \notin {m[2] : m \in ack_request_resource[self]} - THEN ack_request_resource[self] \union {mailbox[self]} - ELSE ack_request_resource[self]] - /\ local_timestamp' = [local_timestamp EXCEPT ![self] = Min(Max(local_timestamp[self], (mailbox[self][3])) + 1, MaxTimestamp)] - /\ mailbox' = [mailbox EXCEPT ![self] = EmptyMailbox] - /\ pc' = [pc EXCEPT ![self] = "S"] - /\ UNCHANGED <> EMPTY_MAILBOX(self) == /\ pc[self] = "EMPTY_MAILBOX" /\ mailbox' = [mailbox EXCEPT ![self] = EmptyMailbox] @@ -286,9 +298,9 @@ Spec == /\ Init /\ [][Next]_vars TypeLocalTimestamp == \A proc \in Processes: /\ local_timestamp[proc] \in Nat /\ local_timestamp[proc] <= MaxTimestamp -TypeAckRequestResource == \A proc \in Processes: \A message \in ack_request_resource[proc]: /\ message[1] = AckRequestResource - /\ message[2] \in Processes - /\ TypeLamportTimestamp(message[3]) +TypeAckRequestResource == \A proc \in Processes: \A message \in ack_request_resource[proc]: /\ message.msg = AckRequestResource + /\ message.proc \in Processes + /\ TypeLamportTimestamp(message.ts) TypeOk == /\ TypeMailbox /\ TypeResourceOwner From 1ab638bdad6b993e1691f9c94df4b7791f2f93d0 Mon Sep 17 00:00:00 2001 From: Federico Ponzi Date: Tue, 30 Jan 2024 23:44:14 +0000 Subject: [PATCH 3/3] Lamport clocks: uses state constraints instead of constant to keep the model bounded --- .../lamport_clock.cfg | 7 +-- .../lamport_clock.tla | 44 +++++++++---------- 2 files changed, 24 insertions(+), 27 deletions(-) diff --git a/logical-clocks-and-mutual-exclusion/lamport_clock.cfg b/logical-clocks-and-mutual-exclusion/lamport_clock.cfg index 3af88f9..e420ab0 100644 --- a/logical-clocks-and-mutual-exclusion/lamport_clock.cfg +++ b/logical-clocks-and-mutual-exclusion/lamport_clock.cfg @@ -3,9 +3,8 @@ SPECIFICATION Spec CONSTANTS Processes = {0, 1} - ProcessCanFail = FALSE + ProcessCanFail = TRUE MaxTimestamp = 15 - INVARIANT Inv TypeOk @@ -14,5 +13,7 @@ PROPERTIES ResourceAcquisition CHECK_DEADLOCK - FALSE \* needed due to MaxTimestamp + FALSE +CONSTRAINTS + MaxtimestampConstraint diff --git a/logical-clocks-and-mutual-exclusion/lamport_clock.tla b/logical-clocks-and-mutual-exclusion/lamport_clock.tla index 3fb625f..19bb54f 100644 --- a/logical-clocks-and-mutual-exclusion/lamport_clock.tla +++ b/logical-clocks-and-mutual-exclusion/lamport_clock.tla @@ -30,8 +30,8 @@ CONSTANT Processes, ProcessCanFail, MaxTimestamp ASSUME IsFiniteSet(Processes) ASSUME Cardinality(Processes) > 1 ASSUME \A p \in Processes : p \in Nat -ASSUME MaxTimestamp \in Nat ASSUME ProcessCanFail \in BOOLEAN +ASSUME MaxTimestamp \in Nat AckRequestResource == "AckRequestResource" RequestResource == "RequestResource" @@ -66,22 +66,17 @@ MessageType == [msg: Commands, proc: Processes, ts: Nat] \cup [msg: {"Empty"}] ELSE IF seq1.proc < seq2.proc THEN TRUE ELSE FALSE - - TypeLamportTimestamp(t) == t \in Nat /\ t <= MaxTimestamp - - TypeMailbox == \A m \in DOMAIN mailbox : mailbox[m] \in MessageType - TypeResourceOwner == \A ro \in resource_owner: ro \in Processes \* SAFETY: Only one process is allowed in the critical section Inv == Cardinality(resource_owner) <= 1 } \* Used for the message sending event macro BumpTimestamp() { - local_timestamp := Min(local_timestamp + 1, MaxTimestamp); + local_timestamp := local_timestamp + 1; } \* Used for the message reciving event. We need to take max of local_timestamp and other and bump the result. macro BumpTimestampO(other) { - local_timestamp := Min(Max(local_timestamp, other) + 1, MaxTimestamp); + local_timestamp := Max(local_timestamp, other) + 1; } fair process (p \in Processes) @@ -181,7 +176,7 @@ EMPTY_MAILBOX: } *) -\* BEGIN TRANSLATION (chksum(pcal) = "7c28162a" /\ chksum(tla) = "5aee13df") +\* BEGIN TRANSLATION (chksum(pcal) = "7c28162a" /\ chksum(tla) = "f8a792b1") VARIABLES resource_owner, mailbox, pc (* define statement *) @@ -205,11 +200,6 @@ SortFunction(seq1, seq2) == THEN TRUE ELSE FALSE -TypeLamportTimestamp(t) == t \in Nat /\ t <= MaxTimestamp - -TypeMailbox == \A m \in DOMAIN mailbox : mailbox[m] \in MessageType -TypeResourceOwner == \A ro \in resource_owner: ro \in Processes - Inv == Cardinality(resource_owner) <= 1 @@ -232,7 +222,7 @@ Init == (* Global variables *) S(self) == /\ pc[self] = "S" /\ \/ /\ /\ CanSendMessage(self) /\ Cardinality(ack_request_resource[self]) = 0 - /\ local_timestamp' = [local_timestamp EXCEPT ![self] = Min(local_timestamp[self] + 1, MaxTimestamp)] + /\ local_timestamp' = [local_timestamp EXCEPT ![self] = local_timestamp[self] + 1] /\ requests_queue' = [requests_queue EXCEPT ![self] = requests_queue[self] \union {[ msg |-> RequestResource, proc |-> self, ts |-> local_timestamp'[self]]}] /\ mailbox' = [p \in Processes |-> IF p = self THEN EmptyMailbox ELSE [ msg |-> RequestResource, proc |-> self, ts |-> local_timestamp'[self]]] /\ ack_request_resource' = [ack_request_resource EXCEPT ![self] = {[ msg |-> AckRequestResource, proc |-> self, ts |-> local_timestamp'[self]]}] @@ -240,7 +230,7 @@ S(self) == /\ pc[self] = "S" /\ UNCHANGED resource_owner \/ /\ mailbox[self].msg = RequestResource /\ requests_queue' = [requests_queue EXCEPT ![self] = requests_queue[self] \union {mailbox[self]}] - /\ local_timestamp' = [local_timestamp EXCEPT ![self] = Min(Max(local_timestamp[self], (mailbox[self].ts)) + 1, MaxTimestamp)] + /\ local_timestamp' = [local_timestamp EXCEPT ![self] = Max(local_timestamp[self], (mailbox[self].ts)) + 1] /\ mailbox[mailbox[self].proc] = EmptyMailbox /\ mailbox' = [mailbox EXCEPT ![mailbox[self].proc] = IF ProcessCanFail /\ \A proc \in Processes \ {self}: proc > self THEN EmptyMailbox @@ -248,23 +238,23 @@ S(self) == /\ pc[self] = "S" /\ pc' = [pc EXCEPT ![self] = "EMPTY_MAILBOX"] /\ UNCHANGED <> \/ /\ mailbox[self].msg = AckRequestResource - /\ ack_request_resource' = [ack_request_resource EXCEPT ![self] = IF /\ \E el \in ack_request_resource[self] : mailbox[self].ts > el.ts - /\ mailbox[self].proc \notin {m.proc : m \in ack_request_resource[self]} + /\ ack_request_resource' = [ack_request_resource EXCEPT ![self] = IF /\ \E el \in ack_request_resource[self] : mailbox[self].ts > el.ts + /\ mailbox[self].proc \notin {m.proc : m \in ack_request_resource[self]} THEN ack_request_resource[self] \union {mailbox[self]} ELSE ack_request_resource[self]] - /\ local_timestamp' = [local_timestamp EXCEPT ![self] = Min(Max(local_timestamp[self], (mailbox[self].ts)) + 1, MaxTimestamp)] + /\ local_timestamp' = [local_timestamp EXCEPT ![self] = Max(local_timestamp[self], (mailbox[self].ts)) + 1] /\ mailbox' = [mailbox EXCEPT ![self] = EmptyMailbox] /\ pc' = [pc EXCEPT ![self] = "S"] /\ UNCHANGED <> \/ /\ mailbox[self].msg = ReleaseResource /\ requests_queue' = [requests_queue EXCEPT ![self] = {req \in requests_queue[self] : req.proc # mailbox[self].proc}] - /\ local_timestamp' = [local_timestamp EXCEPT ![self] = Min(Max(local_timestamp[self], (mailbox[self].ts)) + 1, MaxTimestamp)] + /\ local_timestamp' = [local_timestamp EXCEPT ![self] = Max(local_timestamp[self], (mailbox[self].ts)) + 1] /\ mailbox' = [mailbox EXCEPT ![self] = EmptyMailbox] /\ pc' = [pc EXCEPT ![self] = "S"] /\ UNCHANGED <> \/ /\ self \in resource_owner /\ CanSendMessage(self) /\ requests_queue' = [requests_queue EXCEPT ![self] = SeqToSet(Tail(SetToSortSeq(requests_queue[self], SortFunction)))] - /\ local_timestamp' = [local_timestamp EXCEPT ![self] = Min(local_timestamp[self] + 1, MaxTimestamp)] + /\ local_timestamp' = [local_timestamp EXCEPT ![self] = local_timestamp[self] + 1] /\ mailbox' = [p \in Processes |-> IF p = self THEN EmptyMailbox ELSE [ msg |-> ReleaseResource, proc |-> self, ts |-> local_timestamp'[self]]] /\ resource_owner' = resource_owner \ {self} /\ ack_request_resource' = [ack_request_resource EXCEPT ![self] = {}] @@ -280,7 +270,7 @@ S(self) == /\ pc[self] = "S" EMPTY_MAILBOX(self) == /\ pc[self] = "EMPTY_MAILBOX" /\ mailbox' = [mailbox EXCEPT ![self] = EmptyMailbox] - /\ local_timestamp' = [local_timestamp EXCEPT ![self] = Min(local_timestamp[self] + 1, MaxTimestamp)] + /\ local_timestamp' = [local_timestamp EXCEPT ![self] = local_timestamp[self] + 1] /\ pc' = [pc EXCEPT ![self] = "S"] /\ UNCHANGED << resource_owner, ack_request_resource, requests_queue >> @@ -295,8 +285,12 @@ Spec == /\ Init /\ [][Next]_vars \* END TRANSLATION -TypeLocalTimestamp == \A proc \in Processes: /\ local_timestamp[proc] \in Nat - /\ local_timestamp[proc] <= MaxTimestamp +TypeLamportTimestamp(t) == t \in Nat + +TypeMailbox == \A m \in DOMAIN mailbox : mailbox[m] \in MessageType +TypeResourceOwner == \A ro \in resource_owner: ro \in Processes + +TypeLocalTimestamp == \A proc \in Processes: TypeLamportTimestamp(local_timestamp[proc]) TypeAckRequestResource == \A proc \in Processes: \A message \in ack_request_resource[proc]: /\ message.msg = AckRequestResource /\ message.proc \in Processes @@ -306,6 +300,8 @@ TypeOk == /\ TypeMailbox /\ TypeResourceOwner /\ TypeLocalTimestamp /\ TypeAckRequestResource +\* State constraint to keep the model bounded +MaxtimestampConstraint == \A proc \in Processes: local_timestamp[proc] < MaxTimestamp \* LIVENESS: either we eventually get ownership, or we're at the edge of the timestamp boundary. ResourceAcquisition == \A proc \in Processes : Cardinality(ack_request_resource[proc]) > 0 ~> \/ proc \in resource_owner