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.
SupportedVerified against the source
- 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¶
Does it exist? Confirmed. This work's DOI resolves to a registered record, which fixes its identity. That is all it fixes.
Does it back the claim? Read against the text for 1 of 2 citations: 1 supported. Each verdict is shown under its citation below, with what in the work backs the sentence.
Support is checked per citation rather than per work — the same source can be cited soundly in one article and wrongly in another. Per-citation recording began recently, so a citation with no recorded check is a gap in the record rather than evidence it went unchecked.
See how references were verified.
Registry ID ref:cd9b8d0fd3a2 · see in the full table