Embedded in Academia

Category: Software Correctness

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

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

  • The Little C Function From Hell

    The other day a student and I were trying to understand a subtle part of the C standard. Often, the easiest way to clarify this kind of issue is to recognize that compiler writers have already grappled with it — so just write some code and see what various compilers do with it. I wrote…

  • Better Testing With Undefined Behavior Coverage

    [The bit puzzle results are based on data from Chad Brubaker and the saturating operation results are based on data from Peng Li. They are respectively an undergrad and a grad student in Utah’s CS program.] Klee is a tool that attempts to generate a collection of test cases inducing path coverage on a system…

  • Undefined Integer Behaviors in Student Code, Part 2

    [This post is based on data gathered by my student Peng Li. He also wrote the undefined behavior checker.] The other day I posted about undefined integer behaviors in code written by students in a class I used to teach. This post is more of the same, this time from CS 5785, my advanced embedded…

  • How to Write a C/C++ Compiler That Respects Volatile

    The volatile type qualifier in C/C++ means roughly that accesses to the qualified object happen on the actual machine as they do in the abstract machine. I’ve written about volatile pretty extensively, so won’t repeat myself. An interesting problem with volatile is that in practice, compilers fail to respect it: they add, remove, and reorder…

  • Differential Whitebox Testing Is Good

    [This post is based on data gathered by Chad Brubaker and Peng Li, respectively an undergrad and grad student in CS at Utah.] Two courses I’ve taught at Utah, CS 4400 and CS 5785, have assignments where students write short integer functions for which we — the instructors — have automatic graders. In 4400 the…

  • Visualizing A Few More Math Bugs

    As a followup to last night’s post, here are some saturating signed subtraction functions I’ve received. Hopefully the correct one is obvious.

  • Visualizing Math Bugs

    After getting too tired to work tonight, I realized I had no Netflix and that I’m bored with the books I’m reading. Therefore, I present visualizations of several solutions I’ve received to my saturating arithmetic homework over the years. This is what a correct saturating signed add looks like, where the z-axis is the output:…