DESCRIPTION
A large class of concurrency problems attempt to deal with allocating a set number of resources where access if limited by a "token" that is passed among the users. The dining philosophers with dictionary problem is an example of this.
This is a variation of the standard dining philosophers problem. The philosophers now eat, think, and pass a dictionary around the table. The philosopher currently holding the dictionary cannot pick up any forks. In order to eat, the philosopher would have to pass on the dictionary. By adding the dictionary to the problem, we have removed the possibility of deadlock.
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