COMP2310/COMP6310:
Concurrent and Distributed Systems
Semester 2 2012
Assignment 1
A Self-service Gas Station
Deadline: 17:00 on
Thursday 06 Friday 07 September
(Please report any errors, omissions and ambiguities
to the course lecturer)
(Amendments to this document after its release in
non-
draft will be marked in
blue)
This assignment is worth 22% of your total course mark. It will be
marked out of 44.
Submission
This assignment must be submitted electronically. This can be done
using the following commands (according to your enrollment):
submit comp2310 ass1 ass1.zip
submit comp6310 ass1 ass1.zip
Extensions
See the
course Assessment page.
Late penalties are as follows:
| How Late | Penalty from 44 Marks |
|---|
| less than 1 hour | -2 |
| between 1 and 6 hours | -4 |
| between 6 and 24 hours (1 day) | -8 |
| between 24 and 48 hours (2 days) | -16 |
| between 48 and 72 hours (3 days) | -32 |
| more than 72 hours (4 days) | -64 (forget it!)
|
Objectives
- To model a concurrent system of moderate size, and its
safety and liveness properties.
- To implement the model using threads with monitors.
System Description
(based on Magee&Kramer Ex8.2-8.3)
Simple system:
A self-service gas station has a cashier and a pump. Two customers can
each pay for up to T units of petrol. After a
customer pays, the cashier starts the pump to dispense the
corresponding number of units of gasoline for that customer, and the
customer receives the gas. Note that it should be possible for
the second customer to pay in-between the first
customer's pay and gas actions.
The CUSTOMER process also
models the number of units x of gas that their car
is holding (initially 0). After a receive gas action, they may
engage in up to 0<=d<=x
drive actions before the next pay action, which may not
be for more than T - x + d units.
Include in the model that possibility that the
customer may not receive the correct amount of gas and goes into a
dissatisfied state (ERROR), i.e.
for a simplified CUSTOMER
which did not model units of gas in the tank
or engage in drive actions
const T = 2 // size of tank
range A = 1..T // amount of money or gas
CUSTOMER = ( pay[a:A] -> gas[x:A] -> if (x==a) then CUSTOMER else ERROR ).
Intermediate system: Extend the system to have N
cars and M pumps. It must be possible for each pump to be
servicing a car concurrently. Specify an FSP safety
property, FIFO that
states that customers are served in
the order which they pay.
Specify a composition of
this property with your model -
it is expected that it will violate it (FIFO implies loss of
concurrency for multiple pumps). However, your model
should operate consistently with FIFO, i.e. not deadlock when
composed with a non-property version of it.
Extended System (part 1): The N customers are
divided into two groups: those that always buy standard
petrol (1..NS), and those that always buy E10 petrol
(NS+1..N),
where 1 ≤ NS ≤ N).
The station has both kinds of petrol; however, due to funding limitations,
all pumps must be switched to one kind or another at any time.
Once an E10 customer makes a payment, the cashier can only accept
new payments for E10 customers until all current E10 customers have
received their gas (and conversely for standard petrol customers).
Extended System (part 2):
This now leads to a liveness or progress problem
(for N-NS>1): once an E10 customer
enters the station and causes the switch to the E10 pumps,
a non-E10 customer may never have their pay action
accepted by the cashier, due to subsequently arriving E10 customers!
Specify FSP progress properties that each kind of
customer will always be eventually served, and
write an FSP composition that shows that
(using action priority) that this system does indeed
violate progress.
Extend the system to provide a solution to this problem;
you will probably need to extend the customers to make a req
action before their payment. Show that this system
does not violate this progress property.
Requirements
The ass1.zip file that you submit must contain the following:
- a plain text file called ReadMe.txt
containing:
- a disclaimer with your name and student number
stating what (if any) contributions from others
(not including course staff) are in your submission. Note that
significant contributions may require a revision of your final mark,
as this is intended to be an individual assignment.
- the names of all component files and their purpose (note that
intermediate or junk files should not be included in your submission).
- design decisions made in your modelling (FSP code) of the
system, and any pertinent observations of the model's properties
etc (as produced by the LTSA tool). It should also name the
parallel compositions corresponding to each level, so that
another person (i.e. your tutor!) will easily be able to compile
and check your model.
- design decisions made in your implementation of the model.
- any notable deficiencies, bugs, or issues with your
model or code (e.g. not satisfying a safety property).
- (optional, not assessed) any feedback on what you found helpful
in doing this work, or what from the course could be improved in
helping you to carry out this work.
A template file is available from here.
All files must unzip into the current directory,
i.e. construct the zip file via a command like:
zip ass1.zip ReadMe.txt GasStation.lts RunGasStation.java ...
- an FSP file called GasStation.lts containing a
description of your model. The model should be free from
deadlock and always be able to make progress.
- a file called RunGasStation.java; this contains a
main() method to start and run the simulation.
The classes implementing the gas station should be in separate files.
After the command javac RunGasStation.java, the command:
java -ea RunGasStation T N M NS
should run the simulation with maximum gas amount T (default value 2),
N customers (default value 2)
and M pumps (default value 1),
with NS standard petrol customers (default value N).
- other Java files implementing the gas station model. Each customer
must be implemented by a separate thread (more threads can be optionally
used for other parts of the system). In general you should follow the
systematic approach in translating models to safe concurrent code
that we have developed in this course (i.e. with the use of monitors),
unless there is a good reason to deviate from this - in which case, this
should be explained in ReadMe.txt).
When your code completes an action (from your FSP model), it
must signify this by calling the corresponding event logging method in
the provided
GasStationEvent class. If the monitor is also involved in this action,
the monitor method should make the call (to ensure that the
recorded series of actions on the program output are in exactly the same
order). After performing the action, the active threads should call
the sleepEvents() method: this will cause the thread to sleep
for a random interval, which is needed to get sufficient
interleaving between the actions of different threads
(why is it a bad idea to do the sleeps inside the monitor?).
You can get
GasStationEvent.class from here.
On the CS student system, an up-to-date version of the compiled file
will be available through your CLASSPATH environment; you
will only need a copy of the class file if you are working externally.
Customer ids passed to GasStationEvent methods
must be in the range 1..N; pump ids must be non-negative.
Your program should not produce any output other than that generated
by GasStationEvent.
Your FSP and Java files should follow good programming style
conventions. In particular neat and consistent code layout and
adequate commenting in both are important. Your FSP compositions
corresponding to each stage should pass the default
Safety and Progress checks.
Appropriate defensive programming techniques such as the checking of
monitor invariants and invalid method parameters / return values
should be used; the
Java assert facility can be used for this. Where there is a
choice of actions that it can engage in, you should use
the Random class to select the events with equal
probability. To achieve both variability and reproducibility, the
random generator objects should be seeded by a call
to GasStation's
getSimRandomSeed() method
(this will produce a time dependent seed if
the shell environment variable $GasStationMaxEvent is not
set; otherwise it returns the numerical value of
$GasStationMaxEvent).
Your solution may attempt any of the three levels of the system;
please only submit for marking code for the highest level. Marks
will be allocated to the levels as follows:
Simple system: 60%
Intermediate system: 80%
Extended System: 90% (part 1), 100% (part 2)
The FSP and Java code do not have to be at the same level (in which
case this should be explained in ReadMe.txt); there will be
approximate weighting of 1/3 for the FSP and 2/3 for the Java,
except for the Extended System (where they will be 50% each).
A model/implementation at a particular level with serious flaws/bugs
cannot score better than one at the next lower level.
GasStation Event Class and Applet Version
The GasStationEvent class will provide some ways of controlling the
simulation. It will terminate the simulation after a certain number
of events, controlled by the Unix environment variable
GasStationMaxEvent (default value 30).
Sleep times for event calls will be random;
the seed to generate this can be set by the environment variable
GasStationEventSeed (if this is set to a value,
the sleep times will be repeatable between runs; this may be helpful
when debugging). You can adjust these values in the shell
which you run your program from, e.g. for the Bash shell:
export GasStationMaxEvent=50; java -ea RunGasStation
To return to default behavior:
Similarly for trying to reproduce a previous simulation,
which used a seed of say 525:
export GasStationEventSeed=525; java -ea RunGasStation
unset GasStationEventSeed
The `interface' for the class is as follows:
// construct, with respective station parameters
public GasStationEvent(int T, int N, int M, int NS);
// return the same random number seed that this object uses to its clients
public long getSimRandomSeed();
// sleep for some random time in 0..SleepFactor-1 ms
void sleepEvents();
// log respective gas station actions + their parameters in a consistent format
public void logPay (int cId, int amount);
public void logStart(int cId, int amount, int pumpId);
public void logGas(int cId, int amount, int pumpId);
public void logDrive(int cId);
public void logRequest(int cId);
public void logOtherEvent(String eventDescription);
An applet class for the Gas Station
is now available from here.
Please see the GasStation.html for a description of the applet
and instructions to use it
. This
may provide an alternate way of developing your program.
It however remains secondary to the terminal-based
method.
If there is something you don't like about it, feel free to fix / improve it
(you have all of the source code!) or simply stop using it.
Hints
- Suggest that you start coding your FSP model
from the simplest possible situation: a gas station with 1
simplified customer (i.e. the CUSTOMER code exactly as above)
and 1 pump. Check it in the LTSA tool to see if it does what you expect
and run it by your tutor (or me) if you are not sure.
- The start action will need to contain the customer id as
well as the amount. It can be assumed that the cashier never accepts a
new payment until the start action for the current one is
performed. Thus, the start action in a sense is a sub-action of
the corresponding pay action; taking advantage of this can
result in a simplified implementation.
- When there are more than 1 pumps, the start and
pay gas
actions will also need to include a pump id. The cashier may not start
a pump that is already in use, i.e. start any pump still with an
outstanding pay action associated with it.
- The modelling of the dissatisfied customer (above) will be useful
for checking that your station is dispensing gas correctly.
A corresponding check in your implementation is similarly useful.
- As you develop each FSP process, check its alphabet, LTS, and run it
to ensure that it is doing what you intended.
- Also compose your processes two at a time and check similarly.
Is the composition what you expected?
When there are multiple parallel processes in the program,
there is a pane along the tool bar to specify the Target Composition
for Run.
- Use the minimum values of the parameters
(e.g. T, N and M), at least for
initial testing. In particular, set T=1 for the
intermediate and advanced levels, as it plays no real role there.
The LTS display loses its usefulness after 10 or 20 states. If
you are not careful with your composition, you can actually
generate so many states that the tool `hangs' trying to compose
the system!
- Be careful with process indexing. For example:
P = P[0],
P[x:1..4] = in[v:1..4] -> P[v].
generates a process that immediately goes to the ERROR state!
- Note that the range of indexed events that can be accepted can be
variable, e.g.
P = P[0],
P[x:0..4] = in[v:x..4] -> P[v].
- When renaming indexed events, if you wish to preverve the value
of the index, use { a[x:1..N] / b[x] }; the expression {
a[1..N] / b[1..N] } does not.
- For those attempting the advanced level, it should be possible to
add (in parallel) processes to handle the 2 types of customers,
as this is actually just applying a constraint on the existing
system. Similarly the implementation of the rectification of the
progress policy can be implemented as a parallel process
applying further constraints.
- See Race.java for an example of
reading optional command line parameters, and
CountDownTerm.java
for an example of using Random.
- An internal monitor invariant checking method will also be convenient
for printing out monitor state upon each call for debugging.
- Your monitor may assume that the calling threads produce
the events in the required order.
- Sample traces:
Basic,
Inttermediate,
Extended