-
Who Fuzzes the Fuzzer?
Although it’s fun to act like our tool Csmith is an infallible compiler smashing device, this isn’t really true. Csmith is made of ~40,000 lines of C++, some of it quite complicated and difficult. Csmith probably contains about as many bugs per LOC as your average compiler. So how do we debug the bug-finding tool?…
-
One Day of Winter and Three Days of Spring in the Fins
Bill and I had already made two attempts to backpack into the Fins area, which is part of Ernie’s Country in the Maze District of Canyonlands NP. Spring 2010 was abnormally snowy and Fall 2010 featured torrential rains, both times making roads impassable. This time — Spring 2011 — the weather cooperated. Also it was…
-
Software Bugs and Scientific Progress
When a bug is found in a piece of software, the root cause is often a bug in someone’s thoughts. One way to better understand a bug is to look at how deep the underlying thought error was. In other words: How many assumptions must be revisited as a result of the bug? Level 1…
-
Proposal for a CompCert Superoptimizer
CompCert is a C compiler that is provably correct. It is best characterized as lightly optimizing: it performs a number of standard optimizations but its code improvements are not aggressive when compared to those performed by GCC, Clang, or any number of commercial tools. This piece is about what I believe would be a relatively…
-
Peer Review Poker
Peer review is a bureaucratic, consensus-based approach to making decisions. Thus, it is not inherently entertaining and authors like myself need to amuse ourselves as best we can. One of the games I like to play is peer review poker, where certain combinations of review scores are more desirable than others. Straight: Review scores form…
-
Finding and Understanding Bugs in C Compilers
Today we finished preparing the camera-ready version of our paper that will appear in PLDI 2011. I’m pretty happy with it. Here’s the abstract: Compilers should be correct. To improve the quality of C compilers, we created Csmith, a randomized test-case generation tool, and spent three years using it to find compiler bugs. During this…
-
Race Condition vs. Data Race
A race condition is a flaw that occurs when the timing or ordering of events affects a program’s correctness. Generally speaking, some kind of external timing or ordering non-determinism is needed to produce a race condition; typical examples are context switches, OS signals, memory operations on a multiprocessor, and hardware interrupts. A data race happens…
-
Guidelines for Teaching Assistants
I’ve been teaching university-level courses for the last nine years, usually with the support of teaching assistants (TAs): students who get paid to do things like grading, office hours, fielding email questions, making and debugging assignments, proctoring exams, and perhaps even giving a lecture when I’m sick or traveling. At the start of each semester…
-
The Simplest Queue?
My student Jianjun is proving things about ARM executables that handle interrupts. It’s very difficult work, so when I asked him to write up a “simple” case study where an interrupt and the main context communicate through a ring buffer, I thought it would be helpful if I handed him the simplest possible queue that…
-
Negative Correlation Achieved
Recently I reviewed 19 papers that were submitted to CAV 2011. This is the first time I’ve been involved with a pure verification conference, and consequently I greatly enjoyed reading the papers because almost every one contained something new. Each time I submitted a review I looked at the ones that were already submitted for…