[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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


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