Undefined, Unspecified, Non-deterministic, and Implementation Defined Behavior
summary
Taxonomy of specification holes compares undefined behavior, undefined values and non-determinism and shows why both undefined forms break falsifiability: a single division‑by‑zero can act like a hidden state bit that lets a core produce arbitrary results later, forcing verification to solve a halting‑problem–style proof. RISC‑V defines divide‑by‑zero, prefers implementation‑defined behavior for things like unaligned accesses and optional CSRs, and keeps non‑determinism only for the memory model.
AI-written summary · about
chapters (8)
- 0:00Intro
- 1:10Users of an ISA Specification
- 2:20Taxonomy of not specified stuff
- 5:07Undefined Behavior. Can a correct implementation produce the following trace?
- 7:27Undefined Value: Can a correct implementation produce the following trace?
- 9:45Fully Specified Behavior
- 9:59Specification holes in RISC-V Spec
- 11:14Conclusion (2/2)
related talks
58mGarbage In, Garbage Out: Arguing about Undefined Behavior...
54mUndefined Behaviour is awesome!
49mUndefined Behavior in 2017 (part 1 of 2)
46m“My Little Optimizer: Undefined Behavior is Magic"
49m“Which Machine Am I Coding To?”
15mSymbolic MRD: Dynamic Memory, Undefined Behaviour, and Extrinsic Choice
56mOmnisemantics: Smooth Handling of Nondeterminism (Invited talk)
17mCode-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into(…)