© 1996-2019







VI.11 Exercises

Exercises [Slide 264]

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.

  • definetest_1() = existsA : {
    {A = 0 and empty};
    skip ; {A = 1 and empty}
    }.
  • definetest_2() =
    existsA,B : {A = 0 and B = 0 and A := next(B) + 1}.
  • definetest_3() = existsA :
    {A = 0 and A gets A + 1 and sometimes(A = 5)}.
  • definetest_4() =
    existsA : {empty  and (A = 0 or A = 1)}.

Exercise 33.  

  • Write a Tempura program that ask for the input of a number in the first 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 first 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 specified 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.

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 offer 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 floors.

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

  • CallRequestUp(Floor), from a person waiting on floor Floor wishing to go up.
  • CallRequestDown(Floor), from a person waiting on floor 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 floors 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 floor k to service a request for that floor. If, on the way to floor k, the lift is about to pass a floor j (not equal to k) such that there is an unserviced call request to floor j, then the lift shall stop at floor 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 floor to another floor 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 define the transitions from state [up, close] and [up, open] the following definitions are needed:

  • stop_up: there is either a GotoReq or CallReqUp for the current floor.
  • called_up: there are CallReqUp for floors that are above the current floor.
  • called_down: there are CallReqDown for floors that are below the current floor.

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 floor and there are CallReqUp requests for floors that are above the current floor.
  • to [up, open] when stop_up called_up. There is either a GotoReq or CallReqUp request for the current floor and there are CallReqUp requests for floors that are above the current floor.
  • to [down, open] when stop_up ¬called_up called_down. There is either a GotoReq or CallReqUp request for the current floor and there are CallReqDown requests for floors that are below the current floor.
  • to [stop, open] when stop_up ¬called_up ¬called_down.

    There is either a GotoReq or CallReqUp request for the current floor and there are no CallReqUp requests for floors that are above the current floor and there are no CallReqDown requests for floors that are below the current floor.

  • to [down, close] when ¬stop_up ¬called_up.

    There are no GotoReq and CallReqUp requests for the current floor and there are no CallReqUp requests for floors that are above the current floor.

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 defined in a similar fashion.

Exercise 39.  

The Mutual Exclusion Problem for 2 processes is defined 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 Turn1 do skip;
while Turn2 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 Ci be shared variable with possible values 0 and 1, and that can only be set by process i, initially Ci = 1.

while true do {
while true do {
Non_Critical_Section_1;
Non_Critical_Section_2;
while C21 do skip;
while C11 do skip;
C1 := 0;
C2 := 0;
Critical_Section_1;
Critical_Section_2;
C1 := 1}
C2 := 1}

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

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

while true do {
while true do {
Non_Critical_Section_1;
Non_Critical_Section_2;
C1 := 0;
C2 := 0;
while C21 do skip;
while C11 do skip;
Critical_Section_1;
Critical_Section_2;
C1 := 1}
C2 := 1}

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

Let Ci be shared variable with possible values 0 and 1, and that can only be set by process i, initially Ci = 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;
C1 := 1;
C2 := 1;
Last := 1;
Last := 2;
while C20 Last = 1
while C10 Last = 2
do skip;
do skip;
Critical_Section_1;
Critical_Section_2;
C1 := 0}
C2 := 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 identifier (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 102 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 identifier to its neighbour. Whenever a process receives an identifier 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 identifier 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 figure 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 first phase, each process sends its identifier two steps clockwise (so each process sees the identifiers of its neighbour and its next-to-last neighbour).
  • Each process P makes a decision based on its own identifier and the identifiers it has received. If P’s immediate neighbour’s identifier is the greatest of the three, then P remains “active” in the algorithm and adopts its neighbour’s identifier as its own. Otherwise, P becomes a “relay”.
  • Now, each active process sends its identifier 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 finds 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 specification and then implement it as a Tempura program.







2019-05-10
Contact | Home | ITL home | Course | Proofs | Algebra | FL