DESCRIPTION
A large class of concurrency problems attempt to deal with allocating a set number of resources among several processes. This adds a central server which grants permission to aquire and release the resources. The dining philosophers with host problem is an example of this.
This is a variation of the standard dining philosophers problem. A host is added to the system. A philosopher to start (stop) eating must first gain permission from the host. The host allows at most one less than the number of philosophers in the problem to eat at a time. This ensures that deadlock does not occur.
Our implementation of this problem uses a task for each philosopher, each fork, and the host. There are always an equal number of philosophers and forks. It consists of at least 5 tasks; two philosophers, two forks, and the host. 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, two forks, and the host for a total of five tasks.
PROPERTIES
Some specific properties are provided below:
The property specifications by formalism are:
Back to main