|Title:||Making JCSP Faster: Re-implement with Atomic Operations and Verify its Correctness|
|Conference:||Communicating Process Architectures 2014|
Peter H. Welch
School of Computing, University of Kent
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).
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.