[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ Skip to main content
Springer Nature Link
Log in

GPS\(+\): Reasoning About Fences and Relaxed Atomics

  • Published:
International Journal of Parallel Programming Aims and scope Submit manuscript

Abstract

In order to support efficient compilation to modern architectures, mainstream programming languages, such as C/C\(++\) and Java, have adopted weak (or relaxed) memory models. According to these weak memory models, multithreaded programs are allowed to exhibit behaviours that would have been inconsistent under the traditional strong (i.e., sequentially consistent) memory model. This makes the task of reasoning about concurrent programs even more challenging. The GPS framework, developed by Turon et al. (ACM OOPSLA, pp 691–707, 2014), has made a step forward towards tackling this challenge for the release–acquire fragment of the C11 memory model. By integrating ghost states, per-location protocols and separation logic, GPS can successfully verify programs with release–acquire atomics. In this paper, we introduced GPS\(+\) to support a larger class of C11 programs, that is, programs with release–acquire atomics, relaxed atomics and release–acquire fences. Key elements of our proposed logic include two new types of assertions, a more expressive resource model and a set of new verification rules.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (United Kingdom)

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8
Fig. 9
Fig. 10
Fig. 11
Fig. 12
Fig. 13
Fig. 14
Fig. 15
Fig. 16
Fig. 17

Similar content being viewed by others

Notes

  1. Here we explain these examples in an intuitive manner, leaving the formal introductions of syntax and semantics to the next section.

  2. Or via release sequences, which we do not consider in this paper.

  3. In GPS, \(|r|\) represents the duplicable part of \(r\): \(r=r\oplus |r|\). For duplicable items in \(r\), like atomic values and the known escrow set, stripping keeps them unchanged. That is, we have \(|r|.\varSigma =r.\varSigma \), and if \(\ell _\mathtt {at}\) is an atomic location in \(r\) we have \(|r|.\varPi (\ell _\mathtt {at})=r.\varPi (\ell _\mathtt {at})\). For non-duplicable items, like non-atomic values, stripping removes them. For example, if \(\ell _\mathtt {na}\) is a non-atomic location in \(r\) we have \(|r|.\varPi (\ell _\mathtt {na})=\bot \). The value \(\diamond \) of ghost type \(\mathsf {Tok}\) is also not duplicable, and all ghost locations of type \(\mathsf {Tok}\) will be set as empty after stripping: \(|r|.g(\mathsf {Tok})(-)=\xi \).

References

  1. Batty, M., Owens, S., Sarkar, S., Sewell, P., Weber, T.: Mathematizing C++ concurrency. In: Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’11, pp. 55–66. ACM, New York (2011)

  2. Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: a practical system for verifying concurrent C. In: International Conference on Theorem Proving in Higher Order Logics (TPHOLs ’09), pp. 23–42 (2009)

    Google Scholar 

  3. da Rocha Pinto, P., Dinsdale-Young, T., Gardner, P.: TaDA: a logic for time and data abstraction. In: ECOOP, pp. 207–231 (2014)

  4. Dinsdale-Young, T., Dodds, M., Gardner, P., Parkinson, M.J., Vafeiadis, V.: Concurrent abstract predicates. In: ECOOP, pp. 504–528 (2010)

  5. Dinsdale-Young, T., Birkedal, L., Gardner, P., Parkinson, M.J., Yang, H.: Views: compositional reasoning for concurrent programs. In: ACM POPL, pp. 287–300 (2013)

    Article  Google Scholar 

  6. Dodds, M., Feng, X., Parkinson, M., Vafeiadis, V.: Deny-guarantee reasoning. In: ESOP, pp. 363–377 (2009)

  7. Doko, M., Vafeiadis, V.: A Program Logic for C11 Memory Fences, pp. 413–430. Springer, Berlin (2016)

    Google Scholar 

  8. Feng, X.: Local rely-guarantee Reasoning. In: ACM POPL, pp. 315–327 (2009)

    Article  Google Scholar 

  9. He, M., Vafeiadis, V., Qin, S., Ferreira, J.F.: GPS+: Reasoning About Fences and Relaxed Atomics (Technical Report) (2017). http://pls.tees.ac.uk/gpsp/report.pdf, School of Computing, Teesside University

  10. ISO/IEC 9899:2011. Programming Language C (2011)

  11. Jensen, J.B., Birkedal, L.: Fictional separation logic. In: ESOP, pp. 377–396 (2012)

    Chapter  Google Scholar 

  12. Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM TOPLAS 5, 596–619 (1983)

    Article  Google Scholar 

  13. Jung, R., Swasey, D., Sieczkowski, F., Svendsen, K., Turon, A., Birkedal, L., Dreyer, D.: Iris: monoids and invariants as an orthogonal basis for concurrent reasoning. In: ACM POPL, pp. 637–650 (2015)

    Article  Google Scholar 

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

    Article  Google Scholar 

  15. Leino, K.R., Müller, P., Smans, J.: Verification of concurrent programs with Chalice. In: Foundations of Security Analysis and Design V, pp. 195–222 (2009)

    Chapter  Google Scholar 

  16. Ley-Wild, R., Nanevski, A.: Subjective auxiliary state for coarse-grained concurrency. In: ACM POPL, pp. 561–574 (2013)

    Article  Google Scholar 

  17. Manson, J., Pugh, W., Adve, S.V.: The Java memory model. In: ACM POPL, pp. 378–391 (2005)

    Article  Google Scholar 

  18. Nanevski, A., Ley-Wild, R., Sergey, I., Delbianco, G.: Communicating state transition systems for fine-grained concurrent resources. In: ESOP, pp. 290–310 (2014)

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

    Article  MathSciNet  Google Scholar 

  20. Svendsen, K., Birkedal, L.: Impredicative concurrent abstract predicates. In: ESOP, pp. 149–168 (2014)

    Chapter  Google Scholar 

  21. Tassarotti, J., Dreyer, D., Vafeiadis, V.: Verifying read-copy-update in a logic for weak memory. In: ACM PLDI, Portland, OR, USA (2015)

  22. Turon, A., Dreyer, D., Birkedal, L.: Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency. In: ICFP, pp. 377–390 (2013)

  23. Turon, A., Vafeiadis, V., Dreyer, D.: GPS: Navigating weak memory with ghosts, protocols, and separation. In: ACM OOPSLA, pp. 691–707 (2014)

  24. Vafeiadis, V., Parkinson, M.J.: A marriage of rely/guarantee and separation logic. In: 18th International Conference on Concurrency Theory (CONCUR’07), volume 4703 of Lecture Notes in Computer Science, pp. 256–271 (2007)

  25. Vafeiadis, V., Narayan, C.: Relaxed separation logic: a program logic for C11 concurrency. In: ACM OOPSLA, pp. 867–884 (2013)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Computing, Teesside University, Middlesbrough, UK

    Mengda He, Shengchao Qin & João F. Ferreira

  2. Max Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, Germany

    Viktor Vafeiadis

  3. HASLab/INESC TEC, Universidade do Minho, Braga, Portugal

    João F. Ferreira

Authors
  1. Mengda He
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Viktor Vafeiadis
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Shengchao Qin
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. João F. Ferreira
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Mengda He.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

He, M., Vafeiadis, V., Qin, S. et al. GPS\(+\): Reasoning About Fences and Relaxed Atomics. Int J Parallel Prog 46, 1157–1183 (2018). https://doi.org/10.1007/s10766-017-0518-x

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10766-017-0518-x

Keywords

Search

Navigation