Java程序辅导

COMP2310/COMP6310:
Concurrent and Distributed Systems
Semester 2 2014
Tutorial / Laboratory 1
Introduction to FSP Processes and Concurrent Execution
Objectives
To become familiar with basic aspects of FSP programs, including the corresponding LTS
graphs, event traces and alphabets.
To model simple sequential processes using FSP.
To become familiar with using the LTSA tool.
To become familiar with the basic structure of threaded programs in Java and C.
To appreciate the concepts of interference between threads, and the distinction between
(true) parallelism and concurrency, and issues in the scheduling of threads.
Preparation
Before your session, please:
revise the Processes lecture and the first half of Chapter 2 of Magee&Kramer.
try answering Tutorial Question 1; if you have any problems, get your questions ready to
ask at your session.
have a look at the Race.java and race.c programs and familiarize yourself with their basic
structure.
Tutorial Exercises
Please write your answers on paper (if you have none, then use a text editor of your choice). Do
not use the LTSA tool yet - just concentrate on the ideas for the moment; don't get bogged down in
the details for the syntax. Also proper instructions on how to bring up and use the tool will come
in the Lab Exercises.
(Ex 2.1 Magee & Kramer) For each of the following processes, give a Finite State Process
(FSP) description of the following Labelled Transition System graphs. Note that the
numbering of the states (except initial state 0) is not significant.
MEETING1.
1.
ANU - CECS - COMP2310/6310 TuteLab-1, 2014 http://cs.anu.edu.au/courses/COMP2310/practicals/Tu...
1 of 5 15/07/14 17:19
DOUBLE2.
PERSON3.
(Ex 2.2 Magee & Kramer) A variable stores values in the range 0..N and supports the
actions read[i] and write[j], where i is the variable's current value and j will become
the variable's new value. Assuming that the initial value of the variable is 0, model the
variable as the FSP process VARIABLE. For N=2, check that it can perform the actions given
by the trace:
write[2] -> read[2] -> read[2] -> write[1] -> write[0] -> read[0]
2.
Draw the resulting state machine (Labelled Transition System) diagram for VARIABLE (for
brevity, abbreviate read[0] for r[0], write[0] for w[0] etc).
3.
Write a version of the variable process above whose value can only be changed by at most
one from its current value. Use the when construct and call the FSP process INC_VARIABLE.
4.
(Optional, if there is time). Try Homework Exercise 3, below.5.
* (do this exercise on your own) A simple communication device can receive an (input)
action in[i] where i is either 0 or 1. If i was 1, it performs an ack action and returns to
its initial state. Otherwise, it performs a bye action and stops. Model this device using an
FSP process DEV.
Show your solution to your tutor when done. Worth 1 Prac Point.
6.
Laboratory Exercises
You will first need to customize your command line environment for this course. To do this,
simply add to your ~/.bashrc file the line:
source /dept/dcs/comp2310/login/Bashrc
Make sure the line is properly terminated (press the `Enter' key at the end of the line --
otherwise it won't work!). To ensure that this file always gets sourced when you log in, add to
your ~/.profile file the line:
source ~/.bashrc
ANU - CECS - COMP2310/6310 TuteLab-1, 2014 http://cs.anu.edu.au/courses/COMP2310/practicals/Tu...
2 of 5 15/07/14 17:19
COMP2310/COMP6310:
Concurrent and Distributed Systems
Semester 2 2014
Tutorial / Laboratory 2
Modelling Concurrency and Introduction to Java Threads
Objectives
To understand how concurrency can be modelled in FSP processes.
To have an appreciation of the state space explosion introduced by concurrency.
To understand further the phenomenon of interference between threads and race hazards
To learn basic elements of the Java Threads API, including starting threads.
Preparation
Before your session, please:
revise the Threads and Concurrency lectures and second half of Ch 2 and all of Ch 3 (of
Magee&Kramer.
have a look at the ThreadDemoTerm.java and CountDownTerm.java program and
familiarize yourself with their structure and use of the API.
revise the exercises in the previous session (including the Homework!), and get ready any
questions you might have from it.
remember to bring a pen and paper for the Tutorial Exercises.
Tutorial Exercises
Discuss any outstanding issues from the previous session (including Homework).1.
Consider the following process definitions:
   P = (a -> b -> P).
   Q = (c -> b -> Q).
   ||S1 = (P || Q).
   S2 = (a -> c -> b -> S2 | c -> a -> b -> S2).
Generate traces for ||S1 and S2. Can one generate a different trace from the other? Are the
processes the same? Why?
2.
(COMP6310 level) Use the following rules to show that P||Q is indeed the same as S2. Let A3.
ANU - CECS - COMP2310/6310 TuteLab-2, 2014 http://cs.anu.edu.au/courses/COMP2310/practicals/Tu...
1 of 5 15/07/14 17:09
and B denote the alphabets of processes X = x -> X' and Y = y -> Y' and C be the
intersection of A and B. Then:
X||Y = x -> (X' || Y')        , if x=y (and are in C)     (P1)
X||Y = (x -> (X' || y->Y')      
       |y -> (x->X' || Y'))   , if x,y are not in C       (P2)
X||Y = x -> (X' || y->Y')     , if y is in C and x is not (P3)
X||Y = y -> (x->X' || Y')     , if x is in C and y is not (P3')
(COMP6310 students: quote the process definiution expansion or rules used at each step, as is
donefor the examples in the lectures
The actions of a process repeatedly incrementing a counter variable can be modelled by
the FSP process
INCCTR = (loadCtr -> inc -> storeCtr -> rest -> INCCTR).
Note that here we do not model the value of the counter. Two such process operating in
parallel (updating the same counter, cf. Race.java) can be modelled as:
||INCCTR = (a:INCCTR || b:INCCTR).
Check that the following trace can be generated by ||INCCTR.
a.loadCtr -> a.inc -> b.loadCtr -> a.storeCtr -> b.inc ->
b.storeCtr
Hint: produce a sequenece of independent state transitions in a:INCCTR and
b:INCCTR that reproduces this trace.
1.
Assuming that the following actions represent the corresponding machine
instructions:
loadCtr: load contents of the address Ctr into register A
inc: increment register A
storeCtr: store contents of register A into memory location Ctr
rest: branch back to the loadCtr instruction.
and the value of Ctr was initially 0, what would it be after the above trace is executed
(assume that b:INCCTR updates register B instead of A).
2.
If there was the intention that every time a storeCtr action was performed, the value
of Ctr was incremented by 1, would ||INCCTR preserve this behaviour? What if the
event rest took 103 machine cycles (and the other events took only one)? What if it
took 109 cycles?
3.
4.
* Consider the following process definitions.
      P1 = (x1 -> P1).
      ||P1_2 = (a1:P1 || a2:P1).
      P2 = (x1 -> x2 -> P2).
      ||P2_2 = (a1:P2 || a2:P2).
      ||P2_3 = (a1:P2 || a2:P2 || a3:P2).
How many states do each of these processes have? If we defined in the above fashion
||Px_y, i.e. y independent process with x states combined in parallel, how many states
5.
ANU - CECS - COMP2310/6310 TuteLab-2, 2014 http://cs.anu.edu.au/courses/COMP2310/practicals/Tu...
2 of 5 15/07/14 17:09
would this process have?
Show your solution to your tutor when done. Worth 1 Prac Point.
Note: if you do Build -> compose for these processes in the LTSA tool, you can check
your answer on the Output pane!
(Ex 3.3 Magee & Kramer) Extend the model of the client-server program so that the server
can use two clients.
SERVERv2 = (accept.request -> service -> accept.reply -> SERVERv2).
CLIENTv2 = (call.request -> call.reply -> continue -> CLIENTv2).
||CLIENT_SERVERv2 = (CLIENTv2 || SERVERv2) / {call/accept}.
Hint: prefix the CLIENT prcesses and then do the renaming.
6.
Consider the following process definition:
COUNTDOWN (N=3)   = (start -> COUNTDOWN[N]),
COUNTDOWN[i:0..N] = ( when (i>0)  tick -> COUNTDOWN[i-1]
                    | when (i==0) beep -> STOP
                    | stop -> STOP).
The CountDownTerm.java program is meant to be an implementation of this. The main
program thread performs the stop action; it only performs this if the counter thread,
which performs the tick and beep actions, is not running:
if (c.counter.isAlive()) 
  c.stop(); // sets c.counter to null then prints "stop"
Why does this not prevent the erroneous behaviour ... tick tick stop beep? That is,
the program can produce the output:
  ...
  tick:(count=1)
  stop
  beep
What (if any) erroneous behaviour does the guard prevent?
Hint: in the above situation, the main thread performs the actions:
isAlive[1] -> ctr.write[0] -> print.stop
(call to c.counter.isAlive() returns 1, sets counter to null and prints stop) and the
counter thread performs the actions (for the last iteration):
ctr.read[1] -> print.beep -> threadExit (i.e. reads counter as non-null,
prints beep and terminates)
Note that isAlive() will only return 0 after threadExit is performed. What interleaving
of these actions can cause the above behaviour?
7.
Laboratory Exercises
ANU - CECS - COMP2310/6310 TuteLab-2, 2014 http://cs.anu.edu.au/courses/COMP2310/practicals/Tu...
3 of 5 15/07/14 17:09
(Ex 3.1 Magee & Kramer) In the LTSA tool, verify that the processes ||S1 and S2 are
identical, i.e. that they generate equivalent LTS.
   P = (a -> b -> P).
   Q = (c -> b -> Q).
   ||S1 = (P || Q).
   S2 = (a -> c -> b -> S2 | c -> a -> b -> S2).
   ||S2 = S2
Hint: load each of the two processes in separate tools. Build -> Compile and Build ->
Compose each. Now Build -> Minimize ||S2.
1.
In the tool with ||S1, select Options -> Multiple LTS in Draw Window. In the Draw pane,
select all processes (you will need to drag the top one away to see the others - see the
relevant section of Help -> Manual for more information). Run ||S1 and observe the
transitions in the component and combined LTS diagrams.
2.
The CountDownTerm.java program has a race hazard caused by the stop action being
performed by the the main thread. Rewrite the program so that the start and stop actions
are performed by the counter thread.
Hint: remove the code for starting, sleeping and stopping in main(). The creation and
starting of counter is moved to the constructor. The run() method initially calls
(CountDownTerm's) start(); it calls stop() after t iterations, where t is a random number
in the range 0..N+1 -- you can reuse the code in main() to setup the random number for
this purpose).
You will notice now that the main thread stops much earlier, but the java CountDownTerm
process does not terminate until the counter thread does.
3.
* The program ThreadDemoTerm.java uses a sub-class of the Thread class called
ThreadTerm to create a thread. Rewrite the program in the alternate way in which a
thread may be created, i.e. by a class which implements the Runnable class.
Hint: compare the 2 ways of starting threads on p15-16 of Lectures 2-3.
Show your solution to your tutor when done. Worth 1 Prac Point.
4.
Extend ThreadDemoTerm.java so that it creates three threads.5.
Homework
Implement a version of CountDownTerm.java which uses a sub-class of theThread class to
create the thread. Hint: Initialize counter = this; in the constructor, rename start() to
startE() (this will also need to be modified) and stop() to stopE(). As it is in another
class, main() will have to access N etc through the object c.
1.
Verify the second part to your answer in Tutorial Exercise 7 by removing the guard if
(c.counter.isAlive()) in CountDownTerm.java and running the program.
2.
Model the situation in Tutorial Exercise 7 by as a composite FSP process ||COUNTDOWNEND.3.
ANU - CECS - COMP2310/6310 TuteLab-2, 2014 http://cs.anu.edu.au/courses/COMP2310/practicals/Tu...
4 of 5 15/07/14 17:09
COMP2310/COMP6310:
Concurrent and Distributed Systems
Semester 2 2014
Tutorial / Laboratory 3
Shared Objects, Monitors and Condition Synchronization
Objectives
To improve your understanding of the modelling of mutual exclusion.
To understand how how monitors may be modelled as FSP process and how to implement these in Java.
To understand what are the appropriate condition synchronizations associated with a monitor.
To understand semaphores and their relation with condition synchronization.
To understand more deeply the semantics of synchonized objects and methods.
Preparation
Before your session, please:
revise the exercises in the previous session (including the Homework!), and get ready any questions you
might have from it.
read through these exercises to familiarize yourself with their content.
revise the corresponding lecture notes and corresponding chapters (3, 4 and 5) of the Magee&Kramer. In
particular, ||RESOURCE_SHARE (lect 4, slide 11) and ||SEMADEMO (lect 8, slide 4) - process prefixing for
shared resources under || composition for Tute Q2.2; and the implementation of the Buffer monitor
(lect 8, slide 11) for Tute Q4.
follow this up by studying with the LTSA tool some examples from Chapters 4 & 5 of the textbook.
Remember, to check the `Multiple LTS in Draw Window' option and to use Composite to compile a
composite process. Suggested examples are Garden_lockvar, Counter_lockvar, Carpark, SemaDemo
and BoundedBuffer.
remember to bring a pen and paper for the Tutorial Exercises.
Tutorial Exercises
Discuss any outstanding issues from the previous session (including Homework).1.
ANU - CECS - COMP2310/6310 TuteLab-3, 2014 http://cs.anu.edu.au/courses/COMP2310/practicals/Tu...
1 of 4 15/07/14 17:10
(Ex 4.3 Magee & Kramer) A central computer with a number of terminals is used to reserve seats in a
concert hall. A seat, initially unreserved, can be reserved (only once) and respond to the respective
query action corresponding to its state:
  SEAT = SEAT[0],    // unreserved
  SEAT[res: 0..1] 
     = ( query[res] -> SEAT[res]
       | when (res==0) reserve -> SEAT[1] // now reserved 
       | when (res==1) reserve -> ERROR   // error of being reserved twice
       ).
  range S = 0..1
  ||SEATS = (forall [s:S] seat[s]:SEAT).            
At each terminal, a clerk can choose[s:S] any of the existing S seats and then makes a query on whether
it is reserved; is not reserved, they can then reserve it. However, a double-booking from another
terminal must be avoided! This requires the clerk to acquire a lock before the query on the seat and
release it after either reserving it or finding out it is already reserved.
Model in the FSP process TERMINAL the actions of a clerk at the terminal.
Hint: to query if the chosen seat s is reserved can be modelled by the choice
(seat[s].query[0] -> ... | seat[s].query[1] -> ...).
1.
Using the process LOCK = (acquire -> release -> LOCK) from lectures, compose a system
CONCERT_HALL for a concert hall booking system with 2 terminals.
Hint: use prefix labelling for the LOCK and (composite) SEATS processes so that they can `talk' to
both terminals. As in the ||COUNTER example from lectures, it is not actually the prefixed LOCK
process that enforces mutual exclusion, it is the acquire ... release discipline in TERMINAL.
2.
2.
* (Ex 5.4 Magee & Kramer) The dining savages. A tribe of savages eats communal dinners from a large pot
which can hold M servings of the meal of the day. When a savage wants to eat, he/she gets a serving
from the pot if it is not empty, otherwise they wait. When the pot is empty, the cook refills the pot with
M servings. The (unconstrained) behaviour of each savage and the cook can be described by the
following FSP processes:
  SAVAGE = (getServing -> SAVAGE).
  COOK = (fillPot -> COOK).
Model the behavior of the pot as an FSP process POT which would impose the respective constraints on
the savage and cook processes. Specify a composition of the whole system.
Hint: POT will have M states.
Show your solution to your tutor when done. Worth 1 Prac Point.
3.
(Ex 5.1 Magee & Kramer) A single-slot buffer may be modelled by
ONEBUF = (put -> get -> ONEBUF).
Outline the code in a Java class OneBuf that implements this as a monitor.
Hint: for a buffer containing a single integer, it would have a void put(int c) method which could
only proceed when the buffer was empty and an int get() method which could only proceed if the
buffer had a value in it. You could use the general buffer implementation BufferImpl.java as a template,
replacing the buff array with a single character and count with a boolean variable.
4.
(Ex 5.2 Magee & Kramer) Outline how your would re-write the OneBuf to use the Semaphore class from
lectures. It can be used as follows
sema = new Semaphore(v); // create new semaphore with value v (=0,1) 
sema.down();             // must wait if value is 0 
sema.up();               // release other threads waiting on this semaphore 
5.
ANU - CECS - COMP2310/6310 TuteLab-3, 2014 http://cs.anu.edu.au/courses/COMP2310/practicals/Tu...
2 of 4 15/07/14 17:10
COMP2310/COMP6310:
Concurrent and Distributed Systems
Semester 2 2014
Tutorial / Laboratory 4
Deadlock
Objectives
To consolidate your understanding of parallel composition and mutual exclusion and
monitors.
To improve your understanding of Peterson's algorithm (low-level modelling of mutual
exclusion).
To improve your understanding of how deadlock arises.
Preparation
Before your session, please:
revise the exercises in the previous session (including the Homework!), and get ready any
questions you might have from it.
read through these exercises to familiarize yourself with their content.
revise the corresponding lecture notes and corresponding chapters (5, 6) of the
Magee&Kramer.
follow this up by studying with the LTSA tool some examples from Chapters 5 and 6 of the
textbook. Remember, to check the `Multiple LTS in Draw Window' option and to use
Composite to compile a composite process. Suggested examples are SYS (printer-scanner),
DINERS (including the deadlock free version), SingleLaneBridge (including the congested
and deadlock versions_.
remember to bring a pen and paper for the Tutorial Exercises.
Tutorial Exercises
Discuss any outstanding issues from the previous session (including Homework). Raise any
questions related to Assignment 1 and discuss.
1.
* (Ex 6.2 Magee & Kramer) Consider the Dining Philosopher problem.
PHIL = (sitdown -> right.get -> left.get
        -> eat -> left.put -> right.put  -> arise -> PHIL).
FORK = (get -> put -> FORK).
2.
ANU - CECS - COMP2310/6310 TuteLab-4 2014 http://cs.anu.edu.au/courses/COMP2310/practicals/Tu...
1 of 3 15/07/14 17:21
||DINERS(N=5) = forall [i:0..N-1] 
               (  phil[i]:PHIL 
               || {phil[i].left, phil[((i-1)+N)%N].right}::FORK).
One solution permits only 4 philosophers to sit down at any time. Specify a BUTLER process
which, when composed with DINERS, implements this, i.e. permits a maximum of four
philosophers to engage in a sitdown action before an arise action occurs. Specify an
extended sysem, being the composition of the diners with the butler process.
Show your solution to your tutor when done. Worth 1 Prac Point.
Consider the modelling of Peterson's algorithm as an FSP process.
Model the algorithm in FSP, capturing the essential characteristics for mutual exclusion.
Hint: seperate FSP processes will model each thread. For thread 0, model the execution of
the critical and non-critical regions by the actions t0.crit.enter, t0.crit.exit and
t0.noncrit.enter and t0.noncrit.exit (and similarly for thread 1). The other actions
are the reading and writing of the turn, inCS0 and inCS1 variables. These can be
modelled as {t0,t1}::turn:VAR etc, using a simplified version of the VARIABLE process
for TuteLab-1.
  VAR  = VAR[0],
  VAR[i:0..1] = ( read[i] -> VAR[i]
                | write[j:0..1] -> VAR[j] ).
The if-else construct will be useful for modelling the sub-process corresponding to the
while loops, e.g.
... -> t0.turn.read[t:0..1] -> if (t==...) then ... else ...
Note that the processes modelling each thread share no common actions; they however
communicate though the shared variables {t0,t1}::turn:VAR etc, i.e. after
t0.turn.write[1], when thread 1 offers the choice of actions t1.turn.read[t:0..1], it
will only be able to engage in t1.turn.read[1], i.e. t==1.
Finally, while thread 0 never engages in inCS1.write[0..1] or turn.write[0], it must
have its alphabet extended to include these: otherwise it cannot prevent
3.
ANU - CECS - COMP2310/6310 TuteLab-4 2014 http://cs.anu.edu.au/courses/COMP2310/practicals/Tu...
2 of 3 15/07/14 17:21
COMP2310/COMP6310:
Concurrent and Distributed Systems
Semester 2 2014
Tutorial / Laboratory 5
Safety and Liveness
Objectives
To improve your understanding of Peterson's algorithm (low-level modelling of mutual
exclusion).
To improve your understanding of safety and progress properties, and the underlying
issues in concurrency.
To improve your understanding of ow these properties can be implemented in a monitor.
Preparation
Before your session, please:
revise the exercises in the previous session, and get ready any questions you might have
from it.
read through these exercises to familiarize yourself with their content.
revise the corresponding lecture notes and corresponding chapters (7) of the
Magee&Kramer.
follow this up by studying with the LTSA tool some examples from Chapters 7 of the
textbook. Suggested examples are SingleLaneBridge and ReadersWriters.
remember to bring a pen and paper for the Tutorial Exercises.
Tutorial Exercises
Discuss any outstanding issues from the previous session (including Homework). Raise any
questions related to Assignment 1 and discuss.
1.
(Ex 7.1 Magee & Kramer) What action trace violates the following safety property?
property PS = (a -> (b -> PS | a -> PS) | b -> a -> PS).
2.
(Ex 7.3 Magee & Kramer) Consider the car park example from Chapter 5:
CARPARKCONTROL(N=4) = SPACES[N],
SPACES[i:0..N] = ( when(i>0) arrive -> SPACES[i-1]
3.
ANU - CECS - COMP2310/6310 TuteLab-5 2014 http://cs.anu.edu.au/courses/COMP2310/practicals/Tu...
1 of 3 15/07/14 17:12
                 | when(i SPACES[i+1]
                 ).
ARRIVALS   = (arrive -> ARRIVALS).
DEPARTURES = (depart -> DEPARTURES).
||CARPARK = (ARRIVALS || CARPARKCONTROL(4) || DEPARTURES).
Specify a safety property that asserts that the car park does not overflow. Specify a
progress property which asserts that cars eventually enter the park. If car departure has
lower priority than car arrival, does starvation occur? Specify an FSP composition with
action priority that you could use to check this (via LTSA's Check Safety facility).
* Consider the FSP model of Petersen's algorithm that we developed in TuteLab-4. Recall
that the trace for thread 0 through the cycle, assuming it got immediate access to its critical
region, would:
t0.noncrit.enter -> t0.noncrit.exit -> 
t0.inCS0.write[1] -> t0.turn.write[1] ->            
t0.inCS1.read[0] -> t0.turn.read[0] ->
t0.crit.enter -> t0.crit.exit -> t0.inCS0.write[0]
and similarly for Thread 1.
What sequence of events (actions) would indicate that mutual exclusion was violated
in the system?
1.
Specify an FSP safety property which expresses that mutual exclusion is preserved.
Write a composition of that property with the other processes; why is it necessary to
extend the alphabets for thread 0 and thread 1?
2.
Describe a sequence of events (actions) that would indicate that one thread is being
starved of entry into its critical region?
3.
Specify an FSP progress property which states that, once a thread is waiting to enter
its critical region, it will eventually be allowed to enter.
4.
Show your solution to your tutor when done. COMP2310 students are expected to complete
the first 3 parts, COMP6310 students all 4. Worth 1 Prac Point.
4.
Laboratory Exercises
Verify using the LTSA tool that the CarPark safety and progress properties are kept.1.
Verify using the LTSA tool that your model of Peterson's Algorithm satisfies its safety and
liveness properties. (if not already done so). What does this prove about (our model of)
Peterson's Algorithm?
2.
* Time to start driving some applets! Download and unzip the Book Applets zip file. Go to3.
ANU - CECS - COMP2310/6310 TuteLab-5 2014 http://cs.anu.edu.au/courses/COMP2310/practicals/Tu...
2 of 3 15/07/14 17:12
COMP2310/COMP6310:
Concurrent and Distributed Systems
Semester 2 2014
Tutorial / Laboratory 8
Message Passing
Objectives
To improve your understanding of of how message passing can be implemented using
monitors, and how timeouts may be added to receive operations.
To further your understanding of a synchronous messaging.
To improve your understanding of how message passing may be used implement
concurrent programs - as an alternative to monitors.
Preparation
Before your session, please:
read through these exercises to familiarize yourself with their content.
revise the corresponding lecture notes and corresponding chapter (10) of the
Magee&Kramer.
follow this up by studying with the LTSA tool some examples from Chapters 10 of the
textbook. Suggested examples are AsyncMsg, MsgCarPark, EntryDemo, and Program 10.8.
Tutorial Exercises
ANU - CECS - COMP2310/6310 TuteLab-8 2014 http://cs.anu.edu.au/courses/COMP2310/practicals/Tu...
1 of 4 15/07/14 17:14
* (Ex 10.3 Magee & Kramer) Consider the definition of a port for asynchronous messaging
with buffering of up to N=3 messages:
const NM = 4
range M = 0..NM       // messages with values up to 4
set S = {[M],[M][M]} // queue of up to three messages
PORT                 // empty state, only send permitted
    = (send[x:M]   -> PORT[x]),
PORT[h:M]            // one message queued to port
    = ( send[x:M]  -> PORT[x][h]
      | receive[h] -> PORT),
PORT[t:S][h:M]       //two or more messages queued to port
    = ( send[x:M]  -> PORT[x][t][h]
      | receive[h] -> PORT[t]).
A message passing system with a producer and a consumer can be defined as follows:
PRODUCER = PRODUCER[0],
PRODUCER[i:M] = (send[i] -> PRODUCER[(i+1)%(NM+1)]).
CONSUMER = (receive[i:M] -> CONSUMER).
||PROD_CONS = (PRODUCER || PORT || CONSUMER).
Modify this system so ttat the producer may only send up to N messages before it is blocked
by waiting for the consumer to receive a message. It must use the unmodified PORT process
above in order to do this. Verify using the LTSA tool that the system prevents queue
overflow (for N=3).
Show your solution to your tutor when done.
Hint: you can use an `empty' message to get the desired protocol: the consumer sends
`empty' messages asynchronously to the producer; it can send at most N of these before
going into a state where it must receive the (main) message from the producer before
sending another empty message. A port for (empty) acknowledge messages may be simply
modelled as:
const N = 3
PORT_E = PORT_E[0],
PORT_E[i:0..N]
    =  ( when (i < N) send -> PORT_E[i+1]
       | when (i > 0) receive -> PORT_E[i-1] ).
1.
Laboratory Exercises
The following assume that you have downloaded the Book Applets zip file as described in
TuteLab 5. The relevant sub-directory is concurrency/message.
* Implement a synchronous message passing solution of the Dining Savages problem of
TuteLab-3. (see the answers for the monitor solution). Model the Savage (Cook) as a thread
which repeatedly tries to send a getServing (fillPot message to the Pot thread, which
1.
ANU - CECS - COMP2310/6310 TuteLab-8 2014 http://cs.anu.edu.au/courses/COMP2310/practicals/Tu...
2 of 4 15/07/14 17:14