-
Fuzzers Need Taming
[This post explains a paper that we recently made available; it’s going to be presented at PLDI 2013.] Random testing tools, or fuzzers, are excellent at finding bugs that human testers miss. A particularly important use case for fuzzing is finding exploitable bugs, and companies such as Google use clusters to do high-throughput fuzzing. Whether…
-
Stochastic Superoptimization
“Stochastic Superoptimization” is a fancy way to say “randomized search for fast machine code.” It is also the title of a nice paper that was presented recently at ASPLOS. Before getting into the details, let’s look at some background. At first glance the term “superoptimization” sounds like nonsense because the optimum point is already the best one.…
-
Exhaustive Testing is Not a Proof of Correctness
It is often said that exhaustively testing a piece of software is equivalent to performing a proof of correctness. Although this idea is intuitively appealing—and I’ve said it myself a few times—it is incorrect in a technical sense and also in practice. What’s wrong with exhaustive testing in practice? The problem comes from the question:…
-
Proofs from Tests
An idea that I’ve been interested in for a while is that a good test suite should be able to directly support formal verification. How would this work, given that testing usually misses bugs? The basic insight is that a test case is usually telling us about more than just one execution: it’s telling us…
-
str2long Contest Results Part 1
[NOTE: Reading this post only makes sense if you read and cared about this previous post.] Ok, evaluating the submissions has been more work than I anticipated, and also things have gotten pretty busy at work, so I’m going to split the evaluation of the submissions into two parts. This first part will discuss objective…
-
A Quick Coding Contest: Convert String to Integer Without Overflow
UPDATE: As of Saturday March 9, the contest is closed. Results will be posted in a few days. I’ve created a Github repository containing all submissions and my test harness. Regular readers will know that I’m obsessed with integer overflows. One apparently simple piece of code that many programmers get wrong in this respect is…
-
Four Books on Debugging
It often seems like the ability to debug complex problems is not distributed very evenly among programmers. No doubt there’s some truth to this, but also people can become better over time. Although the main way to improve is through experience, it’s also useful to keep the bigger picture in mind by listening to what…
-
Undefined Behavior Executed by Coq
I built a version of OCaml with some instrumentation for reporting errors in using the C language’s integers. Then I used that OCaml to build the Coq proof assistant. Here’s what happens when we start Coq: [regehr@gamow ~]$ ~/z/coq/bin/coqtop intern.c:617:10: runtime error: left shift of 255 by 56 places cannot be represented in type ‘intnat’…
-
How to Fuzz an ADT Implementation
Sometimes the standard libraries don’t meet your requirements. When this happens you might grab an open source b-tree, splay tree, Judy array, or whatever, or you might implement something yourself. This post is about the situation where you have some code for a data structure, you also have some unit tests, but even so you…
-
Simplest Program Showing the Difference Between Sequential Consistency and TSO
The effects of weak memory models on programs running on shared-memory multiprocessors can be very difficult to understand. Today I was looking for the simplest program that illustrates the difference between sequentially consistent execution and TSO (the memory model provided by x86 and x86-64). Based on an example from Section 8.2.3.4 of the big Intel…