ON STATE CLASSES AND THEIR DYNAMIC SEMANTICS
Ferruccio Damiani, Elena Giachino
Dipartimento di Informatica, Universit
`
a degli Studi di Torino
Corso Svizzera 185, 10149 Torino, Italy
Paola Giannini, Emanuele Cazzola
Dipartimento di Informatica, Universit
`
a del Piemonte Orientale
Via Bellini 25/G, 15100 Alessandria, Italy
Keywords:
Java, concurrent object-oriented language, small-step semantics, core calculus, implementation by translation.
Abstract:
We introduce state classes, a construct to program objects that can be safely concurrently accessed. State
classes model the notion of object’s state (intended as some abstraction over the value of fields) that plays a
key role in concurrent object-oriented programming (as the state of an object changes, so does its coordination
behavior). We show how state classes can be added to Java-like languages by presenting STATEJ, an extension
of JAVA with state classes. The operational semantics of the state class construct is illustrated both at an
abstract level, by means of a core calculus for STATEJ, and at a concrete level, by defining a translation from
STATEJ into JAVA.
1 INTRODUCTION
The notion of object’s state, intended as some ab-
straction on the values of fields, plays a key role
in concurrent object-oriented programming. Various
language constructs for expressing object’s state ab-
stractions have been proposed in the literature (see,
e.g., (Philippsen, 2000) for a survey). We propose
state classes, a programming feature that could be
added to JAVA-like programming languages. The
main novelties in our proposal are: (1) The abil-
ity of states to carry values, thanks to the fact that
states may be parameterized by special fields, that we
call attributes; and (2) The presence of a static type
and effect system guaranteeing that, even though the
state of the objects may vary through states with dif-
ferent attributes, no attempt will be made to access
non-existing attributes (this is, for state attributes, the
standard requirement that well typed programs cannot
cause a field not found error).
This paper focuses on the dynamic semantics of
state classes. Typing issues are addressed in (Damiani
et al., 2006). The paper is organized as follows: Sec-
tion 2 introduces STATEJ, an extension of JAVA with
state classes, through an example. Section 3 gives the
FSJ calculus (a core calculus for STATEJ). Section 4
outlines how STATEJ can be implemented by transla-
tion into plain JAVA. Sections 5 and 6 conclude by
discussing related and further work, respectively.
2 AN EXAMPLE
In this section we motivate STATEJ through an ex-
ample. The state class construct is designed to pro-
gram objects that can be safely concurrently accessed.
Therefore, in a state class, all the fields are private
and all the methods are synchronized (that is, they
are executed in mutual exclusion on the receiver ob-
ject). A state class may extend an ordinary (i.e.,
non-state) class, but only state classes may extend
state classes. Each state class specifies a collection
of states. Each state is parameterized by some special
fields, called attributes, and declares some methods.
The state of an object o can be changed only inside
methods of o, by means of a state transition state-
ment, this!!S(e
1
, . . . , e
n
), where “S” is the name of
the target state and “e
1
, . . . , e
n
” (n ≥ 0) supply the
values for all the attributes of S. An object belonging
to a state class is always in one of the states specified
in its class. Each state class constructor must set the
state of the created object. The default constructor of
the root of a hierarchy of state classes sets the state to
the first state defined in the class.
The class ReaderWriter (in Fig. 1) implements
a multiple reader, single-writer lock — see (Bir-
rel, 1989), for an implementation using traditional
concurrency primitives in a dialect of MODULA 2,
and (Benton et al., 2004), for an implementation using
chords in POLYPHONIC C♯.
5
Damiani F., Giachino E., Giannini P. and Cazzola E. (2006).
ON STATE CLASSES AND THEIR DYNAMIC SEMANTICS.
In Proceedings of the First International Conference on Software and Data Technologies, pages 5-12
DOI: 10.5220/0001317700050012
Copyright
c
SciTePress
public state class ReaderWriter {
state FREE {
public void shared() {this!!SHARED(1);}
public void exclusive() {this!!EXCLUSIVE;}
}
state SHARED(int n) {
public void shared() {n++;}
public void releaseShared()
{n--; if (n==0) this!!FREE;}
}
state EXCLUSIVE {
public void releaseExclusive()
{this!!FREE;}
}
}
Figure 1: A multiple-reader, single-writer lock.
public state class ReaderWriterFair
extends ReaderWriter {
state SHARED(int n) {
public void exclusive()
{this!!PENDING_WRITER(n);
pre_exclusive();
this!!EXCLUSIVE;}
}
state PENDING_WRITER(int n) {
public void releaseShared()
{n--; if (n==0) this!!PRE_EXCLUSIVE;}
}
state PRE_EXCLUSIVE {
private void pre_exclusive() { }
}
}
Figure 2: A fair multiple-reader, single-writer lock.
When a thread e invokes a method m on an ob-
ject o belonging to a state class (e.g., to the class
ReaderWriter in Fig. 1), if either o is in a state that
does not support the invoked method (e.g., shared
invoked on an EXCLUSIVE ReaderWriter) or some
other thread is executing a method on o, then the exe-
cution of e is blocked until o reaches (because of the
action of some other thread) a state where the invoked
method is available and no other thread is executing a
method on o.
The policy implemented by the ReaderWriter
class above is prone to writers’ starvation. The class
ReaderWriterFair (in Fig. 2) extends the class
ReaderWriter to implement a writer starvation free
policy.
An extending class inherits all the states of
the extended class, and may add/override meth-
ods and introduce new states. Thus, class
ReaderWriteFair has states FREE, SHARED,
EXCLUSIVE, PENDING
WRITER and PRE EXCLUSIVE.
When the request exclusive is received by an
object o in state SHARED(n), then the state of o is
set to PENDING
WRITER(n) and the method body
suspends; in this state o can only execute up to n
requests of releaseShared; after the n-th such
request, the state of o is set to PRE
EXCLUSIVE;
in state PRE
EXCLUSIVE the method body for
exclusive can continue, and will set the state of o
to EXCLUSIVE.
The ReaderWriterFair class illustrates a com-
mon pattern in state class programming: the pri-
vate method pre
exclusive has an empty body, and
acts as a test that the receiver has reached the state
PRE EXCLUSIVE.
3 A CALCULUS FOR STATEJ
This section gives syntax and operational seman-
tics of FSJ, a minimal imperative core calculus
for STATEJ. FSJ models the innovative features of
the state construct (namely state classes, state at-
tributes and methods, and state transitions) and multi-
threaded computations.
A FSJ program consists of a set of class definitions
plus an expression to be evaluated, that we will call
the main expression of the program.
3.1 Syntax
The abstract syntax of FSJ class declarations (L),
class constructor declarations (K), state declarations
(N), method declarations (M), and expressions (e) is
given in Fig. 3. The metavariables A, B, C, and D range
over class names; S ranges over state names; f and
g range over attribute names; m ranges over method
names; x ranges over method parameter names; and
a, b, c, d, and e range over expressions.
We write “¯e” as a shorthand for a possibly empty
sequence “e
1
, · · · , e
n
” (and similarly for C, f, S, x)
and write “
¯
N” as a shorthand for “N
1
· · · N
n
” with no
commas (and similarly for
¯
M). We write the empty
sequence as “•” and denote the concatenation of se-
quences using either comma or juxtaposition, as ap-
propriate. We abbreviate operations on pair of se-
quences by writing “
¯
C
¯
f” for “C
1
f
1
, . . . , C
n
f
n
”,
where n is the length of
¯
C and
¯
f. We assume that se-
quences of state declarations or names, attribute dec-
larations or names, method parameter declarations or
names, method declarations do not contain duplicate
names.
The class declaration
state class C extends D {K
¯
N}
defines a state class of name C with superclass D.
The new class has a single constructor K and a set
of states
¯
N. The state declarations
¯
N may either re-
fine (by adding/overrinding methods) states that are
already present in D or add new states.
ICSOFT 2006 - INTERNATIONAL CONFERENCE ON SOFTWARE AND DATA TECHNOLOGIES
6
Syntax:
L ::= state class C extends C {K
¯
N}
K ::= C(
¯
C
¯
f){this!!S(
¯
f)}
N ::= state S (
¯
C
¯
f){
¯
M}
M ::= C m (
¯
C ¯x) {e}
e ::= x | this | this.f | e; e | new C(¯e)
| this!!S(¯e) | spawn(e) | e.m(¯e)
Subtyping:
C <: C
C
1
<: C
2
C
2
<: C
3
C
1
<: C
3
state class C
1
extends C
2
· · · {· · · }
C
1
<: C
2
State attributes lookup:
state class C · · · {· · · state S(
¯
C
¯
f){· · · } · · · }
attributes(C, S) =
¯
C
¯
f
state class C extends D {K
¯
N} S 6∈
¯
N
attributes(C, S) = attributes(D, S)
Method definition lookup:
state class C · · · {K
¯
N} state S{
¯
M} ∈
¯
N
A m(
¯
A ¯x) {e} ∈
¯
M
mDef (m, C, S) = A m(
¯
A ¯x) {e}
state class C extends D {K
¯
N}
(S 6∈
¯
N or (state S{
¯
M} ∈
¯
N and m 6∈
¯
M))
mDef (m, C, S) = mDef (m, D, S)
Figure 3: FSJ syntax, subtyping rules, and lookup func-
tions.
The constructor declaration C(
¯
C
¯
f) {this!!S(
¯
f)}
specifies how to initialize the state and the state at-
tributes of an instance of C. It takes exactly as many
parameters as there are attributes of the state S and its
body consists of a state transition statement.
The state declaration state S(
¯
C
¯
f) {
¯
M} introduces
a state with name S and attributes of names
¯
f and
types
¯
C. The declaration provides a suite of methods
¯
M
that are available in the state S of the class C contain-
ing the state declaration. A state S declared in a class
C inherits all the (not overridden) methods that are de-
fined in the (possible) declarations of S contained in
the superclasses of C.
The method declaration C m (
¯
C ¯x) {e} introduces
a method named m with result type C, parameters ¯x of
types
¯
C, and body e. The variables ¯x and the pseudo-
variable this are bound in e.
The class declarations in a program must satisfy the
following conditions: (1) Object is a distinguished
class name whose declaration does not appear in the
program; (2) For every class name C (except Object)
appearing anywhere in the program, one and only one
class with name C is declared in the program; and (3)
The subtype relation induced by the class declarations
in the program (denoted by <: and formally defined
in the middle of Fig. 3) is acyclic. To simplify the
notation in what follows (as in (Igarashi et al., 2001)),
we always assume a fixed program.
The lookup functions are given at the bottom of
Fig. 3. We write S 6∈
¯
N to mean that no declaration
of the state S is included in
¯
N, and m 6∈
¯
M to mean
that no declaration of the method m is included in
¯
M.
Lookup of the attributes of a state S of a class C, writ-
ten attributes(C, S), returns a sequence
¯
C
¯
f pairing
the type of each attribute declared in the state with its
name. Lookup of the definition of the method m in the
state S of a state class C is denoted by mDef (m, C, S).
1
Note that attributes(C, S) and mDef (m, C, S) are un-
defined when C = Object.
2
3.2 Operational Semantics
In this section we introduce the operational semantics
of FSJ, by defining the reduction rules that transform
configurations representing multi-threaded computa-
tion. A configuration is a pair “¯e, H”, where ¯e is a se-
quence of n ≥ 1 runtime expressions and H is a heap
mapping addresses to objects. Addresses, ranged over
by the metavariable ι, are the elements of the denu-
merable set I. Objects are finite mappings associ-
ating: (1) the distinguished name “class” to a class
name indicating the class of the object; (2) the dis-
tinguished name “state” to a state name indicating
the state of the object; and (3) a mapping associat-
ing a finite number (possibly zero) of state attribute
names to addresses. Objects will be denoted by
[[class : C, state : S,
¯
f : ¯ι]].
The first component of a configuration, ¯e, will be
called “sequence of threads”. A thread of compu-
tation is represented by the evaluation of a runtime
expression e
i
in the heap H. The different threads
share the same heap H. Threads do not have, as in
full STATEJ and JAVA, an associated stack, keeping
the association between parameters and values. In
fact, since FSJ does not include assignment, method
calls are evaluated by directly substituting the for-
mal parameters and the metavariable this with the
corresponding values (in FSJ the only values are ad-
dresses). We call the result of this substitution, which
is no longer an expression of the source language, a
simple runtime expression. Simple runtime expres-
sions, ranged over by s, are obtained from the pseudo
grammar defining expressions (in Fig. 3) by replacing
the clauses “x | this | this.f |” with the clauses
“ι | ι.f |” (see the top of Fig. 4).
Runtime expressions, ranged over by e, are de-
fined by the grammar at top of Fig. 4. In FSJ ev-
ery method is synchronized, therefore on method call
the lock of the object receiving the call must be ac-
1
In full STATEJ, like in JAVA, the lookup functions take
into account method overloading, that (for simplicity) is not
included in FSJ.
2
In full STATEJ the class Object has several methods.
ON STATE CLASSES AND THEIR DYNAMIC SEMANTICS
7
Simple runtime expressions, runtime expressions, evaluation contexts, redexes, and auxiliary functions:
s ::= ι | ι.f | s; s | new C(¯s) | ι!!S(¯s) | spawn(s) | s.m(¯s)
e ::= ι | ι.f | e; s | new C(¯ι, ˙e, ¯s) | ι!!S(¯ι, ˙e, ¯s) | spawn(e) | e.m(¯s) | ι.m(¯ι, ˙e, ¯s)
| ret(ι, m, e) | unlock(ι.m(¯ι))
E ::= [ ] | E; s | new C(¯ι, E, ¯s) | ι!!S(¯ι, E, ¯s) | spawn(E) | E.m(¯s) | ι.m(¯ι, E, ¯s) | ret(ι, m, E)
r ::= ι.f | ι; s | new C(¯ι) | ι!!S(¯ι) | spawn(ι) | ι.m(¯ι) | ret(ι , m, ι) | unlock(ι.m(¯ι))
lockedBy(e) = {ι | ret(ι, · · · , · · · ) is a subexpression of e and unlock(ι. · · · (· · · )) is not a subexpression of e}
lockedBy(e
1
· · · e
n
) =
1≤i≤n
lockedBy(e
i
)
Reduction rules:
H(ι) = o o(f) = ι
′
¯a E[ι.f] ¯c, H −→ ¯a E[ι
′
] ¯c, H
(R-ATTR)
¯a E[ι; s] ¯c, H −→ ¯a E[s] ¯c, H
(R-SEQ)
state class C · · · {C(
¯
C
¯
f){this!!S(
¯
f)} · · · } o = [[class : C, state : S,
¯
f : ¯ι]] ι 6∈ Dom(H)
¯a E[new C(¯ι)] ¯c, H −→ ¯a E[ι] ¯c, H[ι : o]
(R-NEW)
H(ι)(class) = C attributes(C, S) =
¯
C
¯
f o = [[class : C, state : S,
¯
f : ¯ι]]
¯a E[ι!!S(¯ι)] ¯c, H −→ ¯a E[ι] ¯c, H[ι : o]
(R-TRANS)
¯a E[spawn(ι)] ¯c, H −→ ¯a E[ι] ¯c ι.run(), H
(R-SPAWN)
ι 6∈ lockedBy (¯a¯c) H(ι) = [[class : D, state : S, · · · ]] mDef (m, D, S) = C m (
¯
C ¯x) {e}
¯a E[ι.m(¯ι)] ¯c, H −→ ¯a E[ret(ι, m, e[this := ι, ¯x := ¯ι])] ¯c, H
(R-INVK-1)
ι ∈ lockedBy (E[ι.m(¯ι)]) H(ι) = [[class : D, state : S, · · · ]] mDef (m, D, S) undefined
¯a E[ι.m(¯ι)] ¯c, H −→ ¯a E[unlock(ι.m(¯ι))] ¯c, H
(R-INVK-2)
ι 6∈ lockedBy (¯a¯c) H(ι) = [[class : D, state : S, · · · ]] mDef (m, D, S) = C m (
¯
C ¯x) {e}
¯a E[unlock(ι.m(¯ι))] ¯c, H −→ ¯a E[ret(ι, m, e[this := ι, ¯x := ¯ι])] ¯c, H
(R-UNLOCK)
¯a E[ret(ι, m, ι
0
)] ¯c, H −→ ¯a E[ι
0
] ¯c, H
(R-RET)
Figure 4: FSJ (simple) runtime expressions, evaluation contexts, redexes, auxiliary functions, and reduction rules.
quired, unless the call is inside a method of the object
itself, in which case the call can proceed (the lock is
reentrant). Moreover, when the method call is on a
method not defined in the current state, the lock of the
object must be released. This gives to other threads
a chance to change the state of the object to a state
in which the method is defined. Both these situa-
tions are modelled by particular runtime expressions:
(1) ret(ι, m, e), where e does not contain occurrences
of unlock(ι. · · · (· · · )), specifies that a thread is cur-
rently holding the lock of the receiver ι, in order to
evaluate the expression e, which represents the body
of the method m, and (2) unlock(ι.m(¯ι)) specifies that
the lock of ι has been released in order to give a
chance to another thread to change the state of ι to a
state in which m is defined. Note that, the definition of
the syntax for runtime expressions implies that there
can be nested ret expressions but only one unlock.
The metavariables a, b, c, d, and e range over runtime
expressions. We write ¯a as a shorthand for a possibly
empty sequence a
1
· · · a
n
and ˙a as a shorthand for a
possibly empty sequence of length almost one. The
function lockedBy(¯e), defined in Fig. 4, returns the
set of addresses that are locked by the thread sequence
¯e.
The reduction relation has the form “¯a b
1
¯c, H
1
−→
¯a b
2
¯c
˙
d, H
2
”, read “configuration ¯a b
1
¯c, H
1
reduces
to configuration ¯a b
2
¯c
˙
d, H
2
in one step”. The (empty
or singleton) sequence
˙
d indicates that a new thread
might have been spawned because of the reduction of
a spawn expression. We write −→
⋆
for the reflexive
and transitive closure of −→.
By using the definition of evaluation context and
redex (see E and r in Fig. 4), the reduction rules en-
sure that inside each thread the computation follows
a call-by-value left-to-right reduction strategy. This
implies that expressions such as ret and unlock can
only be preceded by values and followed by simple
runtime expressions, which do not contain ret and
unlock (see the definition of s and e in Fig. 4).
The following property asserts that a context can be
decomposed in a unique way in sub-contexts showing
the activation stack of method calls.
Property 1 (Unique Decomposition) Every evalua-
ICSOFT 2006 - INTERNATIONAL CONFERENCE ON SOFTWARE AND DATA TECHNOLOGIES
8
tion context E can be written as
E
1,1
[ret(ι
1
, m
1,1
, · · · E
1,q
1
[ret(ι
1
, m
1,q
1
q
1
· · ·
E
p,1
[ret(ι
p
, m
p,1
, · · · E
p,q
p
[ret(ι
p
, m
p,q
p
q
p
, E
0
)] · · · )]
· · · )] · · · )],
where E
1,1
, . . ., E
1,q
1
, . . ., E
p,1
, . . ., E
p,q
p
(p ≥ 0,
q
1
≥ 1, . . ., q
p
≥ 1) and E
0
do not contain ret(· · · )
subexpressions.
The reduction rules are given at the bottom of
Fig. 4. Each reduction rule rewrites a configuration
of the form “¯a E[r] ¯c, H
1
”, where E is an evaluation
context and r is a redex, into a configuration of the
form “¯a E[e] ¯c
˙
d, H
2
”. The metavariable o ranges over
objects. We use H[ι : o] to denote the heap such that
H[ι : o](ι) = o and H[ι : o](ι
′
) = H(ι
′
), for ι
′
6= ι.
The reduction rules for attribute selection,
(R-ATTR), and sequential composition, (R-SEQ),
are standard. The rule for object creation, (R-NEW),
stores the newly created object at a fresh address of
the heap and returns the address. The pseudo fields
class and state, and the parameters of the initial state
are initialized as specified by the class constructor.
The rule for state transition, (R-TRANS), changes
the current state of the object and returns its address.
Rule (R-SPAWN) replaces the spawn expression
with the address ι and adds a new thread evaluating
the call of the method run on the object at ι. Rule
(R-INVK-1) is applied if the method m is defined in
the current state of the receiver, ι, and no other thread
holds the lock of ι. The expression produced replaces
the call with ret(ι, m, e
′
), indicating that the current
thread holds the lock of ι . The expression e
′
is the
body of the method m in which this and the formal
parameters are replaced with the address ι and the
actual parameters. Rule (R-INVK-2) is applied if the
method m is not defined in the current state of the
receiver and the current thread holds the lock of ι. In
this case, the lock of ι must be released and the thread
must wait that some other thread changes the state of
ι to a state in which m is defined. This is achieved by
replacing the method call redex with the expression
unlock(ι.m(¯ι)). Note that, since the current thread
had the lock of ι, the newly introduced unlock
expression is a subexpression of an expression
ret(ι, m
′
, e
′
) for some m
′
and e
′
. Rule (R-UNLOCK)
replaces the expression unlock(ι.m(¯ι)), if ι is not
locked and the method m is defined in its state, with
ret(ι, m, e
′
), where e
′
is the body of the method
m in which this and the formal parameters are
replaced with the address ι and the actual parameters.
Rule(R-RET), that applies when the body of the
method m on object ι has been evaluated completely,
producing a value, releases the lock of ι by removing
the ret(ι, m, ι
0
) subexpression.
Example 2 (Application of the reduction rules)
First we define the following classes CR and CW repre-
senting the class of threads that have a shared access
to a ReaderWriter object rw and the class of threads
that have an exclusive access to it, respectively.
state class CR extends Object {
CR(ReaderWriter rw) { this!!S(rw) }
state S (ReaderWriter rw) {
Object run () {
rw.shared();
...
rw.releaseShared();
this.run() } }
}
state class CW extends Object {
CW(ReaderWriter rw) { this!!S(rw) }
state S (ReaderWriter rw) {
Object run () {
rw.exclusive();
...
rw.releaseExclusive();
this.run() } }
}
We consider as the main expression of the program,
that is the expression to be evaluated,
spawn(new CR(ι)); (new CW(ι)).run(),
where ι is a ReaderWriter object, so the computa-
tion starts from the following configuration:
spawn(new CR(ι)); (new CW(ι)).run(), H
where H = ι : [[class : ReaderWriterFair, state : FREE]].
A possible computation is as in Fig. 5, where SH
stands for SHARED, PW stands for PENDING
WRITER,
EX stands for EXCLUSIVE, and PE stands for
PRE EXCLUSIVE. We adopt the following notations:
(1) Threads e
1
, e
2
being part of the configuration are
written
e
1
e
2
; (2) Redexes are underlined; (3) Redexes
of suspended threads are underlined and written in
grey; (4) the arrow =⇒ indicates one step of reduction
for each thread of the sequence; (5) In ret expres-
sions we omit method names. As we see in Fig. 5, in
the example we assumed to have integers, decrement
and if-statement. These are assumed, in line (#), to be
reduced following the standard semantics.
4 FROM STATEJ TO JAVA
This section briefly illustrates a translation from
STATEJ to plain JAVA. The basic idea of the trans-
lation is to map a state class into a JAVA class using
synchronized methods and the primitives wait()
and notify(). A class contains a field indicating the
ON STATE CLASSES AND THEIR DYNAMIC SEMANTICS
9
spawn(new CR(ι)); (new CW(ι)).run(), H −→ spawn(ι
′
); (new CW(ι)).run(), H
1
−→ first by (R-NEW) and second by (R-SPAWN)
ι
′
; (new CW(ι)).run()
ι
′
.run()
, H
1
=⇒ by (R-SEQ) and (R-INVK-1)
(new CW(ι)).run()
ret(ι
′
, ι.shared(); ...; ι.releaseShared(); ι
′
.run())
, H
1
=⇒ by (R-NEW) and (R-INVK-1)
ι
′′
.run()
ret(ι
′
, ret(ι, ι!!SH(1)); ...; ι.releaseShared(); ι
′
.run())
, H
2
=⇒ by (R-INVK-1) and (R-TRANS)
ret(ι
′′
, ι.exclusive();...; ι.releaseExclusive(); ι
′′
.run())
ret(ι
′
, ret(ι, ι)
; ...; ι.releaseShared(); ι
′
.run())
, H
3
−→ by (R-RET)
ret(ι
′′
, ι.exclusive(); ...; ι.releaseExclusive(); ι
′′
.run())
ret(ι
′
, ι; ...; ι.releaseShared(); ι
′
.run())
, H
3
−→
⋆
by first applying (R-INVK-1) and (R-SEQ)
ret(ι
′′
, ret(ι, ι!!PW(1); ι.pre exclusive(); ι!! EX); ...; ι.releaseExclusive(); ι
′′
.run())
ret(ι
′
, ι.releaseShared(); ι
′
.run())
, H
3
−→ by (R-TRANS)
ret(ι
′′
, ret(ι, ι; ι.pre exclusive(); ι!!EX); ...; ι.releaseExclusive(); ι
′′
.run())
ret(ι
′
, ι.releaseShared(); ι
′
.run())
, H
4
−→ by (R-SEQ)
ret(ι
′′
, ret(ι, ι.pre exclusive(); ι!! EX); ...; ι.releaseExclusive(); ι
′′
.run())
ret(ι
′
,
ι.releaseShared(); ι
′
.run())
, H
4
−→ by (R-INVK-2)
ret(ι
′′
, ret(ι, unlock(ι.pre exclusive()); ι! ! EX); ...; ι.releaseExclusive(); ι
′′
.run())
ret(ι
′
, ι.releaseShared(); ι
′
.run())
, H
4
−→ by (R-INVK-1)
(#)
ret(ι
′′
, ret(ι, unlock(ι.pre exclusive()); ι!!EX); ...; ι.releaseExclusive(); ι
′′
.run())
ret(ι
′
, ret(ι, n − −; if (n = 0) ι !! PE); ι
′
.run())
, H
4
−→
⋆
ret(ι
′′
, ret(ι, unlock(ι.pre exclusive()); ι! ! EX); ...; ι.releaseExclusive(); ι
′′
.run())
ret(ι
′
, ι; ι
′
.run()
)
, H
5
=⇒ by (R-UNLOCK) and (R-SEQ)
ret(ι
′′
, ret(ι, ret(ι, ); ι!!EX); ...; ι.releaseExclusive(); ι
′′
.run())
ret(ι
′
, ι
′
.run())
, H
5
−→
⋆
by (R-RET) and (R-INVK-1)
ret(ι
′′
, ret(ι, ι.releaseExclusive(); ι
′′
.run()))
ret(ι
′
, ret(ι
′
, ...))
, H
6
−→
⋆
· · ·
where
H = ι : [[class : ReaderWriterFair, state : FREE]]
H
1
= H[ι
′
: [[class : CR, state : S, rw : ι]]] H
2
= H
1
[ι
′′
: [[class : CW, state : S, rw : ι]]]
H
3
= H
2
[ι : [[class : ReaderWriterFair, state : SH, n : 1]]] H
4
= H
3
[ι : [[class : ReaderWriterFair, state : PW, n : 1]]]
H
5
= H
4
[ι : [[class : ReaderWriterFair, state : PE]]] H
6
= H
5
[ι : [[class : ReaderWriterFair, state : EX]]]
Figure 5: An example of reduction.
current state of the object, and methods correspond-
ing to the methods of the original STATEJ class. The
translation can be briefly described as follows.
Method. Methods defined in more than one state have
more than one body. To be able to execute differ-
ent bodies in different states our translation creates
a unique synchronized method containing all the
different bodies. At run-time, when the method is
called, we have to check the current state of the object,
and see whether the method was defined in this state
or not. In case it is defined, then the corresponding
body is executed, otherwise the thread calls a wait()
putting it in hold. To keep the information on the
methods defined in a certain state we use a hash ta-
ble. Due to the limitation of the switch statement of
JAVA, states are codified by the primitive type int.
For example the following class
state class Ex extends Object {
Ex() { this!!A(); }
state A () {
Object m() { /
*
body of m in A
*
/ } }
state B () {
Object m() { /
*
body of m in B
*
/ } } }
is translated into
class Ex extends Object {
Ex() { ... }
final static int A = 1;
final static int B = 2;
Hashtable stateMethods;
int currentState;
synchronized Object m() {
while (!existsInCurrentState) wait();
switch (currentState) {
case A : /
*
body of m in A
*
/ break;
case B : /
*
body of m in B
*
/ break;
} } }
where the existence of a method in a given state and
its selection are done using the hash table of methods.
State Transition. The state transition expression
this!!A() is translated into
ICSOFT 2006 - INTERNATIONAL CONFERENCE ON SOFTWARE AND DATA TECHNOLOGIES
10
currentState = A; notifyAll();
so in addition to change the state of the objects it no-
tifies all the threads waiting for the lock of the cur-
rent object. When the current thread will release the
lock the notified threads will compete to get it to have
a chance to see whether the method that caused the
waiting is defined in the current state. If the method
is defined, then the thread can proceed, otherwise it
calls a wait(). Due to the non deterministic nature of
JAVA scheduling we cannot insure the order in which
notified threads will be waken up.
Constructor. The constructor of the translated class
should initialize the hash table and then include the
translation of the constructor of the original class.
Inheritance. A state class may extend another class
(either state or not). In the subclass we inherit all
the states and may add others. Therefore, we have
to be careful to clashes of constants of state. More-
over, methods may be added/redefined. For instance
method exclusive() of the example in Sect. 2, is
defined in state FREE of ReaderWriter, and rede-
fined in state SHARED of ReaderWriterFair. When
a method is redefined in its translation we use the
default clause as follows.
class ReaderWriterFair
extends ReaderWriter {
...
synchronized void exclusive () {
while (!existsInCurrentState) wait();
switch (currentState) {
case SHARED:
currentState =PENDING_WRITER;
notifyAll();
pre_exclusive();
currentState =EXCLUSIVE;
notifyAll();
break;
default :
super.exclusive;
break; } } }
The current implementation of the translator
(www.di.unito.it/˜giannini/stateJimpl/) takes as in-
put a program written in JAVA 1.4 extended with
state classes with attribute-free states (attributes can
be straightforwardly codified by class fields; however,
their implementation would require to implement the
type and effect analysis). The translation uses the
tool for Language Recognition ANTLR, see (Parr and
project group, 2005), and the StringTemplate tecnol-
ogy, see (Parr, 2005). We first made a JAVA 1.4 to
JAVA 1.4 translation taking advantage of the grammar
defined by Parr and then modified the grammar to in-
clude our state related constructs. The use of ANTLR
and StringTemplate makes the translator easily adapt-
able to different translation schemes and also to addi-
tion to the input language.
5 RELATED WORK
According to (Philippsen, 2000) states provide
a boundary coordination mechanism (we refer to
Sect. 4.2 of (Philippsen, 2000) for a survey of several
COOLs with boundary coordination). In particular,
the state class construct is related to the actor model
(Agha, 1986) and to the behaviour abstraction and
behaviour/enable sets proposals (Kafura and Laven-
der, 1996; Tomlinson and Singh, 1989).
At the best of our knowledge, the main novelties
in our proposal are: the ability of states to carry val-
ues (thanks to the presence of attributes); the for-
malization of an abstract operational semantics of a
notion of state for expressing coordination in JAVA-
like languages; and the presence of a static type and
effect system (presented in (Damiani et al., 2006))
guaranteeing that during the execution there can-
not be any access to undefined attributes of objects.
Type systems for concurrent objects have been in-
vestigated in the literature, see, e.g., “regular object
types” (Nierstrasz, 1993), the TYCO object calcu-
lus (Ravara and Vasconcelos, 2000), and the Fickle
MT
proposal (Damiani et al., 2004).
Various improvements of the concurrency model
of JAVA-like languages have been proposed. In JOIN
JAVA (Itzstein and Kearney, 2001) and POLYPHONIC
C♯ (Benton et al., 2004) the synchronization mecha-
nism relies on the join pattern, called chord in POLY-
PHONIC C♯, construct. Chords can be used to codify
the state of an object through the pattern (illustrated,
for instance, in (Benton et al., 2004)) of using private
asynchronous method to carry object state. However,
this pattern could be misused leading to deadlock or
errors. In STATEJ the notion of object state is in the
language definition, thus eliminating the possibility of
many of such errors. In JEEG (Milicia and Sassone,
2005) the synchronization conditions on an object o
are expressed with linear temporal logic constraints
involving the value of fields and the method invoca-
tion history of o. These constraints could be used to
codify the state of an object o. However, state at-
tributes have to be mapped on object fields and there
is no way to express the fact that some fields should
be accessible only in some states.
STATEJ (as JOIN JAVA, POLYPHONIC C♯, and
JEEG) focuses on a specific coordination mechan-
ishm. The JR programming language (Keen et al.,
2004) takes a different approach: it extends JAVA pro-
viding a rich concurrency model with a variety of
mechanisms. None of this mechanisms directly mod-
els the notion of object state.
ON STATE CLASSES AND THEIR DYNAMIC SEMANTICS
11
6 FUTURE WORK
The current prototypical implementation of STATEJ
(www.di.unito.it/˜giannini/stateJimpl/) is based on
the translation scheme outlined in Sect. 4. It con-
sists of a preprocessor that maps code written in JAVA
1.4 extended with state classes into plain JAVA. The
current approach favors simplicity over efficiency. Its
major drawback is that each state transition of an ob-
ject o notifies all the threads waiting for any state of
o. Note that, notifying just the threads waiting for
the target state of the transition would not represent a
significative improvement, since multiple state transi-
tions may occur before the lock on o is released. A
more significative improvement would be moving no-
tification from state transition on o to lock release on
o: this would allow notifying just the threads wait-
ing for the current state of o. Note that, however,
all but the first (according to the scheduling mecha-
nism of JAVA) of such threads have to sleep again. We
are currently investigating a quite different approach
that support selective wakeups. It can be roughly de-
scribed as follows:
• Each object o is equipped with a set of FIFO queues
(one for each state).
• Whenever a thread invokes a method m on o, IF o is
locked by some other thread OR m is not available
in the current state of o
– THEN the thread is suspended and enqueued in
all the queues associated to the states of o
where m is available, and the lock on o (if held
by the suspended thread) is released
– ELSE the method executed and the lock on o (if
not already held by the invoking thread) is taken.
• Whenever the lock on o is released, IF the queue
associated to the current state of o is not empty,
THEN a thread e is extracted from the queue, re-
moved from all the other queues, resumed, and it
takes the lock on o.
Other future work includes: Refinement of the type
and effect system given in (Damiani et al., 2006);
Further investigations on the expressivity of the state
class construct and on its integration in JAVA-like lan-
guages (by analyzing the interaction of state classes
and their types with the advanced features of JAVA-
like languages); Development of a new prototype
(based on the translation scheme outlined above) in-
cluding state attributes and the related type and effect
analysis; and Development of benchmarks.
REFERENCES
Agha, G. A. (1986). ACTORS: A Model of Concurrency
Computation in Distribuited Systems. MIT Press.
Benton, N., Cardelli, L., and Fournet, C. (2004). Mod-
ern Concurrency Abstractions for C♯. ACM TOPLAS,
26(5):769–804.
Birrel, A. D. (1989). An introduction to programming with
threads. Technical Report 35, DEC SRC.
Damiani, F., Dezani-Ciancaglini, M., and Giannini, P.
(2004). On re-classification and multithreading. JOT
(www.jot.fm), 3(11):5–30. Special issue: OOPS track
at SAC 2004.
Damiani, F., Giachino, E., Giannini, P., Cameron, N., and
Drossopoulou, S. (2006). A state abstraction for co-
ordination in java-like languages. In Electronic pro-
ceedings of FTfJP’06 (www.cs.ru.nl/ftfjp/).
Igarashi, A., Pierce, B., and Wadler, P. (2001). Feather-
weight Java: A minimal core calculus for Java and
GJ. ACM TOPLAS, 23(3):396–450.
Itzstein, G. S. and Kearney, D. (2001). Join Java: an alterna-
tive concurrency semantics for Java. Technical Report
ACRC-01-001, Univ. of South Australia.
Kafura, D. G. and Lavender, R. G. (1996). Concur-
rent object-oriented languages and the inheritance
anomaly. In Casavant, T., Tvrdil, P., and Pl
´
asil, F., ed-
itors, Parallel Computers: Theory and Practice, pages
221–264. IEEE Press.
Keen, A. W., Ge, T., Maris, J. T., and Olsson, R. A. (2004).
JR: Flexible distributed programming in an extended
java. TOPLAS, 26(3):578–608.
Milicia, G. and Sassone, V. (2005). Jeeg: Temporal Con-
straints for the Synchronization of Concurrent Ob-
jects. Concurrency Computat.: Pract. Exper., 17(5-
6):539–572.
Nierstrasz, O. (1993). Regular Types for Active Objects. In
OOPSLA’93, volume 28 of ACM SIGPLAN Notices,
pages 1–15.
Parr, T. (2003-2005). StringTem-
plate Documentation. Available at
www.stringtemplate.org./doc/doc.html.
Parr, T. and project group (2005). ANTLR Ref-
erence Manual, Version 2.7.5. Available at
www.antlr.org./doc/index.html.
Philippsen, M. (2000). A Survey of Concurrent Object-
Oriented Languages. Concurrency Computat.: Pract.
Exper., 12(10):917–980.
Ravara, A. and Vasconcelos, V. T. (2000). Typing Non-
uniform Concurrent Objects. In CONCUR’00, volume
1877 of LNCS, pages 474–488, Berlin. Springer.
Tomlinson, C. and Singh, V. (1989). Inheritance and syn-
chronization with enabled-sets. In OOPSLA’89, pages
103–112. ACM.
ICSOFT 2006 - INTERNATIONAL CONFERENCE ON SOFTWARE AND DATA TECHNOLOGIES
12
