pith. sign in

arxiv: 2606.25422 · v1 · pith:TQ5SMF26new · submitted 2026-06-24 · 💻 cs.LO · cs.CR· cs.PL

Information flow security on persistent memory

Graeme Smith This is my paper

Pith reviewed 2026-06-25 20:08 UTC · model grok-4.3

classification 💻 cs.LO cs.CRcs.PL
keywords information flowpersistent memoryreordering interference freedomassembly languagesecurity logicx86
0
0 comments X

The pith

Reordering interference freedom enables information flow security proofs for both x86 and persistent memory.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper presents an information flow logic for an unstructured assembly language. It uses a notion called reordering interference freedom to account for out-of-order instruction effects in x86 memory models. The same notion is shown to handle the distinct propagation rules of persistent memory. A sympathetic reader would care because persistent memory promises better performance and crash recovery, but these features could create new security vulnerabilities if information can flow improperly.

Core claim

We provide an information flow logic for an unstructured language modelling a simple assembly language. We apply this logic to x86 assembly using a notion of reordering interference freedom (rif) to reason about potential out-of-order propagation of instructions to memory. We then show how this same notion of rif can be used to similarly reason about information flow on persistent memory.

What carries the argument

Reordering interference freedom (rif), a condition that prevents instructions from interfering in out-of-order executions in ways that would violate information flow policies.

If this is right

  • Verified programs on x86 maintain security even with out-of-order memory operations.
  • The logic extends without modification to persistent memory's write persistence model.
  • Information flow security can be established for programs that use persistent memory for crash recovery.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • This approach may allow reuse of x86 security analyses for persistent memory systems.
  • Developers could apply the same verification technique when writing crash-resilient secure code.
  • Testing rif on real persistent memory hardware could reveal if the abstraction holds in practice.

Load-bearing premise

The single notion of reordering interference freedom is sufficient to capture the relevant out-of-order behaviors for both standard x86 memory and persistent memory.

What would settle it

Finding a program that satisfies rif yet leaks information through the specific persistence and recovery mechanisms of persistent memory would disprove the claim.

read the original abstract

Persistent memory is a recently proposed memory paradigm that delivers many system-wide benefits, including improved runtime efficiency and the ability of programs to recover from power outages and system crashes. While recent research has investigated techniques for proving functional correctness of programs running on related architectures, this is not the case for the orthogonal concept of information flow security. In this paper, we provide an information flow logic for an unstructured language (i.e., with gotos rather than loops) modelling a simple assembly language. We apply this logic to x86 assembly using a notion of reordering interference freedom (rif) to reason about potential out-of-order propagation of instructions to memory. We then show how this same notion of rif can be used to similarly reason about information flow on persistent memory.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 3 minor

Summary. The paper presents an information flow logic for an unstructured language (with gotos) modeling a simple assembly language. It applies this logic to x86 assembly by introducing reordering interference freedom (rif) to account for out-of-order instruction propagation to memory. It then shows that the same rif notion, when instantiated with the persistence ordering relation, suffices to reason about information flow security under persistent-memory propagation rules, with the non-interference theorem re-derived under the new model.

Significance. If the central development holds, the work supplies a reusable, parameterized framework for information-flow reasoning across memory models, directly addressing the gap between functional-correctness results and security for persistent memory. The explicit parameterization of rif over the memory model (rather than assuming identical reordering behavior) and the re-derivation of the non-interference theorem are concrete strengths that increase the result's adaptability and falsifiability.

minor comments (3)
  1. The abstract states that 'the same notion of rif' is used for persistent memory; while the body clarifies the parameterization, a brief parenthetical in the abstract would prevent misreading.
  2. [§2] The unstructured language is introduced without a small illustrative program fragment showing gotos and memory operations; adding one early in §2 would aid readability for readers outside the subfield.
  3. [§4] Notation for the rif predicate and its memory-model parameter is introduced in the x86 section but not cross-referenced when the persistent-memory instantiation appears; a single forward pointer would help.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive summary and recommendation of minor revision. No major comments were provided in the report, so there are no specific points to address point-by-point.

Circularity Check

0 steps flagged

No significant circularity detected

full rationale

The paper defines a new information flow logic for an unstructured assembly-like language and introduces a parameterized reordering interference freedom (rif) predicate over a memory model. It instantiates rif first for x86 out-of-order propagation and then for persistent-memory ordering, re-deriving the non-interference result in each case from the rif hypothesis alone. No equations reduce by construction to fitted inputs, no load-bearing self-citations appear, and the central claim is an independent formal development rather than a renaming or ansatz smuggling. The derivation chain is therefore self-contained.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract only; no free parameters, axioms, or invented entities can be identified from the given text.

pith-pipeline@v0.9.1-grok · 5640 in / 1027 out tokens · 24255 ms · 2026-06-25T20:08:07.678090+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

52 extracted references · 41 canonical work pages

  1. [1]

    ACM Comput

    Baldassin, A., Barreto, J., Castro, D., Romano, P.: Persistent memory: A survey of programming support and implementations. ACM Comput. Surv.54(7), 152– 115237 (2022) https://doi.org/10.1145/3465402

    work page doi:10.1145/3465402 2022

  2. [2]

    In: Gavoille, C., Ilcinkas, D

    Izraelevitz, J., Mendes, H., Scott, M.L.: Linearizability of persistent memory objects under a full-system-crash failure model. In: Gavoille, C., Ilcinkas, D. (eds.) Distributed Computing - 30th International Symposium, DISC 2016. Lecture Notes in Computer Science, vol. 9888, pp. 313–327. Springer, Berlin-Heidelberg (2016). https://doi.org/10.1007/978-3-6...

    work page doi:10.1007/978-3-662-53426-7_23 2016

  3. [3]

    Raad, A., Vafeiadis, V.: Persistence semantics for weak memory: integrating epoch persistency with the TSO memory model. Proc. ACM Program. Lang. 2(OOPSLA), 137–113727 (2018) https://doi.org/10.1145/3276507

    work page doi:10.1145/3276507 2018

  4. [4]

    Raad, A., Wickerson, J., Vafeiadis, V.: Weak persistency semantics from the ground up: formalising the persistency semantics of ARMv8 and transactional models. Proc. ACM Program. Lang.3(OOPSLA), 135–113527 (2019) https: //doi.org/10.1145/3360561

    work page doi:10.1145/3360561 2019

  5. [5]

    In: Beek, M.H., McIver, A., Oliveira,J.N.(eds.)FormalMethods-TheNext30Years-ThirdWorldCongress, FM 2019

    Derrick, J., Doherty, S., Dongol, B., Schellhorn, G., Wehrheim, H.: Verifying correctness of persistent concurrent data structures. In: Beek, M.H., McIver, A., Oliveira,J.N.(eds.)FormalMethods-TheNext30Years-ThirdWorldCongress, FM 2019. Lecture Notes in Computer Science, vol. 11800, pp. 179–195. Springer, Berlin-Heidelberg (2019). https://doi.org/10.1007/...

    work page doi:10.1007/978-3-030-30942-8_12 2019

  6. [6]

    Raad, A., Wickerson, J., Neiger, G., Vafeiadis, V.: Persistency semantics of the Intel-x86 architecture. Proc. ACM Program. Lang.4(POPL), 11–11131 (2020) https://doi.org/10.1145/3371079

    work page doi:10.1145/3371079 2020

  7. [7]

    Raad, A., Lahav, O., Vafeiadis, V.: Persistent Owicki-Gries reasoning: a program logic for reasoning about persistent programs on Intel-x86. Proc. ACM Program. Lang.4(OOPSLA), 151–115128 (2020) https://doi.org/10.1145/3428219

    work page doi:10.1145/3428219 2020

  8. [8]

    In: Gotsman, A., Sokolova, A

    Bila, E., Doherty, S., Dongol, B., Derrick, J., Schellhorn, G., Wehrheim, H.: Defining and verifying durable opacity: Correctness for persistent software trans- actional memory. In: Gotsman, A., Sokolova, A. (eds.) Formal Techniques for Distributed Objects, Components, and Systems - 40th IFIP WG 6.1 Inter- national Conference, FORTE 2020. Lecture Notes in...

    2020

  9. [9]

    In: Freund, S.N., Yahav, E

    Cho, K., Lee, S., Raad, A., Kang, J.: Revamping hardware persistency mod- els: view-based and axiomatic persistency models for Intel-x86 and Armv8. In: Freund, S.N., Yahav, E. (eds.) PLDI ’21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, pp. 16–31. ACM, New York (2021). https://doi.org/10.1145/3453483.3454027

    work page doi:10.1145/3453483.3454027 2021

  10. [10]

    Formal Aspects Comput.33(4-5), 547–573 (2021) https://doi.org/10

    Derrick, J., Doherty, S., Dongol, B., Schellhorn, G., Wehrheim, H.: Verify- ing correctness of persistent concurrent data structures: a sound and complete method. Formal Aspects Comput.33(4-5), 547–573 (2021) https://doi.org/10. 1007/S00165-021-00541-8

    2021

  11. [11]

    In: Sergey, I

    Bila,E.,Dongol, B.,Lahav,O., Raad,A.,Wickerson,J.:View-based Owicki-Gries reasoning for persistent x86-TSO. In: Sergey, I. (ed.) Programming Languages and Systems - 31st European Symposium on Programming, ESOP 2022. Lecture Notes in Computer Science, vol. 13240, pp. 234–261. Springer, Berlin-Heidelberg (2022). https://doi.org/10.1007/978-3-030-99336-8_9

    work page doi:10.1007/978-3-030-99336-8_9 2022

  12. [12]

    Bila, E., Derrick, J., Doherty, S., Dongol, B., Schellhorn, G., Wehrheim, H.: Mod- ularising verification of durable opacity. Log. Methods Comput. Sci.18(3) (2022) https://doi.org/10.46298/LMCS-18(3:7)2022

    work page doi:10.46298/lmcs-18(3:7)2022 2022

  13. [13]

    D’Osualdo, E., Raad, A., Vafeiadis, V.: The path to durable linearizability. Proc. ACM Program. Lang.7(POPL), 748–774 (2023) https://doi.org/10.1145/ 3571219

    2023

  14. [14]

    Synthesis Lectures on Computer Architecture

    Sorin, D.J., Hill, M.D., Wood, D.A.: A Primer on Memory Consistency and Cache Coherence. Synthesis Lectures on Computer Architecture. Mor- gan & Claypool Publishers, San Rafael CA (2011). https://doi.org/10.2200/ S00346ED1V01Y201104CAC016 28

    2011

  15. [15]

    Sewell, P., Sarkar, S., Owens, S., Nardelli, F.Z., Myreen, M.O.: x86-TSO: a rig- orous and usable programmer’s model for x86 multiprocessors. Commun. ACM 53(7), 89–97 (2010) https://doi.org/10.1145/1785414.1785443

    work page doi:10.1145/1785414.1785443 2010

  16. [16]

    ACM Trans

    Alglave, J., Maranget, L., Tautschnig, M.: Herding cats: Modelling, simulation, testing, and data mining for weak memory. ACM Trans. Program. Lang. Syst. 36(2), 7–1774 (2014) https://doi.org/10.1145/2627752

    work page doi:10.1145/2627752 2014

  17. [17]

    13085, pp

    Colvin, R.J.: Parallelized sequential composition and hardware weak memory models.In:Calinescu,R.,Pasareanu,C.S.(eds.)SoftwareEngineeringandFormal Methods-19thInternationalConference,SEFM2021.LectureNotesinComputer Science, vol. 13085, pp. 201–221. Springer, Berlin-Heidelberg (2021). https://doi. org/10.1007/978-3-030-92124-8_12

    work page doi:10.1007/978-3-030-92124-8_12 2021

  18. [18]

    In: Huisman, M., Pasareanu, C.S., Zhan, N

    Coughlin, N., Winter, K., Smith, G.: Rely/guarantee reasoning for multicopy atomic weak memory models. In: Huisman, M., Pasareanu, C.S., Zhan, N. (eds.) Formal Methods - 24th International Symposium, FM 2021. Lecture Notes in Computer Science, vol. 13047, pp. 292–310. Springer, Berlin-Heidelberg (2021). https://doi.org/10.1007/978-3-030-90870-6_16

    work page doi:10.1007/978-3-030-90870-6_16 2021

  19. [19]

    Formal Aspects Comput.35(2), 8–1830 (2023) https://doi

    Coughlin, N., Winter, K., Smith, G.: Compositional reasoning for non-multicopy atomic architectures. Formal Aspects Comput.35(2), 8–1830 (2023) https://doi. org/10.1145/3574137

    work page doi:10.1145/3574137 2023

  20. [20]

    In: 32nd IEEE Computer Security Foundations Symposium, CSF 2019, pp

    Cheang, K., Rasmussen, C., Seshia, S.A., Subramanyan, P.: A formal approach to secure speculation. In: 32nd IEEE Computer Security Foundations Symposium, CSF 2019, pp. 288–303. IEEE, New York (2019). https://doi.org/10.1109/CSF. 2019.00027

    work page doi:10.1109/csf 2019

  21. [21]

    Bovet, D.P., Cesati, M.: Understanding the Linux Kernel - from I/O Ports to Process Management: Covers Version 2.6 (3. ed.). O’Reilly, Sebastopol CA (2005)

    2005

  22. [22]

    In: 34th IEEE Computer Security Foundations Symposium, CSF 2021, pp

    Winter, K., Coughlin, N., Smith, G.: Backwards-directed information flow anal- ysis for concurrent programs. In: 34th IEEE Computer Security Foundations Symposium, CSF 2021, pp. 1–16. IEEE, New York (2021). https://doi.org/10. 1109/CSF51468.2021.00017

    arXiv 2021

  23. [23]

    Prentice-Hall, Hoboken NJ (1976)

    Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Hoboken NJ (1976)

    1976

  24. [24]

    Texts and Monographs in Computer Science

    Dijkstra, E.W., Scholten, C.S.: Predicate Calculus and Program Semantics. Texts and Monographs in Computer Science. Springer, Berlin-Heidelberg (1990). https: //doi.org/10.1007/978-1-4612-3228-5

    work page doi:10.1007/978-1-4612-3228-5 1990

  25. [25]

    In: Mason, R.E.A

    Jones, C.B.: Specification and design of (parallel) programs. In: Mason, R.E.A. (ed.) Information Processing 83, Proceedings of the IFIP 9th World Computer Congress, pp. 321–332. North-Holland/IFIP, Amsterdam (1983) 29

    1983

  26. [26]

    Formal Aspects of Computing9(2), 149–174 (1997) https://doi.org/10.1007/BF01211617

    Xu, Q., Roever, W.P., He, J.: The rely-guarantee method for verifying shared variable concurrent programs. Formal Aspects of Computing9(2), 149–174 (1997) https://doi.org/10.1007/BF01211617

    work page doi:10.1007/bf01211617 1997

  27. [27]

    In: 1982 IEEE Symposium on Security and Privacy, 1982, pp

    Goguen, J.A., Meseguer, J.: Security policies and security models. In: 1982 IEEE Symposium on Security and Privacy, 1982, pp. 11–20. IEEE Computer Society, New York (1982). https://doi.org/10.1109/SP.1982.10014

    work page doi:10.1109/sp.1982.10014 1982

  28. [28]

    In: Ernst, M.D., Jensen, T.P

    Barnett, M., Leino, K.R.M.: Weakest-precondition of unstructured programs. In: Ernst, M.D., Jensen, T.P. (eds.) Proceedings of the 2005 ACM SIGPLAN- SIGSOFT Workshop on Program Analysis For Software Tools and Engineering, PASTE’05, pp. 82–87. ACM, New York (2005). https://doi.org/10.1145/1108792. 1108813

    work page doi:10.1145/1108792 2005

  29. [29]

    In: 2018 IEEE European Symposium on Security and Privacy, EuroS&P 2018, pp

    Murray, T.C., Sison, R., Engelhardt, K.: Covern: A logic for compositional verification of information flow control. In: 2018 IEEE European Symposium on Security and Privacy, EuroS&P 2018, pp. 16–30. IEEE, New York (2018). https://doi.org/10.1109/EuroSP.2018.00010

    work page doi:10.1109/eurosp.2018.00010 2018

  30. [30]

    In: Beek, M.H., McIver, A., Oliveira, J.N

    Smith, G., Coughlin, N., Murray, T.: Value-dependent information-flow security on weak memory models. In: Beek, M.H., McIver, A., Oliveira, J.N. (eds.) Formal Methods - The Next 30 Years - Third World Congress, FM 2019. Lecture Notes in Computer Science, vol. 11800, pp. 539–555. Springer, Berlin-Heidelberg (2019). https://doi.org/10.1007/978-3-030-30942-8_32

    work page doi:10.1007/978-3-030-30942-8_32 2019

  31. [31]

    Sabelfeld, A., Sands, D.: Declassification: Dimensions and principles. J. Comput. Secur.17(5), 517–548 (2009) https://doi.org/10.3233/JCS-2009-0352

    work page doi:10.3233/jcs-2009-0352 2009

  32. [32]

    In: Hicks, M.W

    Askarov, A., Sabelfeld, A.: Localized delimited release: combining the what and where dimensions of information release. In: Hicks, M.W. (ed.) Proceedings of the 2007 Workshop on Programming Languages and Analysis for Security, PLAS2007,pp.53–60.ACM,NewYork(2007).https://doi.org/10.1145/1255329. 1255339

    work page doi:10.1145/1255329 2007

  33. [33]

    In: Riesco, A., Zhang, M

    Smith, G.: Declassification predicates for controlled information release. In: Riesco, A., Zhang, M. (eds.) Formal Methods and Software Engineering - 23rd International Conference on Formal Engineering Methods, ICFEM 2022. Lecture Notes in Computer Science, vol. 13478, pp. 298–315. Springer, Berlin-Heidelberg (2022). https://doi.org/10.1007/978-3-031-17244-1_18

    work page doi:10.1007/978-3-031-17244-1_18 2022

  34. [34]

    In: Havelund, K., Peleska, J., Roscoe, B., Vink, E.P

    Colvin, R.J., Smith, G.: A wide-spectrum language for verification of programs on weak memory models. In: Havelund, K., Peleska, J., Roscoe, B., Vink, E.P. (eds.) Formal Methods - 22nd International Symposium, FM 2018. Lecture Notes in Computer Science, vol. 10951, pp. 240–257. Springer, Berlin-Heidelberg (2018). https://doi.org/10.1007/978-3-319-95582-7_14

    work page doi:10.1007/978-3-319-95582-7_14 2018

  35. [35]

    CoRRabs/1812.00996(2018)

    Colvin, R.J., Smith, G.: A high-level operational semantics for hardware weak 30 memory models. CoRRabs/1812.00996(2018)

    Pith/arXiv arXiv 2018

  36. [36]

    In: Yi, K

    Vanbroekhoven, P., Janssens, G., Bruynooghe, M., Catthoor, F.: Transformation to dynamic single assignment using a simple data flow analysis. In: Yi, K. (ed.) Programming Languages and Systems, Third Asian Symposium, APLAS 2005. Lecture Notes in Computer Science, vol. 3780, pp. 330–346. Springer, Berlin- Heidelberg (2005). https://doi.org/10.1007/11575467_22

    work page doi:10.1007/11575467_22 2005

  37. [37]

    In: Proc

    Kildall, G.A.: A unified approach to global program optimization. In: Proc. of POPL, pp. 194–206. ACM, New York (1973)

    1973

  38. [38]

    In: IEEE 29th Computer Security Foundations Symposium, CSF 2016, pp

    Murray, T.C., Sison, R., Pierzchalski, E., Rizkallah, C.: Compositional verifi- cation and refinement of concurrent value-dependent noninterference. In: IEEE 29th Computer Security Foundations Symposium, CSF 2016, pp. 417–431. IEEE Computer Society, New York (2016). https://doi.org/10.1109/CSF.2016.36

    work page doi:10.1109/csf.2016.36 2016

  39. [39]

    In: Chong, S

    Vaughan, J.A., Millstein, T.D.: Secure information flow for concurrent programs under Total Store Order. In: Chong, S. (ed.) 25th IEEE Computer Security Foun- dations Symposium, CSF 2012, pp. 19–29. IEEE Computer Society, New York (2012). https://doi.org/10.1109/CSF.2012.20

    work page doi:10.1109/csf.2012.20 2012

  40. [40]

    In: IEEE 27th Computer Security Foundations Symposium, CSF 2014, pp

    Mantel, H., Perner, M., Sauer, J.: Noninterference under weak memory models. In: IEEE 27th Computer Security Foundations Symposium, CSF 2014, pp. 80–94. IEEE Computer Society, New York (2014). https://doi.org/10.1109/CSF.2014.14

    work page doi:10.1109/csf.2014.14 2014

  41. [41]

    Formal Methods Syst

    Smith, G., Coughlin, N., Murray, T.: Information-flow control on ARM and POWER multicore processors. Formal Methods Syst. Des.58(1-2), 251–293 (2021) https://doi.org/10.1007/S10703-021-00376-2

    work page doi:10.1007/s10703-021-00376-2 2021

  42. [42]

    Coughlin, N., Smith, G.: Compositional noninterference on hardware weak mem- ory models. Sci. Comput. Program.217, 102779 (2022) https://doi.org/10.1016/ j.scico.2022.102779

    arXiv 2022

  43. [43]

    In: Platzer, A., Rozier, K.Y., Pradella, M., Rossi, M

    Coughlin, N., Lam, K., Smith, G., Winter, K.: Detecting speculative execution vulnerabilities on weak memory models. In: Platzer, A., Rozier, K.Y., Pradella, M., Rossi, M. (eds.) Formal Methods - 26th International Symposium, FM 2024. Lecture Notes in Computer Science, vol. 14933, pp. 482–500. Springer, Berlin- Heidelberg (2024). https://doi.org/10.1007/9...

    work page doi:10.1007/978-3-031-71162-6_25 2024

  44. [44]

    In: ACM/IEEE 41st International Symposium on Computer Architecture, ISCA 2014, pp

    Pelley, S., Chen, P.M., Wenisch, T.F.: Memory persistency. In: ACM/IEEE 41st International Symposium on Computer Architecture, ISCA 2014, pp. 265–276. IEEE Computer Society, New York (2014). https://doi.org/10.1109/ISCA.2014. 6853222

    work page doi:10.1109/isca.2014 2014

  45. [45]

    In: Castagna, G., Gordon, A.D

    Kang, J., Hur, C., Lahav, O., Vafeiadis, V., Dreyer, D.: A promising seman- tics for relaxed-memory concurrency. In: Castagna, G., Gordon, A.D. (eds.) 31 Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Program- ming Languages, POPL 2017, pp. 175–189. ACM, New York (2017). https: //doi.org/10.1145/3009837.3009850

    work page doi:10.1145/3009837.3009850 2017

  46. [46]

    Khyzha, A., Lahav, O.: Taming x86-TSO persistency. Proc. ACM Program. Lang. 5(POPL), 1–29 (2021) https://doi.org/10.1145/3434328

    work page doi:10.1145/3434328 2021

  47. [47]

    Acta Informatica6, 319–340 (1976) https://doi.org/10.1007/BF00268134

    Owicki, S.S., Gries, D.: An axiomatic proof technique for parallel programs I. Acta Informatica6, 319–340 (1976) https://doi.org/10.1007/BF00268134

    work page doi:10.1007/bf00268134 1976

  48. [48]

    In: Chatterjee, S., Scott, M.L

    Guerraoui, R., Kapalka, M.: On the correctness of transactional memory. In: Chatterjee, S., Scott, M.L. (eds.) Proceedings of the 13th ACM SIGPLAN Sym- posium on Principles and Practice of Parallel Programming, PPOPP 2008, pp. 175–184. ACM, New York (2008). https://doi.org/10.1145/1345206.1345233

    work page doi:10.1145/1345206.1345233 2008

  49. [49]

    Herlihy and Jeannette M

    Herlihy, M., Wing, J.M.: Linearizability: A correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst.12(3), 463–492 (1990) https://doi. org/10.1145/78969.78972

    work page doi:10.1145/78969.78972 1990

  50. [50]

    Cho, K., Jeon, S., Raad, A., Kang, J.: Memento: A framework for detectable recoverability in persistent memory. Proc. ACM Program. Lang.7(PLDI), 292– 317 (2023) https://doi.org/10.1145/3591232

    work page doi:10.1145/3591232 2023

  51. [51]

    In: Bodík, R., Majumdar, R

    Koskinen, E., Yang, J.: Reducing crash recoverability to reachability. In: Bodík, R., Majumdar, R. (eds.) Proceedings of the 43rd Annual ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages, POPL 2016, pp. 97–108. ACM, New York (2016). https://doi.org/10.1145/2837614.2837648

    work page doi:10.1145/2837614.2837648 2016

  52. [52]

    Surbatovich, M., Spargo, N., Jia, L., Lucia, B.: A type system for safe intermittent computing. Proc. ACM Program. Lang.7(PLDI), 736–760 (2023) https://doi. org/10.1145/3591250 32

    work page doi:10.1145/3591250 2023