Un article de Loria Wiki.
(* --algorithm RAgrawalaMutex2
variables msg_queue = [p \in 1..NbProcess |-> <<>>]
procedure msg_send(msg_send_to, msg_send_what)
begin
send: msg_queue[msg_send_to] := msg_queue[msg_send_to] \o msg_send_what;
end_send: return;
end procedure;
procedure msg_cb()
variables msg_cb_got = <<>>
begin
recv_req:
msg_cb_got := Head(msg_queue[self]);
msg_queue[self] := Tail(msg_queue[self]);
hl := max(msg_cb_got.estm, hl)+1;
if msg_cb_got.type = "Aut" then
aut_counter := aut_counter + 1;
else
if state = "NCS"
\/ (state = "WAIT"
/\ (estm_request > msg_cb_got.estm
\/ (estm_request = msg_cb_got.estm /\ self > msg_cb_got.from)
\/ self = msg_cb_got.from)) then
send_aut_1:
hl := hl + 1;
call msg_send(msg_cb_got.from, << [ type |-> "Aut", from |-> self, estm |-> hl] >>);
else
process_queue := process_queue \o <<msg_cb_got.from>>;
end if;
end if;
end_recv_req : return;
end procedure;
procedure exit_cs()
variables procid = <<>>
begin
send_aut_2:
while process_queue # <<>> do
hl := hl + 1;
procid := Head(process_queue);
process_queue := Tail(process_queue);
call msg_send(procid, <<[type |-> "Aut", from |-> self, estm |-> hl]>>);
end while;
end_send_aut :return;
end procedure;
\* --- Process behavior ---
process proc \in 1..NbProcess
variables
hl = 0 ,\* Current clock.
estm_request = 0,\* Time at whish we made te request.
process_queue = <<>>, \* Processes waiting for us.
aut_counter = 0, \* amount of acknolegments got so far
state = "NCS", \* either NCS, WAIT or CS
j = 0,
CS_todo = 2
begin
ncs:
while CS_todo > 0 do
skip;
allow_buddies:
while msg_queue[self] # <<>> do
call msg_cb();
end while;
hl := hl + 1;
estm_request := hl;
aut_counter := 0;
j := 0;
waiting:
while j <= NbProcess do
j := j+1;
call msg_send(j, <<[type |-> "Req", from |-> self, estm |-> estm_request]>>);
end while;
state := "WAIT";
read_message:
while aut_counter < NbProcess do
if msg_queue[self] # <<>> then
call msg_cb();
end if;
end while;
critical_section:
state := "CS";
skip;
exit_critical_section:
aut_counter := 0;
state := "NCS";
call exit_cs();
plop: CS_todo := CS_todo - 1;
end while;
end process
end algorithm *)
