Java memory model aware software validation

ABSTRACT

The Java Memory Model (JMM) provides a semantics of Java multithreading for any implementation platform. The JMM is defined in a declarative fashion with an allowed program execution being defined in terms of existence of "commit sequences" (roughly, the order in which actions in the execution are committed). In this work, we develop OpMM, an operational under-approximation of the JMM. The immediate motivation of this work lies in integrating a formal specification of the JMM with software model checkers. We show how our operational memory model description can be integrated into a Java Path Finder (JPF) style model checker for Java programs.

REFERENCES

• 1: Sarita V. Adve , Kourosh Gharachorloo, Shared Memory Consistency Models: A Tutorial, Computer, v.29 n.12, p.66-76, December 1996 [doi>10.1109/2.546611]
• 2: D. Bacon et al. The "double-checked locking is broken" declaration. http://www.cs.umd.edu/-pugh/java/memoryModel/DoubleCheckedLocking.html.
• 3: Sebastian Burckhardt , Rajeev Alur , Milo M. K. Martin, CheckFence: checking consistency of concurrent data types on relaxed memory models, Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation, June 10-13, 2007, San Diego, California, USA
• 4: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 5: David E. Culler , Anoop Gupta , Jaswinder Pal Singh, Parallel Computer Architecture: A Hardware/Software Approach, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1997
• 6: A. De, A. Roychoudhury, and D. D'Souza. Java memory model aware software validation. Technical report, 2008. http://arnabde03.googlepages.com/opmm-full.pdf.
• 7: JSR-133 expert group. JSR-133: Java memory model and thread specification, August 2004.
• 8: G. Gopalakrishnan, Y. Yang, and G. Lindstrom. QB or not QB: An efficient execution verification tool for memory orderings. In CAV, 2004.
• 9: James Gosling , Bill Joy , Guy Steele , Gilad Bracha, Java(TM) Language Specification, The (3rd Edition) (Java (Addison-Wesley)), Addison-Wesley Professional, 2005
• 10: T. Q. Huynh and A. Roychoudhury. A memory model sensitive checker for C#. In Formal Methods Symposium (FM), 2006.
• 11: Tim Lindholm , Frank Yellin, Java Virtual Machine Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
• 12: Jeremy Manson , William Pugh , Sarita V. Adve, The Java memory model, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.378-391, January 12-14, 2005, Long Beach, California, USA
• 13: Seungjoon Park , David L. Dill, An Executable Specification and Verifier for Relaxed Memory Order, IEEE Transactions on Computers, v.48 n.2, p.227-235, February 1999 [doi>10.1109/12.752664]
• 14: Douglas C. Schmidt , Tim Harrison, Double-checked locking, Pattern languages of program design 3, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1997
• 15: Willem Visser , Klaus Havelund , Guillaume Brat , SeungJoon Park, Model Checking Programs, Proceedings of the 15th IEEE international conference on Automated software engineering, p.3, September 11-15, 2000