Independence and Concurrency in System Verification (ICSV)

The long-term goal of this project is to develop a new independence based (i.e. true concurrency) semantic model for CSP and novel concurrent programming languages. It is hoped that the new semantic model, unlike its predecessors, can be profitably exploited in practical applications of either software or hardware nature. The project at the current stage is driven mainly by three promising applications where independence is of crucial importance, e.g. diamond mining and FDR2, scalable verification for next-generation concurrent programming platform (e.g. multi-core systems) and semantic theory of Java Memory models. Specifically it is about:

1. Building on our past work on `untangled actions', which provides a compositional (and thus cheap) way to find diamonds, a new technique is developed on independence decorated LTSes. The independence decorated LTSes is an extension of asynchronous transition systems and concurrent automata. Guided by the dynamic refinement of independence information, preliminary experiments show that more diamonds can be found more cheaply. Collaboration for implementation in FDR2 is planned with the Oxford FDR2 team if further experiments confirm the reduction.

2. Vacuous interleaving of independent actions causes state explosions in analyzing concurrent programs. Low synchronization, though holds promise to be more scalable on multi-core processors, causes interleaving to happen at a finer level of granularity. By analyzing dynamic independence of actions we can find truly conflicting actions and only interleave them for system analysis. Using the new independence based semantic model for concurrent programming languages (e.g. reactive action labeled PO-traces), action conflict analysis can be carried out on a solid foundation in a systematic way.

3. The Java Memory Model (JMM) gives informal semantics to shared-memory multi-threading Java programs. It is widely accepted that only partial order models (rather than interleaving models) can provide a faithful formal semantics to JMM. The existing JMM formal specification is low-level and operational in nature, so it is complicated and difficult to understand (actually, a previous version of JMM has been found unusable). Based on recent investigations we propose an abstract, high-level, independence-based (operational as well as denotational) model for JMM which appears promising. We intend to carry on with this work to develop the full model and compare it with existing JMM specification.

Funding: 80K USD from 2008 to 2009 by UNU-IIST

Project members:

Michael Adeniyi Akingbade(until April, 2009), Ming Li, Weisong Li, Shuling Wang, Xu Wang and Yongxin Zhao