Re: [tlaplus] Re: Need help in debugging/understanding concurrency concept

Thanks, Markus. The link you provided was super helpful in understanding how 'with' and 'await' works together

Thanks, Hillel for the detailed explanation behind the root cause of the bug.

Thanks, Leslie for explaining how TLC judges a deadlock situation.

Here is the updated, working model.

EXTENDS Integers, Sequences, TLC

CONSTANTS PHIL

(***************************************************************************

Operator to return tupple containing allowed forks to a philoshper.

A philospher with id=i, should have access to forks i and i+1. In case of

pid = N, <<N,1> is returned

Where N is the max number of philospers.

There is no ordering on output.

Also no input checking is being performed.

***************************************************************************)

GetAllowedForks(pid) == IF pid = PHIL

THEN <<pid,1>>

ELSE <<pid,pid+1>>

Available(allowedForks,forks) == {x \in DOMAIN allowedForks :forks[allowedForks[x]] = 0}

(* --algorithm dine

(***************************************************************************

fork:0 means the fork is not acquired.

fork:pid means the fork is acquired by pid

***************************************************************************)

variables forks = [ f1 \in 1..PHIL |-> 0]

process phil \in 1..PHIL

variables allowed = GetAllowedForks(self), hungry = TRUE;

begin

PICK_FORKS:

while hungry do

with a \in Available(allowed,forks) do

forks[allowed[a]] := self;

end with;

EAT:

\* Run if philoshper owns both the forks

if forks[allowed[1]] = self /\ forks[allowed[2]] = self

then

hungry := FALSE;

\* free the forks please

forks[allowed[1]] := 0 || forks[allowed[2]] := 0;

end if;

end while;

end process;

end algorithm; *)

\* BEGIN TRANSLATION

VARIABLES forks, pc, allowed, hungry

vars == << forks, pc, allowed, hungry >>

ProcSet == (1..PHIL)

Init == (* Global variables *)

/\ forks = [ f1 \in 1..PHIL |-> 0]

(* Process phil *)

/\ allowed = [self \in 1..PHIL |-> GetAllowedForks(self)]

/\ hungry = [self \in 1..PHIL |-> TRUE]

/\ pc = [self \in ProcSet |-> "PICK_FORKS"]

PICK_FORKS(self) == /\ pc[self] = "PICK_FORKS"

/\ IF hungry[self]

THEN /\ \E a \in Available(allowed[self],forks):

forks' = [forks EXCEPT ![allowed[self][a]] = self]

/\ pc' = [pc EXCEPT ![self] = "EAT"]

ELSE /\ pc' = [pc EXCEPT ![self] = "Done"]

/\ forks' = forks

/\ UNCHANGED << allowed, hungry >>

EAT(self) == /\ pc[self] = "EAT"

/\ IF forks[allowed[self][1]] = self /\ forks[allowed[self][2]] = self

THEN /\ hungry' = [hungry EXCEPT ![self] = FALSE]

/\ forks' = [forks EXCEPT ![allowed[self][1]] = 0,

![allowed[self][2]] = 0]

ELSE /\ TRUE

/\ UNCHANGED << forks, hungry >>

/\ pc' = [pc EXCEPT ![self] = "PICK_FORKS"]

/\ UNCHANGED allowed

phil(self) == PICK_FORKS(self) \/ EAT(self)

Next == (\E self \in 1..PHIL: phil(self))

\/ (* Disjunct to prevent deadlock on termination *)

((\A self \in ProcSet: pc[self] = "Done") /\ UNCHANGED vars)

Spec == Init /\ [][Next]_vars

Termination == <>(\A self \in ProcSet: pc[self] = "Done")

\* END TRANSLATION