Category: Software Correctness

  • Scary Compiler Code Motion

    I ran across this blog post about reader-writer locks and thought it would be fun to present them to the Advanced Operating Systems class that I’m running this spring. Here’s my version of the code, which needed to be adapted a bit to work with GCC: At first I was suspicious that some sort of…

  • Use of Assertions

    Assertions are great because they: support better testing, make debugging easier by reducing the distance between the execution of a bug and the manifestation of its effects, serve as executable comments about preconditions and postconditions, can act as a gateway drug to formal methods. Assertions are less than great because they: slow down our code,…

  • Writing Solid Code Week 4

    This week most of the students in the class (but not everyone, since we ran out of time) presented their arguments about the quality of various UNIX utility programs. This was a bit more interesting than it might otherwise have been since some of the utilities running on our student lab machines are hilariously old…

  • Writing Solid Code Week 3

    This week we finished up the triangle classifier. Not all students’ implementations pass all test cases, which is totally fine with me as long as people learned some lessons about when not to use floating point (I did). On Tuesday we also chose a smallish UNIX utility for each student to evaluate as if it…

  • Status of Software Testing

    The other day I received a query from some software engineering researchers who are compiling sort of a survey paper about the status of software testing research; here are the questions, with my answers. I’m interested to hear what the rest of you think about this stuff. What do you think are the most significant…

  • Writing Solid Code Week 2

    First, I wanted to thank everyone for the great discussion on the post about week 1. My single favorite thing about blogging is the discussion and involvement that these posts sometimes generate. During week 2 we worked on issues relating to the triangle classifier. As several commenters predicted, getting correct results using floating point code…

  • Writing Solid Code Week 1

    This semester I’m teaching a new undergraduate course called Writing Solid Code. The idea is to take a lot of lessons I’ve learned on this subject — testing, debugging, defensive coding, code reviews, etc. — and try to teach it. Since I don’t have any slides or even any lecture notes that are good enough…

  • Finding Wrong-Code Bugs in the Wild

    Compiler developers already have some decent ways to find bugs: a self-hosting compiler won’t bootstrap if it’s too buggy any serious compiler has a test suite commercial compiler validation suites are available random testcase generators like Csmith and CCG can expose subtle bugs Of course, these tests don’t find all of the bugs. The remaining bugs…

  • C-Reduce and Frama-C

    Yesterday Pascal wrote a nice article addressing practical issues in automated testcase reduction. One issue is that C-Reduce tends to give you what you asked for instead of what you really wanted. Of course, this problem is a common one when performing algorithmic searches. Beyond computer science, the same problem comes up in basically every…

  • Informative Assertion Failures

    The other day a student was asking me how to make assertion failures in software more informative. I told him there are two pretty easy ways to do this. First, define a customized assert that takes two arguments: the predicate and also a description. For example, in the Botan crypto library we see lines like…