-
Some Goals for High-impact Verified Compiler Research
I believe that translation validation, a branch of formal methods, is just about ready for widespread use. Translation validation means proving that a particular execution of a compiler did the right thing, as opposed to proving once and for all that every execution of a compiler will do the right thing. These are very different.…
-
Publishing for Impact
Choices made in the process of doing research can lead to a 5-10x difference in number of publications for exactly the same underlying work. For example, do I publish my idea in a workshop, then a conference, and then a journal? On the other hand I can just do the conference version. Do I take…
-
Responsible and Effective Bugfinding
NB: This piece is not about responsible disclosure of security issues. For almost as long as people have written code, we have also worked to create methods for finding software defects. Much more recently, it has become common to treat “external bug finding” — looking for defects in other people’s software — as an activity…
-
Sid’s Mountain Backpacking Loop
Last fall my friend Brian and I went on a short backpacking trip in the San Rafael Swell. We left SLC early, drove to Ferron Utah, and then followed a high-clearance dirt road to the rim of North Salt Wash, a wide canyon that feeds the San Rafael River. We dropped into this open canyon…
-
It’s Time for a Modern Synthesis Kernel
Alexia Massalin’s 1992 PhD thesis has long been one of my favorites. It promotes the view that operating systems can be much more efficient than then-current operating systems via runtime code generation, lock-free synchronization, and fine-grained scheduling. In this piece we’ll only look at runtime code generation, which can be cleanly separated from the other…
-
Learning When Values are Changed by Implicit Integer Casts
C and C++ perform implicit casts when, for example, you pass an integer-typed variable to a function that expects a different type. When the target type is wider, there’s no problem, but when the target type is narrower or when it is the same size and the other signedness, integer values may silently change when…
-
Closing the Loop: The Importance of External Engagement in Computer Science Research
Computer scientists tend to work by separating the essence of a problem from its environment, solving it in an abstract form, and then figuring out how to make the abstract solution work in the real world. For example, there is an enormous body of work on solving searching and sorting problems and in general it…
-
A Conversation about Teaching Software Engineering
For better or worse, my impressions of software engineering as a field were shaped by a course I took as an undergrad that I thought was mostly not very interesting or useful. We spent a lot of time on waterfalls and stuff, while not covering testing in any detail. For the final project in the…
-
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…
-
Producing Good Software From Academia
Writing and maintaining good software from academia isn’t easy. I’ve been thinking about this because last week my student Yang Chen defended his thesis. While I’m of course very happy for him, I’m also depressed since Yang’s departure will somewhat decimate the capacity of my group to rapidly produce good code. Yang looked over my…