CWI (THE NETHERLANDS)
muCRL (micro Common Representation Language)
CADP (Construction and Analysis of Distributed Processes)
1800 lines of muCRL
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.
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.
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,
Available on-line at: http://homepages.cwi.nl/~wan/WJFmore/jackal.ps.gz
or from our FTP 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 our FTP site in PDF or PostScript
Dr. Wan Fokkink
CWI / Department of Software Engineering
SEN2 (Specification and Analysis of Embedded Systems)
Kruislaan 413, 1098 SJ Amsterdam, The Netherlands
Tel: +31 20 592 4104
Fax: +31 20 592 4199
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|