Transcript public class PlatformAccess

START
Translation of
process algebras to
Java
Paul Bilokon
Samuel Lau
Andrew Roberts
Introduction




Modelling
Finite State Processes (FSP)
Threads and monitors
Mission statement
Modelling




Simplicity: abstraction from
irrelevant details
Determination of relevant
factors
Predict long term behaviour
“What if” scenarios
Finite State Processes (FSP)




“A process calculus is a small language that allows us to give precise
descriptions of the essential properties of concurrent and communicating
programs.”
FSP is a process calculus.
FSP is finite, so we can do proofs, safety checks, etc.
Example:
SUPREMA_GROUP = (enter -> present -> leave ->
SUPREMA_GROUP).
AUDIENCE = (yawn -> sleep -> wakeUp -> AUDIENCE).
||FUN = (SUPREMA_GROUP || AUDIENCE).

Wishful thinking:
yawn  sleep  enter  wakeUp  present  leave…
Mission statement







Investigate the relationship between FSP and Java
Restrict the subset of FSP under consideration
Consider examples, develop the theory
Discover interesting patterns and methods
Formalize it, if possible, using mathematical notation
Evaluate the results. Refine the model, if necessary
Could we use these results to build an automated
FSP to Java translator? Would this be a useful tool?
Translation







The action prefix and simple processes
Guarded actions
Choice
Variables
Simple parallel composition
Parallel composition of dependent processes
Other FSP constructs
Quick FSP Recap
Actions
P1 =
(a1 -> a2 -> … -> an -> STOP).

FSP Processes  Java classes
FSP Actions  Java Methods

Guards  While-wait loop

Choice  External factor allows
choice

Guarded Actions
P = (when(B) a -> STOP).
Choice
DRINKS_MACHINE =
(red -> coffee -> DRINKS_MACHINE
|blue -> tea
-> DRINKS_MACHINE).
Variables
range T = 0..5

FSP Constructor  Java
constructor

STORE has a state
variable, represented in
Java as a field variable

‘put’ has an action variable,
represented as a parameter
for the put method
STORE = STORE[0],
STORE[i:T]=(put[i:T]->STORE[i]).
public class Store {
private int i;
public Store() {
this.i = 0;
}
synchronized public int
put(int i) {
this.i = i;
}
} //END class
Simple parallel composition
||COMPOSITION = (a1 || a2 || … || an),
No shared actions!
public class Composition {
protected A1 _a1;
protected A2 _a2;
…
protected An _an;
public Composition() {
new Thread(_a1 = new A1());
new Thread(_a2 = new A2());
…
new Thread(_an = new An());
}
}

Instantiate and start threads

Non-simple composition
uses similar composite class
Composition: caller/callee pattern




Two shared actions: designate one the caller and the other
callee
Caller is part of a thread
Calls callee method, which is part of a monitor
Only works with 2 shared actions!
public class Caller implements
Runnable {
public run() {
…
Callee.a();
…
}
}
public class Callee {
synchronized public void a()
{
//do something
}
}
Composition: semaphores


Uses semaphores – not intuitive Java
Works for many shared actions – can become complex!
BILL = (play -> meet -> eat -> STOP).
BEN = (work -> meet -> sleep -> STOP).
public class Bill implements
Runnable {
public void run() {
play();
release(A);
acquire(B);
eat();
}
} //END class
public class Ben implements
Runnable {
public void run() {
work();
acquire(A);
release(B);
sleep();
}
} //END class
General composition of processes

P1 = (… ->
P2 = (… ->
…
P(n – 1) =
Pn = (… ->
a -> … -> STOP).
a -> … -> STOP).
(… -> a -> … -> STOP).
a -> … -> STOP).

Method 1. Extend the semaphore method.
For n shared methods, (2n-2) semaphores required.
Initialize to an ‘acquired’ state.

Method 2. Synchronization object.
Uses Java’s inbuilt synchronization.
This object is a monitor and counts in the shared actions. Once
they have all ‘reported in’ it will let all the threads continue.
Case study: Roller Coaster






Apology 
Monitors and threads revisited
Caller/callee pattern
Problem: parameters or return values?
Problem: action order
Well-formed FSP
Caller/callee pattern
Only one type of process interaction –
monitor/thread.
 In general, this is the most common form of
process communication.
 ‘Directionality’ is an important criterion for
preferring this design pattern. E.g. the thread
Passengers tells the monitor Controller that
a newPassenger has arrived.

Problem: parameters vs return




COASTERCAR has action
getPassenger[i:1..MCar] with a ‘free’ variable
(cf. Prolog).
CONTROLLER has action
getPassenger[carSize]. The variable carSize is
bound.
A method of Coastercar (thread) to be called from
Controller (monitor)?
Use return values instead:
synchronized public int getPassenger()
in Controller.
Problem: action order


PLATFORMACCESS =
(arrive -> depart -> PLATFORMACCESS).
PLATFORMACCESS =
({arrive -> depart} -> PLATFORMACCESS).
public class PlatformAccess {
public boolean arrive_done =
false;
synchronized public void
arrive() {
while (arrive_done) wait();
arrive_done = true;
}
synchronized public void
depart() {
while (! arrive_done) wait();
arrive_done = false;
}
}
Well-formed FSP
Is this translation ‘natural’?
 Does Java ‘match’ FSP?
 Is it easy for an automated FSP2Java program
to spot this?
 Could ask the user to re-write the FSP to
comply with a well-formed FSP standard.
 For example…

Well-formed FSP II

PLATFORMACCESS =
(arrive -> depart -> PLATFORMACCESS).

PLATFORMACCESS = PLATFORMACCESS[0],
PLATFORMACCESS[i:0..1]
= (when(i=0) arrive->PLATFORMACCESS[1]
|when(i=1) arrive->PLATFORMACCESS[0]
).
Conclusions





What is a good translation?
A subset of FSP
Limitation
Automatic Translation
Further work
 FSP modification
 Validation of translation
 Rest of FSP
What is a good translation?
The factors are:
 Complexity
 Readability
We would like to read and understand the Java
code easily.
We have found out that the Caller/Callee pattern is the
most intuitive. However, this pattern cannot be used for
more than 2 shared actions.
Limitation



Caller/Callee pattern: Monitor?
Thread?
Data flow between processes can
be difficult to translate. One
solution is to rewrite the FSP and
merge the actions.
A FSP can send more than 1 item
of data but Java cannot.
Automatic translation




Given more time, we may write a
program that automatically
translates FSP to Java.
Closer relation between FSP and
Java code
Humans have benefit of context,
which will effect implementation
Is this feasible?
FSP modification


We may rewrite the FSP in
some circumstances.
Aim: Make the translation
more effective and concise.
Validation of translation



We are able to translate a
large subset of FSP.
But how can we prove that
the Java code actually
corresponds to the FSP
given?
Very difficult: Logic
reasoning?
I Want More!
You are dazzled, fascinated, intrigued… where do you
want to go today?

Prof. Magee’s home page:
http://www.doc.ic.ac.uk/~jnm/

Our project home page:
http://www.doc.ic.ac.uk/~pb401/
Suprema/


Web articles and project
report.
Test yourself – try Q&A!
That’s all, folks!
http://www.doc.ic.ac.uk/~pb401/Suprema