Verifying Advanced Microarchitectures that Support Speculation and Exceptions
Abstract elided by the publisher.
Related papers
- Speculative Register Promotion Using Advanced Load Address Table (ALAT) CGO 2003
- SWOOP: software-hardware co-design for non-speculative, execute-ahead, in-order cores PLDI 2018
- Delayed Exceptions - Speculative Execution of Trapping Instructions CC 1994
- The Transmeta Code Morphing - Software: Using Speculation, Recovery, and Adaptive Retranslation to Address Real-Life Challenges CGO 2003
- Exploiting Idle Floating-Point Resources for Integer Execution PLDI 1998
- Towards efficient and verified virtual machines for dynamic languages CPP 2021
- SSMR: Statically Detecting Speculation Safe Memory Regions to Mitigate Transient Execution Attacks CC 2026
- Formally verified speculation and deoptimization in a JIT compiler POPL 2021