[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

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



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.


Leslie 

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



--
Regards
Maneet Bansal