COMP3151/9154 Homework 5

Develop solutions to each of the following problems in Promela.

1    Reasoning about message passing

Here is a critical section algorithm that uses synchronous message passing:

Only processes x and y are competing for the critical section; z is an auxiliary process.  The critical sections are at lines x2 and y2; x_1 and y_1 are the non-critical sections. The program variables x,y,z are just dummies; their values and types are unimportant.

The transition diagrams for these processes are as follows.

(The self-loop is not depicted in the code above; it represents the ability to stay in the non-critical section forever).

1.  Construct the closed product of these transition diagrams.  The initial state will be ⟨x1 , y1 , z1 ⟩ .

2.  It’s obvious from inspection of the closed product that this algorithm satisfies mutual exclusion. Why?

3.  Does this algorithm satisfy eventual entry? Briefly motivate.

4.  Does this algorithm still work if we flip all inputs to outputs, and vice versa? Briefly motivate.

5.  The algorithm behaves oddly if we make ch asynchronous. Describe a scenario that (a) assumes an asynchronous, reliable channel; (b) goes on forever in a cycle; and (c) takes transitions other than the self-loops at x1 and y1 infinitely often; and (d) never visits locations x2 and y2.

2    Philosophers

Develop a solution for the dining philosophers problem using only message passing, under the additional restriction that each channel must be connected to exactly one sender and exactly one receiver.

By way of a hint, the following things do not work:

.  Having only 5 processes, one for each philosopher.

.  Having only 5 channels, one for each fork.

Configure the solution to run forever, in a 5 philosopher scenario.

3    Fair Merge

Develop an algorithm to merge two sequences of data.   A  process  called merge is given three channel parameters of type byte, receives data on two input channels and interleaves the data on the output channel, such that if the two inputs are sorted (in ascending order), then the output is sorted.

Try to implement a fair merge that is free from starvation of both in- put channels when possible.  This means that you should try to make sure every input stream is always eventually read from.  This requirement will sometimes be impossible to reconcile with the sortedness requirement.   If so, keeping the outputs sorted takes priority. For example, if the two input channels transmit infinite streams of 1:s and 2:s, respectively, no 2:s should be sent on the output channel.