Re: Need help in debugging/understanding concurrency concept

Hi Maneet,

The problem is in the conditionals:

PICK_ONE:

if forks[allowed[1]] = 0

then

forks[allowed[1]] := self;

else

skip;

end if;

The `else` isn't part of the original spec, but it more clearly shows what's happening: TLC evaluates the conditional, sees it's false, and does a no-op. This means your spec is never deadlocking, because it can always do something. It's just that the "something" happens to not change anything. To give a more minimal example, compare

process if_loop = "if"
begin
If:
    while TRUE do
      if FALSE then
        skip;
      end if;
    end while;
end process;

which will never deadlock, to

process await_loop = "if"
begin
Await:
    while TRUE do
      await FALSE;
      skip;
    end while;
end process;

which immediately deadlocks.

Tangent: forks = <<self,self>> can only be true if you have only two philosophers, as forks is the entire tuple of fork assignments. With three philosophers, the variable will have three elements.

Best,

Hillel

On Thursday, 26 July 2018 20:41:28 UTC-5, Maneet Bansal wrote:

Hi,

I was following Hillel's blog to learn TLA+ (Thanks Hillel for creating this). I tried to use the concepts to write "Dining Philosophers" problem https://learntla.com/concurrency/processes/ by myself.

Surprisingly I am not getting the expected deadlock. Can you please help in debugging? Following is what I have written.

---------------------------- MODULE Philosphers ----------------------------

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>>

(* --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

PICK_ONE:

if forks[allowed[1]] = 0

then

forks[allowed[1]] := self;

end if;

PICK_TWO:

if forks[allowed[2]] = 0

then

forks[allowed[2]] := self;

end if;

EAT:

\* Run if philoshper owns both the forks

if forks = <<self,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 /\ pc' = [pc EXCEPT ![self] = "PICK_ONE"]

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

/\ UNCHANGED << forks, allowed, hungry >>

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

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

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

ELSE /\ TRUE

   /\ forks' = forks

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

/\ UNCHANGED << allowed, hungry >>

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

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

THEN /\ forks' = [forks EXCEPT ![allowed[self][2]] = self]

ELSE /\ TRUE

   /\ forks' = forks

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

/\ UNCHANGED << allowed, hungry >>

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

   /\ IF forks = <<self,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) \/ PICK_ONE(self) \/ PICK_TWO(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

=============================================================================