|
Making JCSP Faster: Re-implement with Atomic Operations and Verify its Correctness
Leader: Peter Welch <p.h.welch@kent.ac.uk>
Estimated time: 1 hour plus
Background
JCSP
is a substantial library for Java providing the occam-pi subset of CSP,
together with pi-calculus mobility for channel-ends and processes.
In fact, it supports more CSP than occam-pi, having pioneered the development
of a fast implementation of external choice over multiway events
– which also yields output guards – and full advantage
of multicore processors. These extras integrate with the library in a way
that imposes no overhead on choice, or committed channel communication,
when multiway events are not involved. JCSP also provides higher level
synchronisations (e.g. variant CALL channels), lots of teaching
material and many demonstrations.
The current JCSP implementation builds upon the standard Java model of
threads and monitors (i.e. synchronized methods
and blocks, wait, notify and notifyAll).
Its algorithms are based on the very low-level concurrency instructions
implemented by Transputer microcode (whose implementation via
high-level monitor constructs has always seemed peculiar, though we had
no alternative when that work was done).
The correctness of JCSP channel communication and choice, with respect to
CSP channel communication and choice, has been verified through the
construction of a CSP model of Java monitors (as just noted, a high-level
synchronisation mechanism and, therefore, somewhat complex), CSP modelling
of the JCSP algorithms that use them and the FDR model checker.
This verification has been a vital factor in the stability of JCSP since 1998
and was reported at CPA 2000
(Formal Analysis of Concurrent Java Systems).
History
JCSP developed from the
Java Threads Workshop
held at the University of Kent in September 1996.
In parallel, CTJ – another CSP concurrency library for Java –
was developed at the University of Twente, members of which also attended the workshop.
The Kent and Twente teams had slightly different goals, but shared ideas
freely and provided valuable mutual support.
The workshops this year are the first WoTUG has organised since then,
so they are somewhat overdue!
No external funding was ever sought for JCSP.
Progress was made thanks to the enthusiasm and skills of numerous
individuals – undergraduates, postgraduates and staff – at
the universities of Kent, Napier and Aberdeen, at least.
JCSP has been open-sourced, under L-GPL, from the beginning.
Verification followed in 1998, when a student project working with the
new JIT compiler for Java threw up a deadlock that should not have happened.
This verification, with the needed correction to the JCSP implementation
of choice (alting), was reported in the
CPA 2000 paper.
That work could, and should, have been done at the outset (1996) and
was an important lesson to us.
The API for JCSP was substantially re-engineered, along with significant
new capabilities, in 2007 and reported at CPA that year
(Integrating and Extending JCSP).
Since then, such have been the distracting pressures on academic life that
no further work on JCSP – at least at Kent – has taken place.
Fortunately, such is its stability that no bug reports have arrived since
the trouble in 1998.
This is despite what seems to be a reasonable amount of continuing use.
Aside from numerous academic papers relating to it, there were over 15300
downloads of JCSP from its
website
in the period from January 2008 through July 2012.
Over the same period, there were almost over 2.4 million visits to the site
from over 60000 unique IP addresses.
The JCSP packages and documentation are also mirrored at a
Codehaus git repository,
from which we have not been able to obtain any statistics.
New Java Concurrency Utilities
Problems working with the Java monitor model for concurrency led
to the addition of a range of new concurrency mechanisms to the standard
JDK library (since version 1.5).
These include high-level safe-to-share data-types (such as queues, which can be
used as channels though without alting, barriers without alting
and a variety of collection classes), classical primitives (such as semaphores
and other forms of lock)
and very low-level primitives (i.e. atomics, that map to machine operations
and with which other synchronisation mechanisms can be efficiently constructed
– though considerable care is needed).
These additions were based largely on the work of
Doug Lea,
who long ago suggested we should look at them to support JCSP.
The classes most relevant for this work are likely to include:
Action
Re-implement the core JCSP methods for channel communication, barriers and choice
(alting) using Java atomics, semaphores and (possibly) locks.
These should be able to follow the Transputer microcoded algorithms in a simpler
way than the current JCSP implementation using Java monitors.
Verify the correctness of the new implementation through:
-
CSP modelling of the atomics, semaphores etc. used – this should be
far simpler than the CSP modelling of monitors;
-
translating the new JCSP algorithms into CSP (using the models described
in the previous bullet);
-
following the route from the
CPA 2000 paper
to put the right questions to FDR3.
An implementation without such verification will lead, sooner or later,
to tears.
Completing these actions may be beyond the time available in this workshop.
A realistic ambition may be to implement and verify 1-1 channels, excluding
alting, and to make a simple demonstration (e.g. CommsTime) from
which timing performance can be observed.
Because the implementation will still rest upon Java threads, which in turn
rest upon the underlying operating system, we should not expect a startling
improvement in performance (e.g. towards occam-pi levels) – but there
should be something worthwhile. And we might be surprised!
Members attending this workshop should come armed with pencil and paper and
some familiarity with the JCSP algorithms and CSP modelling presented in
the CPA 2000 paper – at least the Java code in section 3.2 and,
if we get around to alting, section 7.
Looking at the slides
supporting the paper may help, especially for the CSP modelling.
Hard core engineers might also bring a laptop loaded with JDK (1.7, at least),
JCSP (1.1 rc4)
and FDR3,
together with the
FDR script verifying the current JCSP implementation.
|
