Reading List

arm manual
Anton Podkopaev, et al. Promising Compilation to ARMv8 POP (Extended Version) (copy)
Christonpher Pulte, et al. Simplifying ARM Concurrency: Multicopy-Atomic Axiomatic and Operational Models for ARMv8 (copy)
Christopher Pulte, et al. Promising-ARM/RISC-V: A Simpler and Faster Operational Concurrency Model (copy) (coq impl) (tr)

Yu Guo, et al. Modular Verification of Concurrent Thread Management (Extended Version) (copy)
Ni, et al. Using XCAP to Certify Realistic Systems Code: Machine Context Management (pdf)
BO-YUAN HUANG, et al. Instruction-Level Abstraction (ILA): A Uniform Specification for System-on-Chip (SoC) Verification (copy)

Crellvm:Verified Credible Compilation for LLVM
Daniel Patterson and Amal Ahmed, et al. The Next 700 Compiler Correctness Theorems (Funtional Pearl) (copy)

Xuejun Yang, et al. Finding and Understanding Bugs in C Compilers (copy)
Robin Morisset, et al. Compiler Testing via a Theory of Sound Optimisations in the C11/C++11 Memory Model (link)
Soham Chakraborty, et al. Validating Optimizations of Concurrent C/C++ Programs (link)
Jeehoon Kang, et al. Crellvm: Verified Credible Compilation for LLVM (link)
Nuno P. Lopes, et al. Alive2: Bounded Translation Validation for LLVM (link)

Ronghui Gu, et al. Deep Speciﬁcations and Certiﬁed Abstraction Layers (copy)
Ronghui Gu, et al. Certifed Concurrent Abstraction Layers (copy)
Preemptive OS Kernel Verification Framework (here is a book introducing uCos-III)
Hao Chen, et al. Toward Compositional Veriﬁcation of Interruptible OS Kernels and Device Drivers (copy)

Armin Biere, et al. Symbolic Model Checking without BDDs (copy)
EVGENII MOISEENKO, et al. Model Checking for a Multi-Execution Memory Model (OOPSLA'22) (pdf)
Michalis Kokologiannakis, et al. GenMC: A model checker for weak memory models (html)
Michalis Kokologiannakis, et al. Effective stateless model checking for C/C++ concurrency (POPL'18) (html)
Michalis Kokologiannakis, et al. HMC: Model Checking for Hardware Memory Models (pdf)
Jonas Oberhauser, et al. VSync: Push-Button Verification and Optimization for Synchronization Primitives on Weak Memory Models (ASPLOS'21) (copy)

A Course of Weak Memory Concurrency (link)
A Course: Semantics and tools for low-level concurrent programming (link)
Morisset's PhD thesis. Compiler Optimisations and Relaxed Memory Consistency Models (link)
Sung-Hwan Lee, et al. Promising2.0: Global Optimizations in Relaxed Memory Concurrency (copy)
Conrad Watt, et al. Repairing and Mechanising the JavaScript Relaxed Memory Model (copy)
Jeehoon Kang, et al. A Promising Semantics for Relaxed-Memory Concurrency (copy)
Kasper Svendsen, et al. A Separation Logic for a Promising Semantics (copy)
Anton Podkopaev, et al. Bridging the Gap between Programming Languages and Hardware Weak Memory Models (copy)
Azalea Raad, et al. On Library Correctness under Weak Memory Consistency (copy)
Hans-J. Boehm, et al. Threads Cannot be Implemented as a Library (copy)
Mark Batty, et al. Mathematizing C++ Concurrency (copy)
PhD thesis of Yang Zhang
Viktor Vafeiadis, et al. Relaxed Separation Logic: A Program Logic for C11 Concurrency (copy)
Taming release-acquire consistency

Tianqi Chen, et al. TVM: An Automated End-to-End Optimizing Compiler for Deep Learning (copy)

Chanadan Reddy, et al. Polyhedral Compilation for Domain Specific Languages (copy)
Chris Lattner, et al. MLIR: A Compiler Infrastructure for the End of Moore’s Law (copy)
Polyhedral Compilation as a Design Pattern for Compiler Construction (copy)

Xi Wang, et al. Towards Optimization-Safe Systems: Analyzing the Impact of Undefined Behavior (copy)

Parallelizing Compilers
A "parallelizing compiler" is typically a compiler that finds parallelism in a sequential program and generates appropriate code for a parallel computer.
Parallelizing Compilers for Multicores