Public Reading group timetable for Memory Model/Compiler Verification Reading Group I run at Arm.
A place to collect all papers related to Memory Models, Compiler Verification, and anything with Cats!
Upcoming reading goes here, initial notes and errata will appear in each paper's directory (papers/01, 02 etc...) as they are read.
- George Necula. Translation Validation for an Optimizing Compiler. link
When reading, we aim try and answer the following (or question why they cannot be answered), Thank Nathan Chong for this template:
- What’s the big picture? What is the project trying to accomplish?
- How big is the project: people and KLOC? How much effort has it taken?
- What are the important components and how do they fit together?
- What exactly is being verified? Is it a neat statement, or is it a connection of properties… and, if so, what do they add up to?
- What are the key ideas? Underlying techniques? How applicable are they outside of C compilers?
- What assumptions are being made? Are they implicit or explicit? Are they reasonable?
- What is the trusted computing base needed to believe the result(s)?
- [optional] How are the projects related? Similar? Different? (this makes more sense if we cover a family of related papers)
- [optional] What key feature related to the writing of the paper stands out to you? is it the style of writing or the structure of the argument? etc...
No doubt on second reads, and in context, these questions may get different answers but this is a good first approximation.
Papers we should read after the above.
- Jaroslav Sevcik. Safe Optimisations for Shared-Memory Concurrent Programs. link.
- Jaroslav Sevcik et. al. CompCertTSO: A Verified Compiler for Relaxed-Memory Concurrency. link
- Viktor Vafeiadis and Francesco Zappa Nardelli. Verifying Fence Elimination Optimisations. link
- Mark Batty et. al, Clarifying and Compiling C/C++ Concurrency: from C++11 to POWER. link
- Mark Batty et. al. Mathematizing C++ Concurrency. link
- Dennis Shasha and Marc Snir. Efficient and correct execution of parallel programs that share memory. link
- Sarita Adve and Kourosh Gharcaloo. Shared Memory Consistency Models: A Tutorial. link
- Thomas Sewell, Magnus Myreen, and Gerwin Klein. Translation Validation for a Verified OS Kernel, link
- Xavier Leroy and Sandrine Blazy. Formal verification of a C-like memory model and its uses for verifying program transformations. link
- Zachary Tatlock and Sorin Lerner. Bringing Extensibility to Verified Compilers. link
- Jean-Baptiste Tristan and Xavier Leroy. Formal verification of translation validators: A case study on instruction scheduling optimizations. link
- Lennart Beringer et. al. Verified Compilation for Shared-memory C: link
- Venkatesh Srinivasan and Thomas Reps. Partial Evaluation of Machine Code: link
- Tachio Terauchi and Alex Aiken. Secure Information Flow As a Safety Problem link
- Luke Nelson, et.al Hyperkernel: Push-Button Verification of an OS Kernel. link.
- Martin Abadi et. al Control-Flow integrity, link
- Sergey Bratus et.al From Buffer Overflows to “Weird Machines” and Theory of Computation, link
- Martin Abadi. Protection in Programming-Language Translations, link
- Marco Patrignani et. al. Formal Approaches to Secure Compilation, link
- Carmine Abate et. al. Journey Beyond Full Abstraction: Exploring Robust Property Preservation for Secure Compilation, link
- Marco Patrignani and Deepak Garg. Secure compilation and hyperproperty preservation, link
- Carmine Abate. et. al. Trace-Relating Compiler Correctness and Secure Compilation, link
- Rebecca Shapiro et. al. “Weird Machines” in ELF: A Spotlight on the Underappreciated Metadata. link
- Sebastian Poeplau and Aurélien Francillon. Symbolic execution with SYMCC: Don’t interpret, compile!, link
- Steven Schäfer, Sigurd Schneider, and Gert Smolka. Axiomatic Semantics for Compiler Verification. link
- Leslie Lamport. win and sin: predicate transformers for concurrency. link
- Susan Owicki and David Gries. Verifying properties of parallel programs: an axiomatic approach. link
- Rahul Sharma et. al. Data-Driven Equivalence Checking. link.
- Benjamin Goldberg et. al. Into the loops: Practical issues in translation validation for optimizing compilers. link.
- Sudipta Kundu et. al. Automated refinement checking of concurrent systems. link.
- Sorin Lerner. et. al. Automatically Proving the Correctness of Compiler Optimizations. link.
- Jean-Baptiste Tristan and Xavier Leroy. Verified Validation of lazy code motion. link.
- Lenore Zuck et. al. Translation and run-time validation of loop transformations. link.
- Xavier Rival. Symbolic transfer function-based approaches to certified compilation. link.
- Ross Tate et. al. Equality saturation: A new approach to optimization. link
- Xavier Leroy, Formal verification of a realistic compiler, link
- Zhao et. al. Formalizing the LLVM Intermediate Representation for Verified Program Transformations (Vellvm), link
- Jean-Baptiste Tristan and Xavier Leroy. A simple, verified validator for software pipe-lining, link
- Luke Nelson et. al, Scaling symbolic evaluation for automated verification of systems code with Serval, link
- Thomas Dullian, Weird machines, exploitability, and provable unexploitability, link
- Jennifer Paykin et. al, Weird Machines as Insecure Compilation, link
- Soham Chakraborty and Viktor Vafeiadis. Validating Optimizations of Concurrent C/C++ Programs (this is also translation validation), link
- Jean-Baptiste, Paul Govereau, and Greg Morisset. Evaluating Value-graph translation validation for LLVM, link
- Sudipta Kundu, Zachary Tatlock, Sorin Lerner. Proving optimizations correct using parameterized program equivalence, link
- Viktor Vafeiadis et. al. Common Compiler Optimisations are Invalid in the C11 Memory Model and what we can do about it. link.
- Jade Alglave et. al. Don’t Sit on the Fence: A Static Analysis Approach to Automatic Fence Insertion. link.
- Jade Alglave et. al. Software Verification for Weak Memory via Program Transformation. link.
- Jade Alglave et. al. Fences in Weak Memory Models. link
- Jade Alglave et. al. Herding Cats - Modelling, simulation, testing, and data-mining for weak memory. link.
- Robin Morisset et. al. Compiler Testing via a Theory of Sound Optimisations in the C11/C++11 Memory Model. link
- Armstrong et. al. Isla: Integrating full-scale ISA semantics and axiomatic concurrency models. link
- Michalis Kokologiannakis and Viktor Vadeiadis. GenMC: A ModelC Checker for Weak Memory Models. link
- Leslie Lamport. How to Make a Correct Multiprocess Program Execute Correctly on a Multiprocessor link
- Christopher Lidbury et. al, Many-Core Compiler Fuzzing. link
- Le et. al. Compiler validation via equivalence modulo inputs.link
- Leslie Lamport. Time, Clocks, and the Ordering of Events in a Distributed System. link t