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):

Extensions

See the course Assessment page. Late penalties are as follows:

How LatePenalty 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

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: 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:

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: To return to default behavior: Similarly for trying to reproduce a previous simulation, which used a seed of say 525: 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