-
Some Goals for High-impact Verified Compiler Research
I believe that translation validation, a branch of formal methods, is just about ready for widespread use. Translation validation means proving that a particular execution of a compiler did the right thing, as opposed to proving once and for all that every execution of a compiler will do the right thing. These are very different.…
-
The Real Problem with the US News Rankings
The latest list of Best Global Universities for Computer Science from US News has not been well received. For example, the Computing Research Association issued a statement saying that “Anyone with knowledge of CS research will see these rankings for what they are – nonsense – and ignore them. But others may be seriously misled.”…
-
The Dreaded Practice Talk
[I wrote a post with the same title in 2010; this is an updated version.] In a week you’ll be giving a talk about your work to 600 people at a conference, or perhaps to five people who will sign off (or not) on your thesis. Depending on your area and the type of talk,…
-
Undefined Behavior in 2017
This post is jointly authored by Pascal Cuoq and John Regehr. Recently we’ve heard a few people imply that problems stemming from undefined behaviors (UB) in C and C++ are largely solved due to ubiquitous availability of dynamic checking tools such as ASan, UBSan, MSan, and TSan. We are here to state the obvious —…
-
The Zion Subway
When Josh, my older son’s best friend’s dad, suggested that we take our combined kids through the Left Fork of North Creek in Zion National Park (more commonly called The Subway), I wasn’t immediately excited. For one thing, it’s a somewhat technical canyon, and for another the permit that we got was for mid-May, towards…
-
Pointer Overflow Checking is in LLVM
Production-grade memory safety for legacy C and C++ code has proven to be a frustratingly elusive goal: plenty of research solutions exist but none of them appear to be deployable as-is. So instead, we have a patchwork of partial solutions such as CFI, ASLR, stack canaries, hardened allocators, and NX. Today’s quick post is about…
-
Compiler Optimizations are Awesome
This piece, which I hadn’t gotten around to writing until now since I thought it was all pretty obvious, explains why Daniel J. Bernstein’s talk, The death of optimizing compilers (audio) is wrong, and in fact compiler optimizations are extremely wonderful and aren’t going anywhere. First, the thesis of the talk is that almost all…
-
Translation Validation of Bounded Exhaustive Test Cases
This piece is jointly authored by Nuno Lopes and John Regehr. Compilers should be correct, but it is not straightforward to formally verify a production-quality compiler implementation. It is just too difficult to recover the high-level algorithms by looking at an enormous mess of arithmetic, loops, and memory side effects. One solution is to write…
-
Spring 2017
The hills above Salt Lake City are finally turning green. Earlier in the year my family took a short trip to southeast Utah but it rained so much one day that I didn’t think the dirt roads would be passable, so we visited Ratio, a land art installation near Green River UT. The next day…
-
Taming Undefined Behavior in LLVM
Earlier I wrote that Undefined Behavior != Unsafe Programming, a piece intended to convince you that there’s nothing inherently wrong with undefined behavior as long as it isn’t in developer-facing parts of the system. Today I want to talk about a new paper about undefined behavior in LLVM that’s going to be presented in June…