research-article

Open access

Deciding reachability under persistent x86-TSO

Authors:

Parosh Aziz Abdulla,

Mohamed Faouzi Atig,

Ahmed Bouajjani,

K. Narayan Kumar,

Prakash SaivasanAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 5, Issue POPL

Article No.: 56, Pages 1 - 32

https://doi.org/10.1145/3434337

Published: 04 January 2021 Publication History

Abstract

We address the problem of verifying the reachability problem in programs running under the formal model Px86 defined recently by Raad et al. in POPL'20 for the persistent Intel x86 architecture. We prove that this problem is decidable. To achieve that, we provide a new formal model that is equivalent to Px86 and that has the feature of being a well structured system. Deriving this new model is the result of a deep investigation of the properties of Px86 and the interplay of its components.

References

[1]

P.A. Abdulla, S. Aronis, M. Faouzi Atig, B. Jonsson, C. Leonardsson, and K. Sagonas. 2015. Stateless Model Checking for TSO and PSO. In TACAS (LNCS, Vol. 9035 ). Springer, 353-367.

[2]

Parosh Aziz Abdulla, Stavros Aronis, Mohamed Faouzi Atig, Bengt Jonsson, Carl Leonardsson, and Konstantinos Sagonas. 2017a. Stateless model checking for TSO and PSO. Acta Inf. 54, 8 ( 2017 ), 789-818.

Digital Library

[3]

Parosh Aziz Abdulla, Jatin Arora, Mohamed Faouzi Atig, and Shankara Narayanan Krishna. 2019. Verification of programs under the release-acquire semantics. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, Phoenix, AZ, USA, June 22-26, 2019., Kathryn S. McKinley and Kathleen Fisher (Eds.). ACM, 1117-1132. https://doi.org/10.1145/3314221.3314649

Digital Library

[4]

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, Egor Derevenetc, Carl Leonardsson, and Roland Meyer. 2020. Safety Verification under Power. In NETYS 2020 (Lecture Notes in Computer Science). Springer.

[5]

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, and Tuan Phong Ngo. 2017b. Context-Bounded Analysis for POWER. In TACAS. 56-74.

[6]

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, and Tuan Phong Ngo. 2018a. A Load-Bufer Semantics for Total Store Ordering. Logical Methods in Computer Science 14, 1 ( 2018 ). https://doi.org/10.23638/LMCS-14 ( 1 :9) 2018

[7]

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson, and Carl Leonardsson. 2016. Stateless Model Checking for POWER. In CAV (LNCS, Vol. 9780 ). 134-156.

[8]

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson, and Tuan Phong Ngo. 2018b. Optimal stateless model checking under the release-acquire semantics. PACMPL 2, OOPSLA ( 2018 ), 135 : 1-135 : 29. https://doi.org/10.1145/3276505

Digital Library

[9]

Parosh Aziz Abdulla, Karlis Cerans, Bengt Jonsson, and Yih-Kuen Tsay. 1996. General Decidability Theorems for InfiniteState Systems. In Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27-30, 1996. IEEE Computer Society, 313-321. https://doi.org/10.1109/LICS. 1996.561359

[10]

Parosh Aziz Abdulla and Bengt Jonsson. 1993. Verifying Programs with Unreliable Channels. In Proceedings of the Eighth Annual Symposium on Logic in Computer Science (LICS '93), Montreal, Canada, June 19-23, 1993. IEEE Computer Society, 160-170. https://doi.org/10.1109/LICS. 1993.287591

[11]

Jade Alglave, Daniel Kroening, Vincent Nimal, and Michael Tautschnig. 2013b. Software Verification for Weak Memory via Program Transformation. In Programming Languages and Systems-22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings (Lecture Notes in Computer Science, Vol. 7792 ), Matthias Felleisen and Philippa Gardner (Eds.). Springer, 512-532. https://doi.org/10.1007/978-3-642-37036-6_28

Digital Library

[12]

Jade Alglave, Daniel Kroening, and Michael Tautschnig. 2013a. Partial Orders for Eficient Bounded Model Checking of Concurrent Software. In Computer Aided Verification-25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings (Lecture Notes in Computer Science, Vol. 8044 ), Natasha Sharygina and Helmut Veith (Eds.). Springer, 141-157. https://doi.org/10.1007/978-3-642-39799-8_9

[13]

Jade Alglave, Luc Maranget, and Michael Tautschnig. 2014. Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory. ACM Trans. Program. Lang. Syst. 36, 2 ( 2014 ), 7 : 1-7 : 74.

Digital Library

[14]

ARM. 2018. ARM architecture reference manual ARMv8, for ARMv8-A architecture profile (DDI 0487D.a).

[15]

Joy Arulraj and Andrew Pavlo. 2017. How to Build a Non-Volatile Memory Database Management System. In SIGMOD, Semih Salihoglu, Wenchao Zhou, Rada Chirkova, Jun Yang, and Dan Suciu (Eds.). ACM.

[16]

Mohamed Faouzi Atig, Ahmed Bouajjani, Sebastian Burckhardt, and Madanlal Musuvathi. 2010. On the verification problem for weak memory models. In Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010, Manuel V. Hermenegildo and Jens Palsberg (Eds.). ACM, 7-18. https://doi.org/10.1145/1706299.1706303

Digital Library

[17]

Mohamed Faouzi Atig, Ahmed Bouajjani, Sebastian Burckhardt, and Madanlal Musuvathi. 2012. What's Decidable about Weak Memory Models?. In Programming Languages and Systems-21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24-April 1, 2012. Proceedings (Lecture Notes in Computer Science, Vol. 7211 ), Helmut Seidl (Ed.). Springer, 26-46. https://doi.org/10.1007/978-3-642-28869-2_2

Digital Library

[18]

Mohamed Faouzi Atig, Ahmed Bouajjani, and Gennaro Parlato. 2011. Getting Rid of Store-Bufers in TSO Analysis. In CAV (LNCS, Vol. 6806 ). Springer, 99-115.

[19]

Mohamed Faouzi Atig, Ahmed Bouajjani, and Gennaro Parlato. 2014. Context-Bounded Analysis of TSO Systems. In From Programs to Systems. The Systems perspective in Computing-ETAPS Workshop, FPS 2014, in Honor of Joseph Sifakis, Grenoble, France, April 6, 2014. Proceedings. 21-38.

[20]

M. Batty, S. Owens, S. Sarkar, P. Sewell, and T. Weber. 2011. Mathematizing C+ + concurrency. In POPL. ACM, 55-66.

[21]

Sebastian Burckhardt. 2014. Principles of Eventual Consistency. Foundations and Trends in Programming Languages 1, 1-2 ( 2014 ), 1-150.

Digital Library

[22]

Nachshon Cohen, David T. Aksun, and James R. Larus. 2018. Object-oriented recovery for non-volatile memory. PACMPL 2, OOPSLA ( 2018 ).

[23]

Brian Demsky and Patrick Lam. 2015. SATCheck: SAT-directed stateless model checking for SC and TSO. In OOPSLA. ACM, 20-36.

[24]

Alain Finkel and Philippe Schnoebelen. 2001. Well-structured transition systems everywhere! Theor. Comput. Sci. 256, 1-2 ( 2001 ), 63-92. https://doi.org/10.1016/S0304-3975 ( 00 ) 00102-X

Digital Library

[25]

Shaked Flur, Kathryn E. Gray, Christopher Pulte, Susmit Sarkar, Ali Sezgin, Luc Maranget, Will Deacon, and Peter Sewell. 2016. Modelling the ARMv8 architecture, operationally: concurrency and ISA. In POPL. ACM, 608-621.

[26]

Alexey Gotsman, Hongseok Yang, Carla Ferreira, Mahsa Najafzadeh, and Marc Shapiro. 2016. 'Cause I'm strong enough: reasoning about consistency choices in distributed systems. In POPL 2016. 371-384.

Digital Library

[27]

Intel. 2019a. Architectures Software Developer's Manual (Combined Volumes). Software.intel.com.

[28]

Intel (Ed.). 2019b. Intel 64 and IA-32 Architectures Software Developer's Manual (Combined Volumes). Intel.

[29]

Intel. 2019c. Intel Optane Technology. https://www.intel.com/content/www/us/en/architecture-and-technology/inteloptane-technology. html.

[30]

Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, and Derek Dreyer. 2017. A promising semantics for relaxedmemory concurrency. In POPL 2017. 175-189.

[31]

Artem Khyzha and Ori Lahav. 2021. Taming x86-TSO Persistency. Proc. ACM Program. Lang. 5, POPL, Article 47 ( Jan. 2021 ), 29 pages. https://doi.org/10.1145/3434328

Digital Library

[32]

Michalis Kokologiannakis, Ori Lahav, Konstantinos Sagonas, and Viktor Vafeiadis. 2018. Efective stateless model checking for C/C++ concurrency. PACMPL 2 ( 2018 ), 17 : 1-17 : 32.

[33]

Michalis Kokologiannakis, Azalea Raad, and Viktor Vafeiadis. 2019. Efective lock handling in stateless model checking. Proc. ACM Program. Lang. 3, OOPSLA ( 2019 ), 173 : 1-173 : 26. https://doi.org/10.1145/3360599

Digital Library

[34]

Michalis Kokologiannakis and Viktor Vafeiadis. 2020. HMC: Model Checking for Hardware Memory Models. In ASPLOS '20: Architectural Support for Programming Languages and Operating Systems, Lausanne, Switzerland, March 16-20, 2020 [ ASPLOS 2020 was canceled because of COVID-19], James R. Larus, Luis Ceze, and Karin Strauss (Eds.). ACM, 1157-1171. https://doi.org/10.1145/3373376.3378480

Digital Library

[35]

Ori Lahav and Udi Boker. 2020. Decidable verification under a causally consistent shared memory. In Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020, London, UK, June 15-20, 2020, Alastair F. Donaldson and Emina Torlak (Eds.). ACM, 211-226. https://doi.org/10.1145/3385412.3385966

Digital Library

[36]

Ori Lahav, Nick Giannarakis, and Viktor Vafeiadis. 2016. Taming release-acquire consistency. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20-22, 2016, Rastislav Bodík and Rupak Majumdar (Eds.). ACM, 649-662.

Digital Library

[37]

Sihang Liu, Korakit Seemakhupt, Yizhou Wei, Thomas F. Wenisch, Aasheesh Kolli, and Samira Khan. 2020. Cross Failure Bug Detection in Persistent Memory Programs. In ASPLOS.

[38]

Sihang Liu, Yizhou Wei, Jishen Zhao, Aasheesh Kolli, and Samira Manabi Khan. 2019. PMTest: A Fast and Flexible Testing Framework for Persistent Memory Programs. In Proceedings of the Twenty-Fourth International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2019, Providence, RI, USA, April 13-17, 2019, Iris Bahar, Maurice Herlihy, Emmett Witchel, and Alvin R. Lebeck (Eds.). ACM, 411-425. https://doi.org/10.1145/3297858.3304015

Digital Library

[39]

Sela Mador-Haim, Luc Maranget, Susmit Sarkar, Kayvan Memarian, Jade Alglave, Scott Owens, Rajeev Alur, Milo M. K. Martin, Peter Sewell, and Derek Williams. 2012. An Axiomatic Memory Model for POWER Multiprocessors. In Computer Aided Verification-24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings (Lecture Notes in Computer Science, Vol. 7358 ), P. Madhusudan and Sanjit A. Seshia (Eds.). Springer, 495-512.

Digital Library

[40]

Kyndylan Nienhuis, Kayvan Memarian, and Peter Sewell. 2016. An operational semantics for C/C++11 concurrency. In OOPSLA. ACM, 111-128.

[41]

Steven Pelley, Peter M. Chen, and Thomas F. Wenisch. 2014. Memory persistency. In ISCA.

[42]

Anton Podkopaev, Ori Lahav, and Viktor Vafeiadis. 2019. Bridging the gap between programming languages and hardware weak memory models. Proc. ACM Program. Lang. 3, POPL ( 2019 ), 69 : 1-69 : 31. https://doi.org/10.1145/3290382

Digital Library

[43]

Azalea Raad and Viktor Vafeiadis. 2018. Persistence semantics for weak memory: integrating epoch persistency with the TSO memory model. Proc. ACM Program. Lang. 2, OOPSLA ( 2018 ), 137 : 1-137 : 27. https://doi.org/10.1145/3276507

Digital Library

[44]

Azalea Raad, John Wickerson, Gil Neiger, and Viktor Vafeiadis. 2020. Persistency semantics of the Intel-x86 architecture. PACMPL 4, POPL ( 2020 ), 11 : 1-11 : 31. https://doi.org/10.1145/3371079

Digital Library

[45]

Azalea Raad, John Wickerson, and Viktor Vafeiadis. 2019. Weak persistency semantics from the ground up: formalising the persistency semantics of ARMv8 and transactional models. Proc. ACM Program. Lang. 3, OOPSLA ( 2019 ), 135 : 1-135 : 27. https://doi.org/10.1145/3360561

Digital Library

[46]

Peter Sewell, Susmit Sarkar, Scott Owens, Francesco Zappa Nardelli, and Magnus O. Myreen. 2010. x86-TSO: a rigorous and usable programmer's model for x86 multiprocessors. Commun. ACM 53, 7 ( 2010 ), 89-97.

[47]

Fei Xia, Dejun Jiang, Jin Xiong, and Ninghui Sun. 2017. HiKV: A Hybrid Index Key-Value Store for DRAM-NVM Memory Systems. In USENIX ATC, Dilma Da Silva and Bryan Ford (Eds.).

Cited By

Ambal GDongol BEran HKlimis VLahav ORaad A(2024)Semantics of Remote Direct Memory Access: Operational and Declarative Models of RDMA on TSO ArchitecturesProceedings of the ACM on Programming Languages10.1145/36897818:OOPSLA2(1982-2009)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689781
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
Vafeiadi Bila EDongol B(2024)A verified durable transactional mutex lock for persistent x86-TSOFormal Methods in System Design10.1007/s10703-024-00462-1Online publication date: 31-Jul-2024
https://doi.org/10.1007/s10703-024-00462-1
Show More Cited By

Index Terms

Deciding reachability under persistent x86-TSO
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Formal software verification
2. Theory of computation
  1. Logic
    1. Verification by model checking

Recommendations

Verification under Intel-x86 with Persistency

The full semantics of the Intel-x86 architecture has been defined by Raad et al in POPL 2022, extending the earlier formalization based on the TSO memory model incorporating persistency. This new semantics involves an intricate combination of the SC, TSO,...
Formal Verification for C Program

Iterative abstraction refinement has emerged in the last few years as the leading approach to software model checking. We present an approach for automatically verifying C programs against safety specifications based on finite state machine. The ...
Accelerating Software Model Checking Based on Program Backbone
APPT 2013: Revised Selected Papers of the 10th International Symposium on Advanced Parallel Processing Technologies - Volume 8299

Model checking technique has been gradually applied to verify the reliability of software systems. However, as to software with large scale and complex structure, the verification procedure suffers from the state space explosion, thus leading to a low ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 5, Issue POPL

January 2021

1789 pages

EISSN:2475-1421

DOI:10.1145/3445980

Issue’s Table of Contents

Copyright © 2021 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 04 January 2021

Published in PACMPL Volume 5, Issue POPL

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

9
Total Citations
View Citations
698
Total Downloads

Downloads (Last 12 months)105
Downloads (Last 6 weeks)24

Reflects downloads up to 10 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Ambal GDongol BEran HKlimis VLahav ORaad A(2024)Semantics of Remote Direct Memory Access: Operational and Declarative Models of RDMA on TSO ArchitecturesProceedings of the ACM on Programming Languages10.1145/36897818:OOPSLA2(1982-2009)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689781
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
Vafeiadi Bila EDongol B(2024)A verified durable transactional mutex lock for persistent x86-TSOFormal Methods in System Design10.1007/s10703-024-00462-1Online publication date: 31-Jul-2024
https://doi.org/10.1007/s10703-024-00462-1
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
Krishna SGodbole AMeyer RChakraborty SMilani AWoelfel P(2022)Parameterized Verification under Release Acquire is PSPACE-completeProceedings of the 2022 ACM Symposium on Principles of Distributed Computing10.1145/3519270.3538445(482-492)Online publication date: 20-Jul-2022
https://dl.acm.org/doi/10.1145/3519270.3538445
Raad AMaranget LVafeiadis V(2022)Extending Intel-x86 consistency and persistency: formalising the semantics of Intel-x86 memory types and non-temporal storesProceedings of the ACM on Programming Languages10.1145/34986836:POPL(1-31)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498683
Abdulla PAtig MBouajjani AJonsson BKumar KSaivasan P(2022)Consistency and Persistency in Program Verification: Challenges and OpportunitiesPrinciples of Systems Design10.1007/978-3-031-22337-2_24(494-510)Online publication date: 29-Dec-2022
https://doi.org/10.1007/978-3-031-22337-2_24
Bila EDongol BLahav ORaad AWickerson J(2022)View-Based Owicki–Gries Reasoning for Persistent x86-TSOProgramming Languages and Systems10.1007/978-3-030-99336-8_9(234-261)Online publication date: 29-Mar-2022
https://doi.org/10.1007/978-3-030-99336-8_9
Khyzha ALahav O(2021)Taming x86-TSO persistencyProceedings of the ACM on Programming Languages10.1145/34343285:POPL(1-29)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434328

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents