DESCRIPTION
A large class of concurrency problems attempt to deal with allocating a set number of resources among several processes. The dining philosophers problem is an example of this.
A certain number of philosophers spend their lives alternating between thinking and eating. They are seated around a circular table. There is a fork placed between each pair of neighboring philosophers. Each philosopher has access to the forks at her left and right. In order to eat, a philosopher must be in possession of both forks. A philosopher may only pick up one fork at a time. Each philosopher attempts to pick up the left fork first and then the right fork. When done eating, a philosopher puts both forks back down on the table and begins thinking. Since the philosophers are sharing forks, it is not possible for all of them to be eating at the same time.
Our implementation of this problem uses a task for each philosopher and each fork. There are always an equal number of philosophers and forks. It consists of at least 4 tasks; two philosophers and two forks. It is scalable. To increase the size of the problem, additional philosophers and forks can be added.
ADA SOURCE
The size specifies the numbers of philosophers/forks there are in the source code. For example for size 2, there are two philosophers and two forks for a total of four tasks.
PROPERTIES
Some specific properties are provided below:
The property specifications by formalism are:
Back to main