Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Formal Methods

FM 2006: FM 2006: Formal Methods pp 476–491Cite as

A Memory Model Sensitive Checker for C#

  • Conference paper

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

Abstract

Modern concurrent programming languages like Java and C# have a programming language level memory model; it captures the set of all allowed behaviors of programs on any implementation platform — uni- or multi-processor. Such a memory model is typically weaker than Sequential Consistency and allows reordering of operations within a program thread. Therefore, programs verified correct by assuming Sequential Consistency (that is, each thread proceeds in program order) may not behave correctly on certain platforms! The solution to this problem is to develop program checkers which are memory model sensitive. In this paper, we develop such an invariant checker for the programming language C#. Our checker identifies program states which are reached only because the C# memory model is more relaxed than Sequential Consistency. Furthermore, our checker identifies (a) operation reorderings which cause such undesirable states to be reached, and (b) simple program modifications — by inserting memory barrier operations — which prevent such undesirable reorderings.

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

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Java Specification Request (JSR) 133. Java Memory Model and Thread Specification revision (2004)

    Google Scholar 

  2. Abrams, B.: http://blogs.msdn.com/brada/archive/2004/05/12/130935.aspx

  3. Brumme, C.: Weblog: Memory model, http://blogs.msdn.com/cbrumme/archive/2003/05/17/51445.aspx

  4. Collier, W.W.: Reasoning about Parallel Architectures. Prentice Hall, Englewood Cliffs (1992)

    MATH  Google Scholar 

  5. Dwyer, M.B., et al.: Using static and dynamic escape analysis to enable model reductions in model-checking concurrent object-oriented programs. Technical report, Kansas State Univ. (2003)

    Google Scholar 

  6. Bacon, D., et al.: The ”Double-checked Locking is Broken” declaration, http://www.cs.umd.edu/pugh/java/memoryModel/DoubleCheckedLocking.html

  7. Ford, L.R., Fulkerson, D.R.: Maximum flow through a network. Canad. J. Math 8, 399–404 (1956)

    Article  MATH  MathSciNet  Google Scholar 

  8. JGF. The Java Grande Forum Multi-threaded Benchmarks (2001), http://www.epcc.ed.ac.uk/computing/research_activities/java_grande/threads.html

  9. JPF. The Java Path Finder model checking tool (2005), http://javapathfinder.sourceforge.net/

  10. Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Transactions on Computers 28(9) (1979)

    Google Scholar 

  11. Lea, D.: The JSR-133 cookbook for compiler writers, http://gee.cs.oswego.edu/dl/jmm/cookbook.html

  12. Manson, J., Pugh, W.: The Java Memory Model Simulator. In: Workshop on Formal Techniques for Java-like Programs, in association with ECOOP (2002)

    Google Scholar 

  13. Manson, J., Pugh, W., Adve, S.: The Java Memory Model. In: ACM Symposium on Principles of Programming Languages (POPL) (2005)

    Google Scholar 

  14. Microsoft. Standard ECMA-335 C# Specification (2005), http://www.ecma-international.org/publications/files/ECMA-ST/Ecma-334.pdf

  15. Microsoft. Standard ECMA-335 Common Language Infrastructure (CLI) (2005), http://www.ecma-international.org/publications/standards/Ecma-335.htm

  16. Morrison, V.: Dotnet discussion: The DOTNET Memory Model, http://discuss.develop.com/archives/wa.exe?A2=ind0203B&L=DOTNET&P=R375

  17. Nalumusu, R., et al.: The “test model checking” approach to the verification of memory models of multiprocessors. In: Computer Aided Verification (CAV) (1998)

    Google Scholar 

  18. Nipkow, T., et al.: Special issue on Java bytecode verification. Journal of Automated Reasoning (JAR) 30(3–4) (2003)

    Google Scholar 

  19. Pugh, W.: Test for sequential consistency of volatiles, http://www.cs.umd.edu/pugh/java/memoryModel/ReadAfterWrite.java

  20. Raynal, M.: Algorithms for mutual exclusion. MIT Press, Cambridge (1986)

    MATH  Google Scholar 

  21. Roychoudhury, A., Mitra, T.: Specifying multithreaded Java semantics for program verification. In: ACM Intl. Conf. on Software Engineering (ICSE) (2002)

    Google Scholar 

  22. Schmidt, D., Harrison, T.: Double-checked locking: An optimization pattern for efficiently initializing and accessing thread-safe objects. In: 3rd annual Pattern Languages of Program Design conference (1996)

    Google Scholar 

  23. Stark, R.F., Borger, E.: An ASM specification of C# threads and the.NET memory model. In: ASM Workshop. LNCS, vol. 3065 (2004)

    Google Scholar 

  24. Yang, Y., Gopalakrishnan, G., Lindstrom, G.: Memory model sensitive data race analysis. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 30–45. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, National University of Singapore,  

    Thuan Quang Huynh & Abhik Roychoudhury

Authors
  1. Thuan Quang Huynh
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Abhik Roychoudhury
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. The University of Texas at Austin,  

    Jayadev Misra

  2. Institut für Informatik, Technische Universität, München,  

    Tobias Nipkow

  3. Department of Computing and Software, McMaster University, 1280 Main Street West, L8S 4K1, Hamilton, Ontario, Canada

    Emil Sekerinski

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Huynh, T.Q., Roychoudhury, A. (2006). A Memory Model Sensitive Checker for C#. In: Misra, J., Nipkow, T., Sekerinski, E. (eds) FM 2006: Formal Methods. FM 2006. Lecture Notes in Computer Science, vol 4085. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11813040_32

Download citation

  • DOI: https://doi.org/10.1007/11813040_32

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-37215-8

  • Online ISBN: 978-3-540-37216-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation