Abstract
The Java programming language allows multithreaded programming, where threads can be run on multiprocessor or uniprocessor platforms. The allowed behaviors of any multithreaded Java program on any implementation platform (multi- or uni-processor), are described in terms of a memory consistency model called the Java Memory Model (JMM). However, shared memory multiprocessors have a memory model of their own. To reason about the behavior of multithreaded Java programs on multiprocessors, we need a formal basis for understanding both the hardware memory model (of the multiprocessor platform) and the software memory model (the JMM). For this purpose, we have implemented formal executable specifications of the JMM and certain hardware memory models (such as TSO/PSO from SPARC). These executable specifications can be used for exhaustive search i.e. computing all allowed behaviors of test programs under the JMM and the hardware memory models. Consequently, we can compare the JMM with the hardware memory models (in terms of allowed behaviors). We show that such a comparison can help efficient and reliable multithreaded programming on multiprocessors. Results from comparing the current JMM with SPARC architecture memory models are presented.
This work was partially supported by National University of Singapore Research Project R-252-000-095-112.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Java Specification Request (JSR) 133. Java Memory Model and Thread Specification revision. In http://jcp.org/jsr/detail/133.jsp, 2001.
S.V. Adve and K. Gharachorloo. Shared memory consistency models: A tutorial. IEEE Computer, December 1996.
A. Charlesworth. Starfire: Extending the SMP envelope. IEEE Micro, 1998.
E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2), 1986.
D.E. Culler and J. Pal Singh. parallelComputerArchitecture:AHardware/Software Approach. Morgan Kaufmann Publishers, 1998.
D.L. Weaver and T. Germond, Prentice Hall Publishers. The SPARC Architecture Manual: Version 9, 1994.
D. L. Dill. The Murϕ verification system. In Computer Aided Verification (CAV), LNCS 1102, 1996.
D.L. Dill, S. Park, and A. Nowatzyk. Formal specification of abstract memory models. In Symposium on Research on Integrated Systems. MIT Press, 1993.
J. Gosling, B. Joy, and G. Steele. The Java Language Specification. Chapter 17, Addison Wesley, 1996.
A. Holub. Taming Java Threads. Berkeley CA, APress, 2000.
L. Lamport. How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Transactions on Computers, 28(9), 1979.
J. Maessen, Arvind, and X. Shen. Improving the Java Memory Model using CRF. In ACM OOPSLA, 2000.
J. Manson and W. Pugh. Core semantics of multithreaded Java. In ACM Java Grande Conference, 2001.
S. Park and D.L. Dill. An executable specification and verifier for relaxed memory order. IEEE Transactions on Computers, 48(2), 1999.
W. Pugh. Fixing the Java Memory Model. In ACM Java Grande Conference, 1999.
A. Roychoudhury and T. Mitra. Specifying multithreaded Java semantics for program verification. In ACM S IG S OFT International Conference on Software Engineering (ICSE), 2002.
D. Schmidt and T. Harrison. Double-checked locking: An optimization pattern for efficiently initializing and accessing thread-safe objects. In 3rd Annual Pattern Languages of Program Design conference, 1996.
XSB. The XSB logic programming system v2.2, 2000. Available for downloading from http://xsb.sourceforge.net/.
Y. Yang, G. Gopalakrishnan, and G. Lindstrom. Formalizing the Java Memory Model for multithreaded program correctness and optimization. Technical Report UUCS-02-011, University of Utah, Department of Computer Science, 2002.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Roychoudhury, A. (2002). Formal Reasoning about Hardware and Software Memory Models. In: George, C., Miao, H. (eds) Formal Methods and Software Engineering. ICFEM 2002. Lecture Notes in Computer Science, vol 2495. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36103-0_44
Download citation
DOI: https://doi.org/10.1007/3-540-36103-0_44
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00029-7
Online ISBN: 978-3-540-36103-9
eBook Packages: Springer Book Archive