Objective:
- Practice specification and refinement of CSP processes in FDR
- Practice the refinement of deadlock free
- The dining philosophers problem
Five philosophers dine together at the round table, and each one has one plate of spaghetti. One fork is placed between any adjacent philosophers, and a philosopher must hold two nearby forks to eat. A fork can be held by one philosopher only anytime.
We consider the most simple case in which three events, pickup, putdown and eat, are used. We use a number to name a philosopher or a fork. For example, pickup.0.0 means that the 0th philosopher picks up the 0th fork. We assume all the philosophers pick up the left-side fork first, then pick up the right-side fork and put down the right one, and finally put down the left one. The left-side fork has the same number with the philosopher, and the right-side fork is i+1. For example, the 4th philosopher picks up the right side fork, which is modelled as pickup.4.0
Please exercise the following FDR script.
N = 5
channel pickup, putdown:{0..N-1}.{0..N-1}
channel eat:{0..N-1}
PHIL(i) = pickup.i.i->pickup.i.((i+1)%N)->eat.i->
putdown.i.((i+1)%N)->putdown.i.i->PHIL(i)
FORK(i) = pickup.i.i->putdown.i.i->FORK(i) []
pickup.((i-1)%N).i->putdown.((i-1)%N).i->FORK(i)
PHILS = |||i:{0..N-1}@PHIL(i)
FORKS = |||i:{0..N-1}@FORK(i)
SYSTEM = PHILS [|{|pickup, putdown|}|] FORKS
Now, we can check deadlock free of the system by the following FDR script
assert SYSTEM :[deadlock free[F]]
Can the refinement be passed? If not, what is the counter example?
There are many solutions to make the system deadlock-free. Here, we talk about two solutions only.
First, we introduce a butler to guide the philosophers when to sit down or get up. Therefore, we introduce two new events, sit and getup, and attach them to the beginning and the end of PHIL(i).
PHIL(i) = sit.i->pickup.i.i->pickup.i.((i+1)%N)->eat.i->
putdown.i.((i+1)%N)->putdown.i.i->getup.i->PHIL(i)
Now, we model the behaviour of the butler. The rule is simple. The butler counts the number of the philosophers at the table. New philosopher cannot sit down when the number is less than N-1.
BUTLER(n) = n>0&getup?i -> BUTLER(n-1) [] n<N-1&sit?i -> BUTLER(n+1)
S1 = SYSTEM [|{|sit, getup|}|] BUTLER(0)
assert S1 :[deadlock free[F]]
OK, can the new process pass the deadlock free refinement?
The second solution is to make at least one philosopher pick up the fork in a different order. For example, we consider the 0th philosopher is right-handed.
LPHIL(i) = pickup.i.i->pickup.i.((i+1)%N)->eat.i->
putdown.i.((i+1)%N)->putdown.i.i->LPHIL(i)
RPHIL(i) = pickup.i.((i+1)%N)->pickup.i.i->eat.i->
putdown.i.i->putdown.i.((i+1)%N)->RPHIL(i)
LPHILS = |||i:{1..N-1}@LPHIL(i)
LRPHILS = RPHIL(0) ||| LPHILS
S2 = LRPHILS [|{|pickup, putdown|}|] FORKS
assert S2 :[deadlock free[F]]
Check S2 in FDR again. Can it pass?
- Two children, Kate and Isabella, share an paint box and an easel. Whenever they wish to paint, they first search for the easel and the box until both are found. After they have finished painting, they drop the box and then the easel. Can you prove it’s deadlock free? If not, can you fix it?
Hint: four processes, Kate, Isabella, Easel and Box, should be considered, and they should be synchronised via some events.
