Trip report from SOSP 2007

I spent the last few days at SOSP 2007, the latest instantiation of a biennial conference on operating systems research. This was held in Stevenson, WA, along the Columbia River Gorge about 45 miles east of Portland.

General observations:

• This area is absolutely gorgeous in the fall. Living in California, I tend to forget about the whole trees-changing-colors thing in the fall. We had a couple of days of nice weather at the beginning of the conference and the views of the river and surrounding hills were just spectacular. Of course by the end of the conference we had cold drizzling rain and I remembered why I don't live there.
• For anyone looking for good brewpubs in the area, I highly recommend checking out Walking Man Brewery in Stevenson. The place doesn't look like much, but they had a very nice barleywine and imperial IPA, as well as a good standard IPA and stout. The smoked salmon pizza was also excellent. Double Mountain Brewery in Hood River, OR is also worth a visit.
• The fact that SOSP included 3 papers on OS support for Javascript is a sad reflection of the state of computing. Nothing against the authors of the papers (who were trying to find solutions to real problems), but ~50 years after the introduction of FORTRAN, LISP, and Algol 60, is this the best we can come up with?
• A lot more people care about byzantine fault tolerance (at least in the research community) than I would have thought possible.

Comments on specific talks:

• TxLinux: this looks at how to map the synchronization primitives in Linux (mostly spinlocks) onto transactional memory primitives. Nothing earthshattering, but some decent practical work, including looking at issues like dealing with I/O interrupts in the middle of a transaction, scheduling changes, and priority inversion. One of the problems with moving to new hardware paradigms (such as different consistency models or transactional memory) is figuring out what to do with all of that legacy code, most prominently operating systems, programming language runtimes, and large application platforms like databases.
• Triage: the goal here is to automatically debug problems onsite after a fault is detected (e.g., program crash). The main idea is to use checkpoints to back up to (hopefully) prior to the fault, and replay to introduce different variations to help detect the problem. E.g., if the problem goes away depending on scheduling order it's probably some sort of race condition. The implementation was focused on user level programs using OS checkpoint/replay support but I don't see any reason it wouldn't work for OS kernels (or more complex multi-process applications) with VM based checkpoint/replay.
• iComment: the basic idea here was to apply natural language processing (plus some manually constructed "filters") to infer program assumption based on comments. Aside from the fact that the testbed was the Linux kernel, this didn't really have anything to do with operating systems - the techniques would apply equally well (or equally poorly) to any sufficiently complex application. The assumption of this work is that developers are sufficiently mechanical in the way they write comments (e.g., "assumes lock is held" in the comment that prefaces a function) that a program can infer meaning and automatically test for correctness. But if we're so mechanical, why not use more formal annotations to express intent? The most prominent example of this is ASSERTs, which serve as both verifiable statements of intent and documentation of assumptions. I'd be more interested in research on what other types of annotations would be useful, and perhaps some analysis of why annotations haven't caught on, than in "fuzzy" natural language techniques.
• SecVisor: this project looked at using a small hypervisor (and hardware virtualization support a la SVM or VT) to prevent illicit kernel code execution. The hypervisor used shadow page tables to control the memory permissions, preventing kernel code from being modified or execution of text or user memory while in kernel mode. This relies on being able to detect when the processor switches between user and kernel mode (by tracing the entry/exit points), so that pages can be remapped (e.g., restoring user level execute permissions when exiting the kernel). Of course this assumes a static kernel text - supporting loadable kernel modules gets more complicated (the hypervisor has to get involved in loading the text and doing appropriate validation to make sure the module is OK).