Objective:

• Practice specification and refinement of CSP processes in FDR
• Practice the refinement of deadlock free
1. 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

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)

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

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.

All papers are written by ENL (US, UK, AUSTRALIA) writers with vast experience in the field. We perform a quality assessment on all orders before submitting them.

Do you have an urgent order?  We have more than enough writers who will ensure that your order is delivered on time.

We provide plagiarism reports for all our custom written papers. All papers are written from scratch.