A High-Level Language for Modeling Algorithms and Their Properties - Formal Methods: Foundations and Applications - page 54

begin (* process Site *)

1

loop

2

ncrit : skip ;

3

try : network := broadcast(self, [kind → “request”, clk → clock]);

4

acks := {} ;

5

+enter : when Len(reqQ) > 0 ∧ Head(reqQ.proc) = self ∧ acks = Sites;

6

+crit : skip ;

7

+exit : network := broadcast(self, [kind → “free”]);

8

end loop ;

9

end process (* Site *)

10

end algorithm

11

12
13

invariant ∀ s, t ∈ Site : Site[s]@crit ∧ Site[t]@crit ⇒ s=t

invariant

14

∧ (* each queue holds at most one request per site *)

15

∀ s ∈ Site : ∀ i ∈ 1 .. Len(reqQ[s]) : ∀ j ∈ i+1 .. Len(reqQ[s]) :

16

reqQ[s][j].site = reqQ[s][i].site

17

∧ (* requests stay in queue until ''free'' message received *)

18

∀ s, t ∈ Site :

19

( ∃ i ∈ 1 .. Len(network[s][t]) : network[s][t][i].kind = “free”)

20

⇒∃ j ∈ 1 .. Len(reqQ[t]) : reqQ[t][j].site = s

21

∧ (* site is in critical section only if at the head of every request queue *)

22

∀ s ∈ Site : Site[s]@crit ⇒∀ t ∈ Site : Head(reqQ[t]).site = s

23

temporal ∀ s ∈ Site : Site[s]@enter Site[s]@crit

24

25
26

(* Finite instance for model checking *)

constants N = 3, maxclock = 5

27

constraint ∀ s ∈ Site : Site[s].clock ≤ maxClock

28

Fig. 2. Lamport's mutual-exclusion algorithm (part 2)

its own request (if any). Elements of the request queue are records with fields
site and clock indicating the requesting site and the timestamp of the request.
The definitions beats , insertRequest ,and removeRequest formalize the priorities
between two requests and the insertion and removal of a request in the priority
queue.
The code of a process is given in the code section between the keywords begin
and end process . We describe the statements of PlusCal in more detail in
Section 3.2.
The process section is optionally followed by a code section for the main
algorithm, which executes in parallel to the processes. No such code section is
required for algorithm LamportMutex .
The description of the algorithm itself is followed by the property and instance
sections, which state the properties (invariants and general temporal logic prop-
erties) to be verified. For our example, we state two invariants and one temporal
(liveness) property. The first invariant expresses mutual exclusion between all
sites by asserting that no two sites are simultaneously at label crit . The second
invariant states further safety properties of the algorithm that give more insight
in its functioning. The temporal property asserts that whenever some site s is