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. ,
The semantics of Power and ARM multiprocessor machine code, Proc. DAMP 2009, 2009. ,
, The diy7 tool, pp.2019-2026, 2019.
The herd7 tool, pp.2019-2026, 2019. ,
, The litmus7 tool, pp.2019-2026, 2019.
Fences in weak memory models, Proc. CAV, 2010. ,
URL : https://hal.archives-ouvertes.fr/hal-01100859
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
, , 2011.
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.
, , 2019.
, Proc. 46th ACM SIGPLAN Symposium on Principles of Programming Languages, vol.3, 2019.
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. ,
Reasoning about the ARM weakly consistent memory model, 2008. ,
riscv-plv risc-v isa formal specification, pp.2019-2026, 2019. ,
The ARMv8 application level memory model, 2016. ,
Komodo: Using verification to disentangle secure-enclave hardware from software, Proceedings of the 26th Symposium on Operating Systems Principles, pp.287-305, 2017. ,
, , 2017.
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
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
The x86isa books: Features, usage, and future plans, Proceedings 14th International Workshop on the ACL2 Theorem Prover and its Applications, pp.1-17, 2017. ,
,
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. ,
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. ,
Cer-tiKOS: An extensible architecture for building certified concurrent OS kernels, 12th USENIX Symposium on Operating Systems Design and Implementation, pp.653-669, 2016. ,
Certified concurrent abstraction layers, Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp.646-661, 2018. ,
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.
Comprehensive formal verification of an OS microkernel, ACM Transactions on Computer Systems, vol.32, issue.1, 2014. ,
CakeML: a verified implementation of ML, The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, pp.179-192, 2014. ,
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
COATCheck: Verifying memory ordering at the hardware-OS interface, SIGOPS Oper. Syst. Rev, vol.50, issue.2, pp.233-247, 2016. ,
A tutorial introduction to the ARM and POWER relaxed memory models, 2012. ,
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. ,
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. ,
,
Forvis: A formal RISC-V ISA specification, pp.2019-2026, 2019. ,
, A better x86 memory model: x86-TSO. In: Proceedings of TPHOLs 2009: Theorem Proving in Higher Order Logics, vol.5674, pp.391-407, 2009.
The Semantics of Multicopy Atomic ARMv8 and RISC-V, 2019. ,
Simplifying ARM Concurrency: Multicopy-atomic Axiomatic and Operational Models for ARMv8, Proceedings of the 45th ACM SIGPLAN Symposium on Principles of Programming Languages, 2018. ,
, Persistency semantics of the Intel-x86 architecture. PACMPL 4(POPL), vol.11, p.31, 2020.
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. ,
, Trustworthy specifications of ARM v8-A and v8-M system level architecture, pp.161-168, 2016.
ARM releases machine readable architecture specification, 2017. ,
End-to-end verification of processors with ISA-Formal, Computer Aided Verification -28th International Conference, vol.9780, pp.42-58, 2016. ,
Address translation aware memory consistency, IEEE Micro, vol.31, issue.1, pp.109-118, 2011. ,
,
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. ,
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
,
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
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. ,
x86-TSO: A rigorous and usable programmer's model for x86 multiprocessors, Communications of the ACM, vol.53, issue.7, pp.89-97, 2010. ,
Reasoning about translation lookaside buffers, LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, pp.490-508, 2017. ,
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. ,
The verified CakeML compiler backend, J. Funct. Program, vol.29, p.2, 2019. ,
, document Version 20181221-Public-Reviewdraft. Contributors: Arvind, Krste Asanovi?, Rimas Avi?ienis, 2018.