-
How Much and What to Read?
Grad students often aren’t quite sure how much of their work time should be spent reading, and may also have trouble figuring out what to read during that time. (In principle this problem also applies to professors, but it’s not much of an issue in practice since we have almost no time for discretionary reading.)…
-
Preemption vs. Event Ordering
There’s no doubt that concurrent programming is hard, but it’s not always clear exactly why. Generally, eliminating data races is not the hard part. On the other hand, dealing with event ordering problems can be extremely difficult. To put that another way, if we remove preemption from the picture by programming with non-preemptive threads or…
-
Software Bugs and Scientific Progress
When a bug is found in a piece of software, the root cause is often a bug in someone’s thoughts. One way to better understand a bug is to look at how deep the underlying thought error was. In other words: How many assumptions must be revisited as a result of the bug? Level 1…
-
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…
-
Guidelines for Teaching Assistants
I’ve been teaching university-level courses for the last nine years, usually with the support of teaching assistants (TAs): students who get paid to do things like grading, office hours, fielding email questions, making and debugging assignments, proctoring exams, and perhaps even giving a lecture when I’m sick or traveling. At the start of each semester…
-
The Simplest Queue?
My student Jianjun is proving things about ARM executables that handle interrupts. It’s very difficult work, so when I asked him to write up a “simple” case study where an interrupt and the main context communicate through a ring buffer, I thought it would be helpful if I handed him the simplest possible queue that…
-
Negative Correlation Achieved
Recently I reviewed 19 papers that were submitted to CAV 2011. This is the first time I’ve been involved with a pure verification conference, and consequently I greatly enjoyed reading the papers because almost every one contained something new. Each time I submitted a review I looked at the ones that were already submitted for…
-
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…