Extended Discussion

Jay started with the size of the Flux OS Toolkit. It's about 250,000 lines of code, of which they wrote about 15,000 (the rest they steal). There are basically three kinds of components. The first is low-level kernel support library in boot-strap that sets up the PC and the segment tables, a minimal C library, etc. This provides a subset of POSIX envrionment for applications that want to be kernel and allows low-level kernel code re-use. Another class of components are device drivers. Besides Linux and FreeBSD drivers, there is also a subset of COM interface (which they steal from Microsoft - good ideas come from everywhere). A third type of component is the high-level components such as networking and file system. The idea is that we provide the body parts, you provide the head and the brain.

Jay then gave a "hello world" kernel example. It's only about 5 lines of code. It boots and prints the message on the console. A more complicated example was shown which use device drivers and the file system. Function calls such as fdev_init(), fdev_linux_initall() etc. initialize the device drivers. fs_netbsd_init() initialize the NetBSD file system.

Jay then went on describing the design issues. The toolkit is designed to be usable either as a whole or in arbitrary subsets. You don't have to use the components if you don't want to. Also the OS Kit currently runs on x86 PCs, It is designed to be portable to other architectures.

There were quite a few success stories: A graduate stuent who didn't know anything abut OS and a part-time undergraduate programmer took over a month to get ML booting. SR took a couple of weeks, x-kernel took only one day, etc.

Finally Jay concluded his talk by quoting Gabriel's paper which argues that implementation simplicity is more important than interface perfection, or in other words, "Worse is Better". Jay and his collegues believe the OS toolkit idea is the essence of "worse is better". The OS Kit was evolved from 5 years of OS research. Its surprising popularity shows that pragmatic and client-driven approach to reuse software component is the right approach.

Discussion:

• Margo Selzer (Harvard University) expressed the concern on the restrictiveness of the OS Kit, e.g. the assumptions that are built into the locore or device driver interface such as pre-emptibility. Jay responded that it depends on the device drivers. The device drivers weren't written for SMP. They still work in SMP case, but not highly efficiently. Also you don't want to give the users complete access to the hardware.

• Stefan Savage (University of Washington) commented that they did something similar in SPIN and asked how hard was it to deal with vendor upgrades (e.g. device drivers). Jay responded that since most upgrades in device drivers don't change a lot. They had two upgrades and it took about 1 week for a student to do it.

• Brian Bershad (University of Washington) pointed out that another problem of using other's code is implicit semantics of the code we borrow. Often there is miss communication about what is collectable and what is not. Jay responded that you can use a conservative garbage collector like Java does.

(In Jay's words) Jay has told us why "worse is better", now Patrick, the next speaker also from the University of Utah is going to tell us why "better is better". The title of his talk is "Formal Methods: A Practical Tool For OS Implementors". The idea is to bring mathematics and strong consistent logic into design of engineering to make sure the system is running inthe right direction.

Patrick started by pointing out that formal methods are very relevant to OS becuase operating systems are designed to be concurrent and non-deterministic. At the same time, they must be highly reliable and robust. Formal methods were designed to attack problems of complex systems that need to be done reliably. Patrick attributed the lack of formally verified OSs to three common believes: First, the tools that the formal methods community has come up with are complicated and inaccessible; Second, thre would be a gap between the abstract model to be verified and the actual implementation; Third, the OSs are just too big to be modeled this way.

Patrick then gave a brief overview of formal methods. There are two classes of formal method tools: theorem provers and model checkers. Theorem provers operate at a high level that take axioms, pre-conditions and generate proves. The disadvantage is that they require skilled intervention. Model checkers are more accessible tools. You provide a model, the model checker then tries everything the model can do and reports deadlocks if it finds any. The model checker they used is SPIN from New Jersy.

Their target is the IPC subsystem, a large (about a third to a quarter of the kernel source) and important part of the kernel. The IPC subsystem is also quite complicated. It supports multiple fine-grain locks and roll-back operations. It's also been optimized for speed a number of times. The goal is to get concurrency analysis of the system, e.g. finding dead-lock and live-lock issues, and apply these results to an SMP or a pre-emptive implementation of the kernel. Their approach is to manually translate the C code into Promela, the input specification for the SPIN model checker. They were able to find a couple of bugs in the IPC subsystem, one deadlock and one live lock.

Patrick then briefly described some issues relevant to using formal methods in operating systems. First is the scale of validated systems. They currently cannot verify the entire operating systems yet. This leads to the open issue of composition of separately validated sub-systems. The other issue is maintenance of the model with the implementation since the model is translated from the language the system is implemented in. Some methods to automatically generate both versions should be used in the future. The next issue is the cost vs. traditional methods and finally expoiting code structure that hinders effort of translation.

In conclusion, the formal methods are accessable (to naive grad students). The tools provided by the formal methods community are adequate. Significant components of an OS can be verified and checked. These results can apply directly to the implementation of the OS, not just the model you intend to implement.

Discussion:

• Dave Presotto (Bell Labs) pointed out that the problem with Promela in general has been that it always finds bugs that no one has ever hit. The ones that it seems to miss are from other parts of the operating system. Even worse is that after they have verified the current model, they then change the code and the changes will not be verified. Dave wondered if Patrick had any experience of continuing coding after proving the system. Patrick said that they haven't made significant changes to the IPC subsystems. There were some bugs due to over-abstraction of the existing implementation and some details that were left out. But the big chunk of logic were translated and they have pretty close source-to-source relationship.

• Margo Selzer (Harvard University) raised the doubt about Patrick's claim that you said that he has conclusive proof of the implementation. Her argument was that since you had to do the translation manually, therefore you can only say that you have proof about somebody's interpretation of the implementation. Patrick said that the translation is pretty close, albeit some difficulties in dealing with C pre-processor macro and different naming conventions in coding.

• Freeman Rawson III (IBM) commented that in order to do this in a serious basis, one does need to be able to generate the model checking and the eventual object code from the same set of sources. He mentioned that the peopel who work in CAD tools for semiconductors have models very similar to this and they would regard this scheme as too unreliable. Patrick said there is some active work at Cornell and Wisconsin that aims to achieve this.

Panel Discussion

• The first round of discussions are focued on formal methods. John Carter (University of Utah) asked the entire panel would formal methods have helped the Workplace OS project at IBM and what kind of lessions can you take away from the talk. Freeman Rawson (IBM) answered that some level of formalization would have helped. Brett Fleisch (University of California, Riverside) commented that it was not clear how formal methods could have helped the power management component of the IBM micro kernel. Patrick added that their model checker focuses on deadlock detection and probably wouldn't help.

• David Presotto (Bell Labs) pointed out that the goal of measuring the IPC primitives should be to look at how much these primitives contribute to the actual speed of the application. Since the way each system is composed could vary a lot, you can't just compare primitives of two kernels with very different structures. The right approach is to compare the end-to-end application performance. Jochen agreed that it's important to measure the applications, but you still need to know the basic architectal cost.

• Jeffrey Mogul (DEC Western Research Lab) gave the analogy of a 90 miles/gallon car vs. a 2 miles/gallon bus. If the goal is to carry 50 persons, then it might be better to use the bus. Brian Bershad (University of Washington) also pointed out that this is like Popeye effect where IPC is like the spinach. If your system is strong, that means your IPC is strong. But the fact might be that Popeye is strong because he works out. IPC might not have anything to do with the end-to-end performance. Freeman pointed out that in their implementation IPC performance was relevant. On the other hand, David Black (Open Group Research Institute) said that they ran Linux on Mach and the performance is comparable to monolithic system.

• David Cohn (IBM) asked if IPC cost were zero, will IBM micro kernel be successful? Freeman Rawson III (IBM) said that multi-personality would not have been successful if the IPC cost were zero. Brett Fleisch (University of California, Riverside) added that personalities of the IBM microkernel is not going to scale.

• Noah Mendelsohn (Lotus Development) was confused why this discussion on IPC took so long. He said it's clear that fast IPC is important. But we should not expect that its value has to be that it is always the dominant factor of the performace for all systems.