Skip to main content
SpringerLink
Log in

Local Data Race Freedom with Non-multi-copy Atomicity

  • Conference paper
  • First Online:
Model Checking Software (SPIN 2018)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10869))

Included in the following conference series:

  • 536 Accesses

Abstract

Data race freedom ensures the sequentially consistent behaviors of concurrent programs under relaxed memory consistency models (MCMs), and reduces the state explosion problem for software model checking with MCMs. However, data race freedom is too strong to include all interesting programs. In this paper, we define small-step operational semantics for relaxed MCMs, define an observable equivalence using the notion of bisimulation, and propose the property of local data race freedom (LDRF), which requires a kind of race freedom locally instead of globally. LDRF includes some interesting programs, such as the independent reads independent writes program, which is well known to exhibit curious behaviors under non-multi-copy atomic MCMs, and some concurrent copying garbage collection algorithms. In this paper, we introduce an optimization method called memory sharing for model checking of LDRF programs, and show that memory sharing optimization mitigates state explosion problems with non-multi-copy atomic MCMs through experiments.

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

Access this chapter

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 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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

Institutional subscriptions

References

  1. Abdulla, P.A., Atig, M.F., Jonsson, B., Leonardsson, C.: Stateless model checking for POWER. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016, Part II. LNCS, vol. 9780, pp. 134–156. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41540-6_8

    Chapter  Google Scholar 

  2. Abe, T.: A verifier of directed acyclic graphs for model checking with memory consistency models. Hardware and Software: Verification and Testing. LNCS, vol. 10629, pp. 51–66. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-70389-3_4

    Chapter  Google Scholar 

  3. Abe, T., Maeda, T.: Observation-based concurrent program logic for relaxed memory consistency models. In: Igarashi, A. (ed.) APLAS 2016. LNCS, vol. 10017, pp. 63–84. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47958-3_4

    Chapter  Google Scholar 

  4. Abe, T., Maeda, T.: Concurrent program logic for relaxed memory consistency models with dependencies across loop iterations. J. Inf. Process. 25, 244–255 (2017)

    Google Scholar 

  5. Adve, S.V., Gharachorloo, K.: Shared memory consistency models: a tutorial. Computer 29(12), 66–76 (1996)

    Article  Google Scholar 

  6. ARM Limited: ARM Architecture Reference Manual (ARMv7-A and ARMv7-R edition) (2012)

    Google Scholar 

  7. ARM Limited: ARM Architecture Reference Manual (ARMv8, for ARMv8-A architecture profile) (2017)

    Google Scholar 

  8. Basten, T., Bošnački, D., Geilen, M.: Cluster-based partial-order reduction. Autom. Softw. Eng. 11(4), 365–402 (2004)

    Article  Google Scholar 

  9. Dolan, S., Sivaramakrishnan, K., Madhavapeddy, A.: Bounding data races in space and time. In: Proceedings of PLDI (2018, to appear)

    Google Scholar 

  10. Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: Proceedings of POPL, pp. 110–121 (2005)

    Article  Google Scholar 

  11. Gao, G.R., Sarkar, V.: Location consistency-a new memory model and cache consistency protocol. IEEE Trans. Comput. 49(8), 798–813 (2000)

    Article  Google Scholar 

  12. IBM Corporation: Power ISA Version 3.0 (2015)

    Google Scholar 

  13. Intel Corporation: A Formal Specification of Intel Itanium Processor Family Memory Ordering (2002)

    Google Scholar 

  14. ISO/IEC 14882:2011: Programming Language C++ (2011)

    Google Scholar 

  15. Jones, R., Hosking, A., Moss, E.: The Garbage Collection Handbook. CRC Press, Boca Rotan (2012)

    Google Scholar 

  16. Kokologiannakis, M., Lahav, O., Sagonas, K., Vafeiadis, V.: Effective stateless model checking for C/C++ concurrency. Proc. ACM Program. Lang. 2(POPL:17), 1–32 (2018)

    Google Scholar 

  17. Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comput. c-28(9), 690–691 (1979)

    Article  Google Scholar 

  18. O’Hearn, P.W.: Resources, concurrency, and local reasoning. Theor. Comput. Sci. 375(1–3), 271–307 (2007)

    Article  MathSciNet  Google Scholar 

  19. Owens, S.: Reasoning about the implementation of concurrency abstractions on x86-TSO. In: D’Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 478–503. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14107-2_23

    Chapter  Google Scholar 

  20. Owens, S., Sarkar, S., Sewell, P.: A better x86 memory model: x86-TSO. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 391–407. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03359-9_27

    Chapter  Google Scholar 

  21. Peled, D.: All from one, one for all: on model checking using representatives. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 409–423. Springer, Heidelberg (1993). https://doi.org/10.1007/3-540-56922-7_34

    Chapter  Google Scholar 

  22. Pizlo, F., Ziarek, L., Maj, P., Hosking, A.L., Blanton, E., Vitek, J.: Schism: fragmentation-tolerant real-time garbage collection. In: Proceedings of PLDI, pp. 146–159 (2010)

    Google Scholar 

  23. Pulte, C., Flur, S., Deacon, W., French, J., Sarkar, S., Sewell, P.: Simplifying ARM concurrency: multicopy-atomic axiomatic and operational models for ARMv8. Proc. ACM Program. Lang. 2(POPL:19), 1–29 (2018)

    Article  Google Scholar 

  24. Ritson, C.G., Ugawa, T., Jones, R.: Exploring garbage collection with Haswell hardware transactional memory. In: Proceedings of ISMM, pp. 105–115 (2014)

    Google Scholar 

  25. Saraswat, V., Jagadeesan, R., Michael, M., von Praun, C.: A theory of memory models. In: Proceedings of PPoPP, pp. 161–172 (2007)

    Google Scholar 

  26. Sarkar, S., Sewell, P., Alglave, J., Maranget, L., Williams, D.: Understanding POWER multiprocessors. In: Proceedings of PLDI, pp. 175–186 (2011)

    Article  Google Scholar 

  27. Ugawa, T., Abe, T., Maeda, T.: Model checking copy phases of concurrent copying garbage collection with various memory models. Proc. ACM Program. Lang. 1(OOPSLA:53), 1–26 (2017)

    Article  Google Scholar 

  28. Vafeiadis, V.: Sequential consistency considered harmful. In: New Challenges in Parallelism (Report from Dagstuhl Seminar 17451), p. 21 (2018)

    Google Scholar 

Download references

Acknowledgments

The author thanks Toshiyuki Maeda and Tomoharu Ugawa. The motivation of this work was fostered through discussions with them. The author also thanks the anonymous reviewers for several comments to improve the paper. This work was supported by JSPS KAKENHI Grant Number 16K21335.

Author information

Authors and Affiliations

  1. STAIR Lab, Chiba Institute of Technology, 2-17-1 Tsudanuma, Narashino, Chiba, 275-0016, Japan

    Tatsuya Abe

Authors
  1. Tatsuya Abe
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Tatsuya Abe .

Editor information

Editors and Affiliations

  1. University of Málaga, Málaga, Spain

    María del Mar Gallardo

  2. University of Málaga, Málaga, Spain

    Pedro Merino

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Abe, T. (2018). Local Data Race Freedom with Non-multi-copy Atomicity. In: Gallardo, M., Merino, P. (eds) Model Checking Software. SPIN 2018. Lecture Notes in Computer Science(), vol 10869. Springer, Cham. https://doi.org/10.1007/978-3-319-94111-0_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-94111-0_12

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-94110-3

  • Online ISBN: 978-3-319-94111-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation