Arnab De
Abhik Roychoudhury
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.
- S. V. Adve and K. Gharachorloo. Shared memory consistency models: A tutorial. IEEE Computer, pages 66--76, Dec. 1996. Google Scholar
Digital Library
- D. Bacon et al. The "double-checked locking is broken" declaration. http://www.cs.umd.edu/-pugh/java/memoryModel/DoubleCheckedLocking.html.Google Scholar
- S. Burckhardt, R. Alur, and M. Martin. Checkfence: Checking consistency of concurrent data types on relaxed memory models. In PLDI, 2007. Google ScholarDigital Library
- E. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999. Google ScholarDigital Library
- D. E. Culler and J. Pal Singh. Parallel Computer Architecture: A Hardware/Software Approach. Morgan Kaufmann Publishers, 1998. Google ScholarDigital Library
- A. De, A. Roychoudhury, and D. D'Souza. Java memory model aware software validation. Technical report, 2008. http://arnabde03.googlepages.com/opmm-full.pdf.Google Scholar
- JSR-133 expert group. JSR-133: Java memory model and thread specification, August 2004.Google Scholar
- G. Gopalakrishnan, Y. Yang, and G. Lindstrom. QB or not QB: An efficient execution verification tool for memory orderings. In CAV, 2004.Google Scholar
- J. Gosling, W. Joy, G. Steele, and G. Bracha. Java(TM) Language Specification, The (3rd Edition) (Java (Addison-Wesley)). Addison-Wesley Professional, 2005. Google ScholarDigital Library
- T. Q. Huynh and A. Roychoudhury. A memory model sensitive checker for C#. In Formal Methods Symposium (FM), 2006. Google ScholarDigital Library
- T. Lindholm and F. Yellin. Java Virtual Machine Specification. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 1999. Google ScholarDigital Library
- Jeremy Manson, William Pugh, and Sarita V. Adve. The java memory model. In POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 378--391, New York, NY, USA, 2005. ACM. Google ScholarDigital Library
- S. Park and D. L. Dill. An executable specification and verifier for relaxed memory order. IEEE Transactions on Computers, 48(2), 1999. Google ScholarDigital Library
- D. C. Schmidt and T. Harrison. Double-checked locking. Pattern languages of program design 3, pages 363--375, 1997. Google ScholarDigital Library
- W. Visser, K. Havelund, G. Brat, and S. Park. Model checking programs. In IEEE international conference on Automated software engineering (ASE), 2000. Google ScholarDigital Library
Recommendations
Java memory model-aware model checking
TACAS'12: Proceedings of the 18th international conference on Tools and Algorithms for the Construction and Analysis of SystemsThe Java memory model guarantees sequentially consistent behavior only for programs that are data race free. Legal executions of programs with data races may be sequentially inconsistent but are subject to constraints that ensure weak safety properties. ...
Comments