Exercises

Exercise 32.

Given the following Tempura programs and determine whether they are executable or not. Try to change those that are not executable in such a way that they become executable.

deﬁne test_1() = exists A : {

{A = 0 and empty};

skip ; {A = 1 and empty}

}.
deﬁne test_2() =

exists A,B : {A = 0 and B = 0 and A := next(B) + 1}.
deﬁne test_3() = exists A :

{A = 0 and A gets A + 1 and sometimes(A = 5)}.
deﬁne test_4() =

exists A : {empty and (A = 0 or A = 1)}.

Exercise 33.

Write a Tempura program that ask for the input of a number in the ﬁrst state and output the square of it in the second state. The program should only have two states.
Write a Tempura program that adds a list of numbers. Show the intermediate “add” results.
Write a Tempura program that consists of two processes. The ﬁrst process asks for a number in the odd numbered states and output the square of it in the next even numbered state. The second process asks for a number in the even numbered states and output the cube of it in the next odd numbered state.

Exercise 34.

Change the Liquid Tank V2 example so that the outlet pipe can be controlled by the operator via an interrupt C, i.e., when C = 0 then V 2 should be closed. The controller unit should maintain the level of the liquid in the tank within the speciﬁed limits while honouring the operator interrupts.

Exercise 35.

Change the Robot Control System so that priority is given to the operator.
Change the Robot Control System so that the Infra-red motor commands stay within −20 and 20 boundaries.

Tempura code of the Robot Control System

Exercise 36.

Complete the Alternating Bit Protocol (ABP) program for lossy Data and Ack channel.

Exercise 37.

Write a Tempura program that models the following supermarket: A supermarket consists of a buying area, where the customers collect the items they wish to purchase, and one or more pay tills, where the customers queue up to pay for those items. Each pay till generally has only one queue of customers. A customer can join any queue and move freely among queues (because all pay tills generally oﬀer the same service). A customer may only join the rear of a queue.

The basic properties of the supermarket and its pay tills and customers are summarised as follows:

Location of clients:

A customer may be in any of the following locations:

Outside the supermarket.
In the buying area.
In a queue waiting to pay.
At a pay till.

Movements of clients.

A customer may make the following moves:

From outside the supermarket to the buying area. This is not possible if the supermarket is closing.
From the buying area to outside. This is possible if either the required item is not available or the queues are too long!
From the buying area to the rear of the queue at some cash point. This is only possible if the pay till is not closing.

From the queue to the buying area (this is only possible if the customer is not currently being served).
From the front of the queue to the pay till associated to the queue. This is only possible if the pay till is free and not closed.
From any position in the queue to the rear of another queue. This is only possible if the new queue is not closing.
From a pay till to outside the supermarket.

Status of the pay till.

There are three states:

Closed (i.e., unable to serve).
Open (i.e., able to serve customers).
Closing (i.e., able to serve customers currently in the queue but not new customers).

A pay till which is not closed may additionally be in either of the following sub states:

Busy (currently serving a customer).
Free (currently not serving a customer).

Operation of pay tills:

Open.
Close queue.
Close.
Begin processing (of a customer).
End processing (of a customer).

Status of supermarket:

Open.
Closed.
Closing.

Operation on supermarket:

Open.
Close entrance.
Close.

Exercise 38.

Write a Tempura program that models one or more lifts, with interactive input of (simulated) button presses.

The Tempura program should have the following parameters:

numberOfLifts, the number of lifts.
numberOfFloors, the number of ﬂoors.

The lift shall respond in a timely fashion to the following button presses:

CallRequestUp(Floor), from a person waiting on ﬂoor Floor wishing to go up.
CallRequestDown(Floor), from a person waiting on ﬂoor Floor wishing to go down.
GotoRequest(Floor), from a lift passenger.
DoorOpen, from a lift passenger (keeps door open if already open, opens door if in the process of closing),

If a lift is moving in a given direction, then it continues to move in that direction until there are no more unserviced requests in that direction. But it shall stop at any ﬂoors along the way that have either unserviced CallRequests for the same direction or unserviced GotoRequests. That is, suppose the lift is moving in the direction of ﬂoor k to service a request for that ﬂoor. If, on the way to ﬂoor k, the lift is about to pass a ﬂoor j (not equal to k) such that there is an unserviced call request to ﬂoor j, then the lift shall stop at ﬂoor j if and only if either

k > j and there is an unserviced CallRequestUp(Floor) with Floor= j, or
k < j and there is an unserviced CallRequestDown(Floor) with Floor= j, or
there is an unserviced gotoRequest(Floor) with Floor= j.

The design should make the following assumptions:

(the unit interval consists of two states, i.e., it is skip)

Moving from one ﬂoor to another ﬂoor is done within the unit interval.
The door are kept open for a unit interval.
Opening and closing of the doors is done within the unit interval.

Model the lift as a machine with states and transitions.

The lift can be in the following states:

[stop, open], the lift has received no requests and the doors are open.
[up, close], the direction of the lift is up and the doors are closed.
[up, open], the direction of the lift is up and the doors are open.

[down, close], the direction of the lift is down and the doors are closed.
[down, open], the direction of the lift is down and the doors are open.

The lift starts in state [stop, open] and the lift can move from any state to any state.

In order to deﬁne the transitions from state [up, close] and [up, open] the following deﬁnitions are needed:

stop_up: there is either a GotoReq or CallReqUp for the current ﬂoor.
called_up: there are CallReqUp for ﬂoors that are above the current ﬂoor.
called_down: there are CallReqDown for ﬂoors that are below the current ﬂoor.

The transitions from state [up, close] are then as follows:

to [up, close] when ¬stop_up ∧ called_up. There are no GotoReq and CallReqUp requests for the current ﬂoor and there are CallReqUp requests for ﬂoors that are above the current ﬂoor.
to [up, open] when stop_up ∧ called_up. There is either a GotoReq or CallReqUp request for the current ﬂoor and there are CallReqUp requests for ﬂoors that are above the current ﬂoor.

to [down, open] when stop_up ∧¬called_up ∧ called_down. There is either a GotoReq or CallReqUp request for the current ﬂoor and there are CallReqDown requests for ﬂoors that are below the current ﬂoor.

to [stop, open] when stop_up ∧¬called_up ∧¬called_down.

There is either a GotoReq or CallReqUp request for the current ﬂoor and there are no CallReqUp requests for ﬂoors that are above the current ﬂoor and there are no CallReqDown requests for ﬂoors that are below the current ﬂoor.
to [down, close] when ¬stop_up ∧¬called_up.

There are no GotoReq and CallReqUp requests for the current ﬂoor and there are no CallReqUp requests for ﬂoors that are above the current ﬂoor.

The transitions from state [up, open] are as follows

to [up, open] when called_up ∧ DoorOpen.
to [up, close] when called_up ∧¬DoorOpen.
to [down, open] when ¬called_up ∧ called_down ∧ DoorOpen.
to [down, close] when ¬called_up ∧ called_down ∧¬DoorOpen.
to [stop, open] when ¬called_up ∧¬called_down.

The transitions from the other states should be deﬁned in a similar fashion.

Exercise 39.

The Mutual Exclusion Problem for 2 processes is deﬁned as follows:

2 processes are executing in an endless loop a sequence of instructions which can be divided into subsequences: the Critical and the Non-Critical section. The mutual exclusion property is that instructions from the Critical sections of these two processes must not be interleaved.

The solution will be describe by inserting into the endless loop additional instructions that are to be executed by a process wishing to enter and leave its critical section, the Pre and Post sections.

while true do {

Non_Critical_Section;

Pre_Section;

Critical_Section;

Post_Section}

A process may halt in its Non-Critical section but it may not halt in the Pre, Post and Critical sections. If a process halts in its Non-Critical section, it must not interfere with the other process.

The solution must satisfy the following:

The two processes must not deadlock. If the two process are trying to enter their Critical Section and no process ever succeeds in making the transition from the Pre Section to the Critical Section then we say that the two processes are deadlocked.

There must be no starvation of one of the processes. If a process indicates its intention to enter the Critical Section by entering the Pre Section, eventually it will succeed.

In the absence of contention for the Critical section, a single process wishing to enter its Critical Section will succeed and with minimal overhead.

Examine the following solution by giving its Tempura version and simulate various interesting runs.

Let Turn be a shared variable with possible values 1 and 2, initially it is 1.

while true do {	while true do {
Non_Critical_Section_1;	Non_Critical_Section_2;
while Turn≠1 do skip;	while Turn≠2 do skip;
Critical_Section_1;	Critical_Section_2;
Turn := 2}	Turn := 1}

Examine the following solution by giving its Tempura version and simulate various interesting runs.

Let C_i be shared variable with possible values 0 and 1, and that can only be set by process i, initially C_i = 1.

while true do {	while true do {
Non_Critical_Section_1;	Non_Critical_Section_2;
while C₂≠1 do skip;	while C₁≠1 do skip;
C₁ := 0;	C₂ := 0;
Critical_Section_1;	Critical_Section_2;
C₁ := 1}	C₂ := 1}

Examine the following solution by giving its Tempura version and simulate various interesting runs.

Let C_i be shared variable with possible values 0 and 1, and that can only be set by process i, initially C_i = 1.

while true do {	while true do {
Non_Critical_Section_1;	Non_Critical_Section_2;
C₁ := 0;	C₂ := 0;
while C₂≠1 do skip;	while C₁≠1 do skip;
Critical_Section_1;	Critical_Section_2;
C₁ := 1}	C₂ := 1}

Examine the following solution by giving its Tempura version and simulate various interesting runs.

Let C_i be shared variable with possible values 0 and 1, and that can only be set by process i, initially C_i = 0. Let Last be a shared variable with possible values 1 and 2, initially Last = 1.

while true do {	while true do {
Non_Critical_Section_1;	Non_Critical_Section_2;
C₁ := 1;	C₂ := 1;
Last := 1;	Last := 2;
while C₂≠0 ∧ Last = 1	while C₁≠0 ∧ Last = 2
do skip;	do skip;
Critical_Section_1;	Critical_Section_2;
C₁ := 0}	C₂ := 0}

Exercise 40.

In distributed computing, it is often useful to be able to designate one and only one process as the coordinator of some activity. This selection of a coordinator is known as the leader election problem.

In this exercise you will consider the problem of electing a leader among a group of 10 processes whose communication pattern is arranged in a ring, where each process can only receive messages from its left neighbour and may send messages only to its right neighbour. It is assumed that each process starts out with a unique identiﬁer (an integer).

Implement and test the following two leader election algorithms. Read over the entire assignment before starting.

Le Lann-Chang-Roberts Leader Election: This is perhaps the simplest of all distributed algorithms. It sends around 10² messages in the worst case. Try to construct an execution in which you would get this worst case behaviour.

The idea of this algorithm is that each process starts by passing its own identiﬁer to its neighbour. Whenever a process receives an identiﬁer from its neighbour, it either:

passes it on around the ring, if the id received is greater than its own,
discards it, if the id received is less than its own, or
declares itself the leader, if the id received matches its own.

Notice that the process with the greatest identiﬁer is elected.

Create a Tempura program that implements this algorithm.

Peterson Leader Election Algorithm: This algorithm for leader election in a ring is a bit more involved, but its worst case message complexity is much better. See if you can ﬁgure out the message complexity of this algorithm. (Hint: notice that at least half of the processes become relays after each round of communication.)

The algorithm works as follows:

In the ﬁrst phase, each process sends its identiﬁer two steps clockwise (so each process sees the identiﬁers of its neighbour and its next-to-last neighbour).
Each process P makes a decision based on its own identiﬁer and the identiﬁers it has received. If P’s immediate neighbour’s identiﬁer is the greatest of the three, then P remains “active” in the algorithm and adopts its neighbour’s identiﬁer as its own. Otherwise, P becomes a “relay”.

Now, each active process sends its identiﬁer to its next two active neighbours, clockwise around the ring. Relay processes simply pass along each message they receive.
Steps 2 and 3 continue repeatedly, with more and more processes dropping out as “relays” until a process ﬁnds that its own immediate neighbour is itself, in which case everyone else has dropped out and it declares itself the leader.

Implement this algorithm as a Tempura Program.

Think about how you will manage sending a message two steps around the ring of active processes. Also, print out useful messages in order to demonstrate that your algorithm is working properly. For example, at each round, active processes should print out the round number, the messages received from the two neighbours, and the decision of whether to remain active or become a relay.

Exercise 41.

Write a Tempura program that simulates a cash machine (atm). First write an informal speciﬁcation and then implement it as a Tempura program.

VI.11 Exercises

Exercises [Slide 264]