Skip to content

Commit

Permalink
Lamport clocks: uses state constraints instead of constant to keep th…
Browse files Browse the repository at this point in the history 
…e model bounded
  • Loading branch information
@FedericoPonzi
FedericoPonzi committed Jan 30, 2024
1 parent 48afda3 commit 1ab638b
Show file tree
Hide file tree
Showing 2 changed files with 24 additions and 27 deletions.
7 changes: 4 additions & 3 deletions logical-clocks-and-mutual-exclusion/lamport_clock.cfg
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,9 +3,8 @@ SPECIFICATION Spec

CONSTANTS
Processes = {0, 1}
ProcessCanFail = FALSE
ProcessCanFail = TRUE
MaxTimestamp = 15

INVARIANT
Inv
TypeOk
Expand All @@ -14,5 +13,7 @@ PROPERTIES
ResourceAcquisition

CHECK_DEADLOCK
FALSE \* needed due to MaxTimestamp
FALSE

CONSTRAINTS
MaxtimestampConstraint
44 changes: 20 additions & 24 deletions logical-clocks-and-mutual-exclusion/lamport_clock.tla
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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 *)
Expand All @@ -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

Expand All @@ -232,39 +222,39 @@ 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]]}]
/\ pc' = [pc EXCEPT ![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
ELSE [ msg |-> AckRequestResource, proc |-> self, ts |-> local_timestamp'[self]]]
/\ pc' = [pc EXCEPT ![self] = "EMPTY_MAILBOX"]
/\ UNCHANGED <<resource_owner, ack_request_resource>>
\/ /\ 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 <<resource_owner, requests_queue>>
\/ /\ 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 <<resource_owner, ack_request_resource>>
\/ /\ 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] = {}]
Expand All @@ -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 >>
Expand All @@ -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
Expand All @@ -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
Expand Down

0 comments on commit 1ab638b

Please sign in to comment.