Modelling the Philosophers Dining Problem

[Younes]

Hi everyone,

I'm new to TLA+ and I'm trying to model the Philosophers Dining Problem.

My initial setup puts all philosophers into "thinking" and all forks to be "available".

I have a deadlock in my current model, and I think, it is because :

The Next action describes : the alternation (\/) of Thinking and Eating actions. This state of the system (all philosophers are thinking) can occur indefinitely.

How do I combine alternation of the actions (think & eat) in the system whilst avoiding a deadlock ? An intermediate state ? I'm confused.

Also, I will be grateful to take any remarks/comments about the design, or the approach. I am really looking forward into getting your critics / reviews.

TLA+ Source Code :

https://gist.github.com/YounesTea/35f52a52e50db114e18366bf73da564f#file-diningproblem-tla

Thank you all

[Stephan Merz]

Hello,

two quick remarks.

1. The definition of your next-state relation is

Next == \A p \in Range(Philosophers) : (StartEating(p) /\ StopEating(p)) \/ StartThinking(p)

This is saying that *all* philosophers move at every system transition. You certainly want to specify that *some* philosopher takes a move, so replace \A with \E.

Also, the body of that formula asserts that either a philosopher starts thinking or that she starts and stops eating simultaneously. Again, this is certainly wrong. One could imagine that thinking and eating alternate, so "start thinking" doesn't need to be a separate transition (because a philosopher starts thinking as soon as she stops eating), but starting and stopping eating should not occur simultaneously.

2. The real challenge in the problem is to avoid the deadlock situation that occurs when each philosopher holds one fork but cannot acquire the second one because it is held by her neighbor. You trivialized that problem by having each philosopher take up and lay down both forks simultaneously. The original formulation of the problem states that forks are taken up individually (see also [1]). This is what makes the problem interesting.

Stephan

[1] https://en.wikipedia.org/wiki/Dining_philosophers_problem

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/979b04c6-736f-4722-b986-72edea346f7bn%40googlegroups.com.

[Younes]

Thank you, Stephan, for your remarks.

I have made a few changes in the design (still in progress). I now consider that there are many actions that a philosopher can do : Eating, Taking/Putting the right/left fork, or Doing Nothing. All actions except "Eating" are part of the "Thinking" state. What do you think ?

I know that a philosopher should alternate between eating and thinking, but I think some 'intermediate' states are required to design the problem (especially if a philosopher can either pick or put one fork, but not both at the same).

I have written the "PickFork" action, but not the "PutFork" action yet. What do you think of what I have done so far ? Do you think this design / perspective is "correct" ?

Thank you again,

Link to the TLA+ code : https://gist.github.com/YounesTea/35f52a52e50db114e18366bf73da564f

[Younes]

Hi again,

Given this data :

I have this error in line 36 (https://gist.github.com/YounesTea/35f52a52e50db114e18366bf73da564f#file-diningproblem-tla-L36) :

Attempted to check if the value:

[p1 |-> {}, p2 |-> {}, p3 |-> {}, p4 |-> {}, p5 |-> {}]

is an element of the function [ p1 |-> {{}, {"f1"}, {"f5"}, {"f1", "f5"}},

  p2 |-> {{}, {"f1"}, {"f2"}, {"f1", "f2"}},

  p3 |-> {{}, {"f2"}, {"f3"}, {"f2", "f3"}},

  p4 |-> {{}, {"f3"}, {"f4"}, {"f3", "f4"}},

  p5 |-> {{}, {"f4"}, {"f5"}, {"f4", "f5"}} ]

While working on the initial state:

/\ philosopherDoing = [ p1 |-> "PutLFork",

  p2 |-> "PutLFork",

  p3 |-> "PutLFork",

  p4 |-> "PutLFork",

  p5 |-> "PutLFork" ]

/\ hasForks = [p1 |-> {}, p2 |-> {}, p3 |-> {}, p4 |-> {}, p5 |-> {}]

/\ availableForks = [f1 |-> TRUE, f2 |-> TRUE, f3 |-> TRUE, f4 |-> TRUE, f5 |-> TRUE]

The error occurred when TLC was evaluating the nested

expressions at the following positions:

0. Line 17, column 9 to line 19, column 59 in DiningProblem

1. Line 17, column 12 to line 17, column 74 in DiningProblem

2. Line 18, column 12 to line 18, column 58 in DiningProblem

3. Line 19, column 12 to line 19, column 59 in DiningProblem

4. Line 34, column 18 to line 36, column 97 in DiningProblem

5. Line 36, column 21 to line 36, column 97 in DiningProblem

I don't know what I'm missing in that expression.

[Stephan Merz]

Hello,

sorry for the late reply.

Did you use TLC to check your spec? It tells you that it is deadlocked in the initial state. The reason is the definition

ChangeStatus(p) == /\ LET status == IF Cardinality(PhiloStatus[p].forks) = 2 THEN "Eating" ELSE "Thinking"
                        IN /\ PhiloStatus' = [ PhiloStatus EXCEPT ![p].status = status ]

PickForkP(f,p) == /\ \A ph \in Philosophers : f \notin PhiloStatus[ph].forks \* fork f isn't used by anyone
                  /\ PhiloStatus[p].status = "Thinking"
                  /\ PhiloStatus' = [ PhiloStatus EXCEPT ![p].forks = @ \cup {f} ]
                  /\ ChangeStatus(p)

Here you are trying to do two updates to PhiloStatus, this is not going to work.

Some minor remarks:

- Why do you declare Philosophers, Forks, and Statuses as constant parameters when they can be defined?

- Why even record the thinking or eating status of a philosopher in the state: we can just assume that a philosopher is "eating" if she holds two forks and "thinking" otherwise (or if you prefer, "thinking" is she holds no fork and "waiting" if she hold one fork)?

I simplified your spec based on these ideas, see the attached module. Now TLC gives me the following results (for Max=5):

- when disabling deadlock checking and verifying type correctness, it generates 243 distinct states (so the state space is not trivial anymore),

- when verifying the predicate NeverEat, it produces a counter-example showing that philosophers are indeed able to eat,

- however, when checking for deadlocks, it shows the deadlock state where each philosopher holds one fork and cannot acquire the second one.

Now you'll have to find a way to avoid this deadlock state. Only then worry about verifying liveness properties.

Stephan

[Stephan Merz]

The GitHub link is not valid anymore but it looks like you constructed a function of the form

forks == [ p \in Range(Philosophers) |-> SUBSET {Left(p), Right(p)} ]

and then checked the predicate hasForks \in forks.

What I think you meant to write was something like

/\ hasForks \in [Range(Philosophers) -> Range(Forks)]

/\ \A p \in Range(Philosophers : hasForks[p] \subseteq {Left(p), Right(p)}

In particular, the right-hand side of the first conjunct is a set of functions, not a single function.

See also the typing invariant in the module that I posted.

Stephan

On 20 Feb 2021, at 09:55, Younes <youne...@gmail.com> wrote:

Hi again,

Given this data :

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/fa895ef0-074a-4937-9138-1d2dfe407485n%40googlegroups.com.
<Screenshot from 2021-02-20 09-53-02.png>