CA670 - Concurrent Programming Motivation

CSP
JCSP
CA670 - Concurrent Programming
Formal Specification & JCSP
David Sinclair
CSP
JCSP
Motivation
Developing concurrent programs is arguably more difficult than
developing sequential programs. A concurrent algorithm has to
consider, among other things:
• race conditions
• deadlock
• livelock
• fairness
• starvation
It could be argued that part of the problem is that we are forcing a
sequential view on something that is inherently concurrent.
If we take a concurrent view of the system being developed, with
its underlying mathematical theory, and model and implement the
system using this concurrent view, we could build provably correct
concurrent programs.
CSP
JCSP
Communicating Sequential Programs
Communicating Sequential Processes (CSP) was developed in the
late 1970’s and early 1980’s by Tony Hoare to model and reason
about concurrent systems.
CSP views a systems as a set concurrent processes that interact
with each other and their external environment via atomic
interactions called events. Events are instantaneous and the
alphabet of all events is written as Σ. Events can be observable by
the environment or they can be internal between processes. In this
case they may not be observable by the environment (user).
A CSP process can itself be composed on communicating
processes or processes that are a sequential series of events.
CSP
JCSP
Communicating Sequential Programs (2)
Each system that we model has its own set (alphabet) of events.
• A vending machine might have an event alphabet
{coin, drink, choc, d.button, c.button}.
• A counter might have an event alphabet {up, down, iszero}.
• A cheese shop might have an event alphabet
{{pay .x, change.x|x∈M} ∪
{cheddar .w , parmesan.w , brie.w |w ∈W }} where M is the set
of amounts of money and W is the set of weights used in the
cheese shop.
CSP
JCSP
STOP Process
The STOPA process is the simplest of all process. The STOPA
process does not engage with any events in the alphabet A. It can
be used to model a deadlocked process.
Two different deadlocked processes are distinguishable, even if they
do nothing. For example, given 2 vending machines,
VMα = {coin, drink}
VMβ = {coin, choc}
executing the processes STOPVMα and STOPVMβ , even though
both processes are not interacting with the environment, we know
that STOPVMα might have previously delivered a drink, but has
definitely not delivered a chocolate bar.
CSP
JCSP
Prefix
If x is an event and P is a process then
x →P
describes a process that first engages with event x and the behaves
as process P.
The process (x → P) must have the same alphabet as process P.
Given the alphabet VMα = {coin, drink}, a vending machine that
serves 2 customers before “breaking” (deadlocking) can be
modelled as:
coin → (drink → (coin → (drink → STOPVMα )))
CSP
JCSP
Recursion
Recursion can be used to model non-terminating processes.
To model a vending machine that can always deliver a drink in
response to a coin, we can write:
VMα = (coin → (drink → VMα))
Aside: Since → is right associative, we can drop the brackets from
the above and write:
VMα = coin → drink → VMα
CSP
JCSP
Choice
The notation
(x → P | y → Q)
denotes a process that in response to an event x proceeds as
process P and in response to an event y proceeds as process Q. As
before the alphabets of P and Q must be the same.
To model the vending machine with the alphabet
VM = {coin, drink, choc, d.button, c.button} capable of delivering
both drinks and chocolate bars in response to a coin and
appropriate button event, we can write:
VM = coin → ((d.button → drink → VM) |
(c.button → choc → VM))
CSP
JCSP
Choice (2)
We can extend this to more than 2 choices:
x → P | y → Q | ... | z → R
Each choice is guarded by an event. It is the event that determines
which choice is proceeded with. Therefore it would be wrong to
write:
(x → P) | (y → Q)
as the alternatives are no longer guarded. There are separate
operators for choosing nondeterministically between processes.
CSP
JCSP
Mutual Recursion
We can rewrite the vending machine specification using mutual
recursion.
VMδ = coin → (d.button → DRINK | c.button → CHOC )
DRINK = drink → VMδ
CHOC = choc → VMδ
Writing the specification in this way makes it clear that the
vending machine is in either one of two states, CHOC or DRINK .
CSP
JCSP
Concurrency
The notation
PkQ
denotes two processes P and Q evolving concurrently in lock-step
synchronisation, i.e. if P and Q share an event then they evolve to
that point in their specifications at the same time.
Consider a thirsty customer, THIRSTY , for the vending machine:
THIRSTY = coin → d.button → drink → THIRSTY
Then
THIRSTY k VM
specifies the thirsty customer interacting with the vending machine.
CSP
JCSP
Nondeterminism
A deterministic process is a process where whenever there is a
choice of events, the choice is determined by the environment of
the process, or in a weaker sense the environment can observe the
choice that has been made at the moment of the choice. A
nondeterministic process is a process where the environment
cannot influence or observe the choice of events whenever more
then one event is possible.
P uQ
denotes a process that can evolve either like P or Q and the choice
between each evolution is not controlled by the environment.
A machine that gives e1 and e2 coins as change for a e5 note
could be described as:
CNG = in.5n →
(out.1c → out.1c → out.1c → out.2c → CNG ) u
(out.2c → out.2c → out.1c → CNG )
CSP
JCSP
Nondeterminism (2)
The internal choice, or nondeterministic or, operator u is useful in
specifying the possible behaviours of a system. It is not used the
describe an actual implementation of a system as it would make
little or no sense for a system to be capable of two or more
arbitrary behaviours. The implementation of the change machine
CNG would use the number of e1 and e2 coins stored in the
machine to determine how to compose the e5 in change.
The external choice operator P 2 Q describe a process where the
environment can influence how the process will evolve based on the
very first action of P and Q. If the environment provides the first
action of P then the process evolves as P. If the environment
provides the first action of Q then the process evolves as Q. If the
first action of P and Q are the same, then the process selects
between P and Q nondeterministically.
(c → P 2 d → Q) = (c → P | d → Q)
(c → P 2 c → Q) = (c → P) u(c → Q)
if c 6= d
CSP
JCSP
Concealment
In cases where there are internal events in a system that we do not
want the environment to interact with, we can conceal these
events.
P\C
denotes a process that evolves as P but with the events in C not
visible to the environment. The events in C cannot be observed or
controlled by the environment.
CSP
JCSP
Communications
Two concurrent processes can communicate via a channel between
the two processes. The channel has no memory. Communication
on a channel is synchronous can only occur if a process outputs a
value on a channel when the other process inputs from the
channel. If the receiving channel is not ready to input the value
from the channel, then the sending process blocks until the
receiving channel is ready to input the value. Similarly, if the
sending channel is not ready to output the value to the channel,
then the receiving process blocks until the sending channel is ready
to output the value.
(c!v → P) k (c?x → Q(x)) = c!v → (P k Q(v ))
where c!v denotes outputting the value v on channel c, and c?x
denotes the inputting of a value from channel c and assigning the
value to x. Note that right-hand includes c!v as this is still an
observable event.
CSP
JCSP
Communications (2)
If two processes wish the communication between them to be
unobservable, then we use the concealment operator.
((c!v → P) k (c?x → Q(x))) \ C = (P k Q(v )) \ C
where C = {c.v | v ∈ α(c)}, c.v denotes the value v on channel c
and α(c) denotes the alphabet of channel c.
There is a special case where processes, called piped, have only one
input channel left and one output channel right. In this case they
can be composed as:
P>>Q
left
P
Q
right
CSP
JCSP
Traces
A trace of the behaviour of a process is a sequence of events that
the process has engaged in. A trace is denoted by a comma
separated sequence of events enclosed in angular brackets, e.g.
hx, y , zi
hxi - a singleton trace
hi - the empty trace
Operations on Traces
The concatenation of two traces s and t is denoted by s a t.
Concatenation obeys the following rules.
s a hi = hi a s = s
s a (t a u) = (s a t) a u
s 0 = hi
s n+1 = s a s n
where s n denotes n copies of s concatenated.
CSP
JCSP
Traces (2)
s A denotes the trace s restricted to the symbols in the set A.
hup, left, down, right, downi hup, downi = hup, down, downi
Restriction obeys the following rules.
hi A = hi
(s a t) A = (s A) a (t A)
s {} = hi
(s A) B = s (A ∩ B)
The head of a trace s is denoted by s0 and the tail of a trace s is
denoted by s 0 .
hx, y , zi0 = x
hx, y , zi0 = hy , zi
CSP
JCSP
Traces (3)
A∗ is the set of all finite traces, including hi, derived from the
symbols in A. This yields two definitions:
A∗ = {s | s A = s} or
A∗ = {t | t = hi ∨ (t0 ∈ A ∧ t 0 ∈ A∗ )}
The following rules follow from these definitions:
hi ∈ A∗
hxi ∈ A∗ ≡ x ∈ A
(s a t) ∈ A∗ ≡ s ∈ A∗ ∧ t ∈ A∗
Orderings are defined using prefixes.
s ≤ t = (∃ u.s a u = t)
The ≤ relation gives a partial ordering on traces where the least
element is the empty trace, hi.
CSP
JCSP
Traces (4)
Orderings obeys the following rules:
hi ≤ s
s≤s
s≤t∧t≤s⇒s=t
s≤u∧u≤t⇒s≤t
(hxi a s) ≤ t) ≡ t 6= hi ∧ x = t0 ∧ s ≤ t 0
s≤u∧t≤u⇒s≤t∨t≤s
t ≤ u ⇒ (s a t) ≤ (s a u)
s ≤ t ⇒ (s A) ≤ (t A)
f (s) ≤ f (t) whenever s ≤ t
s is a subsequence of t, denoted s in t if:
s in t = (∃ u, v .t = u a s a v )
and hence
(hxi a s) in t ≡ t 6= hi ∧ ((t0 = x ∧ s ≤ t 0 ) ∨ (hxi a s) in t 0 )
CSP
JCSP
Traces (5)
The length of a trace t, denoted #t, is defined by:
#hi = 0
#hxi = 1
#(s a t) = #s + #t
The length operator obeys the following rules:
#(t (A ∪ B)) = #(t A) + #(t B) − #(t (A ∩ B))
s ≤ t ⇒ #s ≤ #t
#(t n ) = n × (#t)
The number of occurrences of a symbol x in trace s is defined as:
s ↓ x = #(s {x})
CSP
JCSP
Traces (6)
If s ∈ traces(P) then P/s, P after s, is a process that evolves as P
after P has engaged in all the events recorded in s.
Given
VMα = coin → drink → VMα
then
VMα/{coin} = drink → VMα
VMα/{coin, drink} = VMα
The after operator obeys the following rules:
P/hi = P
P/hs a ti = (P/s)/t
(x : B → P(x))/hci = P(c)
traces(P/s) = {t | s a t ∈ traces(P)}
provided c ∈ B
provided s ∈ traces(P)
CSP
JCSP
Process Laws
Prefixes obey the following law:
(x : A → P(x)) = (y : B → Q(y )) ≡ (A = B ∧ ∀ x ∈ A.P(x) = Q(x))
Parallel composition, P k Q, obeys the following laws:
PkQ=QkP
P k (Q k R) = (P k Q) k R
P k STOPαP = STOPαP
(x : A → P(x)) k (y : B → Q(y )) = (z : (A ∩ B) → (P(z) k Q(z)))
CSP
JCSP
Process Laws (2)
Internal choice, P u Q, obeys the following laws:
P uP = P
P uQ = Q uP
P u(Q u R) = (P u Q) u R
x : B → (P(x) u Q(x)) = (x : B → P(x)) u(x : B → Q(x))
P k (Q u R) = (P k Q) u(P k R)
(P u Q) k R) = (P k R) u(Q k R)
External choice, P 2 Q, obeys the following laws:
P 2P = P
P 2Q = Q 2P
P 2(Q 2 R) = (P 2 Q) 2 R
P k STOP = P
CSP
JCSP
Process Laws (3)
(x : A → P(x)) 2(y : B → Q(y )) =
(z : (A ∪ B) → (if z ∈ (A − B) then P(z)
else if z ∈ (B − A) then Q(z)
else if z ∈ (A ∩ B) then (P(z) u Q(z))))
P 2(Q u R) = (P 2 Q) u(P 2 R)
P u(Q 2 R) = (P u Q) 2(P u R)
Concealment, P \ C , obeys the following laws:
P \ {} = P
(P \ B) \ C = P \ (B ∪ C )
(P u Q) \ C = (P \ C ) u(Q \ C )
STOPA \ C = STOPA−C
(x → P) \ C = x → (P \ C )
if x ∈
/C
=P\C
if x ∈ C
CSP
JCSP
Generating Traces
The traces of a process are defined by the following:
traces(STOP) = {hi}
traces(c → P) = {hi} ∪ {hci a t | t ∈ traces(P)}
traces(c → P | d → Q) = {t | t = hi ∨ (t0 = c ∧ t 0 ∈ traces(P)) ∨
(t0 = d ∧ t 0 ∈ traces(Q))}
traces(P k Q) = {t | (t αP) ∈ traces(P) ∧ (t αQ) ∈ traces(Q) ∧
t ∈ (αP ∪ αQ)∗ }
(P k Q)/s = (P/(s αP)) k (Q/(s αQ))
traces(P u Q) = traces(P) ∪ traces(Q)
(P u Q)/s = Q/s
if s ∈ (traces(Q) − traces(P))
= P/s
if s ∈ (traces(P) − traces(Q))
= (P/s) u(Q/s) if s ∈ (traces(P) ∩ traces(Q))
CSP
JCSP
Generating Traces (2)
traces(P 2 Q) = traces(P) ∪ traces(Q)
(P 2 Q)/s = Q/s
if s ∈ (traces(Q) − traces(P))
= P/s
if s ∈ (traces(P) − traces(Q))
= (P/s) u(Q/s) if s 6= hi and s ∈ (traces(P) ∩ traces(Q))
traces(P \ C ) = {t (αP − C ) | t ∈ traces(P)}
provided ∀ s : traces(P).¬diverges(P/s, C )
and diverges(P, C ) = ∀ n. ∃ s : traces(P) ∩ C ∗ .#s > n
i.e. diverges(P, C ) means that P can engage in
an unbounded sequence of hidden events from C
T
(P \ C )/s = ( t:T P/t) \ C where T = traces(P) ∩ {t | t (αP − C ) = s}
and T is finite and s ∈ traces(P \ C )
CSP
JCSP
Proofs
If P is an implementation of a system and S describes the
acceptable traces of the system (its specification), P satisfies S,
denoted P sat S, if every possible observation of P is described by
S.
Formally, P sat S if ∀ t, t ∈ traces(P) ⇒ S.
The following laws define the properties of the satisfies relation
L1
L2
L3
P sat true
If ∀ n.(P sat S(n)) then P sat (∀ n.S(n))
where S(n) is a predicate
If P sat S and S ⇒ T then P sat T
A special case of L2 is If P sat S and P sat T then P sat
(S ∧ T ).
CSP
JCSP
Proofs (2)
L4
L5
L6
S(t1 , t2 ) denote a specification with traces t1 and refusal set t2 .
If ∀ x ∈ B.(P(x) sat S(tr , x))
then (x : B → P(x)) sat (tr = hi ∨ (tr0 ∈ B ∧ S(tr 0 , tr0 )))
If P sat S(tr ) and s ∈ traces(P)
then (P/s) sat S(s a tr )
If F (X ) is guarded and STOP sat S
and ((X sat S) ⇒ (F (X ) sat S))
then (µ X .F (X )) sat X
L3 covers general choice, L4 covers the after operator and L6
covers recursive processes.
Example: Consider the simple vending machine VMα. A
manufacturer wants to ensure that number of drinks dispensed
never exceeds the number of coins and that the implementation
will not take further coins until a drink has been dispensed.
CSP
JCSP
Proof (3)
We can capture this by:
NOLOSS = (#(tr {drink})) ≤ #(tr {coin}))
FAIR = ((tr ↓ coin) ≤ (tr ↓ drink) + 1)
VMSPEC = NOLOSS ∧ FAIR
= (0 ≤ ((tr ↓ coin) − (tr ↓ drink)) ≤ 1)
To prove VMα sat VMSPEC we need to show the base case and
the inductive case.
Base case:
STOP sat tr = hi
⇒ (0 ≤ ((tr ↓ coin) − (tr ↓ drink)) ≤ 1) by a special case of L4.
Since (hi ↓ coin) − (hi ↓ drink)) = 0 this is true.
CSP
JCSP
Proof (4)
Inductive case:
Assume X sat (0 ≤ ((tr ↓ coin) − (tr ↓ drink)) ≤ 1)
Another corollary of L4 specific to double prefixes is:
If P sat S(tr )
then (x → y → P) sat (tr ≤ hx, y i ∨ (tr ≥ hx, y i ∧ S(tr )))
where tr = tr /x/y .
Using this yields:
(coin → drink → X ) sat tr ≤ hcoin, drinki ∨ (tr ≥ hcoin, drinki ∧
(0 ≤ ((tr ↓ coin) − (tr ↓ drink)) ≤ 1))
If tr ≤ hcoin, drinki then tr ∈ {hi, hcoini, hcoin, drinki}. Therefore
(0 ≤ ((tr ↓ coin) − (tr ↓ drink)) ≤ 1)
If tr ≥ hcoin, drinki then
(tr ↓ coin = tr ↓ coin + 1 ∧ tr ↓ drink = tr ↓ drink + 1). Therefore
(0 ≤ ((tr ↓ coin) − (tr ↓ drink)) ≤ 1)
CSP
JCSP
Some Simple Building Blocks
in
in
IdInt
SuccInt
in0
in1
+
out
IdInt(in, out) = in?x → out!x →
IdInt(in, out)
out
SuccInt(in, out) = in?x → out!(x + 1) →
SuccInt(in, out)
out
PlusInt(in0, in1, out) = (in0?x → SKIP k
in1?y → SKIP)
→ out!(x + y ) →
PlusInt(in0, in1, out)
CSP
JCSP
Some Simple Building Blocks (2)
Delta2Int(in, out0, out1) = in?x →
(out0!x → SKIP k
out1!x → SKIP) →
Delta2Int(in, out0, out1)
out0
out1
in
in
n
in
out
TailInt
PrefixInt(n, in, out) = out!n → IdInt(in, out)
out
TailInt(in, out) = in?x → IdInt(in, out)
These are the only set of “building blocks” we can use, but we can
build some other useful processes using them.
CSP
JCSP
A Blocking FIFO Buffer
in
IdInt
c[0]
IdInt
c[1]
...
c[n-2]
IdInt
FifoInt(n)
FifoInt(n, in, out) = IdInt(in, c[0]) k IdInt(c[0], c[1]) k . . . k
IdInt(c[n − 2], out)
As this is a common structure, so some dialects of CSP, e.g.
occam-π, provide a primitive for this.
FifoInt(n, in, out) = IdInt(in, c[0]) k
([k i = 0 FOR n − 2] IdInt(c[i], c[i + 1])) k
IdInt(c[n − 2], out)
out
CSP
JCSP
Sequence Generator
0
out
a
c
b
SuccInt
NumbersInt
NumbersInt = Prefix(0, c, a) k Delta2Int(a, out, b) k SuccInt(b, c)
CSP
JCSP
Integrator
x
y
z
..
.
in
+
out
a
c
b
x
x+y
x+y+z
..
.
0
IntegrateInt
IntegrateInt(in, out) = PlusInt(in, c, a) k Delta2Int(a, out, b) k
PrefixInt(0, b, c)
CSP
JCSP
Pair Generator
a
x
y
z
..
.
in
TailInt
b
c
+
out
x+y
y+z
..
.
PairsInt
PairsInt(in, out) = Delta2Int(in, a, c) k TailInt(a, b) k
PlusInt(b, c, out)
CSP
JCSP
Finonacci Generator
1
a
0
out
b
c
d
PairsInt
FibonacciInt
0
1
1
2
3
5.
..
FibonacciInt = PrefixInt(1, d, a) k PrefixInt(0, a, b) k
Delta2Int(b, out, c) k PairsInt(c, d)
CSP
JCSP
Squares
NumbersInt
a
IntegrateInt b PairsInt
out
SquaresInt
SquaresInt(out) = NumbersInt(a) k IntegrateInt(a, b) k
PairsInt(b, out)
The data on the individual channels is:
< a > = [0, 1, 2, 3, 4, 5, 6, . . .]
< b > = [0, 1, 3, 6, 10, 15, 21, . . .]
< out > = [1, 4, 9, 16, 25, 36, 49, . . .]
CSP
JCSP
JCSP
JCSP is a java library that provides an implementation of CSP.
A CSP process is an object implementing a CSProcess interface.
The process’s behaviour is determined by the object’s run()
method.
The typical JCSP process structure is:
c l a s s Example i m p l e m e n t s C S P r o c e s s
{
. . . private shared synchronisation objects ( e . g . channels )
. . . private state information
}
...
...
public constructors
p u b l i c a c c e s s o r s and m u t a t o r s ( u s e d when n o t r u n n i n g )
...
...
p r i v a t e s u p p o r t methods u s e d by r u n ( )
p u b l i c void run ( )
CSP
JCSP
General Warning!!!
As practically everything in Java is a reference, when we send an
object over a channel to another CSP process, all we are really
sending is a reference to the object. The “sending process” still
can access the sent object and this can lead to a race condition.
The “sending process” should forget (assign NULL) to the sent
object reference.
Even then this can still cause a race condition if the sent object
can access another object referenced by the “sending process”.
CSP
JCSP
Channels
Channels are implemented as Java interfaces. There are 2 types of
channels:
Int Theres channels carry Java ints. These are secure
and its very difficult to introduce race hazards.
Object These channels carry references to arbitrary Java
objects. As they carry object references there is a
significant danger of introducing a race hazard if you
are not careful.
When a channel is defined, we need to specify the channel-end
type. The channel-end type is either:
• input;
• output; or
• ALTing (choice) input.
CSP
JCSP
Parallel
Parallel is a CSProcess that takes an array of CSProcesses.
The run() method of Paralel is the parallel composition of the
array of CSProcesses as per the CSP k operator.
A Parallel CSProcess terminates when all of its constituent
processes have terminated.
The JCSP implementation of the SquaresInt building block
would be:
c l a s s S q u a r e s I n t implements CSProcess
{
p r i v a t e f i n a l ChannelOutputInt out ;
p u b l i c S q u a r e s I n t ( ChannelOutputInt out )
{
t h i s . out = out ;
}
CSP
JCSP
Parallel (2)
p u b l i c void run ( )
{
One2OneChannelInt
One2OneChannelInt
a = Channel . one2oneInt ( ) ;
b = Channel . one2oneInt ( ) ;
new P a r a l l e l (
new C S P r o c e s s [ ]
{
new N u m b e r s I n t ( a . o u t ( ) ) ,
new I n t e g r a t e I n t ( a . i n ( ) , b . o u t ( ) ) ,
new P a i r s I n t ( b . i n ( ) , o u t )
}
) . run ( ) ;
}
}
CSP
JCSP
Sample JCSP Program
The following sample JCSP program consists of 2 processes; one
that outputs even numbers on a channel and another that reads
and displays the number from that channel.
import org . j c s p . lang . ∗ ;
p u b l i c c l a s s DriverProgram
{
p u b l i c s t a t i c v o i d main ( S t r i n g [ ] a r g s )
{
One2OneChannel chan = C h a n n e l . o n e 2 o n e ( ) ;
new P a r a l l e l (
new C S P r o c e s s [ ]
{
new S e n d E v e n I n t s P r o c e s s ( chan . o u t ( ) ) ,
new R e a d E v e n I n t s P r o c e s s ( chan . i n ( ) )
}
) . run ( ) ;
}
}
CSP
JCSP
Sample JCSP Program (2)
import org . j c s p . lang . ∗ ;
p u b l i c c l a s s S e n d E v e n I n t s P r o c e s s implements CSProcess
{
p r i v a t e ChannelOutput out ;
p u b l i c S e n d E v e n I n ts P r o c e s s ( ChannelOutput out )
{
t h i s . out = out ;
}
p u b l i c void run ( )
{
f o r ( i n t i = 2 ; i <= 1 0 0 ; i = i + 2 )
{
o u t . w r i t e ( new I n t e g e r ( i ) ) ;
}
}
}
CSP
JCSP
Sample JCSP Program (3)
import org . j c s p . lang . ∗ ;
p u b l i c c l a s s R e a d E v e n I n t s P r o c e s s implements CSProcess
{
private ChannelInput in ;
public ReadEvenIntsProcess ( ChannelInput in )
{
this . in = in ;
}
p u b l i c void run ( )
{
while ( true )
{
I n t e g e r d = ( I n t e g e r ) in . read ( ) ;
System . o u t . p r i n t l n ( ” Read : ” + d . i n t V a l u e ( ) ) ;
}
}
}
CSP
JCSP
Sample JCSP Program (4)
To compile and execute the JCSP program we need to:
1. Download the JCSP distribution jar file and extract the
constituent jar files in an appropriate directory, say
/jcsp-lib.
jar xvf jcsp-1.1-rc4.jar
2. Compile our program, including the JCSP library.
javac -classpath "/jcsp-lib/*" *.java
3. Execute the program with the JCSP library.
java -cp "/jcsp-lib/*:." DriverProgram
The above commands are for Unix enviroinments.
CSP
JCSP
Alternation
Alternation introduces nondeterminism into JCSP and corresponds
to CSP’s choice operators.
Each choice in an alternation requires a guard. There are 6 JCSP
classes that extend the general Guard class.
AltingChannelInput
AltingChannelInputInt
AltingChannelAccept
AltingBarrier
CSTimer
Skip
Inputting objects on a channel.
Inputting ints on a channel.
A call has been issued on the channel.
Barrier
A timer has timed out.
polling
CSP
JCSP
Alternation (2)
• A channel guard is ready if and only if a process at the other
end has output to (or called) the channel and this has yet to
be read (or accepted).
• A timer guard is ready if and only if its timer has expired.
• A skip guard is always ready.
Each Alternative object is constructed with an array of Guards.
The array of Guards can include any type of guards..
CSP
JCSP
Alternation (3)
An alternation is carried out by invoking one of three types of
select methods.
• select() - Blocks until one or more of its guards are ready.
If one or more guards are ready it make an arbitrary choice of
one of the ready guards and returns its index. If the guard is a
channel, then the process must read (or accept) from the
channel.
• priSelect() - Blocks until one or more of its guards are
ready. If one or more guards are ready it chooses the ready
guard with the lowest index and returns its index. If the guard
is a channel, then the process must read (or accept) from the
channel.
• fairSelect() -Implements weak fairnesses. In successive
invocations of fairSelect(), no guard will be chosen twice
if another guard is ready.
CSP
JCSP
Real-time Sampler
reset
in
Sample (t)
out
• This process services 3 events, 2 inputs and 1 timer.
• The t parameter represents the time interval the process
samples at. Every t seconds the process outputs the last
object that arrived on its in channel. If nothing arrived in the
previous t seconds, the process outputs null.
• The duration of the sampling period, t, may be reset by a
new value arriving on the process’s reset channel.
CSP
JCSP
Real-time Sampler (2)
c l a s s Sample i m p l e m e n t s C S P r o c e s s
{
p r i v a t e f i n a l long t ;
private f i n a l AltingChannelInput in ;
private final AltingChannelInputInt reset ;
p r i v a t e f i n a l ChannelOutput out ;
p u b l i c Sample ( l o n g t , A l t i n g C h a n n e l I n p u t i n ,
AltingChannelInputInt reset ,
ChannelOutput out )
{
this . t = t ;
this . in = in ;
this . reset = reset ;
t h i s . out = out ;
}
CSP
JCSP
Real-time Sampler (3)
p u b l i c void run ( )
{
f i n a l CSTimer t i m = new CSTimer ( ) ;
f i n a l A l t e r n a t i v e a l t = new A l t e r n a t i v e (
new Guard [ ] { r e s e t , tim , i n } ) ;
f i n a l i n t RESET = 0 , TIM = 1 , IN = 2 ;
Object sample = n u l l ;
long timeout = tim . read ( ) + t ;
tim . setAlarm ( timeout ) ;
while ( true )
{
switch ( a l t . preSelect ())
{
c a s e RESET :
t = r e s e t . read ( ) ;
break ;
CSP
JCSP
Real-time Sampler (4)
c a s e TIM :
out . w r i t e ( sample ) ;
sample = n u l l ;
t i m e o u t += t ;
tim . setAlarm ( timeout ) ;
break ;
c a s e IN :
sample = i n . read ( ) ;
break ;
}
}
}
}
CSP
JCSP
Preconditioned Alternation
An array of boolean preconditions can be set on any of the select
() methods of an Alternative.
switch (alt.fairSelect (depends)) {...}
The depends array must have the same length as the Guard array
to which it is bound. Th edepends array allows the programmer,
at run-time, to enable and disable the guards at the corresponding
indices.
CSP
JCSP
Shared Channels
In addition to the one-to-one, zero-buffered, synchronous channels
of CSP, JCSP also provides multi-way shared channels and
buffered channels.
one2any
one2one
any2one
any2any
Alting not allowed