Singularity - C# OS Released on CodePlex
During my research and posts about Design by Contract and Spec# and my interactions with folks from Microsoft Research, I came across Singularity OS, an operating system written in an offshoot language based upon C#. In that time, I realized that the Singularity team extended Spec# and the Design by Contract and static verification pieces of it into a new language called Sing#.
Fast forward to last Tuesday. Almost five years after the start of development, it has finally been released onto CodePlex as an open source non-commercial academic license and can be found here. After reading about it and talking with some Microsoft Research folks about it, I had to give it a shot. That's one of the things I love about working at Microsoft is the fact that I can interact with people like these on a periodic basis.
History of Singularity
During my long commute to and from work, I have the pleasure of listening to many podcasts. Although I like the ones in the .NET space with Hanselminutes and DotNetRocks, I also like to venture into the Ruby and outside community where I'm pretty comfortable as well. So, one of my absolute favorites is Software Engineering Radio for the serious talk and geeking about languages and architecture. Lo and behold, the latest episode, Episode 88, covers Singularity with Galen Hunt where he talks with Markus, the host about the history and features of the OS. I suggest you listen to that before we go any further. Also, a good overview can be found here in PDF format.
If you think about most operating systems we run today, the essence of what they are is dated back in the 1970s and C and Assembly based. Back in 2003, Galen and team started this effort to write an operating system in managed code. Over 90% of the system is written in a language called Sing# which is an extension of Spec# which I will get into shortly. But, Singularity consists of three major parts, Software Isolated Processes (SIPs), contract-based channels, and manifest-based programs.
SIPs are interesting parts of Singularity. They provide a sandbox as it were for program execution free from meddling from outside processes. This includes its own memory space, threads and so on. In fact, memory and threads cannot be shared from one SIP to the other, so the vectors for malicious code are cut way down.
Contract-Based Channels are another interesting aspect of Singularity. It's a built-in feature of the Sing# language which I will get to in the next section. In short, what it provides is a quick and verifiable way of communicating between processes with messages. To support this, the Spec# language had to be extended to support this.
Lastly, manifest based programs are interesting because it defines the code that runs within the SIP and its behaviors. In Singularity, there really is no such thing as Just In Time Compiling (JIT) as all code needs to be loaded into memory and statically verified before it can be executed, which is something a JIT cannot do. But on the other side of this, it makes dynamic languages and late binding impossible as well. So, to work around this, they devised a plan called Compile Time Reflection, so you know your dependencies beforehand and uses Dependency Injection in a way to inject the appropriate dependencies. Really slick stuff!
Sing#
Rustan Leino and others in Microsoft Research had already begun an effort called Spec# to provide Design by Contract features to the C# language and a static verifier to prove that code is in fact working as the contracts were written. Just a quick aside, we're going to be lucky enough to have Rustan at ALT.NET Open Spaces, Seattle to talk about it and Design by Contract (Shameless Plug). Anyhow, back to the topic at hand. Spec# didn't have enough for the static verification that needs to happen. So, instead, Sing# brings us Contract Based Channels for creating message declarations and a set of named protocol sets. Any communication that crosses processes must use contract based channels. These messages that it passes have declarations that state the number and types of arguments for each message and an optional message direction. Each state specifies the possible message sequences leading to other states in the state machine.
I just want to dig through some code to see exactly what that looks like:
class DirectoryServiceWorker
{
private TRef<DirectoryServiceContract.Exp:Start> epRef;
private DirNode! dirNode;
private DirectoryServiceWorker(DirNode! dirNode,
[Claims] DirectoryServiceContract.Exp:Start! i_ep)
requires i_ep.InState(DirectoryServiceContract.Start.Value);
{
epRef = new TRef<DirectoryServiceContract.Exp:Start>(i_ep);
this.dirNode = dirNode;
base();
}
If you notice from above, you can see some Spec# goodness in there including NonNull types using the ! keyword and also requires preconditions. It's pretty well written and a lot of fun to dig through. If you want to learn more about compilers and operating systems, now is the time to sift through the source code and get your geek hat on.
Building the Image
If you want to actually run Singularity, the team has provided as part of the zip file, a way to build the operating system. You'll simply need the following:
- Windows Debugging Tools
- .NET Framework 1.1
- Virtual PC 2007
- MSBuild
I was able to get the results in about 10 minutes or so for the build process. Then again, if you're running Vista, you need to be sure to launch the configure.cmd as an elevated process in order to kick things off properly. That was the first hurdle. But once I got that going, the rest was easy. And I got a pretty cool result as well when I ran the VPC image. Look at the goodness:
I have played with it just yet all that much. I'm figuring what I can do with it next. But, that's part of my copious spare time which doesn't seem to exist much anymore.
Conclusion
I've done well with my learning plan this year to keeping to what is on my plan and not deviating from it. Luckily languages such as Spec# and Sing# still fall into that category. It's pretty fascinating stuff and great to get my hands on an operating system using managed code. It's pretty impressive from the things I've read and the code I've read. I'm only hoping that research projects such as this make a significant impact on future versions of Windows, let alone future versions of most operating systems. Until next time...
