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

algorithm LamportMutex

1

extends Naturals, Sequences (* standard modules *)

2

constants N, maxClock

3

4
5 variable network = [from ∈ Site → [to ∈ Site → ]]

definition send(from, to, msg) = 6

[network EXCEPT ![from][to] = Append(@, msg)] 7

definition broadcast(from, msg) = 8

[network EXCEPT ![from] = [to ∈ Site → Append(network[from][to], msg)]] 9

10
11

process Site[N]

variables

12

clock = 1, (* logical clock of this site *)

13

reqQ = , (* queue of pending requests, ordered by clock values *)

14

acks = {} (* set of acknowledgements received for own request *)

15

definition beats(rq1, rq2) =

16

∨ rq1.clk < rq2.clk

17

∨ rq1.clk = rq2.clk ∧ rq1.site < rq2.site

18

definition insertRequest(from, c) =

19

LET entry = [site

→ from, clk → c]

20

len = Len(reqQ)

21

pos = CHOOSE i ∈ 1 .. len+1 :

22

∧∀ j ∈ 1 .. i-1 : beats(reqQ[j], entry)

23

∧ i = len+1 ∨ beats(entry, reqQ[i])

24

IN SubSeq(reqQ, 1, pos-1)

◦ entry ◦ SubSeq(reqQ, pos, len)

25

definition removeRequest(from) =

26

LET len = Len(reqQ)

27

pos = CHOOSE i

∈ 1 .. len : reqQ[i].site = from

28

IN SubSeq(reqQ, 1, pos-1)

◦ SubSeq(reqQ, pos+1, len)

29

definition max(x,y) = IF x

< y THEN y ELSE x

30

31
32

fair process Communicator[1]

begin

33

loop

34

rcv : with from ∈{ s ∈ Site : Len(network[s][super]) > 0 } ,

35

msg = Head(network[from][super])

36

do network[from][super] := Tail(@);

37

if msg.kind = “request”

38

then reqQ := insertRequest(from, msg.clk);

39

clock := max(clock, msg.clk) + 1;

40

network := send(super, from, [kind → “ack”]);

41

elsif msg.kind = “ack”

42

then acks := acks ∪{ from } ;

43

elsif msg.kind = “free” 44

then reqQ := removeRequest(from); 45

end if ; 46

end with ; 47

end loop ;

48

end process (* Communicator *)

49

Fig. 1. Lamport's mutual-exclusion algorithm in extended PlusCal (part 1)