DESCRIPTION
A large class of concurrency problems attempt to deal with allocating a set number of resources among several processes. The dining philosophers with fork manager problem is an example of this.
In this variation of the dining philosophers problem, the forks are replaced by a fork manager which records the state of all of the forks. A philosopher to start (stop) eating asks the fork manager for permission. Once it is granted, the philosopher now picks up (puts down) both forks simultaneously. By adding the fork manager, we have removed the possibility of deadlock within the system.
Our implementation of this problem uses a task for the fork manager and each philosopher. It consists of at least 3 tasks; the fork manager and two philosophers. It is scalable. To increase the size of the problem, additional philosophers can be added.
ADA SOURCE
The size specifies the numbers of philosophers there are in the source code. For example for size 2, there is the fork manager and two philosophers for a total of three tasks.
PROPERTIES
Some specific properties are provided below:
The property specifications by formalism are:
Back to main