Embedded in Academia

Category: Software Correctness

  • 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…

  • Wanted: Invariant-Based Synchronization

    Although a significant fraction of the programming languages community works on detecting race conditions in multi-threaded software, I haven’t been able to get very excited about this. Certainly race-free programs have some nice properties, but race freedom is neither a necessary nor sufficient condition for concurrency correctness. This research area doesn’t feel to me like…

  • Independence in N-Version Programming

    N-version programming is a way to reduce the impact of software bugs by independently implementing the same specification N times, running the implementations in parallel, and using voting to heuristically choose the right answer. A key weakness of N-version programming is that the increased reliability is predicated on faults occurring independently. As Knight and Leveson…

  • Compiler Bug-Finding Project Milestones

    Despite the Fall semester being crappy for me (double course load, and I keep getting sick) this project has made good progress: Xuejun gave a talk at the LLVM Developer’s Meeting We submitted our 300th compiler bug report (up from 200 in March 2010) We submitted a paper to PLDI 2011 summarizing our methods and…

  • Counting Compiler Crashes

    This is a bit of material from my GCC Summit talk that I thought was worth bringing out in a separate post. As an experiment, we compiled 1,000,000 randomly generated C programs using GCC 3.[0-4].0, GCC 4.[0-5].0, LLVM-GCC 1.9, LLVM-GCC 2.[0-8], and Clang 2.[6-8]. All compilers targeted x86 and were given the -O0, -O1, -O2,…

  • 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…

  • GCC Summit Talk

    I’m at the 2010 GCC Summit in Ottawa today. There’s a lot of interesting work going on; I’ll probably write a more detailed post later. In the meantime, the slides from my talk on finding compiler bugs are below. GCC Summit 2010 View more presentations from regehr.

  • 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…

  • 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…