The April edition of Operating System Review (OSR) was solely dedicated to projects coming out of Microsoft Research, one of the more compelling papers published (pdf) was the long awaited work of Galen Hunt and James Larus on Singularity, Microsoft Research project that aims to addresss the question:
what would a software platform look like if it was designed from scratch with the primary goal of dependability? Singularity is working to answer this question by building on advances in programming languages and tools to develop a new system architecture and operating system (named Singularity), with the aim of producing a more robust and dependable software platform. Singularity demonstrates the practicality of new technologies and architectural decisions, which should lead to the construction of more robust and dependable systems.
The paper coincides with the 1.0 release of Singularity to a small number of universities for their research efforts. While being relieved of commercially viable burdens such as backward compatibility, Singularity contains many alluring ways of solving classic problems using newer programming tools and methodologies.
InfoQ spoke to Galen Hunt and Jim Larus about Singularity. In discussing the need for such a project (aside from research for research's sake), Jim explained how other modern operating systems are not capable of fulfilling the requirements of next generation users and developers, and how Singularity addresses that issue:
The existing OS evolved in response to the pressures of machines and their uses. Our key point is that these systems exist in a very different world than they grew up in, and the systems need fundamental changes to address today’s concerns. Most big OS ideas came from Multics. Machines of that era were very slow (100’s kHz) and very memory limited (10s KB). Programs were written in assembly language (for the most part). Security was limited to protecting my files from another timesharing user. Networking hadn’t been invented. Users were motivated and trained. Etc. Singularity set out with the goal of designing a system that would exist in a world of fast processors, lots of memory, high level programming languages, sophisticated verification techniques, naive users, etc.
On the subject of which of the many innovations listed are the most important to the rest of the research community Jim had the following to say:
I hate to have to choose only one, but I believe that the architecture of Singularity is its biggest contribution. Architecture is a short-hand for our design goal of increasing the robustness and resiliency of a Singularity system by increasing the isolation among the components of the system. It manifests itself in various ways, such as the micro-kernel, lightweight SIP processes [Software Isolated Processes: isolated object space, separate GCs, separate runtimes], lack of shared memory, communication across strongly typed channels, etc.
On his personal favorite section of the system:
I’m very fond of the process/channel design, which came from some of my earlier work on Staged Server and work my group did no verifying web service contracts. I think the channel semantics (lose ownership of a message when it is sent) is a sweet spot in the trade-off among efficiency, verification, and expressiveness.
As described in the paper, “A channel is a bi-directional message conduit with exactly two endpoints. A channel provides a lossless, in-order message queue”. These channels are used for all communications between Software-Isolated Processes (SIPs), as opposed to direct sharing of memory or other commonly used methods. Once a message is sent, the SIP loses ownership of it.
The communication across these channels must meet a “channel contract” in a manner very similar to web services, which allows for a higher level of verification of communications and the use of the pi-calculus as a formalization of the system. As to the benefits of this formalization Jim offered the following:
The pi-calculus and the work my group did with Tony Hoare on conformance checking provided a rigorous understanding of how to specify and verify some aspects of channels. We probably could have come up with something similar, but it would have been like the type systems in early programming languages, such as PL/1 or Pascal, which didn’t have any sound basis for knowing that they were correct. The pi-calculus and conformance check provide that rigorous basis that we can then extend to build practical and hopefully usable systems.
These increased levels of verification have the direct result of lowering the number of bugs in the communications of various systems, which is an area commonly prone to bugs and versioning problems. An example of this as illustrated by Galen Hunt:
The first time we ran the channel verifier across the code base and we found an obscure bug in the web server. The web server code failed to handle the situation where it had an incoming HTTP socket and a slow client. Instantly, the channel verifier said, "Hey, your code doesn't handle the NoData message at line such-and-such.
Many of the "new" programming tools used in Singularity -- the word "new" is used cautiously, since they have existed for some time, but either out of the mainstream or out of the OS world -- are mostly included in its associated language Sing#. Sing# is a derivative of another very well known MSR project Spec#, which is a specification based language allowing for the definitions of pre and post conditions as well as object invariants, allowing for static verification of the system by a theorem prover (boogie).
Static verification offers the promise of finding many common errors in program logic such as possibly improper use of a method at compile time as opposed to at runtime. Many believe that static verification will become mainstream in the next few years as an evolutionary step in an environment requiring us to maintain increasingly complex systems. Asked if static verification and the use of the type safe environment provided by C# (the grandfather of Sing#) has had a dramatic effect on the quality of Singularity, Jim said:
We haven’t made heavy use of Spec#-style verification yet, though we are actively working on it. Boogie, the static verifier, is becoming robust enough to verify large pieces of the system (e.g. drivers). It will be very interesting to see what comes from this effort. The other verification that we rely on (C# type safety and channel contracts) have been very useful. They don’t find all bugs, but prevent many errors. We continually see opportunities to do better with verification, and often feel limited by the difficulty of building new tools.
Galen Hunt also offered an example of the benefits static verification can provide:
This spring we did a major push to improve our performance on the SPECweb99 benchmark. One of our engineers, Orion Hodson, had written a new FAT32 file system from scratch using all of the static verification features in Sing#. It was our most ambitious use of Sing# verification features to date. He had written the code last winter, but never had time to test it. As we beat on the system for a month for the SPECweb99 push, we expected to find bugs in Orion's file system since it had never been tested. Instead, the code just kept on ticking. We didn't find even one correctness bug. No race conditions; no memory corrupts; nothing. It confirmed that we'd made the right choice in emphasizing static verification to make systems more dependable.
It is of importance that these types of reports are noted as Spec# probably will have a much shorter journey towards commercial viability. Although Singularity in its entirety as a commercially available product is still many years in the future if at all, it does provide numerous enlightening examples of alternative solutions in a well-known problem domain. Asked about the possibility of being able to reuse some of the research completed in Singularity in a possibly piece-meal fashion for commercial applications in the near-term, Jim replied with the following:
We sure hope so, since that is one of the goals of MSR. However, it is a long and involved process getting ideas from MSR into products, so it may take a while and the ideas may be difficult to recognize when they are part of a much bigger system.
And concerning the follow up question of what would pose the biggest hurdle in driving these ideas forward:
Backward compatibility in existing systems; we decided to ignore that aspect when we built the system. It gave us a lot of design and implementation freedom, but makes it more difficult for existing products to take a large piece of Singularity. I expect that the design goals mentioned above and the use of a high-level language to be the most easily transferable aspects of the project.
The Singularity project as described in the paper as being a "Journey not a Destination" has explored unique design goals, which led to a significant prototype. This prototype will certainly be used for further research. While commercially viable thoughts like backwards compatibility are missing, Singularity likely represents a foretelling of the OS product offerings from Microsoft; if so this future is managed.