Article

Verifying Reachability for TSO Programs with Dynamic Thread Creation

Authors:

Parosh Aziz Abdulla,

Mohamed Faouzi Atig,

Ahmed Bouajjani,

K. Narayan Kumar,

Prakash SaivasanAuthors Info & Claims

Networked Systems: 10th International Conference, NETYS 2022, Virtual Event, May 17–19, 2022, Proceedings

Pages 283 - 300

https://doi.org/10.1007/978-3-031-17436-0_19

Published: 17 May 2022 Publication History

Abstract

The verification of reachability properties for programs under weak memory models is a hard problem, even undecidable in some cases. The decidability of this problem has been investigated so far in the case of static programs where the number of threads does not change during execution. However, dynamic thread creation is crucial in asynchronous concurrent programming. In this paper, we address the decidability of the reachability problem for dynamic concurrent programs running under TSO. An important issue when considering a TSO model in this case is maintaining causality precedence between operations issued by threads and those issued by their children. We propose a general TSO model that respects causality and prove that the reachability problem for programs with dynamic creation of threads is decidable.

References

[1]

Abdulla PA Well (and better) quasi-ordered transition systems Bull. Symb. Log. 2010 16 4 457-515

[2]

Abdulla, P.A., Arora, J., Atig, M.F., Krishna, S.N.: Verification of programs under the release-acquire semantics. In: McKinley, K.S., Fisher, K. (eds.) Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, Phoenix, AZ, USA, 22–26 June 2019, pp. 1117–1132. ACM (2019).

[3]

Abdulla PA, Atig MF, Bouajjani A, Derevenetc E, Leonardsson C, and Meyer R Georgiou C and Majumdar R On the state reachability problem for concurrent programs under power Networked Systems 2021 Cham Springer 47-59

[4]

Abdulla, P.A., Atig, M.F., Bouajjani, A., Ngo, T.P.: The benefits of duality in verifying concurrent programs under TSO. In: Desharnais, J., Jagadeesan, R. (eds.) 27th International Conference on Concurrency Theory, CONCUR 2016. LIPIcs, Québec City, Canada, 23–26 August 2016, vol. 59, pp. 5:1–5:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2016).

[5]

Abdulla, P.A., Atig, M.F., Bouajjani, A., Ngo, T.P.: A load-buffer semantics for total store ordering. Log. Methods Comput. Sci. 14(1) (2018).

[6]

Abdulla PA, Atig MF, Godbole A, Krishna S, and Vafeiadis V Yoshida N The decidability of verification under PS 2.0 Programming Languages and Systems 2021 Cham Springer 1-29

[7]

Abdulla PA, Atig MF, Lång M, and Ngo TP Bouajjani A and Fauconnier H Precise and sound automatic fence insertion procedure under PSO Networked Systems 2015 Cham Springer 32-47

[8]

Abdulla, P.A., Atig, M.F., Rezvan, R.: Parameterized verification under TSO is PSPACE-complete. Proc. ACM Program. Lang. 4(POPL), 26:1–26:29 (2020).

[9]

Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.: General decidability theorems for infinite-state systems. In: Proceedings 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, 27–30 July 1996, pp. 313–321. IEEE Computer Society (1996).

[10]

Adve, S.V., Hill, M.D.: Weak ordering - a new definition. In: Sohi, G.S. (ed.) 25 Years of the International Symposia on Computer Architecture (Selected Papers), pp. 363–375. ACM (1998).

[11]

Atig, M.F., Bouajjani, A., Burckhardt, S., Musuvathi, M.: On the verification problem for weak memory models. In: Hermenegildo, M.V., Palsberg, J. (eds.) Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, 17–23 January 2010, pp. 7–18. ACM (2010).

[12]

Atig MF, Bouajjani A, Burckhardt S, and Musuvathi M Seidl H What’s decidable about weak memory models? Programming Languages and Systems 2012 Heidelberg Springer 26-46

[13]

Batty, M., Owens, S., Sarkar, S., Sewell, P., Weber, T.: Mathematizing C++ concurrency. In: Ball, T., Sagiv, M. (eds.) Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, 26–28 January 2011, pp. 55–66. ACM (2011).

[14]

Boudol, G., Petri, G.: Relaxed memory models: an operational approach. In: Shao, Z., Pierce, B.C. (eds.) Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, 21–23 January 2009, pp. 392–403. ACM (2009).

[15]

Finkel A and Schnoebelen P Well-structured transition systems everywhere! Theor. Comput. Sci. 2001 256 1–2 63-92

[16]

Kaiser, J., Dang, H., Dreyer, D., Lahav, O., Vafeiadis, V.: Strong logic for weak memory: reasoning about release-acquire consistency in iris. In: Müller, P. (ed.) 31st European Conference on Object-Oriented Programming, ECOOP 2017. LIPIcs, Barcelona, Spain, 19–23 June 2017, vol. 74, pp. 17:1–17:29. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017).

[17]

Lahav, O., Boker, U.: Decidable verification under a causally consistent shared memory. In: Donaldson, A.F., Torlak, E. (eds.) Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020, London, UK, 15–20 June 2020, pp. 211–226. ACM (2020).

[18]

Liu, F., Nedev, N., Prisadnikov, N., Vechev, M.T., Yahav, E.: Dynamic synthesis for relaxed memory models. In: Vitek, J., Lin, H., Tip, F. (eds.) ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2012, Beijing, China, 11–16 June 2012, pp. 429–440. ACM (2012).

[19]

Manson, J., Pugh, W., Adve, S.V.: The Java memory model. In: Palsberg, J., Abadi, M. (eds.) Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, 12–14 January 2005, pp. 378–391. ACM (2005).

[20]

Owens S, Sarkar S, and Sewell P Berghofer S, Nipkow T, Urban C, and Wenzel M A better x86 memory model: x86-TSO Theorem Proving in Higher Order Logics 2009 Heidelberg Springer 391-407

[21]

Sewell P, Sarkar S, Owens S, Nardelli FZ, and Myreen MO x86-TSO: a rigorous and usable programmer’s model for x86 multiprocessors Commun. ACM 2010 53 7 89-97

Cited By

Abdulla PAtig MBouajjani AKumar KSaivasan P(2024)Verification under Intel-x86 with PersistencyProceedings of the ACM on Programming Languages10.1145/36564258:PLDI(1189-1212)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656425
Lahav ODongol BWehrheim H(2023)Rely-Guarantee Reasoning for Causally Consistent Shared MemoryComputer Aided Verification10.1007/978-3-031-37706-8_11(206-229)Online publication date: 17-Jul-2023
https://dl.acm.org/doi/10.1007/978-3-031-37706-8_11

Index Terms

Verifying Reachability for TSO Programs with Dynamic Thread Creation
1. Software and its engineering
2. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning

Index terms have been assigned to the content through auto-classification.

Recommendations

Fast RMWs for TSO: semantics and implementation
PLDI '13

Read-Modify-Write (RMW) instructions are widely used as the building blocks of a variety of higher level synchronization constructs, including locks, barriers, and lock-free data structures. Unfortunately, they are expensive in architectures such as x86 ...
Verification of Boolean programs with unbounded thread creation

Most symbolic software model checkers use abstraction techniques to reduce the verification of infinite-state programs to that of decidable classes. Boolean programs [T. Ball, S.K. Rajamani, Bebop: A symbolic model checker for Boolean programs, in: SPIN ...
Modular verification of concurrent assembly code with dynamic thread creation and termination
Proceedings of the tenth ACM SIGPLAN international conference on Functional programming

Proof-carrying code (PCC) is a general framework that can, in principle, verify safety properties of arbitrary machine-language programs. Existing PCC systems and typed assembly languages, however, can only handle sequential programs. This severely ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

Networked Systems: 10th International Conference, NETYS 2022, Virtual Event, May 17–19, 2022, Proceedings

May 2022

322 pages

ISBN:978-3-031-17435-3

DOI:10.1007/978-3-031-17436-0

Editors:
Mohammed-Amine Koulali
Mohammed First University, Oujda, Morocco
,
Mira Mezini
Technical University of Darmstadt, Darmstadt, Germany

© The Author(s), under exclusive license to Springer Nature Switzerland AG 2022.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 17 May 2022

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 10 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Abdulla PAtig MBouajjani AKumar KSaivasan P(2024)Verification under Intel-x86 with PersistencyProceedings of the ACM on Programming Languages10.1145/36564258:PLDI(1189-1212)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656425
Lahav ODongol BWehrheim H(2023)Rely-Guarantee Reasoning for Causally Consistent Shared MemoryComputer Aided Verification10.1007/978-3-031-37706-8_11(206-229)Online publication date: 17-Jul-2023
https://dl.acm.org/doi/10.1007/978-3-031-37706-8_11

View Options

View options

Figures

Tables

Media

View Table of Conten