Transcript state isolation invariant

Presentation of Singularity
OS Seminar, winter 2005
by Jacob Munk-Stander
November 23rd, 2005
Overview of Singularity
• Singularity is a new research operating system from
Microsoft Research
– Written almost entirely in managed code Sing# (extension
of C#)
– Microkernel
• Primary goal of dependability
– “Dependability thus includes as special cases such
attributes as reliability, availability, safety, security.”
• Participants
– Cambridge, Silicon Valley and Redmond.
– A dozen people are the core contributors (of which two are
from DIKU). In total 40-50 people are working on
Singularity.
– Research groups include Operating Systems,
Programming Languages, Compilers, Tools.
– In total 11-12 research groups, largest in the history of
Microsoft Research.
Dependability
• Dependability realized by:
– Managed code, i.e. type safety
– Software-Isolated Processes, i.e. no
shared memory between processes
Low Level Invariants of Singularity
• Memory Independence Invariant:
– A process does not hold a reference into another
process’s object space.
• State Isolation Invariant:
– A process cannot alter the state of another
process using the ABI.
• Ownership Invariant:
– Ownership of messages are passed from the
sender to the receiver.
• Exchange Heap Invariant:
– Does not contain pointers into any process GC
heap.
Managed Code
• C# is the base managed programming
language
• Spec# - an extension of C# developed in
Microsoft Research.
– Adds support for specifying program behavior,
which can be verified either statically or with runtime tests.
• Singularity is written in Sing# - an extension
of Spec#.
– Adds support for channels and low-level
constructs.
Managed Code, cont.
• Code in Singularity is either verified or trusted:
– Verified code’s type and memory safety is checked by a
compiler
– Trusted code must be trusted by the system
• Most of the kernel is verifiably safe, but portions are
written in trusted assembler, C++ and unsafe C#.
• The rest is written in safe managed code using
Sing#
• Currently: Sing# -> MSIL -> x86 code
– Code is verified at each step
– Uses Bartok compiler for MSIL -> x86 code
• Future: Typed Assembly Language will be used to
verify output of compiler.
Managed Code, cont.
• Base managed code has performance
somewhat comparable to C/C++.
• Given safety invariants of the
language, tools can perform additional
optimizations not possible with unsafe
code, e.g.
– due to no dynamic code loading
=> complete compile time static analysis
– no pointers into other process
=> no memory hardware protection
Software-Isolated Processes
• Self-contained units, providing:
– Information hiding
– Failure isolation
– Strong interfaces
• Run independently, allowing different GCs,
etc.
• Created and terminated by the OS, allowing
for efficient reclamation of resources.
• All processes in one protection domain,
leading to an order of magnitude better
context switch times.
SIPs, cont.
• SIPs are used throughout the OS, in drivers and
application software.
• Application Binary Interfaces maintains system-wide
state isolation invariant, i.e. a process cannot alter the
state of another process using the ABI.
Channels
• Communication between SIPs through
bidirectional, strongly typed, higher-order
channels, specified using contracts.
• Messages on channels are passed between
processes using the Exchange Heap,
allowing for zero-copy message passing.
Channels, cont.
• Integrated into the language, checked
at compile time
• Contracts
– Import Channels
– Export Channels
– State Machine
• Enforces the ownership invariant
• Sending messages is asynchronous
• Receiving message is blocking
Installation Time
• Metadata in applications manifest
• Internal properties
– Verifies application’s assemblies exists and are type and
memory safe
– Verifies channel contracts
– Verifies ABI versions
• External dependencies
– Verifies that hardware resources used do not conflict
– Verifies that all channels exist and do not conflict with
other applications’
• Policies for conflicts, i.e. only one video driver
Performance
• Singularity has not been optimized yet
• Micro benchmarks:
Performance, cont.
• Dynamic memory usage:
• SPECweb99, average response time
– Cassini web server: 23 conn. of 322 millisec./op.
– Windows 2003, IIS: 25 conn. 304 millisec./op.
Additional Information
• Video interview with lead researchers
Jim Larus and Galen Hunt at Channel
9, includes a discussion forum where
they answer additional questions.
• Singularity website.
• Bartok website.
• Software Productivity Tools.