-
Volatile Bugs, Three Years Later
Almost exactly three years ago Eric Eide and I submitted a paper Volatiles Are Miscompiled, and What to Do about It to the 8th International Conference on Embedded Software (EMSOFT 2008). The points made in this paper were that: C compilers fail to reliably translate accesses to volatile-qualified objects we can automatically detect these failures…
-
Who Verifies the Verifiers?
Verification tools, like all complex software systems, contain design flaws and implementation errors. Moreover, they are not necessarily very easy to test. The other day I started to address the question: If someone claims that a piece of software has been formally verified, what should you believe about the software? The previous piece was non-technical;…
-
The Future of Software System Correctness
A few weeks ago I re-read Tanenbaum et al.’s 2006 article Can We Make Operating Systems Reliable and Secure. They begin by observing that it would be nice if our general-purpose operating systems were as reliable as our cars and televisions. Unfortunately, Tanenbaum’s vision is being realized in the worst way: as the amount of…
-
A Critical Look at the SCADE Compiler Verification Kit
While searching for related work on compiler testing and certification, I ran across the SCADE Compiler Verification Kit: a collection of SCADE-generated C code along with some test vectors. The idea is to spot compiler problems early and in a controlled fashion by testing the compiler using the kinds of C code that SCADE generates.…
-
Non-deterministic Compilers?
Compilers are supposed to be deterministic, and they generally are. However, when a compiler has memory safety bugs (use of free memory, usually) and runs on an OS with ASLR (address space layout randomization) enabled, it can behave non-deterministically. Compile a file one time and the result is correct, compile the exact same file again…
-
Verifying a Driver
Last week my student Jianjun Duan gave a talk about his PhD work at the Workshop for Systems Software Verification in Vancouver. Although preliminary — he verified only three small functions — this work is pretty cool. Jianjun started with a model for the ARM instruction set in HOL4 and augmented it so that memory-mapped…
-
More Saturating Arithmetic
In a previous post I guessed that 91 bytes was close to the minimum size for implementing signed and unsigned saturating 32-bit addition and subtraction on x86. A commenter rightly pointed out that it should be possible to do better. Attached is my best shot: 83 bytes. Given the crappy x86 calling convention I’m going…
-
Fun With Saturating Arithmetic
An assignment that I often give my Advanced Embedded Systems class early in the semester is to implement saturating versions of signed and unsigned addition and subtraction. Saturating operations “stick” at the maximum or minimum value. (INT_MAX +sat 1) therefore evaluates to INT_MAX. The only wrinkle in the assignment is that solutions must be capable…
-
Volatile Structs Are Broken
For at least a year we’ve taken a break from reporting volatile bugs to C compiler developers. There were various reasons: the good compilers were becoming pretty much correct, we faced developer apathy about volatile incorrectness, our volatile testing tool had some weird problems, and basically I just got bored with it. Today my PhD…
-
Poll: Do You Want Compiler Bugs to Be Quiet or Loud?
I’m preparing a longer piece on compiler correctness but thought this idea was worth putting into its own short post. The question is: Which would you choose: A compiler that crashes more often, or one that silently generates incorrect code more often? Of course, all real compilers have bugs, and all real compilers display both…