Verification of the Java Causality Requirements | SpringerLink
Skip to main content
Springer Nature Link
Log in

Verification of the Java Causality Requirements

  • Conference paper
Hardware and Software, Verification and Testing (HVC 2005)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 3875))

Included in the following conference series:

  • 592 Accesses

Abstract

The Java Memory Model (JMM) formalizes the behavior of shared memory accesses in a multithreaded Java program. Dependencies between memory accesses are acyclic, as defined by the JMM causality requirements. We study the problem of post-mortem verification of these requirements and prove that the task is NP-complete. We then argue that in some cases the task may be simplified either by considering a slightly stronger memory model or by tracing the actual execution order of Read actions in each thread. Our verification algorithm has two versions: a polynomial version, to be used when one of the aforementioned simplifications is possible, and a non-polynomial version – for short test sequences only – to be used in all other cases. Finally, we argue that the JMM causality requirements could benefit from some fine-tuning. Our examination of causality test case 6 (presented in the public discussion of the JMM) clearly shows that some useful compiler optimizations – which one would expect to be permissible – are in fact prohibited by the formal model.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Causality Test Cases, http://www.cs.umd.edu/~pugh/java/memoryModel/CausalityTestCases.html

  2. JSR-133: Java Memory Model and Thread Specification (August 2004), http://www.cs.umd.edu/~pugh/java/memoryModel/jsr133.pdf

  3. Adve, S.V., Hill, M.D.: A unified formalization of four shared-memory models. IEEE Trans. on Parallel and Distributed Systems 4(6), 613–624 (1993)

    Article  Google Scholar 

  4. Adve, S.V., Manson, J., Pugh, W.: The Java Memory Model. In: POPL 2005 (2005)

    Google Scholar 

  5. Adve, S.V., Gharachorloo, K., Gupta, A., Hennessy, J.L., Hill, M.D.: Sufficient System Requirements for Supporting the PLpc Memory Model. Technical Report #1200, University of Wisconsin-Madison (1993)

    Google Scholar 

  6. Alexandrescu, A., Boehm, H., Henney, K., Lea, D., Pugh, B.: Memory model for multithreaded C++ (2004), http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2004/n1680.pdf

  7. Boehm, H., Lea, D., Pugh, B.: Implications of C++ Memory Model Discussions on the C Language (2005), http://www.open-std.org/jtc1/sc22/wg14/www/docs/n1131.pdf

  8. Boehm, H.-J.: Threads cannot be implemented as a library. SIGPLAN Not., 40(6), 261–268 (2005)

    Article  Google Scholar 

  9. Charles, W.K.: The UPC Memory Model: Problems and Prospects. In: Proceedings of the International Parallel and Distributed Processing Symphosium. IEEE, Los Alamitos (2004)

    Google Scholar 

  10. Doug, L.: The JSR-133 Cookbook for Compiler Writers, http://gee.cs.oswego.edu/dl/jmm/cookbook.html

  11. Gharachorloo, K., Adve, S.V., Gupta, A., Hennessy, J.L., Hill, M.D.: Programming for different memory consistency models. Journal of Parallel and Distributed Computing 15(4), 399–407 (1992)

    Article  Google Scholar 

  12. Gharachorloo, K., Adve, S.V., Gupta, A., Hennessy, J.L., Hill, M.D.: Specifying System Requirements for Memory Consistency Models. Technical Report #CSLTR- 93-594, Stanford University (1993)

    Google Scholar 

  13. Gharachorloo, K., Lenoski, D., Laudon, J., Gibbons, P., Gupta, A., Hennessy, J.: Memory consistency and event ordering in scalable shared-memory multiprocessors. In: Proceedings of the 17th Intl. Symp. on Computer Architecture, May 1990, pp. 15–26 (1990)

    Google Scholar 

  14. Gibbons, P.B., Korach, E.: New results on the complexity of sequential consistency. Technical report, AT&T Bell Laboratories, Murray Hill NJ (September 1993)

    Google Scholar 

  15. Gosling, J., Joy, B., Steele, G., Bracha, G.: The Java Language Specification, 3rd edn. Addison-Wesley, Reading (2005)

    MATH  Google Scholar 

  16. Kohli, P., Neiger, G., Ahamad, M.: A Characterization of Scalable Shared Memories. Technical Report GIT-CC-93/04, College of Computing, Georgia Institute of Technology, Atlanta, Georgia 30332-0280 (January 1993)

    Google Scholar 

  17. The Java Memory Model mailing list archive, http://www.cs.umd.edu/~pugh/java/memoryModel/archive

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Technion, Israel Institute of Technology, Technion City, Haifa, Israel

    Sergey Polyakov & Assaf Schuster

Authors
  1. Sergey Polyakov
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Assaf Schuster
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. IBM Labs, Haifa University, Mount Carmel, 31905, Haifa, Israel

    Eyal Bin

  2. IBM Labs, Haifa University, Mount Carmel,, 31905, Haifa, Israel

    Yaron Wolfsthal

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Polyakov, S., Schuster, A. (2006). Verification of the Java Causality Requirements. In: Ur, S., Bin, E., Wolfsthal, Y. (eds) Hardware and Software, Verification and Testing. HVC 2005. Lecture Notes in Computer Science, vol 3875. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11678779_16

Download citation

  • DOI: https://doi.org/10.1007/11678779_16

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-32604-5

  • Online ISBN: 978-3-540-32605-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation