A. Adir, H. Attiya, and G. Shurek, Information-flow models for shared memory with an application to the PowerPC architecture, IEEE Trans. Parallel Distrib. Syst, vol.14, issue.5, pp.502-515, 2003.

J. Alglave, A. Fox, S. Ishtiaq, M. O. Myreen, S. Sarkar et al., The semantics of Power and ARM multiprocessor machine code, Proc. DAMP 2009, 2009.

J. Alglave and L. Maranget, The diy7 tool, pp.2019-2026, 2019.

J. Alglave and L. Maranget, The herd7 tool, pp.2019-2026, 2019.

J. Alglave, L. Maranget, K. Deplaix, K. Didier, and S. Sarkar, The litmus7 tool, pp.2019-2026, 2019.

J. Alglave, L. Maranget, S. Sarkar, and P. Sewell, Fences in weak memory models, Proc. CAV, 2010.
URL : https://hal.archives-ouvertes.fr/hal-01100859

J. Alglave, L. Maranget, S. Sarkar, and P. Sewell, Litmus: running tests against hardware, Proceedings of TACAS 2011: the 17th international conference on Tools and Algorithms for the Construction and Analysis of Systems, pp.41-44
URL : https://hal.archives-ouvertes.fr/hal-01100851

. Springer-verlag, , 2011.

J. Alglave, L. Maranget, and M. Tautschnig, Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory, ACM TOPLAS, vol.36, issue.2, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01081364

, ARM Limited: ARM architecture reference manual. ARMv8, for ARMv8-A architecture profile, 2018.

A. Armstrong, T. Bauereiss, B. Campbell, S. F. Gray, G. Kerneis et al., , 2019.

A. Armstrong, T. Bauereiss, B. Campbell, A. Reid, K. E. Gray et al., Proc. 46th ACM SIGPLAN Symposium on Principles of Programming Languages, vol.3, 2019.

C. Baumann, O. Schwarz, and M. Dam, Compositional verification of security properties for embedded execution platforms, PROOFS@CHES 2017, 6th International Workshop on Security Proofs for Embedded Systems, pp.1-16, 2017.

N. Chong and S. Ishtiaq, Reasoning about the ARM weakly consistent memory model, 2008.

I. J. Clester, T. Bourgeat, A. Wright, S. Gruetter, and A. Chlipala, riscv-plv risc-v isa formal specification, pp.2019-2026, 2019.

W. Deacon, The ARMv8 application level memory model, 2016.

A. Ferraiuolo, A. Baumann, C. Hawblitzel, and B. Parno, Komodo: Using verification to disentangle secure-enclave hardware from software, Proceedings of the 26th Symposium on Operating Systems Principles, pp.287-305, 2017.

S. Flur, J. French, K. Gray, C. Pulte, S. Sarkar et al., , 2017.

S. Flur, K. E. Gray, C. Pulte, S. Sarkar, A. Sezgin et al., Modelling the ARMv8 architecture, operationally: Concurrency and ISA, Proceedings of POPL: the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01244776

S. Flur, S. Sarkar, C. Pulte, K. Nienhuis, L. Maranget et al., Mixed-size concurrency, The 44st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.429-442, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01413221

S. Goel, The x86isa books: Features, usage, and future plans, Proceedings 14th International Workshop on the ACL2 Theorem Prover and its Applications, pp.1-17, 2017.

,

S. Goel, W. A. Hunt, M. Kaufmann, and S. Ghosh, Simulation and formal verification of x86 machine-code programs that make system calls, Proceedings of the 14th Conference on Formal Methods in Computer-Aided Design, 2014.

K. E. Gray, G. Kerneis, D. Mulligan, C. Pulte, S. Sarkar et al., An integrated concurrency and core-ISA architectural envelope definition, and test oracle, for IBM POWER multiprocessors, Proc. MICRO-48, the 48th Annual IEEE/ACM International Symposium on Microarchitecture, 2015.

R. Gu, Z. Shao, H. Chen, X. N. Wu, J. Kim et al., Cer-tiKOS: An extensible architecture for building certified concurrent OS kernels, 12th USENIX Symposium on Operating Systems Design and Implementation, pp.653-669, 2016.

R. Gu, Z. Shao, J. Kim, X. N. Wu, J. Koenig et al., Certified concurrent abstraction layers, Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp.646-661, 2018.

R. Guanciale, H. Nemati, M. Dam, and C. Baumann, Provably secure memory isolation for linux on ARM, Journal of Computer Security, vol.24, issue.6, pp.793-837, 2016.

, Intel Corporation: Intel 64 and ia-32 architectures software developer's manual combined volumes: 1, 2a, 2b, 2c, 2d, 3a, 3b, 3c, pp.325462-070, 2019.

G. Klein, J. Andronick, K. Elphinstone, T. Murray, T. Sewell et al., Comprehensive formal verification of an OS microkernel, ACM Transactions on Computer Systems, vol.32, issue.1, 2014.

R. Kumar, M. O. Myreen, M. Norrish, and S. Owens, CakeML: a verified implementation of ML, The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, pp.179-192, 2014.

X. Leroy, A formally verified compiler back-end, J. Autom. Reasoning, vol.43, issue.4, pp.363-446, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00360768

D. Lustig, G. Sethi, M. Martonosi, and A. Bhattacharjee, COATCheck: Verifying memory ordering at the hardware-OS interface, SIGOPS Oper. Syst. Rev, vol.50, issue.2, pp.233-247, 2016.

L. Maranget, S. Sarkar, and P. Sewell, A tutorial introduction to the ARM and POWER relaxed memory models, 2012.

D. P. Mulligan, S. Owens, K. E. Gray, T. Ridge, and P. Sewell, Lem: reusable engineering of real-world semantics, Proceedings of ICFP 2014: the 19th ACM SIG-PLAN International Conference on Functional Programming, pp.175-188, 2014.

M. O. Myreen, Verified just-in-time compiler on x86, Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.107-118, 2010.

,

R. S. Nikhil and N. N. Sharma, Forvis: A formal RISC-V ISA specification, pp.2019-2026, 2019.

S. Owens, S. Sarkar, and P. Sewell, A better x86 memory model: x86-TSO. In: Proceedings of TPHOLs 2009: Theorem Proving in Higher Order Logics, vol.5674, pp.391-407, 2009.

C. Pulte, The Semantics of Multicopy Atomic ARMv8 and RISC-V, 2019.

C. Pulte, S. Flur, W. Deacon, J. French, S. Sarkar et al., Simplifying ARM Concurrency: Multicopy-atomic Axiomatic and Operational Models for ARMv8, Proceedings of the 45th ACM SIGPLAN Symposium on Principles of Programming Languages, 2018.

A. Raad, J. Wickerson, G. Neiger, and V. Vafeiadis, Persistency semantics of the Intel-x86 architecture. PACMPL 4(POPL), vol.11, p.31, 2020.

A. Raad, J. Wickerson, and V. Vafeiadis, Weak persistency semantics from the ground up: Formalising the persistency semantics of ARMv8 and transactional models, Proc. ACM Program. Lang. 3(OOPSLA), vol.135, pp.1-135, 2019.

A. Reid, Trustworthy specifications of ARM v8-A and v8-M system level architecture, pp.161-168, 2016.

A. Reid, ARM releases machine readable architecture specification, 2017.

A. Reid, R. Chen, A. Deligiannis, D. Gilday, D. Hoyes et al., End-to-end verification of processors with ISA-Formal, Computer Aided Verification -28th International Conference, vol.9780, pp.42-58, 2016.

B. Romanescu, A. Lebeck, and D. J. Sorin, Address translation aware memory consistency, IEEE Micro, vol.31, issue.1, pp.109-118, 2011.

,

B. F. Romanescu, A. R. Lebeck, and D. J. Sorin, Specifying and dynamically verifying address translation-aware memory consistency, Proceedings of the Fifteenth Edition of ASPLOS on Architectural Support for Programming Languages and Operating Systems, pp.323-334, 2010.

S. Sarkar, K. Memarian, S. Owens, M. Batty, P. Sewell et al., Synchronising C/C++ and POWER, Proceedings of PLDI 2012, the 33rd ACM SIGPLAN conference on Programming Language Design and Implementation (Beijing), pp.311-322, 2012.
URL : https://hal.archives-ouvertes.fr/hal-01100798

,

S. Sarkar, P. Sewell, J. Alglave, L. Maranget, and D. Williams, Understanding POWER multiprocessors, Proceedings of PLDI 2011: the 32nd ACM SIGPLAN conference on Programming Language Design and Implementation, pp.175-186, 2011.
URL : https://hal.archives-ouvertes.fr/hal-01100824

S. Sarkar, P. Sewell, F. Zappa-nardelli, S. Owens, T. Ridge et al., The semantics of x86-CC multiprocessor machine code, Proceedings of POPL 2009: the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages, pp.379-391, 2009.

P. Sewell, S. Sarkar, S. Owens, F. Zappa-nardelli, and M. O. Myreen, x86-TSO: A rigorous and usable programmer's model for x86 multiprocessors, Communications of the ACM, vol.53, issue.7, pp.89-97, 2010.

H. Syeda and G. Klein, Reasoning about translation lookaside buffers, LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, pp.490-508, 2017.

H. T. Syeda and G. Klein, Program verification in the presence of cached address translation, Interactive Theorem Proving -9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC, pp.542-559, 2018.

Y. K. Tan, M. O. Myreen, R. Kumar, A. C. Fox, S. Owens et al., The verified CakeML compiler backend, J. Funct. Program, vol.29, p.2, 2019.

A. Waterman, . Jacob, C. F. Bachmeyer, A. J. Batten, A. Baum et al., document Version 20181221-Public-Reviewdraft. Contributors: Arvind, Krste Asanovi?, Rimas Avi?ienis, 2018.