Towards Optimization-Safe Systems¶
Wang, X., Zeldovich, N., Kaashoek, M. F., & Solar-Lezama, A. (2013). Towards Optimization-Safe Systems: Analyzing the Impact of Undefined Behavior. ACM, 260-275.
Cited by¶
2 citations across 2 artifacts.
Each citation links to the sentence it supports in the citing article.
Primes¶
- Equivalence-Preserving Rewriting
- The canonical instance is the compiler optimisation that is "correct" under the language-standard equivalence but "wrong" under the programmer's intuitive model — the equivalence relation is doing work the user did not notice.
This sourceDocuments 'optimization-unstable code' — code an optimizer discards because it is technically correct under the language standard's undefined-behavior rules yet violates the programmer's intuitive model; the canonical instance of an equivalence relation (the language standard) doing work the user did not notice.
- The canonical instance is the compiler optimisation that is "correct" under the language-standard equivalence but "wrong" under the programmer's intuitive model — the equivalence relation is doing work the user did not notice.
Domain-specific¶
- Integer Overflow
- Signed overflow in C is undefined behaviour, giving the compiler latitude to assume it cannot happen and optimise accordingly, which can silently eliminate the overflow check the programmer thought they wrote.
This sourceDocuments compilers exploiting undefined behaviour to delete programmer-written overflow checks, with signed integer overflow listed among C's undefined behaviours and real instances in FFmpeg, Postgres and Plan9port.
- Signed overflow in C is undefined behaviour, giving the compiler latitude to assume it cannot happen and optimise accordingly, which can silently eliminate the overflow check the programmer thought they wrote.
Verification¶
This reference passed the adversarial substantiation pipeline: it was checked to exist and to support the claim it is attached to. See how references were verified.
Registry ID ref:cd9b8d0fd3a2 · see in the full table