Singularity: Rethinking the Software Stack

Singularity: Rethinking the Software Stack.
Galen C. Hunt; James R. Larus. April 2007

...Singularity systems incorporate three key architectural features: software-isolated processes for protection of programs and system services, contract-based channels for communication, and manifest-based programs for verification of system properties. We describe this foundation in detail and sketch the ongoing research in experimental systems that build upon it.

Singularity comes up in discussion every now and then. This seems like a nice and recent overview.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Contrary to my belief

Contrary to my belief expressed in a forum thread on Singularity, this paper says,

In addition, the Sing# compiler can statically verify that send and receive operations on channels never are applied in the wrong protocol state. A separate contract verifier can read a program’s byte code and statically verify which contracts are used within a program and that the code conforms to the state machine described in the contract’s protocol.

I would have supposed such a thing to be undecidable in general. Does anyone know any details?

Static Verification may be check-able

I breezed through the paper. It looks like they could take a proof-carrying-code-like approach and use the type checking as an aid to safety verification.

It's pretty easy to make

It's pretty easy to make this decidable when you control the source language and can impose a strict discipline. What's actually implemented is more than a standard (flow-insensitive) type system, but not _that_ much more involved.

Paper on Sing# language features.

Paper on Sing# language features.

The basic idea is that types can be annotated with states. For example, let's say you have a "Connection" type with three possible states: "Begin", "Connected", "End". Given a protocol object whose type is "Connection!Begin", you can call the "Connect(...)" method. After that method returns, the type is "Connection!Connected" and the compiler will no longer allow calls to "Connect(...)", but will allow calls to "Send(...)" and "Receive(...)".

They make this statically enforceable by restricting aliasing. I don't remember the details, but it was something like "if you want to track the object's state statically, then the compiler has to know about all aliases of the object".

Protocol free objects

Interesting! I haven't yet read the paper (I'll promise to read it when my new printer arrives (hopefully) in a few days), but your example reminds me of a design pattern, if you may, that I discovered a long time a ago.

Yes, organizing the

Yes, organizing the classes/types to ensure valid state transitions is handy, but you still can't enforce proper usage statically without some kind of linear or alias type system. What if you needed an explicit Close() funtion (putting it in a finalizer isn't always acceptable); can you think of a way to ensure that a client can't call Conn.Send() after calling Close() in ordinary ML? It's the aliasing that's the problem, and I can't think of any way to do it.

The closest I've gotten, is that Modem have only one operation, Process(), which accepts a function that takes a Conn, and once that function finishes executing, the connection is closed automatically. Of course, with mutable references this can be circumvented, since the Conn reference can then escape the scope of the Process() function; of course, this usage is fairly bizarre in itself, but it's not statically preventable, which is what I'm looking for.

You can use a monad

You've gotten quite close. The next step is to make the parameter to Process() a monad instead of a plain function and lift operations on a connection to the monad. This way the user can't get a handle to the connection at all so there is no way have aliases. This is a fairly well known trick. I recall seeing posts on this on at least some O'Caml mailing list and, IIRC, on comp.lang.functional quite recently.

Thanks for the suggestion.

Thanks for the suggestion. I've been going through some of the documentation on Monads, and I understand the Haskell monad signature. I'm not familiar with type classes however, so I'm not sure how a Monad is implemented/overridden (or whatever the terminology might be). Does each instance of a monad need a custom implementation for bind, return, etc. or is a monad a simple polymorphic type?

Are you aware of any monad implementations in SML or OCaml? Or perhaps some demonstration code in C# or Java? I haven't been able to find anything that maps clearly to the Haskell monad signature at that link, so I'm having a bit of trouble mapping to C#.

[OT] ML monads

Does each instance of a monad need a custom implementation for bind, return, etc.

Yes (in general; sharing may be possible in particular cases).

Are you aware of any monad implementations in SML or OCaml?

Take a look at the Syntax extension for Monads in Ocaml. Or, if you're comfortable with Scheme, try Oleg's Monadic Programming in Scheme.

The basic monad signature can be expressed in OCaml like this:

module type MONAD =
    type monad 'a = 'abstract;
    value unit : 'a -> monad 'a;
    value bind : monad 'a -> ('a -> monad 'b) -> monad 'b;

(That's using OCaml's revised syntax, because I was working with the new version of Camlp4 when I wrote this. Also, 'unit' is used instead of 'return' because of a keyword conflict in OCaml.)

The implementation of the identity monad would then look like this:

module Identity_Monad : MONAD =
    type monad 'a = 'a;
    value unit a = a;
    value bind m k = k m;

And here's a Maybe monad:

module type MAYBE_MONAD =
    include MONAD;
    value fail : monad 'a;

module Maybe : MAYBE_MONAD =
    type monad 'a = option 'a;
    value unit a = Some a;
    value fail = None;

    value bind m k = match m with
      [ None   -> None
      | Some x -> k x ];

[OT] Excellent!

Thanks for the very clear explanation. I've created monad interfaces and implementations of the identity and maybe monads in C# for my FP# library. I look forward to playing with monads to learn more. :-)

Perhaps of interest to others: the translation from a single module in OCaml ends up requiring two interfaces in C#. If C# permitted static methods on interfaces, only one interface would be needed. I'd appreciate any comments on the correctness of my implementation.

Edit: altered the implementation to use a single abstract base to reduce the boilerplate. Also added the Plus monad.

Previous discussion about linear types:

It's been discussed here before:

mutating types

Sing# shows clearly that the notion of type extends to individual values, as I have previously discussed here in LtU. Much of the problems that exist in today's mainstream languages is that they completely miss that concept. FP languages are vastly better in this domain.

Temporal Logic

I just read the paper and was wondering how Sing's contracts (based on a state automaton and apparently verifiable by a byte code verifier) do relate to temporal logic assertions ?