Spirea: A Mechanized Concurrent Separation Logic for Weak Persistent Memory

data/desc.txt

@@ -1,3 +1,3 @@
-A Pretty Expressive Printer
-Porncharoenwase, Sorawee, et al. “A Pretty Expressive Printer.” Proceedings of the ACM on Programming Languages, vol. 7, no. OOPSLA2, Oct. 2023, pp. 1122–49. Crossref, https://doi.org/10.1145/3622837.
-Pretty printers make trade-offs between the expressiveness of their pretty printing language, the optimality objective that they minimize when choosing between different ways to lay out a document, and the performance of their algorithm. This paper presents a new pretty printer, Π e , that is strictly more expressive than all pretty printers in the literature and provably minimizes an optimality objective. Furthermore, the time complexity of Π e is better than many existing pretty printers. When choosing among different ways to lay out a document, Π e consults a user-supplied cost factory , which determines the optimality objective, giving Π e a unique degree of flexibility. We use the Lean theorem prover to verify the correctness (validity and optimality) of Π e , and implement Π e concretely as a pretty printer that we call PrettyExpressive. To evaluate our pretty printer against others, we develop a formal framework for reasoning about the expressiveness of pretty printing languages, and survey pretty printers in the literature, comparing their expressiveness, optimality, worst-case time complexity, and practical running time. Our evaluation shows that PrettyExpressive is efficient and effective at producing optimal layouts. PrettyExpressive has also seen real-world adoption: it serves as a foundation of a code formatter for Racket.
+Spirea: A Mechanized Concurrent Separation Logic for Weak Persistent Memory
+Vindum, Simon Friis, and Lars Birkedal. “Spirea: A Mechanized Concurrent Separation Logic for Weak Persistent Memory.” Proceedings of the ACM on Programming Languages, vol. 7, no. OOPSLA2, Oct. 2023, pp. 632–57. Crossref, https://doi.org/10.1145/3622820.
+Weak persistent memory (a.k.a. non-volatile memory) is an emerging technology that offers fast byte-addressable durable main memory. A wealth of algorithms and libraries has been developed to explore this exciting technology. As noted by others, this has led to a significant verification gap. Towards closing this gap, we present Spirea, the first concurrent separation logic for verification of programs under a weak persistent memory model. Spirea is based on the Iris and Perennial verification frameworks, and by combining features from these logics with novel techniques it supports high-level modular reasoning about crash-safe and thread-safe programs and libraries. Spirea is fully mechanized in the Coq proof assistant and allows for interactive development of proofs with the Iris Proof Mode. We use Spirea to verify several challenging examples with modular specifications. We show how our logic can verify thread-safety and crash-safety of non-blocking durable data structures with null-recovery, in particular the Treiber stack and the Michael-Scott queue adapted to persistent memory. This is the first time durable data structures have been verified with a program logic.

data/history.txt

@@ -33,4 +33,5 @@ https://doi.org/10.1145/3622828
 https://doi.org/10.1145/3632882
 https://doi.org/10.1145/3607862
 https://doi.org/10.1145/3586038
-https://doi.org/10.1145/3622837
+https://doi.org/10.1145/3622837
+https://doi.org/10.1145/3622820

data/next.txt

@@ -1 +1 @@
-https://doi.org/10.1145/3622837
+https://doi.org/10.1145/3622820

data/past.txt

@@ -5,4 +5,5 @@ https://doi.org/10.1145/3622828
 https://doi.org/10.1145/3632882
 https://doi.org/10.1145/3607862
 https://doi.org/10.1145/3586038
-https://doi.org/10.1145/3622837
+https://doi.org/10.1145/3622837
+https://doi.org/10.1145/3622820

docs/index.md

@@ -32,7 +32,7 @@ Our tools for paper selection: [plgroup on Github](https://github.com/the-au-for
 | 7.  | October 11   | _Fall pause_                                                                 |
 | 8.  | October 18   | Fat Pointers for Temporal Memory Safety of C                                 |
 | 9.  | October 25   | A Pretty Expressive Printer                                                  |
-| 10. | November 1   | Paper 7 discussion                                                           |
+| 10. | November 1   | Spirea: A Mechanized Concurrent Separation Logic for Weak Persistent Memory  |
 | 11. | November 8   | Paper 8 discussion                                                           |
 | 12. | November 22  | Fall Finale and Awards Gala                                                  |
 

docs/papers.md

@@ -3,4 +3,5 @@
 3. Castagna, Giuseppe, et al. “Polymorphic Type Inference for Dynamic Languages.” Proceedings of the ACM on Programming Languages, vol. 8, no. POPL, Jan. 2024, pp. 1179–210. Crossref, <a href='https://doi.org/10.1145/3632882' target='_blank'>https://doi.org/10.1145/3632882</a>.
 4. Abel, Andreas, et al. “A Graded Modal Dependent Type Theory with a Universe and Erasure, Formalized.” Proceedings of the ACM on Programming Languages, vol. 7, no. ICFP, Aug. 2023, pp. 920–54. Crossref, <a href='https://doi.org/10.1145/3607862' target='_blank'>https://doi.org/10.1145/3607862</a>.
 5. Zhou, Jie, et al. “Fat Pointers for Temporal Memory Safety of C.” Proceedings of the ACM on Programming Languages, vol. 7, no. OOPSLA1, Apr. 2023, pp. 316–47. Crossref, <a href='https://doi.org/10.1145/3586038' target='_blank'>https://doi.org/10.1145/3586038</a>.
-6. Porncharoenwase, Sorawee, et al. “A Pretty Expressive Printer.” Proceedings of the ACM on Programming Languages, vol. 7, no. OOPSLA2, Oct. 2023, pp. 1122–49. Crossref, <a href='https://doi.org/10.1145/3622837' target='_blank'>https://doi.org/10.1145/3622837</a>.
+6. Porncharoenwase, Sorawee, et al. “A Pretty Expressive Printer.” Proceedings of the ACM on Programming Languages, vol. 7, no. OOPSLA2, Oct. 2023, pp. 1122–49. Crossref, <a href='https://doi.org/10.1145/3622837' target='_blank'>https://doi.org/10.1145/3622837</a>.
+7. Vindum, Simon Friis, and Lars Birkedal. “Spirea: A Mechanized Concurrent Separation Logic for Weak Persistent Memory.” Proceedings of the ACM on Programming Languages, vol. 7, no. OOPSLA2, Oct. 2023, pp. 632–57. Crossref, <a href='https://doi.org/10.1145/3622820' target='_blank'>https://doi.org/10.1145/3622820</a>.