developing and verifying relaxed and release-acquire versions of these more
sophisticated algorithms. We leave such studies for future work.

###### Acknowledgements.

The authors would also like to thank the anonymous referees for their valuable
comments and helpful suggestions. Dalvandi and Dongol are supported by Sponsor
EPSRC https://epsrc.ukri.org/ Grant Grant #EP/R032556/1. Dongol is
additionally supported by Sponsor EPSRC https://epsrc.ukri.org/ Grant Grant
#EP/V038915/1, Sponsor EPSRC https://epsrc.ukri.org/ Grant Grant
#EP/R025134/2, Sponsor ARC https://www.arc.gov.au/ Grant Grant #DP190102142
and VeTSS.

## References

  * (1)
  * Abdulla et al. (2019) P. A. Abdulla, J. Arora, M. F. Atig, and S. N. Krishna. 2019\.  Verification of programs under the release-acquire semantics. In _PLDI_ , K. S. McKinley and K. Fisher (Eds.). ACM, 1117–1132.  https://doi.org/10.1145/3314221.3314649
  * Alglave and Cousot (2017) J. Alglave and P. Cousot. 2017.  Ogre and Pythia: an invariance proof method for weak consistency models. In _POPL_ , G. Castagna and A. D. Gordon (Eds.). ACM, 3–18.
  * Alglave et al. (2014) J. Alglave, L. Maranget, and M. Tautschnig. 2014.  Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory.  _ACM Trans. Program. Lang. Syst._ 36, 2 (2014), 7:1–7:74.
  * Armstrong and Dongol (2017) A. Armstrong and B. Dongol. 2017.  Modularising Opacity Verification for Hybrid Transactional Memory. In _FORTE_ _(LNCS, Vol. 10321)_ , A. Bouajjani and A. Silva (Eds.). Springer, 33–49.
  * Armstrong et al. (2017) A. Armstrong, B. Dongol, and S. Doherty. 2017.  Proving Opacity via Linearizability: A Sound and Complete Method. In _FORTE_ _(LNCS, Vol. 10321)_ , A. Bouajjani and A. Silva (Eds.). Springer, 50–66.
  * Assa et al. (2020) G. Assa, H. Meir, G. Golan-Gueta, I. Keidar, and A. Spiegelman. 2020.  Nesting and composition in transactional data structure libraries. In _PPoPP ’20_ , R. Gupta and X. Shen (Eds.). ACM, 405–406.  https://doi.org/10.1145/3332466.3374514
  * Assa et al. (2021) G. Assa, H. Meir, G. Golan-Gueta, I. Keidar, and A. Spiegelman. 2021.  Using Nesting to Push the Limits of Transactional Data Structure Libraries. In _OPODIS_ _(LIPIcs, Vol. 217)_ , Q. Bramas, V. Gramoli, and A. Milani (Eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 30:1–30:17.  https://doi.org/10.4230/LIPIcs.OPODIS.2021.30
  * Attiya et al. (2018) H. Attiya, A. Gotsman, S. Hans, and N. Rinetzky. 2018\.  Characterizing Transactional Memory Consistency Conditions Using Observational Refinement.  _J. ACM_ 65, 1 (2018), 2:1–2:44.
  * Batty et al. (2016) M. Batty, A. F. Donaldson, and J. Wickerson. 2016\.  Overhauling SC atomics in C11 and OpenCL. In _POPL_. ACM, 634–648.
  * Batty et al. (2011) M. Batty, S. Owens, S. Sarkar, P. Sewell, and T. Weber. 2011.  Mathematizing C++ concurrency. In _POPL_ , T. Ball and M. Sagiv (Eds.). ACM, 55–66.
  * Beillahi et al. (2021a) S. M. Beillahi, A. Bouajjani, and C. Enea. 2021a.  Checking Robustness Between Weak Transactional Consistency Models. In _ESOP_ _(LNCS, Vol. 12648)_ , N. Yoshida (Ed.). Springer, 87–117.  https://doi.org/10.1007/978-3-030-72019-3_4
  * Beillahi et al. (2021b) S. M. Beillahi, A. Bouajjani, and C. Enea. 2021b.  Robustness Against Transactional Causal Consistency.  _Log. Methods Comput. Sci._ 17, 1 (2021).  https://lmcs.episciences.org/7149
  * Bila et al. (2022) E. Vafeiadi Bila, B. Dongol, O. Lahav, A. Raad, and J. Wickerson. 2022.  View-Based Owicki-Gries Reasoning for Persistent x86-TSO. In _ESOP_ _(Lecture Notes in Computer Science, Vol. 13240)_ , I. Sergey (Ed.). Springer, 234–261.  https://doi.org/10.1007/978-3-030-99336-8_9
  * Böhme and Nipkow (2010) S. Böhme and T. Nipkow. 2010.  Sledgehammer: Judgement Day. In _IJCAR_ _(LNCS, Vol. 6173)_. Springer, 107–121.
  * Bronson et al. (2010) N. G. Bronson, J. Casper, H. Chafi, and K. Olukotun. 2010\.  Transactional predication: high-performance concurrent sets and maps for STM. In _PODC_ , A. W. Richa and R. Guerraoui (Eds.). ACM, 6–15.  https://doi.org/10.1145/1835698.1835703
  * Chong et al. (2018) N. Chong, T. Sorensen, and J. Wickerson. 2018.  The semantics of transactions and weak memory in x86, Power, ARM, and C++. In _PLDI_ , J. S. Foster and D. Grossman (Eds.). ACM, 211–225.  https://doi.org/10.1145/3192366.3192373
  * cppreference.com (2022) cppreference.com. 2022\.  std::atomic_compare_exchange.  https://en.cppreference.com/w/cpp/atomic/atomic_compare_exchange Accessed 18 July, 2022.
  * Dalessandro et al. (2010) L. Dalessandro, D. Dice, M. L. Scott, N. Shavit, and M. F. Spear. 2010.  Transactional Mutex Locks. In _Euro-Par (2)_ _(LNCS, Vol. 6272)_. Springer, 2–13.
  * Dalvandi et al. (2020a) S. Dalvandi, S. Doherty, B. Dongol, and H. Wehrheim. 2020a.  Owicki-Gries Reasoning for C11 RAR. In _ECOOP_ _(LIPIcs, Vol. 166)_ , R. Hirschfeld and T. Pape (Eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 11:1–11:26.  https://doi.org/10.4230/LIPIcs.ECOOP.2020.11
  * Dalvandi et al. (2020b) S. Dalvandi, S. Doherty, B. Dongol, and H. Wehrheim. 2020b.  Owicki-Gries Reasoning for C11 RAR (Artifact).  _Dagstuhl Artifacts Ser._ 6, 2 (2020), 15:1–15:2.  https://doi.org/10.4230/DARTS.6.2.15
  * Dalvandi and Dongol (2021) S. Dalvandi and B. Dongol. 2021.  Verifying C11-style weak memory libraries. In _PPoPP_ , J. Lee and E. Petrank (Eds.). ACM, 451–453.  https://doi.org/10.1145/3437801.3441619
  * Dalvandi and Dongol (2022) S. Dalvandi and B. Dongol. 2022.  _Implementing and Verifying Release-Acquire Transactional Memory (Artifact)_.  https://doi.org/10.5281/zenodo.6899919
  * Dalvandi et al. (2022) S. Dalvandi, B. Dongol, S. Doherty, and H. Wehrheim. 2022\.  Integrating Owicki-Gries for C11-Style Memory Models into Isabelle/HOL.  _J. Autom. Reason._ 66, 1 (2022), 141–171.  https://doi.org/10.1007/s10817-021-09610-2
  * Dang et al. (2022) H.-H. Dang, J. Jung, J. Choi, D.-T. Nguyen, W. Mansky, J. Kang, and D. Dreyer. 2022.  Compass: strong and compositional library specifications in relaxed memory separation logic. In _PLDI_ , R. Jhala and I. Dillig (Eds.). ACM, 792–808.  https://doi.org/10.1145/3519939.3523451
  * de Roever and Engelhardt (1998) W. P. de Roever and K. Engelhardt. 1998.  _Data Refinement: Model-oriented Proof Theories and their Comparison_. Cambridge Tracts in Theoretical Computer Science, Vol. 46.  Cambridge University Press.
  * Derrick et al. (2018) J. Derrick, S. Doherty, B. Dongol, G. Schellhorn, O. Travkin, and H. Wehrheim. 2018\.  Mechanized proofs of opacity: a comparison of two techniques.  _Formal Aspects Comput._ 30, 5 (2018), 597–625.  https://doi.org/10.1007/s00165-017-0433-3
  * Dice et al. (2006) D. Dice, O. Shalev, and N. Shavit. 2006.  Transactional Locking II. In _DISC_ _(Lecture Notes in Computer Science, Vol. 4167)_ , S. Dolev (Ed.). Springer, 194–208.  https://doi.org/10.1007/11864219_14
  * Doherty et al. (2016) S. Doherty, B. Dongol, J. Derrick, G. Schellhorn, and H. Wehrheim. 2016.  Proving Opacity of a Pessimistic STM. In _OPODIS_ _(LIPIcs, Vol. 70)_ , P. Fatourou, E. Jiménez, and F. Pedone (Eds.). Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 35:1–35:17.
  * Doherty et al. (2018) S. Doherty, B. Dongol, H. Wehrheim, and J. Derrick. 2018\.  Making Linearizability Compositional for Partially Ordered Executions. In _iFM_ _(LNCS, Vol. 11023)_ , C. A. Furia and K. Winter (Eds.). Springer, 110–129.  https://doi.org/10.1007/978-3-319-98938-9_7
  * Doherty et al. (2019) S. Doherty, B. Dongol, H. Wehrheim, and J. Derrick. 2019\.  Verifying C11 programs operationally. In _PPoPP_ , Jeffrey K. Hollingsworth and Idit Keidar (Eds.). ACM, 355–365.
  * Doherty et al. (2013) S. Doherty, L. Groves, V. Luchangco, and M. Moir. 2013\.  Towards formally specifying and verifying transactional memory.  _Formal Asp. Comput._ 25, 5 (2013), 769–799.
  * Doko and Vafeiadis (2017) M. Doko and V. Vafeiadis. 2017.  Tackling Real-Life Relaxed Concurrency with FSL++. In _ESOP_. 448–475.
  * Dolan et al. (2018) S. Dolan, KC Sivaramakrishnan, and A. Madhavapeddy. 2018\.  Bounding Data Races in Space and Time. In _PLDI_ (Philadelphia, PA, USA) _(PLDI 2018)_. ACM, New York, NY, USA, 242–255.
  * Dongol and Groves (2016) B. Dongol and L. Groves. 2016.  Contextual Trace Refinement for Concurrent Objects: Safety and Progress. In _ICFEM_ _(Lecture Notes in Computer Science, Vol. 10009)_ , K. Ogata, M. Lawford, and S. Liu (Eds.). 261–278.  https://doi.org/10.1007/978-3-319-47846-3_17
  * Dongol et al. (2018a) B. Dongol, R. Jagadeesan, and J. Riely. 2018a.  Transactions in relaxed memory architectures.  _PACMPL_ 2, POPL (2018), 18:1–18:29.
  * Dongol et al. (2019) B. Dongol, R. Jagadeesan, and J. Riely. 2019.  Modular transactions: bounding mixed races in space and time. In _PPoPP_ , J. K. Hollingsworth and I. Keidar (Eds.). ACM, 82–93.  https://doi.org/10.1145/3293883.3295708
  * Dongol et al. (2018b) B. Dongol, R. Jagadeesan, J. Riely, and A. Armstrong. 2018b.  On abstraction and compositionality for weak-memory linearisability. In _VMCAI_ _(LNCS, Vol. 10747)_. Springer, 183–204.
  * Emmi and Enea (2019) M. Emmi and C. Enea. 2019\.  Weak-consistency specification via visibility relaxation.  _Proc. ACM Program. Lang._ 3, POPL (2019), 60:1–60:28.  https://doi.org/10.1145/3290373
  * Gotsman and Yang (2011) A. Gotsman and H. Yang. 2011.  Liveness-Preserving Atomicity Abstraction. In _ICALP_ _(Lecture Notes in Computer Science, Vol. 6756)_ , L. Aceto, M. Henzinger, and J. Sgall (Eds.). Springer, 453–465.  https://doi.org/10.1007/978-3-642-22012-8_36
  * Guerraoui and Kapalka (2010) R. Guerraoui and M. Kapalka. 2010.  _Principles of Transactional Memory_.  Morgan & Claypool Publishers.
  * He et al. (2016) M. He, V. Vafeiadis, S. Qin, and J. F. Ferreira. 2016\.  Reasoning about Fences and Relaxed Atomics. In _PDP_. IEEE Computer Society, 520–527.
  * Herlihy and Moss (1993) M. Herlihy and J. E. B. Moss. 1993.  Transactional Memory: Architectural Support for Lock-Free Data Structures. In _ISCA_ , A. J. Smith (Ed.). ACM, 289–300.
  * Herlihy and Wing (1990) M. Herlihy and J. M. Wing. 1990.  Linearizability: A Correctness Condition for Concurrent Objects.  _ACM TOPLAS_ 12, 3 (1990), 463–492.
  * Jagadeesan et al. (2020) R. Jagadeesan, A. Jeffrey, and J. Riely. 2020.  Pomsets with preconditions: a simple model of relaxed memory.  _Proc. ACM Program. Lang._ 4, OOPSLA (2020), 194:1–194:30.  https://doi.org/10.1145/3428262
  * Kaiser et al. (2017) J.-O. Kaiser, H.-H. Dang, D. D., O. Lahav, and V. Vafeiadis. 2017.  Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris. In _ECOOP_ _(LIPIcs, Vol. 74)_ , P. Müller (Ed.). Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 17:1–17:29.
  * Kang et al. (2017) J. Kang, C.-K. Hur, O. Lahav, V. Vafeiadis, and D. Dreyer. 2017.  A promising semantics for relaxed-memory concurrency. In _POPL_. ACM, 175–189.
  * Khyzha and Lahav (2022) A. Khyzha and O. Lahav. 2022.  Abstraction for Crash-Resilient Objects. In _ESOP_ _(Lecture Notes in Computer Science, Vol. 13240)_ , Ilya Sergey (Ed.). Springer, 262–289.  https://doi.org/10.1007/978-3-030-99336-8_10
  * Kokologiannakis et al. (2019) M. Kokologiannakis, A. Raad, and V. Vafeiadis. 2019\.  Model checking for weakly consistent libraries. In _PLDI_ , K. S. McKinley and K. Fisher (Eds.). ACM, 96–110.  https://doi.org/10.1145/3314221.3314609
  * Krishna et al. (2020) S. Krishna, M. Emmi, C. Enea, and D. Jovanovic. 2020\.  Verifying Visibility-Based Weak Consistency. In _ESOP_ _(LNCS, Vol. 12075)_ , P. Müller (Ed.). Springer, 280–307.  https://doi.org/10.1007/978-3-030-44914-8_11
  * Lahav et al. (2021) O. Lahav, E. Namakonov, J. Oberhauser, A. Podkopaev, and V. Vafeiadis. 2021.  Making weak memory models fair.  _Proc. ACM Program. Lang._ 5, OOPSLA (2021), 1–27.  https://doi.org/10.1145/3485475
  * Lahav and Vafeiadis (2015) O. Lahav and V. Vafeiadis. 2015.  Owicki-Gries Reasoning for Weak Memory Models. In _ICALP_ _(LNCS, Vol. 9135)_ , M. M. Halldórsson, K. Iwama, N. Kobayashi, and B. Speckmann (Eds.). Springer, 311–323.
  * Lahav et al. (2017) O. Lahav, V. Vafeiadis, J. Kang, C.-K. Hur, and D. Dreyer. 2017.  Repairing sequential consistency in C/C++11. In _PLDI_. ACM, 618–632.
  * Lamport (1979) L. Lamport. 1979\.  How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs.  _IEEE Trans. Computers_ 28, 9 (1979), 690–691.
  * Lee et al. (2020) S.-H. Lee, M. Cho, A. Podkopaev, S. Chakraborty, C.-K. Hur, O. Lahav, and V. Vafeiadis. 2020.  Promising 2.0: global optimizations in relaxed memory concurrency. In _PLDI_ , A. F. Donaldson and E. Torlak (Eds.). ACM, 362–376.  https://doi.org/10.1145/3385412.3386010
  * Lesani et al. (2012) M. Lesani, V. Luchangco, and M. Moir. 2012.  Putting Opacity in Its Place. In _WTTM_.
  * Lesani et al. (2022) M. Lesani, L. Xia, A. Kaseorg, C. J. Bell, A. Chlipala, B. C. Pierce, and S. Zdancewic. 2022.  C4: verified transactional objects.  _Proc. ACM Program. Lang._ 6, OOPSLA (2022), 1–31.  https://doi.org/10.1145/3527324
  * Lynch (1996) N. A. Lynch. 1996\.  _Distributed Algorithms_.  Morgan Kaufmann.
  * Margalit and Lahav (2021) R. Margalit and O. Lahav. 2021.  Verifying Observational Robustness against a C11-Style Memory Model.  _Proc. ACM Program. Lang._ 5, POPL, Article 4 (Jan. 2021), 33 pages.  https://doi.org/10.1145/3434285
  * Matveev and Shavit (2015) A. Matveev and N. Shavit. 2015.  Reduced Hardware NOrec: A Safe and Scalable Hybrid Transactional Memory. In _ASPLOS_ , Ö. Ö., K. Ebcioglu, and S. Dwarkadas (Eds.). ACM, 59–71.  https://doi.org/10.1145/2694344.2694393
  * Minh et al. (2008) C. C. Minh, J. Chung, C. Kozyrakis, and K. Olukotun. 2008\.  STAMP: Stanford Transactional Applications for Multi-Processing. In _IISWC_ , D. Christie, A. Lee, O. Mutlu, and B. G. Zorn (Eds.). IEEE Computer Society, 35–46.  https://doi.org/10.1109/IISWC.2008.4636089
  * Owicki and Gries (1976) S. S. Owicki and D. Gries. 1976.  An Axiomatic Proof Technique for Parallel Programs I.  _Acta Inf._ 6 (1976), 319–340.
  * Paviotti et al. (2020) M. Paviotti, S. Cooksey, A. Paradis, D. Wright, S. Owens, and M. Batty. 2020\.  Modular Relaxed Dependencies in Weak Memory Concurrency. In _ESOP_ _(LNCS, Vol. 12075)_ , P. Müller (Ed.). Springer, 599–625.  https://doi.org/10.1007/978-3-030-44914-8_22
  * Podkopaev et al. (2016) A. Podkopaev, I. Sergey, and A. Nanevski. 2016.  Operational Aspects of C/C++ Concurrency.  _CoRR_ abs/1606.01400 (2016).  arXiv:1606.01400
  * Raad et al. (2019a) A. Raad, M. Doko, L. Rozic, O. Lahav, and V. Vafeiadis. 2019a.  On library correctness under weak memory consistency: specifying and verifying concurrent libraries under declarative consistency models.  _Proc. ACM Program. Lang._ 3, POPL (2019), 68:1–68:31.  https://doi.org/10.1145/3290381
  * Raad et al. (2018) A. Raad, O. Lahav, and V. Vafeiadis. 2018.  On Parallel Snapshot Isolation and Release/Acquire Consistency. In _ESOP_ _(LNCS, Vol. 10801)_ , A. Ahmed (Ed.). Springer, 940–967.  https://doi.org/10.1007/978-3-319-89884-1_33
  * Raad et al. (2019b) A. Raad, O. Lahav, and V. Vafeiadis. 2019b.  On the Semantics of Snapshot Isolation. In _VMCAI_ _(LNCS, Vol. 11388)_ , C. Enea and R. Piskac (Eds.). Springer, 1–23.  https://doi.org/10.1007/978-3-030-11245-5_1
  * Rodriguez and Spear (2020) M. Rodriguez and M. F. Spear. 2020.  Brief Announcement: On Implementing Software Transactional Memory in the C++ Memory Model. In _PODC_ , Y. Emek and C. Cachin (Eds.). ACM, 224–226.  https://doi.org/10.1145/3382734.3405746
  * Scargall (2020) S. Scargall. 2020\.  _Programming Persistent Memory: A Comprehensive Guide for Developers_.  APress.  https://doi.org/10.1007/978-1-4842-4932-1_8
  * Sela et al. (2021) G. Sela, M. Herlihy, and E. Petrank. 2021.  Brief Announcement: Linearizability: A Typo. In _PODC_ , A. Miller, K. Censor-Hillel, and J. H. Korhonen (Eds.). ACM, 561–564.  https://doi.org/10.1145/3465084.3467944
  * Shavit and Touitou (1997) N. Shavit and D. Touitou. 1997.  Software Transactional Memory.  _Distributed Computing_ 10, 2 (1997), 99–116.
  * Spear et al. (2020) M. Spear, H. Boehm, V. Luchangco, M. L. Scott, and M. Wong. 2020.  _Transactional Memory Lite Support in C++_.  Technical Report. isocpp.
  * Summers and Müller (2018) A. J. Summers and P. Müller. 2018.  Automating Deductive Verification for Weak-Memory Programs. In _TACAS_ _(LNCS, Vol. 10805)_ , D. Beyer and M. Huisman (Eds.). Springer, 190–209.
  * Svendsen et al. (2018) K. Svendsen, J. Pichon-Pharabod, M. Doko, O. Lahav, and V. Vafeiadis. 2018.  A Separation Logic for a Promising Semantics. In _ESOP_ _(LNCS, Vol. 10801)_ , A. Ahmed (Ed.). Springer, 357–384.
  * Tassarotti et al. (2015) J. Tassarotti, D. Dreyer, and V. Vafeiadis. 2015.  Verifying read-copy-update in a logic for weak memory. In _PLDI_ , D. Grove and S. Blackburn (Eds.). ACM, 110–120.  https://doi.org/10.1145/2737924.2737992
  * Turon et al. (2014) A. Turon, V. Vafeiadis, and D. Dreyer. 2014.  GPS: navigating weak memory with ghosts, protocols, and separation. In _OOPSLA_ , A. P. Black and T. D. Millstein (Eds.). ACM, 691–707.
  * Vafeiadis and Narayan (2013) V. Vafeiadis and C. Narayan. 2013.  Relaxed separation logic: A program logic for C11 concurrency. In _OOPSLA_. 867–884.
  * Wright et al. (2021) D. Wright, M. Batty, and B. Dongol. 2021.  Owicki-Gries Reasoning for C11 Programs with Relaxed Dependencies.  13047 (2021), 237–254.  https://doi.org/10.1007/978-3-030-90870-6_13
  * Xiong et al. (2020) S. Xiong, A. Cerone, A. Raad, and P. Gardner. 2020\.  Data Consistency in Transactional Storage Systems: A Centralised Semantics. In _ECOOP_ _(LIPIcs, Vol. 166)_ , R. Hirschfeld and T. Pape (Eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 21:1–21:31.  https://doi.org/10.4230/LIPIcs.ECOOP.2020.21
  * Zardoshti et al. (2019) P. Zardoshti, T. Zhou, P. Balaji, M. L. Scott, and M. F. Spear. 2019.  Simplifying Transactional Memory Support in C++.  _ACM Trans. Archit. Code Optim._ 16, 3 (2019), 25:1–25:24.  https://doi.org/10.1145/3328796

$\inference[{\sc Read}]{a\in\\{rd(x,v),rd^{\mathsf{A}}(x,v)\\}\qquad
w\in\gamma.{\it OW}_{\tau}(x)\qquad{\sf val}(w)=v\\\ {\tt
tview}^{\prime}=\textsf{{if}}\ \gamma.{\tt rel}(w)\wedge
a=rd^{\mathsf{A}}(x,v)\ \textsf{{then}}\ \gamma.{\tt
tview}_{\tau}\otimes\gamma.{\tt mview}_{w}\ \textsf{{else}}\ \gamma.{\tt
tview}_{\tau}[x:=w]}{\gamma\ \mathrel{\raisebox{0.90005pt}{ \\!\\!\\!\\!
\leavevmode\hbox to8.32pt{\vbox to7.84pt{\pgfpicture\makeatletter\hbox{\hskip
4.15819pt\lower-4.54938pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.66505pt}{-1.35625pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\scriptstyle a$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}}{}{{}}{}{{}} {}{}
{}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}} }{{{{}{}{{}}
}}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {{}} } {{{{}{}{{}} }}{{}}{{}}}
\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.71132pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{3.14796pt}{-3.49373pt}\pgfsys@lineto{-0.19746pt}{-3.49373pt}\pgfsys@lineto{-1.05104pt}{-4.19373pt}\pgfsys@lineto{-2.75821pt}{-2.79373pt}\pgfsys@lineto{-3.80254pt}{-3.49373pt}\pgfsys@lineto{-3.80254pt}{-3.49373pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.14796pt}{-3.49373pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}_{\tau}\ \gamma[{\tt
tview}_{\tau}:={\tt tview}^{\prime}]}$

$\inference[{\sc Write}]{a\in\\{wr(x,v),wr^{\sf R}(x,v)\\}\qquad{\it
w}\in\gamma.{\it
OW}_{\tau}(x)\setminus\gamma.\mathtt{cvd}\qquad\mathit{fresh}_{\gamma}(x,q)\qquad{\sf
tst}(w)<q\\\
\mathtt{writes}^{\prime}=\gamma.\mathtt{writes}\cup\\{(x,v,q)\\}\qquad{\tt
tview}^{\prime}=\gamma.{\tt tview}_{\tau}[x:=(x,v,q)]\qquad b=(a=wr^{\sf
R}(x,v))}{\gamma\ \mathrel{\raisebox{0.90005pt}{ \\!\\!\\!\\! \leavevmode\hbox
to8.32pt{\vbox to7.84pt{\pgfpicture\makeatletter\hbox{\hskip
4.15819pt\lower-4.54938pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.66505pt}{-1.35625pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\scriptstyle a$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}}{}{{}}{}{{}} {}{}
{}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}} }{{{{}{}{{}}
}}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {{}} } {{{{}{}{{}} }}{{}}{{}}}
\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.71132pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{3.14796pt}{-3.49373pt}\pgfsys@lineto{-0.19746pt}{-3.49373pt}\pgfsys@lineto{-1.05104pt}{-4.19373pt}\pgfsys@lineto{-2.75821pt}{-2.79373pt}\pgfsys@lineto{-3.80254pt}{-3.49373pt}\pgfsys@lineto{-3.80254pt}{-3.49373pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.14796pt}{-3.49373pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}_{\tau}\ \gamma[{\tt
tview}_{\tau}:={\tt tview}^{\prime},{\tt mview}_{(x,v,q)}:={\tt
tview}^{\prime},\mathtt{writes}:=\mathtt{writes}^{\prime},{\tt
rel}:=\gamma.{\tt rel}[w:=b]]}$

$\inference[{\sc RMW-RA}]{a=rmw^{\sf RA}(x,u,v)\qquad{\it w}\in\gamma.{\it
OW}_{\tau}(x)\setminus\gamma.\mathtt{cvd}\qquad{\sf val}({\it
w})=u\qquad\mathit{fresh}_{\gamma}(x,q)\qquad{\sf tst}(w)<q\\\
\mathtt{writes}^{\prime}=\gamma.\mathtt{writes}\cup\\{(x,v,q)\\}\qquad\mathtt{cvd}^{\prime}=\gamma.\mathtt{cvd}\cup\\{(x,v,q)\\}\\\
{\tt tview}^{\prime}=\textsf{{if}}\ \gamma.{\tt rel}(w)\ \textsf{{then}}\
\gamma.{\tt tview}_{\tau}[x:=(x,v,q)]\otimes\gamma.{\tt mview}_{w}\
\textsf{{else}}\ \gamma.{\tt tview}_{\tau}[x:=(x,v,q)]}{\gamma\
\mathrel{\raisebox{0.90005pt}{ \\!\\!\\!\\! \leavevmode\hbox to8.32pt{\vbox
to7.84pt{\pgfpicture\makeatletter\hbox{\hskip 4.15819pt\lower-4.54938pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.66505pt}{-1.35625pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\scriptstyle a$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}}{}{{}}{}{{}} {}{}
{}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}} }{{{{}{}{{}}
}}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {{}} } {{{{}{}{{}} }}{{}}{{}}}
\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.71132pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{3.14796pt}{-3.49373pt}\pgfsys@lineto{-0.19746pt}{-3.49373pt}\pgfsys@lineto{-1.05104pt}{-4.19373pt}\pgfsys@lineto{-2.75821pt}{-2.79373pt}\pgfsys@lineto{-3.80254pt}{-3.49373pt}\pgfsys@lineto{-3.80254pt}{-3.49373pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.14796pt}{-3.49373pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}_{t}\
\gamma\left[\begin{array}[c]{@{}l@{}}{\tt tview}_{\tau}:={\tt
tview}^{\prime},{\tt mview}_{(x,v,q)}:={\tt tview}^{\prime},\\\
\mathtt{writes}:=\mathtt{writes}^{\prime},\mathtt{cvd}:=\mathtt{cvd}^{\prime},{\tt
rel}:=\gamma.{\tt rel}[(x,v,{\it q}):={\it true}]\end{array}\right]}$

Figure 11. Memory semantics for reads, writes and updates, where
$\mathit{fresh}_{\gamma}(x,q)$ holds iff there is no write in
$\gamma.\mathtt{writes}$ on $x$ with timestamp $q$, i.e.,
$(x,\\_,q)\notin\gamma.\mathtt{writes}$

Memory semantics for reads, writes and updates

##  Appendix A RC11 RAR Operational Semantics

We now briefly review the C11 operational semantics (introduced by (Dalvandi
et al., 2020a)) used in our framework.

##### Component State

Here we detail the C11 state as modelled by the operational semantics. The
first state component is $\mathtt{writes}$ which is the set of all global
writes to shared locations. Each global write is represented by a tuple
$(x,v,q)$, where $x$ is a shared location, $q$ is a rational number used as a
timestamp, and $v$ is the value written by the global write. The writes to
each variable are totally ordered by timestamps.

For any write $w=(x,v,q)$, we have $\mathtt{var}(w)=x$, $\mathtt{tst}(w)=q$
and $\mathtt{val}(w)=v$. The state needs to record the writes that are
observable by each thread. A function ${\tt tview}_{t}$ is included in the
state to record the viewfront of thread $t$ (i.e. the latest write that a
thread has seen so far). All the writes with a timestamp greater than or equal
to the timestamp of the viewfront of thread $t$ are $observable$ by the
thread. Another component of the state is a function ${\tt mview}_{w}$ that
records the viewfront of write $w$, which is set to be the viewfront of the
thread that executed $w$ at the time of $w$’s execution. ${\tt mview}_{w}$ is
used to compute a new value for ${\tt tview}_{t}$ if a thread $t$ synchronizes
with $w$. The state also must record If a global write is $releasing$. This is
recorded by a function ${\tt rel}_{w}$ which returns ${\it true}$ if $w$ is
releasing or ${\it false}$ otherwise. Finally, the state maintains a variable
$\mathtt{cvd}\subseteq\mathtt{writes}$. The semantics assumes that each update
action occurs in the modification order immediately after the write that it
reads from to preserve the atomicity of updates. To prevent any newer write to
intervene between any update and the write that it reads from, we add all the
writes read by an update operation to the the covered set $\mathtt{cvd}$ so
newer writes should never interact with covered writes.

##### Initialisation

The initial state $\gamma^{\mathbf{Init}}$ is defined as follows.

$\displaystyle\gamma^{\mathbf{Init}}.\mathtt{writes}$
$\displaystyle\mathrel{\hat{=}}\\{(x,0,0)\mid x\in{\it Loc}\\}$
$\displaystyle\gamma^{\mathbf{Init}}.\mathtt{cvd}$
$\displaystyle\mathrel{\hat{=}}\emptyset$
$\displaystyle\gamma^{\mathbf{Init}}.{\tt rel}$
$\displaystyle\mathrel{\hat{=}}\lambda(x,0,0).\,{\it false}$
$\displaystyle\gamma^{\mathbf{Init}}.{\tt tview}_{\tau}$
$\displaystyle\mathrel{\hat{=}}\lambda x\in{\it Loc}.\,(x,0,0)$
$\displaystyle\gamma^{\mathbf{Init}}.{\tt mview}_{w}$
$\displaystyle\mathrel{\hat{=}}\lambda x\in{\it Loc}.\,(x,0,0)$

##### Transition semantics.

The transition relation of our semantics for global reads and writes is given
in Fig. 11 (Dalvandi et al., 2020a).

#####  Read transition by thread $\tau$.

Assume that $a$ is either a relaxed or acquiring read to variable $x$, $w$ is
a write to $x$ that $t$ can observe (i.e., $(w,q,v)\in\gamma.{\it
OW}_{\tau}(x)$), and the value read by $a$ is the value written by $w$. Each
read causes the viewfront of $t$ to be updated. For an unsynchronised read,
${\tt tview}_{t}$ is simply updated to include the new write. A synchronised
read causes the executing thread’s view of the executing component and context
to be updated. In particular, for each variable $x$, the new view of $x$ will
be the later (in timestamp order) of either ${\tt tview}_{t}(x)$ or ${\tt
mview}_{w}(x)$.

#####  Write transition by thread $t$.

A write transition must identify the write $(w,v,q)$ after which $a$ occurs.
This $w$ must be observable and must not be covered — the second condition
preserves the atomicity of read-modify-write (RMW) updates. We must choose a
fresh timestamp $q^{\prime}\in\mathbb{Q}$ for $a$, which for a C11 state
$\gamma$ is formalised by
$\mathit{fresh}_{\gamma}(q,q^{\prime})=q<q^{\prime}\wedge\forall
w^{\prime}\in\gamma.\mathtt{writes}.\ q<\mathtt{tst}(w^{\prime})\Rightarrow
q^{\prime}<\mathtt{tst}(w^{\prime})$. That is, $q^{\prime}$ is a new timestamp
for variable $x$ and that $(a,q^{\prime},v^{\prime})$ occurs immediately after
$(w,v,q)$. The new write is added to the set $\mathtt{writes}$.

We update $\gamma.{\tt tview}_{t}$ to include the new write, which ensures
that $t$ can no longer observe any writes prior to
$(a,v^{\prime},q^{\prime})$. Moreover, we set the viewfront of
$(a,v^{\prime},q^{\prime})$ to be the new viewfront of $t$ in $\gamma$
together with the thread viewfront of the environment state $\beta$. If some
other thread synchronises with this new write in some later transition, that
thread’s view will become at least as recent as $t$’s view at this transition.
Since ${\tt mview}$ keeps track of the executing thread’s view of both the
component being executed and its context, any synchronisation through this new
write will update views across components.

#####  Update (aka RMW) transition by thread $t$.

These transitions are best understood as a combination of the read and write
transitions. As with a write transition, we must choose a valid fresh
timestamp $q^{\prime}$, and the state component $\mathtt{writes}$ is updated
in the same way. State component ${\tt mview}$ includes information from the
new view of the executing thread $t$. As discussed earlier, in Update
transitions it is necessary to record that the write that the update interacts
with is now covered, which is achieved by adding that write to $\mathtt{cvd}$.
Finally, we must compute a new thread view, which is similar to a Read
transition, except that the thread’s new view always includes the new write
introduced by the update.

##  Appendix B TMS2-RA Operational Semantics

This section presents further details of the operational semantics from §3.3
of TMS2-RA as formalised in our Isabelle/HOL development.

##### Component State

Here we present the transactional state of TMS2-RA which builds on the earlier
semantics of TMS2 (Doherty et al., 2013). The state space of TMS2-RA extends
the state space of TMS2 and comprises several components. The first component
is $\mathit{M}$ which is a sequence that keeps track of memory snapshots
(memory states). The status of each transaction $t$ is stored in
$\mathtt{status}_{t}$ which can have any of the following values: ${\tt
NOTSTARTED}$, ${\tt READY}$, ${\tt COMMITTED}$, ${\tt ABORTED}$. Each
transaction $t$ also has a write set ($\mathtt{wrSet}_{t}$) and a read set
($\mathtt{rdSet}_{t}$) where the writes and reads performed by the transaction
are stored. For each transaction $t$ there is also a $\mathtt{beginIdx}_{t}$
variable which is set to the most recent memory version when the transaction
begins. We extend the TMS2 state space with a number of new components. The
$\mathtt{seenIdxs}_{t}$ variable stores the memory version of all the reads
performed by the transaction. $\mathtt{V}_{i}$ is the memory modification view
of a stored memory $i$ ($0\leq i\leq|\mathit{M}|-1$). Memory modification view
of memory $i$ is an snapshot of the transaction’s client thread view at the
time of commiting taht memory. $\mathit{S}_{i}$ indicates that if the
transaction that committed memory version $i$ was releasing.

##### Initialisation

The initial state $\gamma^{\mathbf{Init}}$ is defined as follows:

$\displaystyle\gamma^{\mathbf{Init}}.\mathit{M}$
$\displaystyle\mathrel{\hat{=}}\langle(\lambda l\in Loc.~{}0)\rangle$
$\displaystyle\gamma^{\mathbf{Init}}.V$
$\displaystyle\mathrel{\hat{=}}\langle(\lambda l\in Loc.\ \ \
~{}\beta^{\mathbf{Init}}.{\tt tview}_{t}(l))\rangle$
$\displaystyle\gamma^{\mathbf{Init}}.\mathit{S}$
$\displaystyle\mathrel{\hat{=}}\langle{\it false}\rangle$
$\displaystyle\gamma^{\mathbf{Init}}.\mathtt{status}_{t}$
$\displaystyle\mathrel{\hat{=}}{\tt NOTSTARTED}$
$\displaystyle\gamma^{\mathbf{Init}}.\mathtt{rdSet}_{t}$
$\displaystyle\mathrel{\hat{=}}\emptyset$ $\displaystyle\gamma_{\it
init}.\mathtt{wrSet}_{t}$ $\displaystyle\mathrel{\hat{=}}\emptyset$
$\displaystyle\gamma^{\mathbf{Init}}.\mathtt{seenIdxs}_{t}$
$\displaystyle\mathrel{\hat{=}}\emptyset$
$\displaystyle\gamma^{\mathbf{Init}}.\mathtt{beginIdx}_{t}$
$\displaystyle\mathrel{\hat{=}}0$

where $\beta^{\mathbf{Init}}$ is the initial state of the client program.

##### Transition semantics of TMS2-RA

The transition relation of our TMS2-RA semantics for various transactional
operations is given in Fig. 6 and explained below.

#####  TxBegin operation by transaction $t$.

A transaction starts with a TxBegin operation and should specify if it is a
relaxed or releasing/acquiring transaction. The TxBegin operation takes $a$
and $r$ and sets the value of $\mathtt{synctype}_{t}$ accordingly. It also
sets the value $\mathtt{beginIdx}_{t}$ to be the latest memory version at the
time of begining the transaction and changes the $\mathtt{status}_{t}$ to
${\tt READY}$. Values of $\mathtt{seenIdxs}_{t}$, $\mathtt{rdSet}_{t}$, and
$\mathtt{wrSet}_{t}$ are set to empty.

#####  TxWrite operation by transaction $t$.

Assuming that $l$ is a location and $v$ is a value and
$\mathtt{status}_{t}={\tt READY}$, TxWrite operation of transaction $t$ adds
the $l\mapsto v$ pair to the write set of transaction $t$ (i.e.
$\mathtt{wrSet}_{t}$). Other state components remain unchanged.

#####  TxRead operation by transaction $t$.

The transactional read operation (TxRead) reads the value ($v$) of location
$l$ from the transaction $t$’s write set ($\mathtt{wrSet}_{t}$) if the
transaction $t$ has previously wrote to the location $l$
($l\in\operatorname{\mathbf{dom}}(\mathtt{wrSet}_{t})$). In this case the
state will remain unchanged.

If $t$ has not previously written to $l$
($l\notin\operatorname{\mathbf{dom}}(\mathtt{wrSet}_{t})$) then the value of
$l$ will be read from a memory version $i$ where $i$ is greater than or equal
to $\mathtt{beginIdx}_{t}$ and the $\mathtt{rdSet}_{t}$ is consistent with
that memory version (i.e. $\mathtt{rdSet}_{t}\subseteq\mathit{M}_{i}$). In
this case version $i$ will be added to $\mathtt{seenIdxs}_{t}$ and the
transaction’s read set ($\mathtt{rdSet}_{t}$) is also updated to include the
$l\mapsto v$. $\mathtt{seenIdxs}$ is particularly important for
synchronisation if the transaction is acquiring.

#####  TxEndRO operation by transaction $t$.

A read-only transaction is committed by TxEndRO. If a transaction is read-only
($\mathtt{wrSet}_{t}=\emptyset$) then it updates $\mathtt{status}_{t}$ of the
transaction state ($\gamma$) to be ${\tt COMMITTED}$ and will leave the rest
of the state unchanged. If the transaction was set to be acquiring by TxBegin
($\mathtt{isAcq}_{t}=True$) and the transaction’s read set is not empty
($\mathtt{rdSet}_{t}\neq\emptyset$) then the client’s thread view ($\beta.{\tt
tview}_{t}$) may also get synchronised as well.

#####  TxEndWR operation by transaction $t$.

A writer transaction is committed by TxEndWR. Simillar to a read-only
transaction, a writer transaction ($\mathtt{wrSet}_{t}\neq\emptyset$) will set
$status_{t}$ to ${\tt COMMITTED}$. A writer transaction also add a new memory
version $i$ to $\mathit{M}$ where $i$ is equal to the size of
$\gamma.\mathit{M}$ meaning that the new memory version is added to the end of
$\mathit{M}$ sequence. The new memory version is obtained by overrwriting the
latest memory version in $\gamma.\mathit{M}$ with the transaction’s write set:
$mem^{\prime}=\mathit{last}(\gamma.\mathit{M})\oplus{}\mathtt{wrSet}_{t}$).
The function $last$ is defined as $last(m)\mathrel{\hat{=}}m_{|m|-1}$. The
memory modification view ($V_{i}$) of the new memory version $i$ and the
updated thread view of the clinet state (${\tt tview}_{t}$) is going to be the
same and determined by ${\tt tview}^{\prime}$. The value of ${\tt
tview}^{\prime}$ is determined in the same way as explained for TxEndRO.

#####  TxAbort operation by transaction $t$.

If transaction $t$ aborts, TxAbort will set $\mathtt{status}_{t}$ to ${\tt
ABORTED}$. At this point, other transaction operations (except TxBegin) cannot
be executed. The client state $\beta$ will remain unchanged.

##  Appendix C Forward Simulation implies Observational Refinement

We have already shown that there exists a forward simulation between TMS2-ra
and TML-ra. In this section, we show that if there exists a forward simulation
between an abstract TM specification $AO$ and a concrete implementation $CO$
as defined in Definition 4, then for any client $P$, $P[CO]$ is a contextual
refinement of $P[AO]$ ($P[CO]\leq P[AO]$).

See 5

###### Proof.

Assume ${\it ft}$ is a full trace of $P[CO]$, where for each $i$, ${\it
ft}_{i}$ is a triple is of the form $(\mathit{ls}_{i},\gamma_{i},\beta_{i})$.
We show that there exists a full trace ${\it aft}$ of $P[AO]$ such that
$\xi({\it ft})\leq\xi({\it aft})$ (see Definition 1), where $\xi({\it ft})$
projects the full trace to the client trace, i.e., for each $i$, $\xi({\it
ft})_{i}=(\mathit{ls}_{i}{{}_{|P}},\beta_{i})$ (and similarly $\xi({\it
aft})$), and additionally removes any stuttering.

The proof is by induction over prefixes ${\it ft}^{\prime}$ of ${\it ft}$.

For the base case, ${\it
ft}^{\prime}=\langle(\mathit{ls}^{\mathbf{Init}},\gamma_{C}^{\mathbf{Init}},\beta_{C}^{\mathbf{Init}})\rangle$
is a trace containing just the initial state of $C$. By “Initialisation” of
Definition 4 there exists a
$(\mathit{als}^{\mathbf{Init}},\gamma_{A}^{\mathbf{Init}},\beta_{A}^{\mathbf{Init}})$
such that

$R((\mathit{als}^{\mathbf{Init}},\gamma_{A}^{\mathbf{Init}},\beta_{A}^{\mathbf{Init}}),(\mathit{ls}^{\mathbf{Init}},\gamma_{C}^{\mathbf{Init}},\beta_{C}^{\mathbf{Init}}))$

Moreover, by “Client observation” of Definition 4, we have
$\mathit{als}^{\mathbf{Init}}_{|P}=\mathit{ls}^{\mathbf{Init}}_{|P}$ and for
all threads $\tau$ and locations $x$, $\beta^{\mathbf{Init}}_{C}.{\it
OW}(\tau,x)\subseteq\beta^{\mathbf{Init}}_{A}.{\it OW}(\tau,x)$. Thus, for
$\xi({\it ft})$ there exists an ${\it aft}$ such that $\xi({\it
ft})\leq\xi({\it aft})$.

For our inductive hypothesis, assume the result holds for ${\it ft}^{\prime}$,
i.e., there exists an abstrace prefix ${\it aft}^{\prime}$ of an abstract
trace ${\it aft}$ of $P[AO]$ such that $\xi({\it ft}^{\prime})\leq\xi({\it
aft}^{\prime})$. Moreover, we assume that $R(\mathit{last}({\it
aft}^{\prime}),\mathit{last}({\it ft}^{\prime}))$. Suppose ${\it
ft}^{\prime\prime}={\it
ft}^{\prime}\cdot\langle(\mathit{ls},\gamma_{C},\beta_{C})\rangle$ where
$(\mathit{ls},\gamma_{C},\beta_{C})$ is generated by a concrete step from
$\mathit{last}({\it ft}^{\prime})$. There are three possibilites based on the
step taken by the concrete program.

  * •

The first case is when the concrete program takes a library step and ${\it
ft}^{\prime\prime}$ is the program trace after the execution of the library
step, because we already proved $CO\leq AO$ then by preservation rule of
Definition 4 we know that there exists an abstract trace ${\it
aft}^{\prime\prime}={\it
aft}^{\prime}\cdot\langle(\mathit{als},\gamma_{A},\beta_{A})\rangle$ such that
$R((\mathit{als},\gamma_{A},\beta_{A}),(\mathit{ls},\gamma_{C},\beta_{C}))$.
Moreover using “Client observation” of Definition 4, we have $\xi({\it
ft}^{\prime\prime})\leq\xi({\it aft}^{\prime\prime})$.

  * •

The next case is when the concrete program takes a non-synchronising client
step. Since the abstract and concrete takes the same non-synchronising step,
the abstract and concrete library states remain unchanged, thus
$R_{O}((\mathit{als}_{|AO},\gamma_{A}),(\mathit{ls}_{|CO},\gamma_{C}))$.
Moreover, the thread view and local state of both abstract and concrete
programs will be updated in the same way, thus we also have
$R_{V}((\mathit{als},\beta_{A}),(\mathit{ls},\beta_{C}))$. Finally, by the
client observation property and the refinement relation $R$ are preserved.
Since we match the concrete step at the abstract level, we have $\xi({\it
ft}^{\prime\prime})\leq\xi({\it aft}^{\prime\prime})$.

  * •

The last case is when the concrete program takes a synchronising client step.
Like the unsynchronising case, the abstract and concrete client steps are
identical and they both update the thread view and local state of the client
in the same way, thus
$R_{V}((\mathit{als},\beta_{A}),(\mathit{ls},\beta_{C}))$. Thus, we have
$\xi({\it ft}^{\prime\prime})\leq\xi({\it aft}^{\prime\prime})$. We must now
show that the refinement relation holds in the post-state. As opposed to the
previous case, the synchronising client step potentially updates the library
state by advancing the library thread view for the executing thread, $\tau$.
However, this is equivalent to moving the library view forward using the
“Thread view stability” property of Definition 4. Thus, we have
$R_{O}((\mathit{als}_{|AO},\gamma_{A}),(\mathit{ls}_{|CO},\gamma_{C}))$.

∎

##  Appendix D Selection of TARO Proof Rules

We present a selection of TARO proof rules that we use in our examples. The
full development (Dalvandi and Dongol, 2022) contains many other rules, but we
do not present all of these, since they are less interesting. Note that $z$
below is a client variable.

###  D.1. Assertions over TxBegin

  1. (1)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\neg[\hat{x}\approx
u]_{\tau}\end{array}\right\\}}~{}{\tt
TxBegin}_{\\_}(\\_,\\_)~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\neg[\hat{x}\approx
u]_{\tau}\end{array}\right\\}}$

  2. (2)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\langle\hat{x}=u\rangle[z=v]_{\tau}\end{array}\right\\}}~{}{\tt
TxBegin}_{\\_}(\\_,\\_)~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\langle\hat{x}=u\rangle[z=v]_{\tau}\end{array}\right\\}}$

  3. (3)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}[z=u]_{\tau}\end{array}\right\\}}~{}{\tt
TxBegin}_{\\_}(\\_,\\_)~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}[z=u]_{\tau}\end{array}\right\\}}$

  4. (4)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}{\it
true}\end{array}\right\\}}~{}{\tt TxBegin}_{\tau}({\sf
R},\\_)~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}Rel_{\tau}\end{array}\right\\}}$

  5. (5)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}{\it
true}\end{array}\right\\}}~{}{\tt TxBegin}_{\tau}({\sf
A},\\_)~{}~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}Acq_{\tau}\end{array}\right\\}}$

  6. (6)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}(\hat{y},v)\in{\it
WS}_{\tau^{\prime}}\wedge\tau\neq\tau^{\prime}\end{array}\right\\}}~{}{\tt
TxBegin}_{\tau}(\\_,\\_)~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}(\hat{y},v)\in{\it
WS}_{\tau^{\prime}}\end{array}\right\\}}$

###  D.2. Assertions over TxRead

  1. (1)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\neg[\hat{x}\approx
u]_{\tau}\end{array}\right\\}}~{}{\tt
TxRead}_{\\_}(\\_,\\_)~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\neg[\hat{x}\approx
u]_{\tau}\end{array}\right\\}}$

  2. (2)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}[\hat{x}=u]_{\tau^{\prime}}\end{array}\right\\}}~{}{\tt
TxRead}_{\tau}(\\_,\\_)~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}status_{\tau}={\tt
READY}\Rightarrow[\hat{x}=u]_{\tau^{\prime}}\end{array}\right\\}}$

  3. (3)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}{\it
WS}_{\tau}=\emptyset\end{array}\right\\}}~{}{\tt
TxRead}_{\tau}(\hat{x},r)~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}(\hat{x},r)\in{\it
RS}_{\tau}\end{array}\right\\}}$

  4. (4)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}(\hat{x},r)\not\in{\it
WS}_{\tau}\end{array}\right\\}}~{}{\tt
TxRead}_{\tau}(\hat{x},r)~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}[\hat{x}\approx
r]_{\tau}\end{array}\right\\}}$

  5. (5)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}[\hat{x}=u]_{\tau}\wedge\hat{x}\notin\operatorname{\mathbf{dom}}({\it
WS}_{\tau})\end{array}\right\\}}~{}{\tt
TxRead}_{\tau}(\hat{x},r)~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}r=u\end{array}\right\\}}$

  6. (6)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}(\hat{y},v)\in{\it
WS}_{\tau}\end{array}\right\\}}~{}{\tt
TxRead}_{\\_}(\\_,\\_)~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}(\hat{y},v)\in{\it
WS}_{\tau}\end{array}\right\\}}$

  7. (7)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}(\hat{y},v)\in{\it
RS}_{\tau^{\prime}}\wedge\tau\neq\tau^{\prime}\end{array}\right\\}}~{}{\tt
TxRead}_{\tau}(\\_,\\_)~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}(\hat{y},v)\in{\it
RS}_{\tau^{\prime}}\end{array}\right\\}}$

###  D.3. Assertions over TxWrite

  1. (1)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\neg[\hat{x}\approx
u]_{\tau}\end{array}\right\\}}~{}{\tt
TxWrite}_{\\_}(\\_,\\_)~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\neg[\hat{x}\approx
u]_{\tau}\end{array}\right\\}}$

  2. (2)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}[z=u]_{\tau}\end{array}\right\\}}~{}{\tt
TxWrite}_{\\_}(\\_,\\_)~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}[z=u]_{\tau}\end{array}\right\\}}$

  3. (3)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}{\it
true}\end{array}\right\\}}~{}{\tt
TxWrite}_{\tau}(\hat{y},v)~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}(\hat{y},v)\in{\it
WS}_{\tau}\end{array}\right\\}}$

  4. (4)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\langle\hat{x}=u\rangle[z=v]_{\tau}\wedge
w\neq u\end{array}\right\\}}~{}{\tt
TxWrite}_{\tau}(\hat{y},w)~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\langle\hat{x}=u\rangle[z=v]_{\tau}\end{array}\right\\}}$

  5. (5)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\hat{x}\neq\hat{y}\wedge(\hat{y},v)\in{\it
WS}_{\tau}\end{array}\right\\}}~{}{\tt
TxWrite}_{\\_}(\hat{x},\\_)~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}(\hat{y},v)\in{\it
WS}_{\tau}\end{array}\right\\}}$

###  D.4. Assertions over TxEnd

  1. (1)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\langle\hat{x}=u\rangle[z=v]_{\tau^{\prime}}\wedge{\it
WS}_{\tau}=\emptyset\end{array}\right\\}}~{}{\tt
TxEnd}_{\tau}~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\langle\hat{x}=u\rangle[z=v]_{\tau^{\prime}}\end{array}\right\\}}$

  2. (2)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\begin{array}[c]{@{}l@{}}(\hat{x},u)\in{\it
WS}_{\tau}\wedge\neg[\hat{x}\approx u]_{\tau^{\prime}}\wedge{}\\\
{[}z=v]_{\tau}\wedge
Rel_{\tau}\wedge\tau\neq\tau^{\prime}\end{array}\end{array}\right\\}}~{}{\tt
TxEnd}_{\tau}~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}status_{\tau}={\tt
COMMITTED}\Rightarrow\langle\hat{x}=u\rangle[z=v]_{\tau^{\prime}}\end{array}\right\\}}$

  3. (3)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\langle\hat{x}=u\rangle[z=v]_{\tau}\wedge(\hat{x},u)\notin{\it
WS}_{\tau}\wedge Rel_{\tau}\end{array}\right\\}}~{}{\tt
TxEnd}_{\tau}~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\langle\hat{x}=u\rangle[z=v]_{\tau}\end{array}\right\\}}$

  4. (4)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\langle\hat{x}=u\rangle[z=v]_{\tau^{\prime}}\end{array}\right\\}}~{}{\tt
TxEnd}_{\tau}~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}status_{\tau}={\tt
ABORTED}\Rightarrow\langle\hat{x}=u\rangle[z=v]_{\tau^{\prime}}\end{array}\right\\}}$

  5. (5)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\begin{array}[c]{@{}l@{}}\langle\hat{x}=u\rangle[z=v]_{\tau}\wedge(\hat{x},u)\in{\it
RS}_{\tau}\wedge{}\\\ Acq_{\tau}\wedge{\it
WS}_{\tau}=\emptyset\end{array}\end{array}\right\\}}~{}{\tt
TxEnd}_{\tau}~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}status_{\tau}={\tt
COMMITTED}\Rightarrow[z=v]_{\tau}\end{array}\right\\}}$

  6. (6)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\neg[\hat{x}\approx
u]_{\tau^{\prime}}\wedge(\hat{x},u)\notin{\it
WS}_{\tau}\end{array}\right\\}}~{}{\tt
TxEnd}_{\tau}~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\neg[\hat{x}\approx
u]_{\tau^{\prime}}\end{array}\right\\}}$

  7. (7)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}[y=v]_{\tau}\end{array}\right\\}}~{}{\tt
TxEnd}_{\tau}~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}[y=v]_{\tau}\end{array}\right\\}}$

  8. (8)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}[x\approx
u]_{\tau^{\prime}}\wedge\neg Acq_{\tau}\end{array}\right\\}}~{}{\tt
TxEnd}_{\tau}~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}[x\approx
u]_{\tau^{\prime}}\end{array}\right\\}}$

  9. (9)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}(\hat{y},v)\in{\it
WS}_{\tau^{\prime}}\end{array}\right\\}}~{}{\tt
TxEnd}_{\tau}~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}(\hat{y},v)\in{\it
WS}_{\tau^{\prime}}\end{array}\right\\}}$

###  D.5. Assertions over client actions

  1. (1)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\langle\hat{x}=u\rangle[z=v]_{\tau^{\prime}}\end{array}\right\\}}~{}r\leftarrow_{\tau}z^{\prime}~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\langle\hat{x}=u\rangle[z=v]_{\tau^{\prime}}\end{array}\right\\}}$

  2. (2)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\langle\hat{x}=u\rangle[z=v]_{\tau}\wedge
z\neq
z^{\prime}\end{array}\right\\}}~{}z^{\prime}:=_{\tau}m~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\langle\hat{x}=u\rangle[z=v]_{\tau}\end{array}\right\\}}$

##  Appendix E Additional examples

This section provides the full proof outline for two additional examples. The
proof outline presented in Fig. 13 includes two new assertions that were not
introduced previously:

  * •

Memory-value assertion: A memory-value assertion, denoted as
$\mathit{M}[\hat{x},v]_{i}$, holds iff the value of location $x$ in memory
version $i$ is $v$.

$\displaystyle\mathit{M}[\hat{x},v]_{i}\mathrel{\hat{=}}i\in\operatorname{\mathbf{dom}}(\mathit{M})\land\mathit{M}_{i}(\hat{x})=v$

  * •

Never-written assertion: A never-written assertion, denoted as
$NW[\hat{x},v]$, holds iff none of the recorded memories in $\mathit{M}$ has
the value $v$ for location $x$.

$\displaystyle NW[\hat{x},v]\mathrel{\hat{=}}\forall
i\in\operatorname{\mathbf{dom}}(\mathit{M}).\ \neg\mathit{M}[\hat{x},v]_{i}$

A selection of proof rules over memory-value and never-written predicates are
given below.

  1. (1)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\mathit{M}[\hat{x},u]_{i}\end{array}\right\\}}~{}{\tt
TxBegin}_{\tau}(\\_,\\_){\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\mathit{M}[\hat{x},u]_{i}\end{array}\right\\}}$

  2. (2)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\mathit{M}[\hat{x},u]_{i}\end{array}\right\\}}~{}{\tt
TxRead}_{\tau}(\\_,\\_){\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\mathit{M}[\hat{x},u]_{i}\end{array}\right\\}}$

  3. (3)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\mathit{M}[\hat{x},u]_{i}\end{array}\right\\}}~{}{\tt
TxWrite}_{\tau}(\\_,\\_){\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\mathit{M}[\hat{x},u]_{i}\end{array}\right\\}}$

  4. (4)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}(\hat{x},u)\in{\it
WS}_{\tau}\wedge|\mathit{M}|=n\end{array}\right\\}}~{}{\tt
TxEnd}_{\tau}~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}status_{\tau}={\tt
COMMITTED}\Rightarrow\mathit{M}[\hat{x}=u]_{n}\end{array}\right\\}}$

  5. (5)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\mathit{M}[\hat{x}=v]_{i}\wedge
i<|\mathit{M}|-1\end{array}\right\\}}~{}{\tt
TxEnd}_{\tau}~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\mathit{M}[\hat{x}=v]_{i}\end{array}\right\\}}$

  6. (6)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\mathit{M}[\hat{x}=u]_{i-1}\wedge\mathit{M}[\hat{x}=v]_{i}\wedge{}\\\
\mathit{M}[\hat{y}=l]_{i-1}\wedge\mathit{M}[\hat{y}=n]_{i}\wedge{}\\\ u\neq
v\wedge l\neq n\wedge i=|\mathit{M}|-1\wedge{}\\\ \mathtt{txn}_{\tau}=t\wedge
beginIndex_{t}=i-1\wedge{}\\\ (\hat{x},v)\in{\it RS}_{\tau}\wedge{\it
WS}_{\tau}=\emptyset\end{array}\right\\}}~{}{\tt
TxRead}_{\tau}(\hat{y},r)~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}status_{\tau}={\tt
READY}\Rightarrow r=n\end{array}\right\\}}$

  7. (7)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}NW[\hat{x},v]\end{array}\right\\}}~{}{\tt
TxBegin}_{\tau}(\\_,\\_)~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\neg[\hat{x}\approx
v]_{\tau^{\prime}}\end{array}\right\\}}$

  8. (8)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}NW[\hat{x},v]\end{array}\right\\}}~{}{\tt
TxBegin}_{\tau}(\\_,\\_)~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}NW[x,v]\end{array}\right\\}}$

  9. (9)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}NW[\hat{x},v]\end{array}\right\\}}~{}{\tt
TxRead}_{\tau}(\\_,\\_)~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}NW[x,v]\end{array}\right\\}}$

  10. (10)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}NW[\hat{x},v]\end{array}\right\\}}~{}{\tt
TxWrite}_{\tau}(\\_,\\_)~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}NW[\hat{x},v]\end{array}\right\\}}$

  11. (11)

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}NW[\hat{x},v]\wedge(\hat{x},v)\not\in{\it
WS}_{\tau}\end{array}\right\\}}~{}{\tt
TxEnd}_{\tau}~{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}NW[\hat{x},v]\end{array}\right\\}}$

###### Theorem 1.

The proof outlines in Fig. 12 and Fig. 13 are valid.

###### Proof.

This theorem has been verified in Isabelle/HOL. ∎

$\begin{array}[]{@{}l@{~~~~}||@{~~~~}l@{~~~~}||@{~~~~}l}\lx@intercol\qquad\qquad\qquad\qquad{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\forall\tau\in\\{\tau{1},\tau{2},\tau{3}\\}.\
[\hat{f}=0]_{\tau}\wedge[d_{1}=0]_{\tau}\wedge[d_{2}=0]_{\tau}\end{array}\right\\}}\hfil\lx@intercol\\\
\begin{array}[t]{@{}l@{}}{\bf Thread}\ \tau{1}\\\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}[\hat{f}\not\approx
1]_{\tau{2}}\wedge[d_{1}=0]_{\tau{1}}\wedge\neg{\it
tf}_{1}\end{array}\right\\}}\\\ 1\\!:d_{1}:=5;\\\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}[\hat{f}\not\approx
1]_{\tau{2}}\wedge[d_{1}=5]_{\tau{1}}\wedge\neg{\it
tf}_{1}\end{array}\right\\}}\\\ 2\\!:\hbox{\pagecolor{black!8}${\tt
TxBegin}(\sf R,\emptyset)$}\\\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}[\hat{f}\not\approx
1]_{\tau{2}}\wedge[d_{1}=5]_{\tau{1}}\wedge{}\\\ {\it
Rel}_{\tau{1}}\wedge\neg{\it tf}_{1}\end{array}\right\\}}\\\
3\\!:\hbox{\pagecolor{black!8}${\tt TxWrite}(f,1)$};\\\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}[\hat{f}\not\approx
1]_{\tau{2}}\wedge[d_{1}=5]_{\tau{1}}\wedge{}\\\ {\it
Rel}_{\tau{1}}\wedge(\hat{f},1)\in{\it WS}_{\tau{1}}\wedge\neg{\it
tf}_{1}\end{array}\right\\}}\\\ 4\\!:\hbox{\pagecolor{black!8}$\langle{\tt
TxEnd},{\it tf}_{1}:={\it true}\rangle$};\\\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\langle\hat{f}=1\rangle[d_{1}=5]_{\tau{2}}\wedge{\it
tf}_{1}\end{array}\right\\}}\end{array}\hfil~{}~{}~{}~{}\vrule\vrule~{}~{}~{}~{}&\begin{array}[t]{@{}r@{~}l@{}}\lx@intercol{\bf
Thread}\ \tau{2}\hfil\lx@intercol\\\
\lx@intercol{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}P(0)\wedge([\hat{f}\approx
1]_{\tau{2}}\Rightarrow{\it tf}_{1})\end{array}\right\\}}\hfil\lx@intercol\\\
5\\!:~{}&d_{2}:=10;\\\
\lx@intercol{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}P(10)\wedge([\hat{f}\approx
1]_{\tau{2}}\Rightarrow{\it tf}_{1})\end{array}\right\\}}\hfil\lx@intercol\\\
6\\!:~{}&\hbox{\pagecolor{black!8}${\tt TxBegin}(\sf RA,\\{r_{2}\\})$}\\\
\lx@intercol{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}P(10)\wedge([\hat{f}\approx
1]_{\tau{2}}\Rightarrow{\it tf}_{1})\wedge{}\\\ {\it Acq}_{\tau{2}}\wedge{\it
Rel}_{\tau{2}}\wedge{\it
WS}_{\tau{2}}=\emptyset\end{array}\right\\}}\hfil\lx@intercol\\\
7\\!:~{}&\hbox{\pagecolor{black!8}${\tt TxRead}(f,r_{2})$};\\\
\lx@intercol{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}P(10)\wedge{}\\\
(r_{2}=1\Rightarrow[d_{1}\stackrel{{\scriptstyle
S}}{{=}}5]_{\tau{2}}\wedge{\it tf}_{1})\wedge{}\\\ {\it
Acq}_{\tau{2}}\wedge{\it Rel}_{\tau{2}}\wedge{}\\\ {\it
WS}_{\tau{2}}=\emptyset\wedge(\hat{f},r_{2})\in{\it
RS}_{\tau{2}}\end{array}\right\\}}\hfil\lx@intercol\\\
8\\!:~{}&\hbox{\pagecolor{black!8}$\textsf{{if}}\ r_{2}=1\
\textsf{{then}}$}\\\
\lx@intercol\quad{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}P(10)\wedge[d_{1}\stackrel{{\scriptstyle
S}}{{=}}5]_{\tau{2}}\wedge{\it tf}_{1}\wedge{}\\\ r_{2}=1\wedge{\it
Acq}_{\tau{2}}\wedge{\it Rel}_{\tau{2}}\wedge{}\\\ {\it
WS}_{\tau{2}}=\emptyset\wedge(\hat{f},r_{2})\in{\it
RS}_{\tau{2}}\end{array}\right\\}}\hfil\lx@intercol\\\
9\\!:~{}&\hbox{\pagecolor{black!8}$\quad{\tt TxWrite}(f,2)$}\\\
\lx@intercol\quad{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}P(10)\wedge[d_{1}\stackrel{{\scriptstyle
S}}{{=}}5]_{\tau{2}}\wedge{\it tf}_{1}\wedge{}\\\ r_{2}=1\wedge{\it
Acq}_{\tau{2}}\wedge{\it Rel}_{\tau{2}}\wedge{}\\\ {\it
WS}_{\tau{2}}=\\{(\hat{f},2)\\}\wedge{}\\\ (\hat{f},r_{2})\in{\it
RS}_{\tau{2}}\end{array}\right\\}}\hfil\lx@intercol\\\
\lx@intercol{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}P(10)\wedge{\it
Acq}_{\tau{2}}\wedge{\it Rel}_{\tau{2}}\wedge{}\\\ (r_{2}\neq 1\Rightarrow{\it
WS}_{\tau{2}}=\emptyset)\wedge{}\\\
\left(\begin{array}[c]{@{}l@{}}r_{2}=1\Rightarrow[d_{1}\stackrel{{\scriptstyle
S}}{{=}}5]_{\tau{2}}\wedge{}\\\ \qquad{\it tf}_{1}\wedge(\hat{f},2)\in{\it
WS}_{\tau{2}}\end{array}\right)\wedge{}\\\ (\hat{f},r_{2})\in{\it
RS}_{\tau{2}}\end{array}\right\\}}\hfil\lx@intercol\\\
10\\!:~{}&\hbox{\pagecolor{black!8}${\tt TxEnd}$};\\\
\lx@intercol{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\langle\hat{f}=2\rangle[d_{2}=10]_{\tau{3}}\wedge{}\\\
\left(\begin{array}[c]{@{}l@{}}r_{2}\neq 1\Rightarrow\\\
\quad[\hat{f}\not\approx 2]_{\tau{1}}\wedge[\hat{f}\not\approx
2]_{\tau{3}}\end{array}\right)\wedge{}\\\
\left(\begin{array}[c]{@{}l@{}}r_{2}=1\Rightarrow\\\ \quad{\it
tf}_{1}\wedge\langle\hat{f}=2\rangle[d_{1}=_{\tau{3}}5]\end{array}\right)\end{array}\right\\}}\hfil\lx@intercol\end{array}\hfil~{}~{}~{}~{}\vrule\vrule~{}~{}~{}~{}&\begin{array}[t]{@{}r@{~}l@{}}\lx@intercol{\bf
Thread}\ \tau{3}\hfil\lx@intercol\\\
\lx@intercol{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\langle\hat{f}=2\rangle[d_{1}=5]_{\tau{3}}\wedge{}\\\
\langle\hat{f}=2\rangle[d_{2}=10]_{\tau{3}}\wedge{}\\\ (\neg{\it
tf}_{1}\Rightarrow[\hat{f}\not\approx 1]_{\tau{3}}\wedge[\hat{f}\not\approx
2]_{\tau{3}})\end{array}\right\\}}\hfil\lx@intercol\\\
11\\!:~{}&\hbox{\pagecolor{black!8}${\tt TxBegin}(\sf A,\\{r_{3}\\})$}\\\
\lx@intercol{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\langle\hat{f}=2\rangle[d_{1}=5]_{\tau{3}}\wedge{}\\\
\langle\hat{f}=2\rangle[d_{2}=10]_{\tau{3}}\wedge{}\\\ (\neg{\it
tf}_{1}\Rightarrow[\hat{f}\not\approx 1]_{\tau{3}}\wedge[\hat{f}\not\approx
2]_{\tau{3}}){}\\\ \wedge{}{\it WS}_{\tau{3}}=\emptyset\wedge{\it
Acq}_{\tau{3}}\\\ \end{array}\right\\}}\hfil\lx@intercol\\\
12\\!:~{}&\hbox{\pagecolor{black!8}${\tt TxRead}(f,r_{3})$};\\\
\lx@intercol{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\langle\hat{f}=2\rangle[d_{1}=5]_{\tau{3}}\wedge{}\\\
\langle\hat{f}=2\rangle[d_{2}=10]_{\tau{3}}\wedge{}\\\
\left(\begin{array}[c]{@{}l@{}}\neg{\it tf}_{1}\Rightarrow\\\
\qquad[\hat{f}\not\approx 1]_{\tau{3}}\wedge[\hat{f}\not\approx
2]_{\tau{3}}\end{array}\right)\wedge{}\\\ {\it
WS}_{\tau{3}}=\emptyset\wedge{}\\\ (\hat{f},r_{3})\in{\it
RS}_{\tau{3}}\wedge{\it Acq}_{\tau{3}}\wedge{}\\\
\left(\begin{array}[c]{@{}l@{}}r_{3}=2\Rightarrow\\\
\qquad[d_{1}\stackrel{{\scriptstyle
S}}{{=}}5]_{\tau{3}}\wedge[d_{2}\stackrel{{\scriptstyle
S}}{{=}}10]_{\tau{3}}\end{array}\right)\end{array}\right\\}}\hfil\lx@intercol\\\
13\\!:~{}&\hbox{\pagecolor{black!8}${\tt TxEnd}$};\\\
\lx@intercol{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}r_{3}=2\Rightarrow[d_{1}=5]_{\tau{3}}\wedge[d_{2}=10]_{\tau{3}}\end{array}\right\\}}\hfil\lx@intercol\\\
14\\!:~{}&\textsf{{if}}\ r_{3}=2\ \textsf{{then}}\\\
\lx@intercol\qquad{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}[d_{1}=5]_{\tau{3}}\wedge[d_{2}=10]_{\tau{3}}\end{array}\right\\}}\hfil\lx@intercol\\\
15\\!:~{}&\ \ \ \ s_{1}\leftarrow d_{1}\\\
\lx@intercol\qquad{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}s_{1}=5\wedge[d_{2}=10]_{\tau{3}}\end{array}\right\\}}\hfil\lx@intercol\\\
16\\!:~{}&\ \ \ \ s_{2}\leftarrow d_{2}\\\
\lx@intercol\qquad{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}s_{1}=5\wedge
s_{2}=10\end{array}\right\\}}\hfil\lx@intercol\\\
\lx@intercol{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}r_{3}=2\Rightarrow
s_{1}=5\wedge
s_{2}=10\end{array}\right\\}}\hfil\lx@intercol\end{array}\end{array}$

$\\{r_{3}=2\Rightarrow s_{1}=5\wedge s_{2}=10\\}$

Figure 12. Proof outline for extended transactional MP, where
$P(k)\mathrel{\hat{=}}[d_{2}=k]_{\tau{2}}\wedge\langle\hat{f}=1\rangle[d_{1}=42]_{\tau{2}}\wedge{[}\hat{f}\not\approx
2]_{\tau{1}}\wedge{}{[}\hat{f}\not\approx 2]_{\tau{3}}$

Proof outline for extended transactional MP

$\begin{array}[]{@{}l@{~~~~}||@{~~~~}l@{}}\begin{array}[t]{@{}l@{}}{\bf
Thread}\ \tau{1}\\\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}NW[\hat{f},1]\land
NW[\hat{d}2,10]\\\
\land[d1=0]_{\tau{1}}\land|\mathit{M}|=0\end{array}\right\\}}\\\
1\\!:d_{1}:=5;\\\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}NW[\hat{f},1]\land
NW[\hat{d}2,10]\\\
\land[d1=5]_{\tau{1}}\land|\mathit{M}|=0\end{array}\right\\}}\\\
2\\!:\hbox{\pagecolor{black!8}${\tt TxBegin}(\sf RX,\emptyset)$};\\\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\neg[\hat{f}\approx
1]_{\tau{2}}\land\neg[\hat{d}2\approx 10]_{\tau{2}}\\\
\land[d1=5]_{\tau{1}}\land\neg{\it Rel}_{\tau{1}}\\\
\land~{}\mathtt{status}_{\tau{1}}=R\\\ \land\neg{\it
Acq}_{\tau{1}}\land|\mathit{M}|=0\end{array}\right\\}}\\\
3\\!:\hbox{\pagecolor{black!8}${\tt TxWrite}(d_{2},10)$};\\\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}(\hat{d}_{2},10)\in{\it
WS}_{t}\land\neg[\hat{f}\approx 1]_{\tau{2}}\\\ \land\neg[\hat{d}_{2}\approx
10]_{\tau{2}}\land[d1=5]_{\tau{1}}\\\ \land\neg{\it
Rel}_{\tau{1}}\land~{}\mathtt{status}_{\tau{1}}=R\land\\\ \neg{\it
Acq}_{\tau{1}}\land|\mathit{M}|=0\end{array}\right\\}}\\\
4\\!:\hbox{\pagecolor{black!8}${\tt TxWrite}(f,1)$};\\\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}(\hat{f},1)\in{\it
WS}_{\tau{1}}\land(\hat{d}_{2},10)\in{\it WS}_{\tau{1}}\\\
\land\neg[\hat{f}\approx 1]_{\tau{2}}\land\neg[\hat{d}2\approx
10]_{\tau{2}}\\\ \land[d1=5]_{\tau{1}}\land\neg{\it Rel}_{\tau{1}}\land\\\
~{}\mathtt{status}_{\tau{1}}=R\land\neg{\it
Acq}_{\tau{1}}\land|\mathit{M}|=0\end{array}\right\\}}\\\
5\\!:\hbox{\pagecolor{black!8}${\tt TxEnd}$};\\\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}{\it
true}\end{array}\right\\}}\end{array}\hfil~{}~{}~{}~{}\vrule\vrule~{}~{}~{}~{}&\begin{array}[t]{@{}r@{~}l@{}}\lx@intercol{\bf
Thread}\ \tau{2}\hfil\lx@intercol\\\
\lx@intercol{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\mathit{M}[\hat{f}=0]_{0}\land\mathit{M}[\hat{d}2=0]_{0}\land\\\
(\mathtt{status}_{\tau{1}}=C\Rightarrow\mathit{M}[\hat{f}=1]_{1}\land\mathit{M}[\hat{d}2=10]_{1})\land\\\
(\mathtt{status}_{\tau{1}}=C\Rightarrow([\hat{f}\approx
0]_{t}\lor[\hat{f}\approx 1]_{t}))\land\\\
(\mathtt{status}_{\tau{1}}=C\Rightarrow([\hat{d2}\approx
0]_{t}\lor[\hat{d2}\approx 10]_{t}))\land\\\ (\forall
v.v\not\in\\{0,5\\}\Rightarrow\neg[d1\approx_{\tau 2}v])\land\\\
(\mathtt{status}_{\tau{1}}\neq
C\Rightarrow[\hat{f}=0]_{t}\land[\hat{d2}=0]_{t})\land\\\
WS_{t}=\emptyset\land\\\ (\forall i.i\neq 0\land
i\leq|\mathit{M}|\Rightarrow\neg\mathit{M}[\hat{d}2=0]_{i})\land\\\ (\forall
i.i\neq 1\land
i\leq|\mathit{M}|\Rightarrow\neg\mathit{M}[\hat{f}=1]_{i})\end{array}\right\\}}\hfil\lx@intercol\\\
6\\!:~{}&\hbox{\pagecolor{black!8}${\tt TxBegin}(\sf
RX,\\{r_{1},r_{2}\\})$}\\\
\lx@intercol{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\mathit{M}[\hat{f}=0]_{0}\land\mathit{M}[\hat{d2}=0]_{0}\land\\\
(\mathtt{status}_{\tau{1}}=C\Rightarrow\mathit{M}[\hat{f}=1]_{1}\land\mathit{M}[\hat{d2}=10]_{1})\land\\\
(\mathtt{status}_{\tau{1}}=C\Rightarrow([\hat{f}\approx 0]_{\tau
1}\lor[\hat{f}\approx 1]_{\tau 1}))\land\\\
(\mathtt{status}_{\tau{1}}=C\Rightarrow([\hat{d2}\approx 0]_{\tau
1}\lor[\hat{d2}\approx 10]_{\tau 1}))\land\\\ (\forall
v.v\not\in{0,5}\Rightarrow\neg[d1\approx_{\tau 2}v])\land\\\
(\mathtt{status}_{\tau{1}}\neq C\Rightarrow[\hat{f}=0]_{\tau
1}\land[\hat{d2}=0]_{\tau 1})\land\\\ WS_{\tau 1}=\emptyset\land\\\ (\forall
i.i\neq 0\land i\leq|M|\Rightarrow\neg\mathit{M}[\hat{d2}=0]_{i})\land\\\
(\forall i.i\neq 1\land
i\leq|M|\Rightarrow\neg\mathit{M}[\hat{f}=1]_{i})\land\neg Acq_{\tau 1}\\\
\end{array}\right\\}}\hfil\lx@intercol\\\
7\\!:~{}&\hbox{\pagecolor{black!8}${\tt TxRead}(f,r_{1})$};\\\
\lx@intercol{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\mathit{M}[\hat{f}=0]_{0}\land\mathit{M}[\hat{d2}=0]_{0}\land\\\
(r1=1\Rightarrow\mathtt{status}_{\tau{1}}=C)\land\\\
(r1=1\Rightarrow(\hat{f},1)\in RS_{\tau 1})\land\\\
(r1=1\Rightarrow\mathit{M}[\hat{f}=1]_{1}\land\mathit{M}[\hat{d2}=10]_{1})\land\\\
(\forall v.v\not\in{0,5}\Rightarrow\neg[d1\approx_{\tau 2}v])\land\\\ WS_{\tau
1}=\emptyset\land\\\ (\forall i.i\neq 0\land
i\leq|M|\Rightarrow\neg\mathit{M}[\hat{d2}=0]_{i})\land\\\ (\forall i.i\neq
1\land i\leq|M|\Rightarrow\neg\mathit{M}[\hat{f}=1]_{i})\land\neg Acq_{\tau
1}\end{array}\right\\}}\hfil\lx@intercol\\\
8\\!:~{}&\hbox{\pagecolor{black!8}{{if}}\ $r_{1}=1$\ {{then}}\ }\\\
\lx@intercol{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\mathit{M}[\hat{f}=0]_{0}\land\mathit{M}[\hat{d2}=0]_{0}\\\
\land\mathit{M}[\hat{f}=1]_{1}\land\mathit{M}[\hat{d2}=10]_{1}\\\ \land
r1=1\land(\hat{f},1)\in RS_{\tau 1}\land\\\ (\forall
v.v\not\in{0,5}\Rightarrow\neg[d1\approx_{\tau 2}v])\land\\\ WS_{\tau
1}=\emptyset\land\\\ (\forall i.i\neq 0\land
i\leq|M|\Rightarrow\neg\mathit{M}[\hat{d2}=0]_{i})\land\\\ (\forall i.i\neq
1\land i\leq|M|\Rightarrow\neg\mathit{M}[\hat{f}=1]_{i})\land\neg Acq_{\tau
1}\land\mathtt{status}_{\tau{1}}=C\end{array}\right\\}}\hfil\lx@intercol\\\
9\\!:~{}&\hbox{\pagecolor{black!8}\quad${\tt TxRead}(d_{2},r_{2})$};\\\
\lx@intercol{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}(r1=1\Rightarrow
r2=10)\land\\\ (\forall v.v\not\in{0,5}\Rightarrow\neg[d1\approx_{\tau
2}v])\land\\\ WS_{\tau 1}=\emptyset\land\neg Acq_{\tau
1}\end{array}\right\\}}\hfil\lx@intercol\\\
10\\!:~{}&\hbox{\pagecolor{black!8}${\tt TxEnd}$};\\\
\lx@intercol{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}(\forall
v.v\not\in{0,5}\Rightarrow\neg[d1\approx_{\tau 2}v])\land\\\
(\mathtt{status}_{\tau{2}}=C\land r1=1\Rightarrow r2=10)\\\
\end{array}\right\\}}\hfil\lx@intercol\\\ 11\\!:~{}&r_{3}\leftarrow d_{1};\\\
\lx@intercol{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}(\mathtt{status}_{\tau{2}}=C\land
r_{1}=1\Rightarrow r_{2}=10\land
r_{3}\in\\{0,5\\})\end{array}\right\\}}\hfil\lx@intercol\\\
\end{array}\end{array}$

$\\{\mathtt{status}_{\tau{2}}=C\land r_{1}=1\Rightarrow r_{2}=10\land
r_{3}\in\\{0,5\\}\\}$

Figure 13. Proof outline for relaxed transactions where $C$ and $R$ are
shorthand for ${\tt COMMITTED}$ and ${\tt READY}$, respectively.

Proof outline for relaxed transactions