In this tutorial we will use the famous Dining philosophers problem as an example of resource allocation problems where several processes compete for resources. It also illustrates the power and convenience of Petri nets as a formalism for modelling and analysis of such problems. There are five philosophers sitting around a table. Each philosopher is either thinking or eating. There are five forks on the table, one between each pair of adjacent philosophers, shared by them; that is, each fork can be used by a philosopher either on its left or on its right. To eat a philosopher has to acquire both forks, the one on his left and the one in his right, in any order. If a fork is already taken by a neighbouring philosopher, he will be waiting until the fork becomes available again. After eating, a philosopher returns to thinking while putting back both his forks.

The behaviour of a single philosopher can be modelled with take_left_fork, put_left_fork, take_right_fork, put_right_fork, start_eating and start_thinking transitions. The state of the philosopher is captured with a token in either the eating or thinking place and the availability of forks is determined by the presence of a token in fork1_free and fork2_free places respectively (the corresponding fork is on the table), as shown in the following Petri net.

For simplicity let us model the problem with two philosophers and two forks only. In this case, fork1_free and fork2_free are shared by the philosophers north and south, sitting at the North and South sides of the table respectively. This is modelled by the following Petri net.

Capture this Petri net within Workcraft as follows (see Help on editing Petri nets, in particular you can double-click on a place to put/remove a token):

1. Build a Petri net model for a single dining philosopher.
2. Select the places and transitions representing the philosopher (exclude the fork1_free and fork2_free places) and combine them using the paging tool . The created page is our philosopher model.
3. Make use of copy-paste features to replicate the philosopher model. Name one of the pages south and the other north.
4. Rotate the north page using the rotation tool or . Position the north and south pages opposite each other.
5. Share fork1_free and fork2_free places between the south and north philosophers by connection fork_take_* and fork_put_* transitions accordingly.

Enter the simulation tool by pressing the button and play with the dining philosophers model. Initially both forks are on the table and places fork1_free and fork2_free are marked. Each philosopher can take any of the forks - the take_left_fork and take_right_fork transitions are enabled for both norht and south philosophers.

If you allow the same philosopher to take both forks (e.g., by clicking transitions south.take_left_fork and south.take_right_fork), then he can eat, while the other philosopher thinks. When he is finished with the meal he enters the thinking state (click transition south.start_thinking) and returns the forks (click transitions south.put_left_fork and south.put_right_fork). This trace of transitions brings us to the initial marking where the philosophers compete for the forks again.

Another scenario is possible when each philosopher takes only one of the forks (e.g. click transitions south.take_left_fork and north.take_left_fork). This leads to a deadlock as the philosophers wait for each other to return the fork, but none of them can do it until they acquire the other fork and eat.

Simulate the above distinctive scenarios for dining philosophers. Explore the navigation buttons in the Control panel and go back and forth through the trace of events in your simulation. Try random simulation at different animation speeds.

Various properties of a Petri net model can be verified using Punf and MPSat as the backend tools (see overview of backend tools for more details). The tool interfaces available for Petri net verification are collected under Verification menu.

The easiest and most obvious property to check is that the model does not have a deadlock – choose the Verification→Deadlock freeness [MPSat] menu item for this. As our dining philosophers model is not deadlock-free, this should result in the following error message with a trace leading to the deadlock (you can analyse the trace in the simulator by clicking the Play button).

Verification of custom properties is based on reachability analysis on the Petri net. For this a custom property should be expressed in REACH language. For example, you can try and verify that both philosophers cannot be eating at the same time:

1. Open REACH assertion window via Verification→REACH assertion [MPSat]… menu.
2. In MPSat settings section set the Mode into Reachability analysis and the Solution into minimise cost function.
3. Enter the following Reach expression as the property predicate: $P"north.eating" & $P"south.eating". Note that . is used as a hierarchy separator in Reach expression.
4. Select unsatisfiable to denote that the property holds if predicate is unsatisfiable.
5. Save this property as a preset for future use (Save as… button), e.g. under the name simultaneous eating.

The result should be similar to the following screenshot.

Let us explain how to interpret the Reach predicate. Consider an expression $P"place_name". It instructs MPSat to check if a marking is reachable where the place place_name has a token. In basic cases one can apply logical operations and quantifiers (e.g. &, |, forall, exists, etc.) to a marking which violates the property. For expressing more sophisticated properties refer to Reach language documentation.

In our case, the expression $P"north.eating" & $P"south.eating" tells MPSat to check if a marking is reachable where both places north.eating and south.eating contain tokens, which corresponds to both philosophers eating at the same time. If such a marking is reachable, then our property is violated and a trace of Petri net transitions leading to this marking is reported. If this Petri net marking is not reachable, then the property holds, as shown in the following screenshot.

Complete the following tasks:

1. Verify the model of dining philosophers for deadlocks. Simulate the trace leading to the deadlock.
2. Modify the model in such a way that the deadlock is prevented (hint: force the philosophers to take the forks in particular order, one of them always takes the fork to his left first, while the other always takes the fork to his right first).
3. Verify that none of the philosophers can be eating with one of the forks still on the table (hint: ($P"north.eating" | $P"south.eating") & ($P"fork1_free" | $P"fork2_free")).

Download all the Workcraft models discussed in this section here:

Dining philosophers models (20 KiB)