pith. sign in

arxiv: 2305.08486 · v3 · submitted 2023-05-15 · 💻 cs.PL · cs.LO

Rely-Guarantee Reasoning for Causally Consistent Shared Memory (Extended Version)

Ori Lahav , Brijesh Dongol , Heike Wehrheim This is my paper

Pith reviewed 2026-05-24 08:57 UTC · model grok-4.3

classification 💻 cs.PL cs.LO
keywords rely-guarantee reasoningcausal consistencyshared memoryprogram logicconcurrent programsHoare triplesmutual exclusion
0
0 comments X

The pith

Rely-guarantee reasoning extends parametrically to any memory model axiomatized by Hoare triples and applies directly to causal consistency.

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

The paper develops a rely-guarantee framework that works for any shared-memory model whose behavior is captured by Hoare triples. It then specializes the framework to causal consistency by using a potential-based operational semantics, producing a program logic called Piccolo whose assertions describe ordered sequences of states each thread may reach. This supplies the first compositional proof method for programs running under that semantics. A reader would care because it brings standard verification techniques to the relaxed memory models that real hardware and languages actually implement. The authors illustrate the method on standard litmus tests and on an adapted version of Peterson's mutual-exclusion algorithm.

Core claim

The authors introduce an RG framework parametric in the memory model whenever the model admits an axiomatic characterization by Hoare triples, instantiate the framework for causal consistency via its potential-based operational semantics, and obtain the Piccolo logic whose novel assertion language specifies ordered sequences of states reachable by each thread; they apply the logic to litmus tests and to a causally consistent variant of Peterson's algorithm.

What carries the argument

The parametric rely-guarantee framework, instantiated as the Piccolo logic whose assertions describe ordered sequences of states each thread may reach.

If this is right

  • Compositional proofs become available for any program whose memory model is given by Hoare triples.
  • Standard litmus tests for causal consistency can be verified directly in the logic.
  • Mutual-exclusion algorithms such as the adapted Peterson protocol can be shown correct under causal consistency.
  • The same parametric construction applies to any other memory model that possesses a Hoare-triple axiomatization.

Where Pith is reading between the lines

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

  • Similar parametric generalizations may be possible for other classic proof techniques that rest on Hoare logic.
  • Tool support for causal-consistency verification could reuse existing rely-guarantee infrastructure once the Hoare-triple interface is supplied.
  • The approach suggests that potential-based operational models are not inherently harder to reason about than sequentially consistent ones.

Load-bearing premise

Memory models of interest can be fully characterized by collections of Hoare triples.

What would settle it

A concrete concurrent program under the potential-based causal semantics whose safety property holds yet admits no Piccolo proof.

Figures

Figures reproduced from arXiv: 2305.08486 by Brijesh Dongol, Heike Wehrheim, Ori Lahav.

Figure 1
Figure 1. Figure 1: Message passing in SC  T0⋉[y 6= 1] Thread T1  True 1 : STORE(x, 1);  T1⋉[x = 1] 2 : STORE(y, 1)  True Thread T2  T2⋉[y 6= 1] ; [x = 1] 3 : a := LOAD(y);  a = 1 ⇒ T2⋉[x = 1] 4 : b := LOAD(x)  a = 1 ⇒ b = 1  a = 1 ⇒ b = 1 [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 3
Figure 3. Figure 3: Program syntax γ ′ = γ[r 7→ γ(e)] r := e ≫ γ ε−→ γ ′ l = W(x, γ(e)) STORE(x, e) ≫ γ l−→ γ l = R(x, v) γ ′ = γ[r 7→ v] r := LOAD(x) ≫ γ l−→ γ ′ l = RMW(x, v, γ(e)) SWAP(x, e) ≫ γ l−→ γ c ≫ γ lε−→ γ0 r1 := e1 ≫ γ0 ε−→ γ1 ... rn := en ≫ γn−1 ε−→ γn hc,hr1, ... ,rni := he1, ... ,enii ≫ γ lε −→ γn [PITH_FULL_IMAGE:figures/full_fig_p006_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Small-step semantics of (instrumented) primitive commands (c˜ ≫ γ lε −→ γ ′ ) components are instrumented commands c˜, which are meant to atomically exe￾cute a primitive command c and a (multiple) assignment ~r := ~e. Such instructions are needed to support auxiliary (a.k.a. ghost) variables in RG proofs. In addi￾tion, SWAP (a.k.a. atomic exchange) is an example of an RMW instruction. For brevity, other st… view at source ↗
Figure 5
Figure 5. Figure 5: Small-step semantics of commands (hC, γi lε−→ hC ′ , γ′ i) hC, γi lε−→ hC ′ , γ ′ i hC0 ⊎ {τ 7→ C}, γi τ,lε −−→ hC0 ⊎ {τ 7→ C ′ }, γi C(τ ) = C1 τ1 ||τ2 C2 τ1 6∈ dom(C) τ2 6∈ dom(C) l = FORK(τ1, τ2) C ′ = {τ1 7→ C1, τ2 7→ C2} hC, γi τ,l −−→ hC ⊎ C′ , γi C =  τ 7→ C1 τ1 ||τ2 C2, τ1 7→ skip, τ2 7→ skip l = JOIN(τ1, τ2) C ′ = {τ 7→ skip} hC0 ⊎ C, γi τ,l −−→ hC0 ⊎ C′ , γi [PITH_FULL_IMAGE:figures/full_fig_p… view at source ↗
Figure 6
Figure 6. Figure 6: Small-step semantics of command pools (hC, γi τ,lε −−→ hC′ , γ′ i) Definition 2. A register store is a mapping γ : Reg → Val. Register stores are extended to expressions as expected. We denote by Γ the set of all register stores. The semantics of (instrumented) primitive commands is given in [PITH_FULL_IMAGE:figures/full_fig_p007_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Generic sequential RG proof rules (letting JeK = {hγ, mi | γ(e) = true}) • if α ∈ {FORK(τ1, τ2), JOIN(τ1, τ2)}, then mi τ,α −−→M mi+1 and γi = γi+1. – ξ admits Q if hγlast(ξ) , mlast(ξ)i ∈ Q whenever ξ is finite and Clast(ξ)(τ) = skip for every τ ∈ dom(Clast(ξ)). We denote by Assume(P, R) the set of all computations that admit P and R, and by Commit(G, Q) the set of all computations that admit G and Q. The… view at source ↗
Figure 8
Figure 8. Figure 8: Steps of SRA (defining δ[x 7→ hv, u, τi](y) = hv, u, τi if y = x and δ(y) else, and δ[x 7→ R] to set all RMW-flags for x to R; both pointwise lifted to lists) Definition 12. The (overloaded) partial order ⊑ is defined as follows: 1. on potential store lists: L ′ ⊑ L if L ′ is a nonempty subsequence of L; 2. on potentials: D′ ⊑ D if ∀L ′ ∈ D′ . ∃L ∈ D. L′ ⊑ L; 3. on potential mappings: D′ ⊑ D if D′ (τ) ⊑ D(… view at source ↗
Figure 9
Figure 9. Figure 9: Assertions of Piccolo Theorem 2. A trace is generated by SRA iff it is generated by opSRA. The proof is of this theorem is by simulation arguments (forward simulation in one direction and backward for the converse). It is mechanized in Coq and available in [29]. The mechanized proof does not consider fork and join steps, but they can be straightforwardly added. 6 Program Logic For the instantiation of our … view at source ↗
Figure 10
Figure 10. Figure 10: Memory triples for Piccolo using WRITE ∈ {SWAP, STORE} and assuming τ 6= π 6. hγ, Di |= ϕ1 ∧ ϕ2 if hγ, Di |= ϕ1 and hγ, Di |= ϕ2 (similarly for ∨). Note that with ∧ and ∨ as well as negation on expressions,4 the logic provides the operators on sets of states necessary for an instantiation of our RG frame￾work. Further, the requirements from SRA states guarantee certain properties: – For ϕ1 = τ⋉[Eτ 1 ] ; .… view at source ↗
Figure 11
Figure 11. Figure 11: RRC for two threads (a.k.a. CoRR0)  T0⋉I x 0 [PITH_FULL_IMAGE:figures/full_fig_p018_11.png] view at source ↗
Figure 12
Figure 12. Figure 12: RRC for four threads (a.k.a. CoRR2) 7 Examples We discuss examples verified in Piccolo. Additional examples can be found in the appendix. Coherence. We provide two coherence examples in Figures 11 and 12, using the notation I x v1v2...vn = [x = v1] ; [x = v2] ; ... ; [x = vn] [PITH_FULL_IMAGE:figures/full_fig_p018_12.png] view at source ↗
Figure 13
Figure 13. Figure 13: Peterson’s algorithm, where P = T1⋉[R(turn)] ; [flag2 ∧turn = 1]. Thread T2 is symmetric and we assume a stopper thread T3 that sets stop to true. SRA, all accesses to the shared variable turn are via a SWAP, which ensures that turn behaves like an SC variable. Correctness is encoded via registers mx1 and mx2 into which the contents of shared variable cs is loaded. Mutual exclusion should guarantee both r… view at source ↗
read the original abstract

Rely-guarantee (RG) is a highly influential compositional proof technique for concurrent programs, which was originally developed assuming a sequentially consistent shared memory. In this paper, we first generalize RG to make it parametric with respect to the underlying memory model by introducing an RG framework that is applicable to any model axiomatically characterized by Hoare triples. Second, we instantiate this framework for reasoning about concurrent programs under causally consistent memory, which is formulated using a recently proposed potential-based operational semantics, thereby providing the first reasoning technique for such semantics. The proposed program logic, which we call Piccolo, employs a novel assertion language allowing one to specify ordered sequences of states that each thread may reach. We employ Piccolo for multiple litmus tests, as well as for an adaptation of Peterson's algorithm for mutual exclusion to causally consistent 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

1 major / 0 minor

Summary. The paper generalizes rely-guarantee (RG) reasoning to a parametric framework applicable to any memory model that admits an axiomatic characterization via Hoare triples. It then instantiates the framework for causally consistent shared memory, formulated via potential-based operational semantics, yielding the Piccolo program logic whose novel assertion language specifies ordered sequences of states reachable by each thread. The logic is applied to multiple litmus tests and an adaptation of Peterson's mutual-exclusion algorithm under causal consistency.

Significance. If the parametric soundness argument and the causal-consistency instantiation hold, the work supplies the first RG-style compositional technique for potential-based semantics of causal consistency. This is valuable because causal consistency is widely used in distributed systems, and the parametric design permits reuse for other models that satisfy the Hoare-triple characterization. Concrete examples on litmus tests and Peterson's algorithm provide initial evidence of practicality.

major comments (1)
  1. The soundness of the entire parametric RG framework rests on the claim that any memory model axiomatically characterized by Hoare triples yields sound RG rules. No general theorem stating the precise conditions on those triples (e.g., stability or framing properties) appears in the abstract or the supplied description; without such a theorem the instantiation for causal consistency cannot be verified as a special case.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the positive evaluation of the work's significance and for the constructive comment on the parametric framework. We address the concern below and will revise the manuscript accordingly.

read point-by-point responses

  1. Referee: The soundness of the entire parametric RG framework rests on the claim that any memory model axiomatically characterized by Hoare triples yields sound RG rules. No general theorem stating the precise conditions on those triples (e.g., stability or framing properties) appears in the abstract or the supplied description; without such a theorem the instantiation for causal consistency cannot be verified as a special case.

    Authors: The full manuscript (Section 3) defines the parametric RG framework and states Theorem 3.1, which proves soundness of the RG rules for any memory model whose axioms are given by Hoare triples satisfying the stability and framing properties listed in Definition 3.3. The causal-consistency instantiation (Section 4) verifies that the potential-based semantics meets exactly those conditions, allowing the general theorem to apply directly. The abstract was intentionally concise; we will revise the introduction to explicitly reference Theorem 3.1 and the required conditions on the triples so that the parametric claim is self-contained without needing the full body. revision: yes

Circularity Check

0 steps flagged

No significant circularity detected

full rationale

The paper's derivation consists of a parametric generalization of rely-guarantee reasoning to any memory model axiomatically characterized by Hoare triples, followed by an instantiation for causal consistency via an existing potential-based operational semantics and the introduction of the Piccolo logic with its assertion language. No equations, fitted parameters, predictions, or self-citations appear in the abstract or described structure that reduce any central claim to its inputs by construction. The framework is explicitly scoped to models admitting the Hoare-triple characterization, and the provided examples and logic constitute independent content rather than a renaming or self-referential fit.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

Review performed on abstract only; ledger therefore contains only the domain assumption stated in the abstract.

axioms (1)
  • domain assumption Memory models can be axiomatically characterized by Hoare triples
    Invoked to make the RG framework parametric (first sentence of abstract).

pith-pipeline@v0.9.0 · 5673 in / 1192 out tokens · 22382 ms · 2026-05-24T08:57:32.292885+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

47 extracted references · 47 canonical work pages

  1. [1]

    In: PLDI

    Abdulla, P.A., Arora, J., Atig, M.F., Krishna, S.N.: Veri fication of programs under the release-acquire semantics. In: PLDI. pp. 1117–11 32. ACM (2019), https://doi.org/10.1145/3314221.3314649 20

    work page doi:10.1145/3314221.3314649 2019

  2. [2]

    Abdulla, P.A., Atig, M.F., Bouajjani, A., Kumar, K.N., Sa ivasan, P.: Deciding reachability under persistent x86-tso. Proc. ACM Program. Lang. 5(POPL), 1–32 (2021), https://doi.org/10.1145/3434337

    work page doi:10.1145/3434337 2021

  3. [3]

    In: NETYS

    Abdulla, P.A., Atig, M.F., Bouajjani, A., Kumar, K.N., Sa ivasan, P.: Verifying reachability for TSO programs with dynamic threa d cre- ation. In: NETYS. LNCS, vol. 13464, pp. 283–300. Springer (2 022), https://doi.org/10.1007/978-3-031-17436-0_19

    work page doi:10.1007/978-3-031-17436-0_19

  4. [4]

    In: CONCU R

    Abdulla, P.A., Atig, M.F., Bouajjani, A., Ngo, T.P.: The b enefits of du- ality in verifying concurrent programs under TSO. In: CONCU R. LIPIcs, vol. 59, pp. 5:1–5:15. Schloss Dagstuhl - Leibniz-Zentrum f ür Informatik (2016), https://doi.org/10.4230/LIPIcs.CONCUR.2016.5

    work page doi:10.4230/lipics.concur.2016.5 2016

  5. [5]

    Abdulla, P.A., Atig, M.F., Bouajjani, A., Ngo, T.P.: A loa d-buffer seman- tics for total store ordering. Log. Methods Comput. Sci. 14(1) (2018), https://doi.org/10.23638/LMCS-14(1:9)2018

    work page doi:10.23638/lmcs-14(1:9)2018 2018

  6. [6]

    Distribute d Comput

    Ahamad, M., Neiger, G., Burns, J.E., Kohli, P., Hutto, P.W .: Causal memory: Definitions, implementation, and programming. Distribute d Comput. 9(1), 37–49 (1995), https://doi.org/10.1007/BF01784241

    work page doi:10.1007/bf01784241 1995

  7. [7]

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

    Alglave, J., Cousot, P.: Ogre and Pythia: an invariance pr oof method for weak consistency models. In: Castagna, G., Gordon, A.D. (eds.) P OPL. pp. 3–18. ACM (2017), https://doi.org/10.1145/3009837.3009883

    work page doi:10.1145/3009837.3009883 2017

  8. [8]

    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:1–7:74 (2014), https://doi.org/10.1145/2627752

    work page doi:10.1145/2627752 2014

  9. [9]

    Texts in Computer Science, Springer ( 2009), https://doi.org/10.1007/978-1-84882-745-5

    Apt, K.R., de Boer, F.S., Olderog, E.: Verification of Sequ ential and Concurrent Programs. Texts in Computer Science, Springer ( 2009), https://doi.org/10.1007/978-1-84882-745-5

    work page doi:10.1007/978-1-84882-745-5 2009

  10. [10]

    Beillahi, S.M., Bouajjani, A., Enea, C.: Robustness aga inst transac- tional causal consistency. Log. Methods Comput. Sci. 17(1) (2021), https://lmcs.episciences.org/7149

    work page 2021

  11. [11]

    In: ESOP

    Bila, E.V., Dongol, B., Lahav, O., Raad, A., Wickerson, J .: View-Based Owicki- Gries Reasoning for Persistent x86-TSO. In: ESOP. LNCS, vol . 13240, pp. 234–261. Springer (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]

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

    Bouajjani, A., Enea, C., Guerraoui, R., Hamza, J.: On ver ifying causal consistency. In: POPL. pp. 626–638. ACM (2017), https://doi.org/10.1145/3009837.3009888

    work page doi:10.1145/3009837.3009888 2017

  13. [13]

    Chaochen, Z., Hoare, C.A.R., Ravn, A.P.: A calculus of du rations. Inf. Process. Lett. 40(5), 269–276 (1991), https://doi.org/10.1016/0020-0190(91)90122-X

    work page doi:10.1016/0020-0190(91)90122-x 1991

  14. [14]

    Coughlin, N., Winter, K., Smith, G.: Rely/guarantee rea soning for multicopy atomic weak memory models. In: FM. LNCS, vol. 13047, pp. 292– 310. Springer (2021), https://doi.org/10.1007/978-3-030-90870-6_16

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

  15. [15]

    Coughlin, N., Winter, K., Smith, G.: Compositional reas oning for non-multicopy atomic architectures. Form. Asp. Comput. (d ec 2022), https://doi.org/10.1145/3574137

    work page doi:10.1145/3574137 2022

  16. [16]

    In: ECOOP

    Dalvandi, S., Doherty, S., Dongol, B., Wehrheim, H.: Owi cki-Gries Reasoning for C11 RAR. In: ECOOP. LIPIcs, vol. 166, pp. 11:1–11:26. Schlos s Dagstuhl - Leibniz- Zentrum für Informatik (2020), https://doi.org/10.4230/LIPIcs.ECOOP.2020.11

    work page doi:10.4230/lipics.ecoop.2020.11 2020

  17. [17]

    Dalvandi, S., Dongol, B., Doherty, S., Wehrheim, H.: Int egrating Owicki-Gries for C11-Style Memory Models into Isabelle/HOL. J. Autom. Reaso n. 66(1), 141–171 (2022), https://doi.org/10.1007/s10817-021-09610-2

    work page doi:10.1007/s10817-021-09610-2 2022

  18. [18]

    In: POPL

    Dinsdale-Young, T., Birkedal, L., Gardner, P., Parkins on, M.J., Yang, H.: Views: compositional reasoning for concurrent programs. In: POPL . pp. 287–300. ACM (2013), https://doi.org/10.1145/2429069.2429104 21

    work page doi:10.1145/2429069.2429104 2013

  19. [19]

    ACM Trans

    Doherty, S., Dalvandi, S., Dongol, B., Wehrheim, H.: Uni fying Operational Weak Memory Verification: An Axiomatic Approach. ACM Trans. Comp ut. Log. 23(4), 27:1–27:39 (2022), https://doi.org/10.1145/3545117

    work page doi:10.1145/3545117 2022

  20. [20]

    In: PPoPP

    Doherty, S., Dongol, B., Wehrheim, H., Derrick, J.: Veri fying C11 programs operationally. In: PPoPP. pp. 355–365. ACM (2019) , https://doi.org/10.1145/3293883.3295702

    work page doi:10.1145/3293883.3295702 2019

  21. [21]

    ACM Trans

    Jones, C.B.: Tentative steps toward a development metho d for interfer- ing programs. ACM Trans. Program. Lang. Syst. 5(4), 596–619 (1983), https://doi.org/10.1145/69575.69577

    work page doi:10.1145/69575.69577 1983

  22. [22]

    Jung, R., Krebbers, R., Jourdan, J., Bizjak, A., Birkeda l, L., Dreyer, D.: Iris from the ground up: A modular foundation for higher-order concur rent separation logic. J. Funct. Program. 28, e20 (2018), https://doi.org/10.1017/S0956796818000151

    work page doi:10.1017/s0956796818000151 2018

  23. [23]

    In: ECOOP

    Kaiser, J., Dang, H., Dreyer, D., Lahav, O., Vafeiadis, V .: Strong logic for weak memory: Reasoning about release-acquire consistency in ir is. In: ECOOP. LIPIcs, vol. 74, pp. 17:1–17:29. Schloss Dagstuhl - Leibniz-Zentru m für Informatik (2017), https://doi.org/10.4230/LIPIcs.ECOOP.2017.17

    work page doi:10.4230/lipics.ecoop.2017.17 2017

  24. [24]

    Kan, S., Lin, A.W., Rümmer, P., Schrader, M.: CertiStr: a certified string solver. In: CPP. pp. 210–224. ACM (2022), https://doi.org/10.1145/3497775.3503691

    work page doi:10.1145/3497775.3503691 2022

  25. [25]

    In: POPL

    Kang, J., Hur, C., Lahav, O., Vafeiadis, V., Dreyer, D.: A promising seman- tics for relaxed-memory concurrency. In: POPL. pp. 175–189 . ACM (2017), https://doi.org/10.1145/3009837.3009850

    work page doi:10.1145/3009837.3009850 2017

  26. [26]

    ACM SIGLOG News 6(2), 43–56 (2019), https://doi.org/10.1145/3326938.3326942

    Lahav, O.: Verification under causally consistent share d memory. ACM SIGLOG News 6(2), 43–56 (2019), https://doi.org/10.1145/3326938.3326942

    work page doi:10.1145/3326938.3326942 2019

  27. [27]

    In: PLDI

    Lahav, O., Boker, U.: Decidable verification under a caus ally con- sistent shared memory. In: PLDI. pp. 211–226. ACM (2020), https://doi.org/10.1145/3385412.3385966

    work page doi:10.1145/3385412.3385966 2020

  28. [28]

    Lahav, O., Boker, U.: What’s Decidable About Causally Co nsistent Shared Memory? ACM Trans. Program. Lang. Syst. 44(2), 8:1–8:55 (2022), https://doi.org/10.1145/3505273

    work page doi:10.1145/3505273 2022

  29. [29]

    Zenodo (2 023), https://doi.org/10.5281/zenodo.7875360

    Lahav, O., Dongol, B., Wehrheim, H.: Artifact: Rely-gua rantee reasoning for causally consistent shared memory. Zenodo (2 023), https://doi.org/10.5281/zenodo.7875360

    work page doi:10.5281/zenodo.7875360

  30. [30]

    In: POPL

    Lahav, O., Giannarakis, N., Vafeiadis, V.: Taming relea se-acquire consistency. In: POPL. pp. 649–662. ACM (2016), https://doi.org/10.1145/2837614.2837643

    work page doi:10.1145/2837614.2837643 2016

  31. [31]

    In: ICALP

    Lahav, O., Vafeiadis, V.: Owicki-Gries Reasoning for We ak Memory Models. In: ICALP. LNCS, vol. 9135, pp. 311–323. Springer (2 015), https://doi.org/10.1007/978-3-662-47666-6_25

    work page doi:10.1007/978-3-662-47666-6_25

  32. [32]

    IEEE Trans

    Lamport, L.: How to make a multiprocessor computer that c orrectly exe- cutes multiprocess programs. IEEE Trans. Computers 28(9), 690–691 (1979), https://doi.org/10.1109/TC.1979.1675439

    work page doi:10.1109/tc.1979.1675439 1979

  33. [33]

    In: FMCAD

    de León, H.P., Furbach, F., Heljanko, K., Meyer, R.: BMC w ith memory models as modules. In: FMCAD. pp. 1–9. IEEE (2018), https://doi.org/10.23919/FMCAD.2018.8603021

    work page doi:10.23919/fmcad.2018.8603021 2018

  34. [34]

    Moszkowski, B.C.: A complete axiom system for propositi onal interval tem- poral logic with infinite time. Log. Methods Comput. Sci. 8(3) (2012), https://doi.org/10.2168/LMCS-8(3:10)2012

    work page doi:10.2168/lmcs-8(3:10)2012 2012

  35. [35]

    In: TPHOLs

    Owens, S., Sarkar, S., Sewell, P.: A better x86 memory mod el: x86- tso. In: TPHOLs. LNCS, vol. 5674, pp. 391–407. Springer (200 9), https://doi.org/10.1007/978-3-642-03359-9_27

    work page doi:10.1007/978-3-642-03359-9_27

  36. [36]

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

    Owicki, S.S., Gries, D.: An Axiomatic Proof Technique fo r Parallel Programs I. Acta Informatica 6, 319–340 (1976), https://doi.org/10.1007/BF00268134 22

    work page doi:10.1007/bf00268134 1976

  37. [37]

    Peterson, G.L.: Myths about the mutual exclusion proble m. Inf. Process. Lett. 12(3), 115–116 (1981)

    work page 1981

  38. [38]

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

    work page doi:10.1145/3428219 2020

  39. [39]

    In: VSTTE

    Ridge, T.: A Rely-Guarantee Proof System for x86-TSO. In: VSTTE. LNCS, vol. 6217, pp. 55–70. Springer (2010), https://doi.org/10.1007/978-3-642-15057-9_4

    work page doi:10.1007/978-3-642-15057-9_4 2010

  40. [40]

    Schellhorn, G., Tofan, B., Ernst, G., Pfähler, J., Reif, W.: RGITL: A temporal logic framework for compositional reasoning about interleaved p rograms. Ann. Math. Artif. Intell. 71(1-3), 131–174 (2014), https://doi.org/10.1007/s10472-013-9389-z

    work page doi:10.1007/s10472-013-9389-z 2014

  41. [41]

    In: IJCAR

    Sheng, Y., Nötzli, A., Reynolds, A., Zohar, Y., Dill, D.L ., Grieskamp, W., Park, J., Qadeer, S., Barrett, C.W., Tinelli, C.: Reasoning about vectors using an SMT theory of sequences. In: IJCAR. LNCS, vol. 13385, pp. 125–14 3. Springer (2022), https://doi.org/10.1007/978-3-031-10769-6_9

    work page doi:10.1007/978-3-031-10769-6_9 2022

  42. [42]

    In: ESOP

    Svendsen, K., Pichon-Pharabod, J., Doko, M., Lahav, O., Vafeiadis, V.: A sepa- ration logic for a promising semantics. In: ESOP. LNCS, vol. 10801, pp. 357–384. Springer (2018), https://doi.org/10.1007/978-3-319-89884-1_13

    work page doi:10.1007/978-3-319-89884-1_13 2018

  43. [43]

    Vafeiadis, V.: Modular fine-grained concurrency verific a- tion. Ph.D. thesis, University of Cambridge, UK (2008), https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.612221

    work page 2008

  44. [44]

    In: OOPSLA

    Vafeiadis, V., Narayan, C.: Relaxed separation logic: a program logic for C11 concurrency. In: OOPSLA. pp. 867–884. ACM (201 3), https://doi.org/10.1145/2509136.2509532

    work page doi:10.1145/2509136.2509532

  45. [45]

    In: CONCUR

    Vafeiadis, V., Parkinson, M.J.: A marriage of rely/guar antee and separa- tion logic. In: CONCUR. LNCS, vol. 4703, pp. 256–271. Spring er (2007), https://doi.org/10.1007/978-3-540-74407-8_18

    work page doi:10.1007/978-3-540-74407-8_18 2007

  46. [46]

    Wright, D., Batty, M., Dongol, B.: Owicki-Gries Reasoni ng for C11 Programs with Relaxed Dependencies. In: FM. LNCS, vol. 13047, pp. 237–254 . Springer (2021), https://doi.org/10.1007/978-3-030-90870-6_13

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

  47. [47]

    Formal Aspects Comput

    Xu, Q., de Roever, W.P., He, J.: The Rely-Guarantee Metho d for Verifying Shared Variable Concurrent Programs. Formal Aspects Comput. 9(2), 149–174 (1997), https://doi.org/10.1007/BF01211617 23 A Auxiliary Variables and Rule of Consequence Here, we provide the necessary definitions and the rule for au xiliary variables. Definition 14. For a setZ ⊆ Reg, two ...

    work page doi:10.1007/bf01211617 1997