We provide here three simple examples to illustrate modelling concurrent systems with Symmetric Nets:
The “Dining Philosophers” Example
This is the famous example provided by E. W. Dijkstra to illustrate an inappropriate use of shared resources generating deadlocks. N philosophers are seated at a round table with N plates and forks. Each of the philosophers has a plate in front of him and two forks: one on his left and one on his right. The fork situated to the left side of a philosopher is the one situated to the right side of the next philosopher around the table. The philosophers are thinking and, when they need to eat, they grab one fork from one side of their plate, then the second from the other side, then eat, and then go back thinking.
Each philosopher can be in two states, either he thinks or either he eats. Initially, all the philosophers are thinking. To go in the eating state, a philosopher has to take the two forks: one situated to his right side and one situated to his left side. Therefore, two adjacent philosophers cannot eat simultaneously.
An eating philosopher conserves the two forks as long as he eats. When he has finished eating the philosopher puts the two forks back.
This system can be modelled by the symmetric net shown in the figure below for a configuration involving 5 philosophers. Let us note that the use of the “<Philo.all>” expression (that generates one token per value in the Philo colour class) as initial marking of Think makes the model parameterised by the definition of the Philo colour class only.
The “Shared Memory” Example
Let us consider a system composed of P processors, each with a local memory. Each processor can access its local memory using a dedicated local bus and the other memories using a unique shared bus. A processor accessing a remote memory has priority over those accessing their own memory. It is assumed that external access request causes preemption of the owner processor eventually accessing its local memory.
This system can be modelled by the symmetric net shown in the figure below for a configuration involving 10 Processors.
The “Referendum” Example
Let us consider the model of a referendum. Any participant votes either yes or no. The final result is stored in places voted_yes and voted_no. Once again, the expression “<Voters.all>” denotes the constant function that generates one token per value in the Voters colour class.
This system can be modelled by the symmetric net shown in the figure below for a configuration involving 10 voters.