-
Hints for Computer System Design
On the last day of my advanced OS course this spring we discussed one of my all-time favorite computer science papers: Butler Lampson’s Hints for Computer System Design. Why is it so good? It’s hard-won advice. Designing systems is not easy — a person can spend a lifetime learning to do it well — and…
-
How Should You Write a Fast Integer Overflow Check?
Detecting integer overflow in languages that have wraparound semantics (or, worse, undefined behavior on overflow, as in C/C++) is a pain. The issue is that programming languages do not provide access to the hardware overflow flag that is set as a side effect of most ALU instructions. With the condition codes hidden, overflow checks become…
-
Testing with Small Capacities
The goal of testing is to expose bugs. To find a bug we must drive the software under test into a part of its state space where the bug becomes evident, for example by causing a crash. Many bugs lurk in dark corners of the state space that are ordinarily difficult to reach. This piece…
-
Find the Integer Bug
Not all of the functions below are correct. The first person to leave a comment containing a minimal fix to a legitimate bug will get a small prize. I’m posting this not because the bug is particularly subtle or interesting but rather because I wrote this code for a piece about integer overflow and thought…
-
Research Advice from Alan Adler
Although I am a happy French press user, I enjoyed reading an article about Alan Adler and the AeroPress that showed up recently on Hacker News. In particular, I love Adler’s advice to inventors: Learn all you can about the science behind your invention. Scrupulously study the existing state of your idea by looking at…
-
A New Development for Coverity and Heartbleed
As a consequence of my last post, I spent some time on the phone Friday with Andy Chou, Coverity’s CTO and former member of Dawson Engler’s research group at Stanford, from which Coverity spun off over a decade ago. Andy confirmed that Coverity does not spot the heartbleed flaw and said that it remained stubborn…
-
Heartbleed and Static Analysis
Today in my Writing Solid Code class we went through some of the 151 defects that Coverity Scan reports for OpenSSL. I can’t link to these results but take my word for it that they are a pleasure to read — the interface clearly explains each flaw and the reasoning that leads up to it,…
-
xv6
I’m teaching a small Advanced Operating Systems course this spring. Preparing for the course over winter break, I spent some time reading various Linux subsystems such as the scheduler, and was a bit shocked at how complex it has become. I’ve been using Linux, looking at its code, and occasionally hacking it for more than…
-
Automated Reasoning About LLVM Optimizations and Undefined Behavior
Following up on last week’s toy use of Z3 and my LLVM superoptimizer post from a few weeks ago, I wanted to try to prove things about optimizations that involve undefined behavior. We’ll be working with the following example: Clang’s -O0 output for this code is cluttered but after running mem2reg we get a nice…
-
That Was Easy
I wanted to play around with the Python interface to Z3 and the classic SEND + MORE = MONEY puzzle seemed like a good way to get started. This turned out to be so easy that my code worked almost on the first try: Then: $ python ./send_more_money.py sat D = 7 S = 9…