Research Interests

Currently I am working on my Ph.D. degree in Computer Science under the supervision of Prof. Ganesh Gopalakrishnan and Prof. Gary Lindstrom. My main research interest is to apply formal verification techniques to the specification and analysis of memory consistency models in general, and the Java Memory Model (JMM) in particular.

Standardized language level support for threads is one of the most important features in Java. The JMM describes how Java threads interact with each other in a shared memory environment. The original JMM specification is given in Chapter 17 of the Java Language Specification. Unfortunately, the existing specification is flawed and hard to understand. The need for improvements in JMM has stimulated broad research interests. Two new semantics have been proposed for Java threads, one by Manson and Pugh, the other by Maessen, Arvind, and Shen. The JMM is currently under an official revisionary process (JSR 133) and will be replaced in the future. There is also an ongoing discussion in the JMM mailing list.

Given the growing interest in multithreaded Java programming, it is essential to have a sound framework that would allow formal reasoning about the JMM. In our research, we have adapted the CRF JMM to an executable specification using guarded commands. A model checking tool based on Murphi is integrated with the memory model specification. This enables us to exercise the underlying model with a suite of test programs to reveal pivotal properties and verify common programming idioms. Our formal analysis of the CRF JMM has demonstrated that formal methods, such as model checking, are feasible and effective techniques for understanding a language level memory model. This work is presented in our paper Analyzing the CRF Java Memory Model.

A memory model specification framework should be generic instead of being constrained by any specific architectural designs. It is also useful to have a common memory model specification interface that allows one to easily compare and understand different models. Based on these observations, we have designed the Uniform Memory Model (UMM). UMM is a simple and flexible specification framework with the built-in support for formal verification. It defines memory operations as events controlled by a carefully designed abstract machine. This provides an abstraction mechanism to capture different memory model properties into an executable specification. In addition, UMM also provides additional supports for a language level memory model by including state information of local variables. Thread local data dependency can be precisely specified as explicit conditions in the transition system which is desired to reduce the gap between program and memory semantics. The UMM prototype has been developed in Murphi. An alternative formal specification of the JMM, primarily based on the semantics proposed by Manson and Pugh, is implemented in UMM. Interesting results have been revealed by the systematic analysis using idiom-driven test programs. This work is summerized in our paper Specifying Java Thread Semantics Using a Uniform Memory Model.

Publications

bullet Yue Yang, Ganesh Gopalakrishnan and Gary Lindstrom, Analyzing the CRF Java Memory Model, the 8th Asia-Pacific Software Engineering Conference, pages 21-28, 2001. (PDF, PS, Presentation, Murphi Program)

This work has also been presented at the Workshop on Software Model Checking (SWMC01) and the Java Verification Workshop (JVW02).

bullet Yue Yang, Ganesh Gopalakrishnan, and Gary Lindstrom, Specifying Java Thread Semantics Using a Uniform Memory Model, in Joint ACM Java Grande/ISCOPE Conference, November 2002. (PDF, Presentation, Murphi Implementation)


Back Home