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

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



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;



      while hungry do

      with a \in Available(allowed,forks) do

            forks[allowed[a]] := self;

      end with;  



        \* Run if philoshper owns both the forks

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


           hungry := FALSE;

            \* free the forks please

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

        end if;

      end while;

end process;

end algorithm; *)


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


On Fri, Jul 27, 2018 at 5:55 PM, Leslie Lamport <tlapl...@xxxxxxxxx> wrote:

I don't have time to look at the example itself, but the discussion
suggests that the problem is the confusion between a deadlocked state
and a state in which TLC reports a deadlock.


- A deadlocked state is one in which the only step allowed by the
  spec's next-state action is a stuttering step--one that changes none
  of the spec's variables.


- TLC reports deadlock for a state in which the next-state action allows
  no step.


Thus, TLC will not report a deadlock for a deadlocked state in which
the next-state action allows a stuttering step.


You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@googlegroups.com.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

Maneet Bansal