It's Only Illegal If You Get Caught: Breaking Invariants and Getting Away with It
Presenter: Mehmet
Preview
Mehmet will present “It’s Only Illegal If You Get Caught: Breaking Invariants and Getting Away with It” by Raphaël Proust and Alan Mycroft.
Summary
The paper explains how invariants help manage larger code bases and argues why breaking them sometimes is necessary to implement certain functionality (e.g. JIT compilers need to cast a byte array to a function) or to implement certain algorithms efficiently (e.g. efficiency of some graph algorithms rely on mutating the marks on nodes). Then, the paper gives examples of languages giving ways to break invariants and how extending a language with new features (i.e. new semantic transition rules) may expose invariants that weren’t observable before. For example, in a language with no concurrency one can break and restore invariants inside a function in a way that isn’t observable by other functions however concurrency breaks this guarantee thus the programmer needs synchronization primitives to restore the opaqueness.
The paper proposes a solution of introducing “negative transition rules” that guard a transition rule and prohibit future transitions that break the guarding condition. They define an opaque keyword to demonstrate that. The state during computation of code block marked opaque is not observable from outside. The paper says that if the language developers keep this guarantee then it guarantees not breaking existing programs’ invariant breaking shenanigans. Then the paper gives two example extensions of a language showing how new features interact with opaque:
- Exceptions: Exception throws can expose state during middle of computation to callers of a function. To guarantee opaqueness the compiler needs to perform effect analysis to prove that opaque code blocks don’t throw exceptions outside.
- Concurrency: Proving opaqueness in presence of concurrency is trickier. The paper argues that the compiler may insert dynamic checks in cases it can’t prove.
As a note, this is an Onward! paper so it explores an idea rather than solving a problem fully like regular research papers.
Discussion
Nemanja pointed out that the case for exceptions for growing a language is somewhat contrived as most relatively mainstream languages that support exceptions support them from the get go.