Jackal Distributed Shared Memory Implementation of Java.

Organisation:	CWI (THE NETHERLANDS)
Method:	muCRL (micro Common Representation Language)
Tools used:	muCRL toolset CADP (Construction and Analysis of Distributed Processes)
Domain:	Coordination Architectures.
Period:	2003
Size:	1800 lines of muCRL
Description:	Jackal is a fine-grained, distributed shared memory implementation of the Java programming language. It is based upon a self-invalidation based, multiple-writer cache coherency protocol for regions (i.e., objects or fixed-size partitions of an array). Jackal allows processors to cache a region created on another processor (the region's home node). All threads on one processor share one copy of a cached region. The protocol follows exactly the Java memory model specification, which requires that all data in a thread's working memory (including cached copies of regions) is invalidated whenever the thread reaches a synchronization point. Jackal implements several run-time optimizations intended to reduce interprocessor communication, such as automatic home node migration and adaptive lazy flushing. A formal specification of Jackal's cache coherency protocol was developed in muCRL. The specification consists of a parallel composition of threads, processors, regions, protocol lock managers, and message queues. The state space corresponding to several configurations of the specification (containing up to three processors and three threads) were generated using the muCRL toolset on a cluster of eight nodes. Four types of requirements were formulated for the protocol: deadlock freedom, assertion checking, relaxed cache coherency (for any region, at any time there exists one home node), and liveness of writing and flushing regions. The first two kinds of requirements were checked using the muCRL toolset, and the two others by expressing them in regular alternation-free mu-calculus and using the EVALUATOR model-checker of CADP. The verification allowed to discover two errors in the implementation of the cache coherency protocol. The first error was a deadlock occurring when the home of a region accessed by a thread migrates to the node of the thread while the thread is blocked waiting for the region's lock. The second error was a cache coherency problem (region without home node) occurring when a thread tries to write to a region from remote, and the home of the region migrates to the thread's node while the thread is waiting for an up-to-date copy of the region. Both errors were corrected, and the resulting specifications were successfully checked against all aforementioned requirements.
Conclusions:	This case-study assessed the benefits of applying formal methods and verification tools for enhancing the reliability of real-life industrial systems. The specification and analysis of the Jackal's cache coherency protocol allowed to find and correct two non-trivial errors in its implementation. Also, a large number of inconsistencies and misunderstandings were found, mostly caused by the evolutions of the implementation simultaneously with the formal analysis process. Such gaps between an implementation and its formal model could be avoided if formal methods were employed at an earlier design phase.
Publications:	[Pang-Fokkink-Hofman-Veldema-03] Jun Pang, Wan Fokkink, Rutger Hofman, and Ronald Veldema. "Model Checking a Cache Coherence Protocol for a Java DSM Implementation". Proceedings of the 8th International Workshop on Formal Methods for Parallel Programming: Theory and Applications FMPPTA'2003 (Nice, France), IEEE Computer Society Press, April 2003. Available on-line at: http://homepages.cwi.nl/~wan/WJFmore/jackal.ps.gz or from the CADP Web site in PDF or PostScript [Pang-Fokkink-Hofman-Veldema-07] Jun Pang, Wan Fokkink, Rutger Hofman, and Ronald Veldema. "Model Checking a Cache Coherence Protocol for a Java DSM Implementation". Journal of Logic and Algebraic Programming 71(1), pages 1-43, March 2007. Available on-line at: http://seshome.informatik.uni-oldenburg.de/~jun/papers/JLAP07.pdf or from the CADP Web site in PDF or PostScript
Contact:	Dr. Wan Fokkink CWI / Department of Software Engineering SEN2 (Specification and Analysis of Embedded Systems) Kruislaan 413, 1098 SJ Amsterdam, The Netherlands Room: M342 Tel: +31 20 592 4104 Fax: +31 20 592 4199 E-mail: wan@cwi.nl
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page