[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ skip to main content
research-article
Open access

Persistency semantics of the Intel-x86 architecture

Published: 20 December 2019 Publication History

Abstract

Emerging non-volatile memory (NVM) technologies promise the durability of disks with the performance of RAM. To describe the persistency guarantees of NVM, several memory persistency models have been proposed in the literature. However, the persistency semantics of the ubiquitous x86 architecture remains unexplored to date. To close this gap, we develop the Px86 (‘persistent x86’) model, formalising the persistency semantics of Intel-x86 for the first time. We formulate Px86 both operationally and declaratively, and prove that the two characterisations are equivalent. To demonstrate the application of Px86, we develop two persistent libraries over Px86: a persistent transactional library, and a persistent variant of the Michael–Scott queue. Finally, we encode our declarative Px86 model in Alloy and use it to generate persistency litmus tests automatically.

Supplementary Material

WEBM File (a11-raad.webm)

References

[1]
Parosh Aziz Abdulla, Mohamed Faouzi Atig, and Tuan-Phong Ngo. 2015. The Best of Both Worlds: Trading Efficiency and Optimality in Fence Insertion for TSO. In Proceedings of the 24th European Symposium on Programming on Programming Languages and Systems - Volume 9032. Springer-Verlag New York, Inc., New York, NY, USA, 308–332.
[2]
Hillel Avni, Eliezer Levy, and Avi Mendelson. 2015. Hardware Transactions in Nonvolatile Memory. In Proceedings of the 29th International Symposium on Distributed Computing - Volume 9363 (DISC 2015). Springer-Verlag, Berlin, Heidelberg, 617–630.
[3]
Hans-J. Boehm and Dhruva R. Chakrabarti. 2016. Persistence Programming Models for Non-volatile Memory. In Proceedings of the 2016 ACM SIGPLAN International Symposium on Memory Management (ISMM 2016). ACM, New York, NY, USA, 55–67.
[4]
Dhruva R. Chakrabarti, Hans-J. Boehm, and Kumud Bhandari. 2014. Atlas: Leveraging Locks for Non-volatile Memory Consistency. SIGPLAN Not. 49, 10 (Oct. 2014), 433–452.
[5]
Andreas Chatzistergiou, Marcelo Cintra, and Stratis D. Viglas. 2015. REWIND: Recovery Write-ahead system for In-memory Non-volatile Data-structures. Proc. VLDB Endow. 8, 5 (Jan. 2015), 497–508.
[6]
Nathan Chong, Tyler Sorensen, and John Wickerson. 2018. The Semantics of Transactions and Weak Memory in x86, Power, ARM, and C++. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2018). ACM, New York, NY, USA, 211–225.
[7]
Joel Coburn, Adrian M. Caulfield, Ameen Akel, Laura M. Grupp, Rajesh K. Gupta, Ranjit Jhala, and Steven Swanson. 2011. NV-Heaps: Making Persistent Objects Fast and Safe with Next-generation, Non-volatile Memories. SIGPLAN Not. 46, 3 (March 2011), 105–118.
[8]
Jeremy Condit, Edmund B. Nightingale, Christopher Frost, Engin Ipek, Benjamin Lee, Doug Burger, and Derrick Coetzee. 2009. Better I/O Through Byte-addressable, Persistent Memory. In Proceedings of the ACM SIGOPS 22Nd Symposium on Operating Systems Principles (SOSP ’09). ACM, New York, NY, USA, 133–146.
[9]
Harold Cooper. 2008. Persistent Collections. (2008). https://pcollections.org/
[10]
Michal Friedman, Maurice Herlihy, Virendra Marathe, and Erez Petrank. 2018. A Persistent Lock-free Queue for Non-volatile Memory. In Proceedings of the 23rd ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP ’18). ACM, New York, NY, USA, 28–40.
[11]
Kourosh Gharachorloo, Daniel Lenoski, James Laudon, Phillip Gibbons, Anoop Gupta, and John Hennessy. 1990. Memory Consistency and Event Ordering in Scalable Shared-memory Multiprocessors. SIGARCH Comput. Archit. News 18, 2SI (May 1990), 15–26.
[12]
Vaibhav Gogte, Stephan Diestelhorst, William Wang, Satish Narayanasamy, Peter M. Chen, and Thomas F. Wenisch. 2018. Persistency for Synchronization-free Regions. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2018). ACM, New York, NY, USA, 46–61.
[13]
Maurice P. Herlihy and Jeannette M. Wing. 1990. Linearizability: A Correctness Condition for Concurrent Objects. ACM Trans. Program. Lang. Syst. 12, 3 (July 1990), 463–492.
[14]
Intel. 2014. Intel architecture instruction set extensions programming reference. (2014). https://software.intel.com/sites/ default/files/managed/07/b7/319433- 023.pdf
[15]
Intel. 2015. Persistent Memory Programming. (2015). http://pmem.io/
[16]
Intel. 2019. 3D XPoint. (2019). https://www.intel.com/content/www/us/en/architecture- and- technology/intel- optanetechnology.html
[17]
Intel. 2019. Intel 64 and IA-32 Architectures Software Developer’s Manual (Combined Volumes). (May 2019). https:// software.intel.com/sites/default/files/managed/39/c5/325462- sdm- vol- 1- 2abcd- 3abcd.pdf Order Number: 325462-069US.
[18]
ITRS. 2011. Process Integration, devices, and structures. (2011). http://www.maltiel- consulting.com/ITRS_2011- ProcessIntegration- Devices- Structures.pdf International technology roadmap for semiconductors.
[19]
Joseph Izraelevitz, Terence Kelly, and Aasheesh Kolli. 2016a. Failure-Atomic Persistent Memory Updates via JUSTDO Logging. In Proceedings of the Twenty-First International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS ’16). ACM, New York, NY, USA, 427–442.
[20]
Joseph Izraelevitz, Hammurabi Mendes, and Michael L. Scott. 2016b. Linearizability of Persistent Memory Objects Under a Full-System-Crash Failure Model. In Distributed Computing, Cyril Gavoille and David Ilcinkas (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 313–327.
[21]
Daniel Jackson. 2012. Software Abstractions – Logic, Language, and Analysis (revised edition ed.). MIT Press.
[22]
Abhishek Kumar Jain, Scott Lloyd, and Maya Gokhale. 2018. Microscope on Memory: MPSoC-Enabled Computer Memory System Assessments. In 2018 IEEE 26th Annual International Symposium on Field-Programmable Custom Computing Machines (FCCM). 173–180.
[23]
Arpit Joshi, Vijay Nagarajan, Marcelo Cintra, and Stratis Viglas. 2015. Efficient Persist Barriers for Multicores. In Proceedings of the 48th International Symposium on Microarchitecture (MICRO-48). ACM, New York, NY, USA, 660–671.
[24]
T. Kawahara, K. Ito, R. Takemura, and H. Ohno. 2012. Spin-transfer torque RAM technology: Review and prospect. Microelectronics Reliability 52, 4 (2012), 613 – 627.
[25]
Michalis Kokologiannakis, Azalea Raad, and Viktor Vafeiadis. 2019a. Effective Lock Handling in Stateless Model Checking. Proc. ACM Program. Lang. 3, OOPSLA, Article 173 (Oct. 2019), 26 pages.
[26]
Michalis Kokologiannakis, Azalea Raad, and Viktor Vafeiadis. 2019b. Model Checking for Weakly Consistent Libraries. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2019). ACM, New York, NY, USA, 96–110.
[27]
Aasheesh Kolli, Vaibhav Gogte, Ali Saidi, Stephan Diestelhorst, Peter M. Chen, Satish Narayanasamy, and Thomas F. Wenisch. 2017. Language-level Persistency. In Proceedings of the 44th Annual International Symposium on Computer Architecture (ISCA ’17). ACM, New York, NY, USA, 481–493.
[28]
Aasheesh Kolli, Steven Pelley, Ali Saidi, Peter M. Chen, and Thomas F. Wenisch. 2016a. High-Performance Transactions for Persistent Memories. SIGPLAN Not. 51, 4 (March 2016), 399–411.
[29]
Aasheesh Kolli, Jeff Rosen, Stephan Diestelhorst, Ali Saidi, Steven Pelley, Sihang Liu, Peter M. Chen, and Thomas F. Wenisch. 2016b. Delegated Persist Ordering. In The 49th Annual IEEE/ACM International Symposium on Microarchitecture (MICRO-49). IEEE Press, Piscataway, NJ, USA, Article 58, 13 pages. http://dl.acm.org/citation.cfm?id=3195638.3195709
[30]
Leslie Lamport. 1979. How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs. IEEE Trans. Computers 28, 9 (Sept. 1979), 690–691.
[31]
Benjamin C. Lee, Engin Ipek, Onur Mutlu, and Doug Burger. 2009. Architecting Phase Change Memory As a Scalable Dram Alternative. In Proceedings of the 36th Annual International Symposium on Computer Architecture (ISCA ’09). ACM, New York, NY, USA, 2–13.
[32]
Sihang Liu, Yizhou Wei, Jishen Zhao, Aasheesh Kolli, and Samira 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 ’19).
[33]
Daniel Lustig, Andrew Wright, Alexandros Papakonstantinou, and Olivier Giroux. 2017. Automated Synthesis of Comprehensive Memory Model Litmus Test Suites. In Proceedings of the Twenty-Second International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS ’17).
[34]
Maged M. Michael and Michael L. Scott. 1996. Simple, Fast, and Practical Non-blocking and Blocking Concurrent Queue Algorithms. In Proceedings of the Fifteenth Annual ACM Symposium on Principles of Distributed Computing (PODC ’96). ACM, New York, NY, USA, 267–275.
[35]
Aleksandar Milicevic, Joseph P. Near, Eunsuk Kang, and Daniel Jackson. 2015. Alloy*: A General-Purpose Higher-Order Relational Constraint Solver. In International Conference on Software Engineering (ICSE).
[36]
Faisal Nawab, Joseph Izraelevitz, Terence Kelly, Charles B. Morrey, Dhruva R. Chakrabarti, and Michael James Scott. 2017. Dalí: A Periodically Persistent Hash Map. In DISC.
[37]
Scott Owens. 2010. Reasoning About the Implementation of Concurrency Abstractions on x86-TSO. In Proceedings of the 24th European Conference on Object-oriented Programming (ECOOP’10). Springer-Verlag, Berlin, Heidelberg, 478–503. http://dl.acm.org/citation.cfm?id=1883978.1884011
[38]
PCJ. 2016. Persistent Collections for Java. (2016). https://github.com/pmem/pcj
[39]
Steven Pelley, Peter M. Chen, and Thomas F. Wenisch. 2014. Memory Persistency. In Proceeding of the 41st Annual International Symposium on Computer Architecuture (ISCA ’14). IEEE Press, Piscataway, NJ, USA, 265–276. http://dl.acm.org/citation. cfm?id=2665671.2665712
[40]
Azalea Raad, Marko Doko, Lovro Rožić, Ori Lahav, and Viktor Vafeiadis. 2019. On Library Correctness Under Weak Memory Consistency: Specifying and Verifying Concurrent Libraries Under Declarative Consistency Models. Proc. ACM Program. Lang. 3, POPL, Article 68 (Jan. 2019), 31 pages.
[41]
Azalea Raad, Ori Lahav, and Viktor Vafeiadis. 2018. On Parallel Snapshot Isolation and Release/Acquire Consistency. In Programming Languages and Systems, Amal Ahmed (Ed.). Springer International Publishing, Cham, 940–967.
[42]
Azalea Raad, Ori Lahav, and Viktor Vafeiadis. 2019a. On the Semantics of Snapshot Isolation. In Verification, Model Checking, and Abstract Interpretation, Constantin Enea and Ruzica Piskac (Eds.). Springer International Publishing, Cham, 1–23.
[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, Article 137 (Oct. 2018), 27 pages.
[44]
Azalea Raad, John Wickerson, and Viktor Vafeiadis. 2019b. Weak Persistency Semantics from the Ground Up: Formalising the Persistency Semantics of ARMv8 and Transactional Models. Proc. ACM Program. Lang. 3, OOPSLA, Article 135 (Oct. 2019), 27 pages.
[45]
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 (July 2010), 89–97.
[46]
Hongping Shu, Hongyu Chen, Hao Liu, Youyou Lu, Qingda Hu, and Jiwu Shu. 2018. Empirical Study of Transactional Management for Persistent Memory. 61–66.
[47]
SPARC. 1992. The SPARC Architecture Manual: Version 8. Prentice-Hall, Inc., Upper Saddle River, NJ, USA.
[48]
D. B. Strukov, G. S. Snider, D. R. Stewart, and R. S. Williams. 2008. The missing memristor found. Nature 453 (2008), 80 – 83.
[49]
Arash Tavakkol, Aasheesh Kolli, Stanko Novakovic, Kaveh Razavi, Juan Gómez-Luna, Hasan Hassan, Claude Barthels, Yaohua Wang, Mohammad Sadrosadati, Saugata Ghose, Ankit Singla, Pratap Subrahmanyam, and Onur Mutlu. 2018. Enabling Efficient RDMA-based Synchronous Mirroring of Persistent Memory Transactions. CoRR abs/1810.09360 (2018). arXiv: 1810.09360 http://arxiv.org/abs/1810.09360
[50]
Haris Volos, Andres Jaan Tack, and Michael M. Swift. 2011. Mnemosyne: Lightweight Persistent Memory. SIGPLAN Not. 47, 4 (March 2011), 91–104.
[51]
Xiaojian Wu and A. L. Narasimha Reddy. 2011. SCMFS: A File System for Storage Class Memory. In Proceedings of 2011 International Conference for High Performance Computing, Networking, Storage and Analysis (SC ’11). ACM, New York, NY, USA, Article 39, 11 pages.
[52]
Jishen Zhao, Sheng Li, Doe Hyun Yoon, Yuan Xie, and Norman P. Jouppi. 2013. Kiln: Closing the Performance Gap Between Systems with and Without Persistence Support. In Proceedings of the 46th Annual IEEE/ACM International Symposium on Microarchitecture (MICRO-46). ACM, New York, NY, USA, 421–432.
[53]
Yoav Zuriel, Michal Friedman, Gali Sheffi, Nachshon Cohen, and Erez Petrank. 2019. Efficient Lock-free Durable Sets. Proc. ACM Program. Lang. 3, OOPSLA, Article 128 (Oct. 2019), 26 pages.

Cited By

View all
  • (2025)Verification of forward simulations with thread-local, step-local proof obligationsScience of Computer Programming10.1016/j.scico.2024.103227241(103227)Online publication date: Apr-2025
  • (2024)Discovering Likely Program Invariants for Persistent MemoryProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering10.1145/3691620.3695544(1795-1807)Online publication date: 27-Oct-2024
  • (2024)Compositionality and Observational Refinement for Linearizability with CrashesProceedings of the ACM on Programming Languages10.1145/36897928:OOPSLA2(2296-2324)Online publication date: 8-Oct-2024
  • Show More Cited By

Index Terms

  1. Persistency semantics of the Intel-x86 architecture

      Recommendations

      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 4, Issue POPL
      January 2020
      1984 pages
      EISSN:2475-1421
      DOI:10.1145/3377388
      Issue’s Table of Contents
      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: 20 December 2019
      Published in PACMPL Volume 4, Issue POPL

      Permissions

      Request permissions for this article.

      Check for updates

      Author Tags

      1. Intel-x86
      2. memory persistency
      3. non-volatile memory
      4. weak memory

      Qualifiers

      • Research-article

      Funding Sources

      • ERC
      • EPSRC

      Contributors

      Other Metrics

      Bibliometrics & Citations

      Bibliometrics

      Article Metrics

      • Downloads (Last 12 months)276
      • Downloads (Last 6 weeks)51
      Reflects downloads up to 21 Dec 2024

      Other Metrics

      Citations

      Cited By

      View all
      • (2025)Verification of forward simulations with thread-local, step-local proof obligationsScience of Computer Programming10.1016/j.scico.2024.103227241(103227)Online publication date: Apr-2025
      • (2024)Discovering Likely Program Invariants for Persistent MemoryProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering10.1145/3691620.3695544(1795-1807)Online publication date: 27-Oct-2024
      • (2024)Compositionality and Observational Refinement for Linearizability with CrashesProceedings of the ACM on Programming Languages10.1145/36897928:OOPSLA2(2296-2324)Online publication date: 8-Oct-2024
      • (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
      • (2024)Verification under Intel-x86 with PersistencyProceedings of the ACM on Programming Languages10.1145/36564258:PLDI(1189-1212)Online publication date: 20-Jun-2024
      • (2024)Toast: A Heterogeneous Memory Management SystemProceedings of the 2024 International Conference on Parallel Architectures and Compilation Techniques10.1145/3656019.3676944(53-65)Online publication date: 14-Oct-2024
      • (2024)Challenges in Empirically Testing Memory Persistency ModelsProceedings of the 2024 ACM/IEEE 44th International Conference on Software Engineering: New Ideas and Emerging Results10.1145/3639476.3639765(82-86)Online publication date: 14-Apr-2024
      • (2024)Skip It: Take Control of Your Cache!Proceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 210.1145/3620665.3640407(1077-1094)Online publication date: 27-Apr-2024
      • (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
      • (2024)Specifying and Verifying Persistent LibrariesProgramming Languages and Systems10.1007/978-3-031-57267-8_8(185-211)Online publication date: 5-Apr-2024
      • Show More Cited By

      View Options

      View options

      PDF

      View or Download as a PDF file.

      PDF

      eReader

      View online with eReader.

      eReader

      Login options

      Full Access

      Media

      Figures

      Other

      Tables

      Share

      Share

      Share this Publication link

      Share on social media