LIPIcs.CALCO.2021.4.pdf
- Filesize: 367 kB
- 3 pages
Document
The Challenges of Weak Persistency (Invited Talk)
Author
-
Part of:
Volume:
9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Conference on Algebra and Coalgebra in Computer Science (CALCO) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2021-11-08
Cite AsGet BibTex
Viktor Vafeiadis. The Challenges of Weak Persistency (Invited Talk). In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 4:1-4:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.CALCO.2021.4
https://doi.org/10.4230/LIPIcs.CALCO.2021.4
Abstract
Non-volatile memory (NVM) is a new hardware technology that provides durable storage at performance similar to that of plain volatile RAM. As such, there is a lot of interest in exploiting this technology to improve the performance of existing disk-bound applications and to find new applications for it. Nevertheless, developing correct programs that interact with non-volatile memory is by no means easy, since mainstream architectures provide rather weak persistency semantics and rather low-level and expensive mechanisms in order to avoid weak behaviors. This creates many opportunities for researchers in programming language semantics, logic, and verification to develop techniques to assist programmers writing NVM programs. This short paper and the associated talk outline the challenges caused by NVM and the research opportunities for PL researchers.
Subject Classification
ACM Subject Classification
- Theory of computation → Logic and verification
Keywords
- Weak Persistency
- Non-Volatile Memory
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, and Prakash Saivasan. Deciding reachability under persistent x86-tso. Proc. ACM Program. Lang., 5(POPL):1-32, 2021. URL: https://doi.org/10.1145/3434337.
- John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, and Heike Wehrheim. Verifying correctness of persistent concurrent data structures: A sound and complete method. Formal Aspects Comput., 33(4):547-573, 2021. URL: https://doi.org/10.1007/s00165-021-00541-8.
- Marko Doko and Viktor Vafeiadis. A program logic for C11 memory fences. In VMCAI 2016, volume 9583 of LNCS, pages 413-430. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-49122-5_20.
- Hamed Gorjiara, Guoqing Harry Xu, and Brian Demsky. Jaaru: Efficiently model checking persistent memory programs. In ASPLOS 2021, pages 415-428. ACM, 2021. URL: https://doi.org/10.1145/3445814.3446735.
- Michalis Kokologiannakis, Ilya Kaysin, Azalea Raad, and Viktor Vafeiadis. PerSeVerE: Persistency semantics for verification under ext4. Proc. ACM Program. Lang., 5(POPL):1-29, 2021. URL: https://doi.org/10.1145/3434324.
- Azalea Raad, Ori Lahav, and Viktor Vafeiadis. Persistent Owicki-Gries reasoning: A program logic for reasoning about persistent programs on Intel-x86. Proc. ACM Program. Lang., 4(OOPSLA):151:1-151:28, 2020. URL: https://doi.org/10.1145/3428219.
- Azalea Raad and Viktor Vafeiadis. Persistence semantics for weak memory: Integrating epoch persistency with the TSO memory model. Proc. ACM Program. Lang., 2(OOPSLA):137:1-137:27, 2018. URL: https://doi.org/10.1145/3276507.
- Azalea Raad, John Wickerson, Gil Neiger, and Viktor Vafeiadis. Persistency semantics of the intel-x86 architecture. Proc. ACM Program. Lang., 4(POPL):11:1-11:31, 2020. URL: https://doi.org/10.1145/3371079.
- Azalea Raad, John Wickerson, and Viktor Vafeiadis. Weak persistency semantics from the ground up: Formalising the persistency semantics of ARMv8 and transactional models. Proc. ACM Program. Lang., 3(OOPSLA):135:1-135:27, 2019. URL: https://doi.org/10.1145/3360561.
- Aaron Turon, Viktor Vafeiadis, and Derek Dreyer. GPS: Navigating weak memory with ghosts, protocols, and separation. In OOPSLA 2014, pages 691-707. ACM, 2014. URL: https://doi.org/10.1145/2660193.2660243.