pith. sign in

arxiv: 2604.21084 · v1 · submitted 2026-04-22 · 💻 cs.LO

Deductive Verification of Weak Memory Programs with View-based Protocols (extended version)

\"Omer \c{S}akar , Soham Chakraborty , Marieke Huisman , Anton Wijs This is my paper

Pith reviewed 2026-05-09 22:28 UTC · model grok-4.3

classification 💻 cs.LO
keywords weak memory concurrencydeductive verificationseparation logicSLR logicVerCorsprotocol automataconcurrent programsautomated verification
0
0 comments X

The pith

We extend VerCors into VerCors-relaxed and encode the relaxed fragment of SLR to enable automated deductive verification of weak memory programs.

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

The paper develops a way to bring automated deductive verification to concurrent programs that run under weak memory models, where behaviors deviate from simple thread interleaving. It extends the VerCors verifier with support for relaxed atomics and protocol automata concepts drawn from permission-based separation logics. The key step is an encoding of the relaxed fragment of the SLR logic into this new VerCors-relaxed setting. This encoding is then used to check several published examples automatically and with practical running times.

Core claim

The central claim is that an encoding of the relaxed fragment of the SLR program logic into VerCors-relaxed faithfully preserves the original logic's soundness and suffices to cover the behaviors of chosen examples, thereby allowing the VerCors tool to automatically verify weak memory programs that previously required manual proofs.

What carries the argument

VerCors-relaxed, the extension of VerCors that augments its atomic support with concepts from protocol automata to encode permission-based separation logics for weak memory concurrency.

Load-bearing premise

The encoding of the relaxed fragment of SLR into VerCors-relaxed must preserve soundness and be expressive enough for the chosen examples.

What would settle it

A literature example known to be correct under weak memory that the VerCors-relaxed encoding fails to verify automatically.

Figures

Figures reproduced from arXiv: 2604.21084 by Anton Wijs, Marieke Huisman, \"Omer \c{S}akar, Soham Chakraborty.

Figure 1
Figure 1. Figure 1: A PVL program summing an array in parallel. of register variables Reg. Without loss of generality, we assume that all variables in A ∪ Reg are of a generic type V, and v ∈ V is a value from this domain. There are three ways to interact with atomic memory: 1. Writing of the value v ∈ V to atomic location x ∈ A by thread t ∈ T, corresponding to a relaxed write instruction, e.g., the store operation x := 1. 2… view at source ↗
Figure 2
Figure 2. Figure 2: Two example programs using atomics with relaxed orderings [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Protocols for the 2+2W and COH examples in [PITH_FULL_IMAGE:figures/full_fig_p005_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: The Readt x and PReadt x functions. (Write) t ∈ T L t x(t) v−→t,x s ⟨L, π, τ ⟩ x:=v −−−→t,x ⟨L[(t, x) 7→ Lt x[t 7→ s]], π[x 7→ s], τ [x 7→ τ (x) ∪ {(π(x), s)}]⟩ (Read) t, t′ ∈ T s ∈ Readt x(L, π, τ ) ∩ S t ′ x x = V t ′ x (s) ⟨L, π, τ ⟩ a:=x −−−→t,x ⟨L[(t, x) 7→ Lt x[t ′ 7→ s]], π[x 7→ s], τ [x 7→ τ (x) ∪ {(π(x), s)}]⟩ [PITH_FULL_IMAGE:figures/full_fig_p007_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Operational semantics for protocol views with load and store operations. In [PITH_FULL_IMAGE:figures/full_fig_p007_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: The w−rlx rule the next two possible load operations are associated with s 0,1 x and s 1,1 x , meaning that both 1 and 2 can be read. Hence, the result indicated in [PITH_FULL_IMAGE:figures/full_fig_p009_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: The coherence properties ⊢{ O(x, −, ts) } r := x { ∃ts′ ≥ ts. O(x, v, ts′ ) ∗ r = v ∗ ϕ(v) } (r−rlx) ⊢{ W1 (x, X) } r := x { ∃ts. (v, ts) = max(X) ∗ W1 (x, X) ∗ r = v ∗ O(x, v, ts) ∗ ϕ(v)} (r−rlx∗ ) [PITH_FULL_IMAGE:figures/full_fig_p011_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: The r−rlx and r−rlx∗ rules ing from x, the value v is observed at a timestamp ts′ > ts, and the predicate ϕ(v) can be established (dually from the w−rlx rule). In the Read-rule (in [PITH_FULL_IMAGE:figures/full_fig_p011_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: Skeleton code for a protocol encoding. 5 Encoding Protocols and Views into VerCors-relaxed In this section, we explain parts of the encoding of the protocols and thread￾local views into VerCors-relaxed. For presentation purposes, we omit the contract template for parallel programs (see Appendix A). Furthermore, we leave out the encoding for τ in the method contracts for load and store, addressing the SOS R… view at source ↗
Figure 10
Figure 10. Figure 10: The contract of the constructor. 1 /*@ given seq<ps> oldLV; 2 yields seq<ps> newLV; 3 given int N, t; 4 given ps prevPi; 5 yields ps nextPi; 6 1)context Perm(G[*], 1\2); 7 ensures (∀* int t1=0..N; G[t1] == \old(G[t1])); 8 2)ensures newLV[t] == \old(oldLV[t]); 9 requires (∀ int t1,t2=0..N; intra(oldLV[t1][t2]) <= intra(G[t2]) 10 || intra(G[t2]) <= intra(oldLV[t1][t2]))); 11 ensures(∀ int t1,t2=0..N; intra(… view at source ↗
Figure 11
Figure 11. Figure 11: The contract of the load method. Figs. 10 to 12 shows contracts for the atomic methods. Here, a global view G is used, which is an array of ps, where ∀t ∈ T.L[t][t] = G[t]. G is used as a shorthand to simplify notation. The atomic location is represented by a class a_V ( [PITH_FULL_IMAGE:figures/full_fig_p014_11.png] view at source ↗
Figure 12
Figure 12. Figure 12: The contract of the store method. 1. Permission annotations: To read from the protocol of a different thread, load requires thread read permission to all global views (l.6). A thread acquires this permission from a global invariant (at the call site of load). It is specified that the global view does not change (l.7), since the load method only requires read permission and does not change the global view.… view at source ↗
Figure 13
Figure 13. Figure 13: The examples, including their executions [PITH_FULL_IMAGE:figures/full_fig_p017_13.png] view at source ↗
Figure 14
Figure 14. Figure 14: General template for using relaxed atomics on a location x. A General contract for parallel programs with atomics With protocols defined (see [PITH_FULL_IMAGE:figures/full_fig_p022_14.png] view at source ↗
Figure 15
Figure 15. Figure 15: Operational semantics for protocol views with successful and unsuccessful rmw operations. (l.11). Finally, all threads ensure their global view ends up in an accepting state (l.12), encoding condition CC1 mentioned in Section 3. After the parallel block, a case distinction is made (l.16). In the end, a view is consistent iff there are no speculations anymore, i.e., the property in l.5 holds. We only reaso… view at source ↗
Figure 16
Figure 16. Figure 16: An example program with rmw operations (left) and its protocols (right). Once the verification procedure for a program with rmw operations has fin￾ished, the final consistency check involves two more conditions. ∀s ∈ S.σ(s) = 0 ∨ σ(s) = 1 (CC3) ∀x ∈ A, s, s′ ∈ Sx.(s ̸= s ′ ∧ σ(s) = σ(s ′ ) = 1) =⇒ s ̸∈ Sˆ x ∨ s ′ ̸∈ Sˆ x (CC4) CC3 expresses that every state occurs at most once in σ. If a state would occur… view at source ↗
Figure 17
Figure 17. Figure 17: The contract of the rmw method. 1. rmw fail: When the operation fails, the global view of t does not change (l.5). The call to load updates the local view. The return value of load cannot be equivalent to oldVal (l.6). Finally, a description of newLV can be given (l.7). The predicate descriptionFail is a placeholder and is to be defined by the user to use in further proofs. It can be used to exclude certa… view at source ↗
Figure 18
Figure 18. Figure 18: The encoding of the COH example [PITH_FULL_IMAGE:figures/full_fig_p026_18.png] view at source ↗
read the original abstract

Concurrent programming under weak memory concurrency faces substantial challenges to ensure correctness due to program behaviors that cannot be explained by thread interleaving, a.k.a. sequential consistency. While several program logics are proposed to reason about weak memory concurrency, their usage has been limited to intricate manual proofs. On the other hand, the VerCors verifier provides a rich toolset for automated deductive verification for sequential consistency. In this paper, we bridge this gap for automated deductive verification of weak memory concurrent programs with the VerCors deductive verification tool. We propose an approach to encode weak memory concurrency in VerCors. We develop VerCors-relaxed, where we extend the VerCors atomics support and bring concepts from several protocol automata to encode permission-based separation logics for weak memory concurrency models. To demonstrate the effectiveness of our approach, we encode the relaxed fragment of the SLR program logic, a recent state-of-the-art permission-based separation logic for weak memory concurrency in VerCors-relaxed, our extension of VerCors. We use the SLR encoding on VerCors-relaxed to automatically verify several examples from the literature within realistic performance.

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 / 1 minor

Summary. The paper extends the VerCors deductive verifier to VerCors-relaxed, adding support for weak memory models via extended atomics and protocol automata concepts drawn from permission-based separation logics. It encodes the relaxed fragment of the SLR logic into this infrastructure and reports automated verification of several literature examples under realistic performance bounds.

Significance. If the encoding is faithful, the work meaningfully reduces the manual-proof burden for weak-memory programs by reusing VerCors infrastructure and SLR, enabling automated verification of realistic examples that were previously out of reach for deductive tools.

major comments (1)
  1. [Abstract] Abstract: the central claim that the SLR encoding 'faithfully' supports the chosen examples rests on an unshown soundness argument for the protocol-automata embedding; without an explicit statement of the preservation theorem or the restrictions imposed on the relaxed fragment, the verification results cannot be assessed for soundness.
minor comments (1)
  1. The abstract and title refer to both 'protocol automata' and 'view-based protocols' without clarifying whether these are synonymous or how views are represented in the encoding.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the careful reading of our manuscript and the recommendation for minor revision. The comment raises a valid point about the need for greater explicitness regarding soundness, which we will address directly.

read point-by-point responses

  1. Referee: [Abstract] Abstract: the central claim that the SLR encoding 'faithfully' supports the chosen examples rests on an unshown soundness argument for the protocol-automata embedding; without an explicit statement of the preservation theorem or the restrictions imposed on the relaxed fragment, the verification results cannot be assessed for soundness.

    Authors: We agree that the presentation would benefit from greater explicitness. The manuscript encodes only the relaxed fragment of SLR and relies on the protocol-automata embedding to preserve the relevant properties of that fragment. To make this fully assessable, we will revise the abstract to qualify the claim and add an explicit statement of the preservation theorem (including the precise restrictions on the relaxed fragment) in the body of the paper, most likely as a short dedicated subsection or paragraph following the description of the encoding. This change clarifies the soundness argument without requiring new technical results. revision: yes

Circularity Check

0 steps flagged

No significant circularity in derivation chain

full rationale

The paper presents an encoding of the relaxed fragment of the SLR separation logic into an extended VerCors tool (VerCors-relaxed) and reports automated verification of literature examples. This is an implementation and demonstration effort that applies prior logics and infrastructure rather than deriving new results from fitted parameters or self-referential definitions. The central claim (successful verification via the encoding) is empirical and does not reduce by construction to its inputs; soundness preservation is stated as an assumption without being tautologically forced by the reported outcomes. No self-definitional steps, fitted-input predictions, or load-bearing self-citation chains appear in the described approach.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The approach rests on standard permission-based separation logic axioms and the soundness of the SLR logic from prior work; no free parameters or invented entities are introduced in the abstract description.

axioms (1)
  • domain assumption Permission-based separation logic axioms for weak memory views
    Invoked when extending VerCors atomics support and encoding SLR protocols; assumed from prior SLR literature.

pith-pipeline@v0.9.0 · 5503 in / 1107 out tokens · 29931 ms · 2026-05-09T22:28:35.847753+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

41 extracted references · 41 canonical work pages

  1. [1]

    In: TACAS

    Abdulla, P.A., Atig, M.F., Chen, Y.F., Leonardsson, C., Rezine, A.: Memorax, a precise and sound tool for automatic fence insertion under TSO. In: TACAS. LNCS, vol. 7795, pp. 530–536. Springer (2013)

    work page 2013

  2. [2]

    In: ESOP

    Abdulla, P.A., Atig, M.F., Ngo, T.P.: The best of both worlds: Trading efficiency and optimality in fence insertion for TSO. In: ESOP. LNCS, vol. 9032, pp. 308–332. Springer (2015)

    work page 2015

  3. [3]

    ACM Trans

    Alglave, J., Kroening, D., Nimal, V., Poetzl, D.: Don’t sit on the fence: a static analysis approach to automatic fence insertion. ACM Trans. on Progr. Lang. and Syst. 39(2), 6 (2017)

    work page 2017

  4. [4]

    Alglave, J., Maranget, L.: Stability in weak memory models. In: CAV. LNCS, vol. 6806, pp. 50–66. Springer (2011)

    work page 2011

  5. [5]

    Alglave, J., Maranget, L., Sarkar, S., Sewell, P.: Fences in weak memory models. In: CAV. LNCS, vol. 6174, pp. 258–272. Springer (2010)

    work page 2010

  6. [6]

    Amighi, A.: Specification and verification of synchronisation classes in Java: A practical approach. Ph.D. thesis, University of Twente (2018).https://doi.org/ 10.3990/1.9789036544399, chapter 5 - Verification of Synchronisers: Exclusive Access

    work page doi:10.3990/1.9789036544399 2018

  7. [7]

    In: Asian Symposium on Programming Languages and Systems

    Amighi, A., Blom, S., Huisman, M.: Resource protection using atomics: Patterns and verification. In: Asian Symposium on Programming Languages and Systems. pp. 255–274. Springer (2014)

    work page 2014

  8. [8]

    Armborst, L., Bos, P., van den Haak, L.B., Huisman, M., Rubbens, R., Şakar, Ö., Tasche, P.: The VerCors Verifier: A Progress Report. In: CAV. LNCS, vol. 14682, pp. 3–18. Springer (2024)

    work page 2024

  9. [9]

    Atig, M.F., Bouajjani, A., Parlato, G.: Getting rid of store-buffers in TSO analysis. In: CAV. LNCS, vol. 6806, pp. 99–115. Springer (2011) 20 Ö. Şakar et al

    work page 2011

  10. [10]

    In: de Boer, F., Bonsangue, M., Graf, S., de Roever, W

    Berdine, J., Calcagno, C., O’Hearn, P.: Smallfoot: Modular Automatic Asser- tion Checking with Separation Logic. In: de Boer, F., Bonsangue, M., Graf, S., de Roever, W. (eds.) FMCO. LNCS, vol. 4111, pp. 115–137. Springer (2005)

    work page 2005

  11. [11]

    Bornat, R., Calcagno, C., O’Hearn, P., Parkinson, M.: Permission accounting in separationlogic.In:Proceedingsofthe32ndACMSIGPLAN-SIGACTSymposium on Principles of programming languages. pp. 259–270 (2005).https://doi.org/ 10.1145/1040305.1040327

    work page doi:10.1145/1040305.1040327 2005

  12. [12]

    In: ESOP

    Bouajjani, A., Derevenetc, E., Meyer, R.: Checking and enforcing robustness against TSO. In: ESOP. LNCS, vol. 7792, pp. 533–553. Springer (2013)

    work page 2013

  13. [13]

    In: Cousot, R

    Boyland, J.: Checking Interference with Fractional Permissions. In: Cousot, R. (ed.) SAS. LNCS, vol. 2694, pp. 55–72. Springer (2003).https://doi.org/10. 1007/3-540-44898-5_4

    work page 2003

  14. [14]

    Burckhardt, S., Musuvathi, M.: Effective program verification for relaxed memory models. In: CAV. LNCS, vol. 5123, pp. 107–120. Springer (2008)

    work page 2008

  15. [15]

    Chakraborty, S., Krishna, S., Pavlogiannis, A., Tuppe, O.: GPUMC: A Stateless Model Checker for GPU Weak Memory Concurrency. In: CAV. LNCS, vol. 15933, pp. 321–346. Springer (2025)

    work page 2025

  16. [16]

    In: International Conference on Verification, Model Checking, and Abstract Interpretation

    Doko, M., Vafeiadis, V.: A program logic for c11 memory fences. In: International Conference on Verification, Model Checking, and Abstract Interpretation. pp. 413–

    work page

  17. [17]

    Doko, M., Vafeiadis, V.: Tackling real-life relaxed concurrency with FSL++. In: Programming Languages and Systems: 26th European Symposium on Program- ming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017, Proceed- ings 26. pp. 448–475. Springer (2017)

    work page 2017

  18. [18]

    Fang, X., Lee, J., Midkiff, S.: Automatic fence insertion for shared memory multi- processing. In: ICS. pp. 285–294. ACM Press (2003)

    work page 2003

  19. [19]

    IEEE Access8, 173874–173903 (2020).https://doi.org/10

    He, M., Qin, S., Xu, Z.: A Program Logic for Reasoning About C11 Programs With Release-Sequences. IEEE Access8, 173874–173903 (2020).https://doi.org/10. 1109/ACCESS.2020.3024681

    work page arXiv 2020

  20. [20]

    International Journal of Parallel Programming46(6), 1157–1183 (2018)

    He, M., Vafeiadis, V., Qin, S., Ferreira, J.F.: GPS+: Reasoning about fences and relaxed atomics. International Journal of Parallel Programming46(6), 1157–1183 (2018)

    work page 2018

  21. [21]

    CW Reports (2014)

    Jacobs, B.: Verifying tso programs. CW Reports (2014)

    work page 2014

  22. [22]

    ACM SIGARCH Computer Architecture News36, 65–71 (2009)

    Jonsson, B.: State-space exploration for concurrent algorithms under weak memory orderings. ACM SIGARCH Computer Architecture News36, 65–71 (2009)

    work page 2009

  23. [23]

    ACM SIGPLAN Notices52(1), 175–189 (2017)

    Kang, J., Hur, C.K., Lahav, O., Vafeiadis, V., Dreyer, D.: A promising semantics for relaxed-memory concurrency. ACM SIGPLAN Notices52(1), 175–189 (2017)

    work page 2017

  24. [24]

    In: PLDI

    Kuperstein, M., Vechev, M., Yahav, E.: Partial-coherence abstractions for relaxed memory models. In: PLDI. pp. 187–198. ACM Press (2011)

    work page 2011

  25. [25]

    ACM SIGPLAN Notices52(6), 618–632 (2017)

    Lahav, O., Vafeiadis, V., Kang, J., Hur, C.K., Dreyer, D.: Repairing sequential consistency in c/c++ 11. ACM SIGPLAN Notices52(6), 618–632 (2017)

    work page 2017

  26. [26]

    IEEE Trans

    Lee, J., Padua, D.: Hiding relaxed memory consistency with a compiler. IEEE Trans. Comput.50, 824–833 (2001)

    work page 2001

  27. [27]

    In: PLDI

    Lee, S.H., Cho, M., Podkopaev, A., Chakraborty, S., Hur, C.K., Lahav, O., Vafeiadis, V.: Promising 2.0: global optimizations in relaxed memory concurrency. In: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation. pp. 362–376. PLDI 2020, Association for Comput- ing Machinery, New York, NY, USA (2020).https://doi...

    work page doi:10.1145/3385412 2020

  28. [28]

    In: TACAS

    Linden, A., Wolper, P.: A verification-based approach to memory fence insertion in PSO memory systems. In: TACAS. LNCS, vol. 7795, pp. 339–353. Springer (2013)

    work page 2013

  29. [29]

    Margalit, R., Lahav, O.: Verifying observational robustness against a c11-style memory model. Proc. ACM Program. Lang.5(POPL) (Jan 2021).https://doi. org/10.1145/3434285, https://doi.org/10.1145/3434285

    work page doi:10.1145/3434285 2021

  30. [30]

    In: Jobstmann, B., Leino, K.R.M

    Müller, P., Schwerhoff, M., Summers, A.: Viper - a verification infrastructure for permission-based reasoning. In: Jobstmann, B., Leino, K.R.M. (eds.) Verification, Model Checking, and Abstract Interpretation. VMCAI. Springer Berlin Heidelberg (2016). https://doi.org/10.1007/978-3-662-49122-5_2

    work page doi:10.1007/978-3-662-49122-5_2 2016

  31. [31]

    de Putter, S., Wijs, A.: Lock and Fence When Needed: State Space Exploration + Static Analysis = Improved Fence and Lock Insertion. In: iFM. LNCS, vol. 12546, pp. 297–317. Springer (2020)

    work page 2020

  32. [32]

    https://doi.org/10.4121/cd7ac73c-883e-4340-8425-35b4faa00146

    Şakar, Ö., Chakraborty, S., Huisman, M., Wijs, A.: Artifact for the paper: De- ductive verification of weak memory programs with view-based protocols (2026). https://doi.org/10.4121/cd7ac73c-883e-4340-8425-35b4faa00146

    work page doi:10.4121/cd7ac73c-883e-4340-8425-35b4faa00146 2026

  33. [33]

    International Journal on Software Tools for Technol- ogy Transfer22(6), 709–728 (2020)

    Summers, A.J., Müller, P.: Automating deductive verification for weak-memory programs (extended version). International Journal on Software Tools for Technol- ogy Transfer22(6), 709–728 (2020)

    work page 2020

  34. [34]

    In: PPOPP

    Sura, Z., Fang, X., Wong, C.L., Midkiff, S., Lee, J., Padua, D.: Compiler techniques for high performance sequentially consistent Java programs. In: PPOPP. pp. 2–13. ACM Press (2005)

    work page 2005

  35. [35]

    In: ESOP

    Svendsen, K., Pichon-Pharabod, J., Doko, M., Lahav, O., Vafeiadis, V.: A sep- aration logic for a promising semantics. In: Ahmed, A. (ed.) Programming Lan- guages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20,...

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

  36. [36]

    SIGPLAN Not

    Turon, A., Vafeiadis, V., Dreyer, D.: GPS: navigating weak memory with ghosts, protocols, and separation. SIGPLAN Not. 49(10), 691–707 (Oct 2014). https://doi.org/10.1145/2714064.2660243, https://doi.org/10.1145/ 2714064.2660243

    work page doi:10.1145/2714064.2660243 2014

  37. [37]

    Electronic Notes in Theoretical Computer Science 276, 335–351 (2011)

    Vafeiadis, V.: Concurrent separation logic and operational seman- tics. Electronic Notes in Theoretical Computer Science 276, 335–351 (2011). https://doi.org/https://doi.org/10.1016/j.entcs.2011.09.029, https://www.sciencedirect.com/science/article/pii/S1571066111001204, twenty-seventh Conference on the Mathematical Foundations of Programming Semantics (M...

    work page doi:10.1016/j.entcs.2011.09.029 2011

  38. [38]

    In: Majumdar, R., Kunčak, V

    Vafeiadis, V.: Program verification under weak memory consistency using separa- tion logic. In: Majumdar, R., Kunčak, V. (eds.) Computer Aided Verification. pp. 30–46. Springer International Publishing, Cham (2017)

    work page 2017

  39. [39]

    In: Proceedings of the 2013 ACM SIGPLAN international conference on Object oriented programming systems languages & applications

    Vafeiadis, V., Narayan, C.: Relaxed separation logic: A program logic for c11 con- currency. In: Proceedings of the 2013 ACM SIGPLAN international conference on Object oriented programming systems languages & applications. pp. 867–884 (2013) 22 Ö. Şakar et al. 1 a_V x = new a_V(N); 2 invariant inv( /*@ Global invariant 3 Perm(x.G[*], 1\2) ** 4 Perm(x.L[*]...

    work page 2013

  40. [40]

    The call toload updates the local view

    rmw fail: When the operation fails, the global view oft does not change (l.5). The call toload updates the local view. The return value ofload cannot be equivalent tooldVal (l.6). Finally, a description ofnewLV can be given (l.7). The predicatedescriptionFail is a placeholder and is to be defined by the user to use in further proofs. It can be used to exc...

    work page

  41. [41]

    In addition to this, a tokenCASSuccess is given to signify that the operation has succeeded (l.13)

    rmw success: The newLV is specified to have changed similarly to thestore method’s contract. In addition to this, a tokenCASSuccess is given to signify that the operation has succeeded (l.13). This token captures the state that oldValisreadfrom.Thetokenisusedtoexcludemultipleoperationsreading from the same write. Again, a description ofnewLV can be given ...

    work page