More Web Proxy on the site http://driver.im/

research-article

Open access

Persistence semantics for weak memory: integrating epoch persistency with the TSO memory model

Authors:

Viktor VafeiadisAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 2, Issue OOPSLA

Article No.: 137, Pages 1 - 27

https://doi.org/10.1145/3276507

Published: 24 October 2018 Publication History

Abstract

Emerging non-volatile memory (NVM) technologies promise the durability of disks with the performance of volatile memory (RAM). To describe the persistency guarantees of NVM, several memory persistency models have been proposed in the literature. However, the formal semantics of such persistency models in the context of existing mainstream hardware has been unexplored to date. To close this gap, we integrate the buffered epoch persistency model with the 'total-store-order' (TSO) memory model of the x86 and SPARC architectures. We thus develop the PTSO ('persistent' TSO) model and formalise its semantics both operationally and declaratively. We demonstrate that the two characterisations of PTSO are equivalent. We then formulate the notion of persistent linearisability to establish the correctness of library implementations in the context of persistent memory. To showcase our formalism, we develop two persistent implementations of a queue library, and apply persistent linearisability to show their correctness.

Supplementary Material

WEBM File (a137-raad.webm)

Download
81.75 MB

References

[1]

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.

Digital Library

[2]

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.

Digital Library

[3]

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.

Digital Library

[4]

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.

Digital Library

[5]

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.

Digital Library

[6]

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.

Digital Library

[7]

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.

Digital Library

[8]

IBM. 2013. IBM solidDB. (2013). https://www.ibm.com/support/knowledgecenter/en/SSPK3V_7.0.0/master/welcome.kc.html

[9]

Intel. 2014. Intel architecture instruction set extensions programming reference. (2014). https://software.intel.com/sites/ default/files/managed/07/b7/319433- 023.pdf

[10]

International technology roadmap for semiconductors. 2007. Process Integration, devices, and structures. (2007). http: //www.maltiel- consulting.com/ITRS_2011- Process- Integration- Devices- Structures.pdf

[11]

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.

Digital Library

[12]

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.

[13]

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.

Digital Library

[14]

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.

[15]

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.

Digital Library

[16]

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

Digital Library

[17]

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.

Digital Library

[18]

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.

Digital Library

[19]

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.

[20]

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

Digital Library

[21]

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

Digital Library

[22]

Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, and Peter Sewell. 2017. Simplifying ARM Concurrency: Multicopy-atomic Axiomatic and Operational Models for ARMv8. Proc. ACM Program. Lang. 2, POPL, Article 19 (Dec. 2017), 29 pages.

Digital Library

[23]

Azalea Raad and Viktor Vafeiadis. 2018. Technical Appendix. (2018). http://plv.mpi- sws.org/ptso/

[24]

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.

Digital Library

[25]

SPARC. 1992. The SPARC Architecture Manual: Version 8. Prentice-Hall, Inc., Upper Saddle River, NJ, USA.

Digital Library

[26]

D. B. Strukov, G. S. Snider, D. R. Stewart, and R. S. Williams. 2008. The missing memristor found. Nature 453 (2008), 80 – 83.

[27]

TimesTen Team. 1999. In-memory Data Management for Consumer Transactions the Timesten Approach. SIGMOD Rec. 28, 2 (June 1999), 528–529.

Digital Library

[28]

Viktor Vafeiadis and Chinmay Narayan. 2013. Relaxed Separation Logic: A Program Logic for C11 Concurrency. In Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications. 867–884.

Digital Library

[29]

Haris Volos, Andres Jaan Tack, and Michael M. Swift. 2011. Mnemosyne: Lightweight Persistent Memory. SIGPLAN Not. 47, 4 (March 2011), 91–104.

Digital Library

[30]

Zhaoguo Wang, Hao Qian, Jinyang Li, and Haibo Chen. 2014. Using Restricted Transactional Memory to Build a Scalable In-memory Database. In Proceedings of the Ninth European Conference on Computer Systems (EuroSys ’14). ACM, New York, NY, USA, Article 26, 15 pages.

Digital Library

[31]

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.

Digital Library

[32]

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.

Digital Library

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
Stefanesco LRaad AVafeiadis V(2024)Specifying and Verifying Persistent LibrariesProgramming Languages and Systems10.1007/978-3-031-57267-8_8(185-211)Online publication date: 6-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-57267-8_8
Soh YSwanson SZhao J(2023)ENTS: Flush-and-Fence-Free Failure Atomic TransactionsProceedings of the International Symposium on Memory Systems10.1145/3631882.3631907(1-16)Online publication date: 2-Oct-2023
https://dl.acm.org/doi/10.1145/3631882.3631907
Show More Cited By

Index Terms

Persistence semantics for weak memory: integrating epoch persistency with the TSO memory model
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
2. Theory of computation
  1. Models of computation
    1. Concurrency
  2. Semantics and reasoning

Recommendations

Taming x86-TSO persistency

We study the formal semantics of non-volatile memory in the x86-TSO architecture. We show that while the explicit persist operations in the recent model of Raad et al. from POPL'20 only enforce order between writes to the non-volatile memory, it is ...
Persistency semantics of the Intel-x86 architecture

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 ...
Weak persistency semantics from the ground up: formalising the persistency semantics of ARMv8 and transactional models

Emerging non-volatile memory (NVM) technologies promise the durability of disks with the performance of volatile memory (RAM). To describe the persistency guarantees of NVM, several memory persistency models have been proposed in the literature. However, ...

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 2, Issue OOPSLA

November 2018

1656 pages

EISSN:2475-1421

DOI:10.1145/3288538

Issue’s Table of Contents

Copyright © 2018 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: 24 October 2018

Published in PACMPL Volume 2, Issue OOPSLA

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

European Research Council

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

25
Total Citations
View Citations
630
Total Downloads

Downloads (Last 12 months)84
Downloads (Last 6 weeks)17

Reflects downloads up to 21 Dec 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
Stefanesco LRaad AVafeiadis V(2024)Specifying and Verifying Persistent LibrariesProgramming Languages and Systems10.1007/978-3-031-57267-8_8(185-211)Online publication date: 6-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-57267-8_8
Soh YSwanson SZhao J(2023)ENTS: Flush-and-Fence-Free Failure Atomic TransactionsProceedings of the International Symposium on Memory Systems10.1145/3631882.3631907(1-16)Online publication date: 2-Oct-2023
https://dl.acm.org/doi/10.1145/3631882.3631907
Surbatovich MSpargo NJia LLucia B(2023)A Type System for Safe Intermittent ComputingProceedings of the ACM on Programming Languages10.1145/35912507:PLDI(736-760)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591250
D'Osualdo ERaad AVafeiadis V(2023)The Path to Durable LinearizabilityProceedings of the ACM on Programming Languages10.1145/35712197:POPL(748-774)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571219
Marmanis IVafeiadis V(2023)SMT-Based Verification of Persistency Invariants of Px86 ProgramsVerified Software. Theories, Tools and Experiments.10.1007/978-3-031-25803-9_6(92-110)Online publication date: 1-Feb-2023
https://doi.org/10.1007/978-3-031-25803-9_6
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
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
Simner BArmstrong APichon-Pharabod JPulte CGrisenthwaite RSewell P(2022)Relaxed virtual memory in Armv8-AProgramming Languages and Systems10.1007/978-3-030-99336-8_6(143-173)Online publication date: 29-Mar-2022
https://doi.org/10.1007/978-3-030-99336-8_6
Han JKimura K(2021)Durable Queue Implementations Built on a Formally Defined Strand Persistency ModelJournal of Information Processing10.2197/ipsjjip.29.82329(823-838)Online publication date: 2021
https://doi.org/10.2197/ipsjjip.29.823
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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