fers do not permit sharing between the sender and re- ceiver since static verification prevents a sender from accessing memory it no longer owns.
Channel communication is governed by statically ver- ified channel contracts that describe messages, mes- sage argument types, and valid message interaction sequences as finite state machines similar to session types [17, 21].
Channel endpoints can be sent in messages over chan- nels. Thus, the communication network can evolve dynamically.
Sending and receiving on a channel requires no mem-
Sends are non-blocking and non-failing.
The next section provides context for the present work by describing Singularity. Section 2 presents channels and how programs use them. Section 3 describes the programming model allowing static verification of resource management. The implementation of channels is described in Section 4 along with some extensions in Section 5. Section 6 discusses benchmarks and experience with the system. Finally, Sec- tions 7 and 8 discuss related and future work.
The Singularity project combines the expertise of researchers in operating systems, programming language and verifica- tion, and advanced compiler and optimization technology to explore novel approaches in architecting operating sys- tems, services, and applications so as to guarantee a higher level of dependability without undue cost.
The increased reliability we are seeking stems in good part from the following design and architectural decisions:
All code, with the exception of the hardware abstrac- tion layer and parts of the trusted runtime, is writ- ten in an extension of C# called Sing#, a type-safe, object-oriented, and garbage collected language. Sing# provides support for message-based communication. Using a type and memory safe language gurantees that memory cannot be corrupted and that all failures of the code are explicit and manifest as high-level ex- ceptions (possibly uncaught), not random crashes or failures.
The operating system itself is structured as a micro- kernel in which most services and drivers are separate processes communicating with other processes and the kernel solely via channels. Processes and the kernel do not share memory. This promotion of smaller inde- pendent components allows for independent failure of smaller parts of the system. Failure can be detected reliably and compensating actions can be taken, for example restarting of services.
Implemented naively, these design decisions lead to an inef- ficient system due to the high frequency of process boundary crossings implied by the large number of small isolated com- ponents, the cost of copying message data from one process to another, and the overhead imposed by a high-level lan- guage and garbage collection. Singularity avoids these costs using the following techniques:
Isolation among processes and the kernel is achieved via the statically verified type safety of the program- ming language rather than hardware memory protec- tion. Software based isolation allows all code to run in the highest privileged processor mode and in a sin- gle virtual address space, thereby removing the cost of changing VM protections and processor mode on process transitions.
The efficient communication technique described in this paper enables the exchange of data over channels without copying. Such an approach is hard to make safe in traditional systems not based on type safe lan- guages. In our setting, we obtain safety via compile- time verification guaranteeing that threads only access memory they own. The static verification of this prop- erty is vital to the integrity of process isolation.
3. All code of a processes is known on startup (no dy- namic code loading), enabling the compiler to perform a whole program analysis on each process during com- pilation to machine code. Global program optimiza- tions can eliminate many of the costs incurred with high-level object-oriented languages, such as for in- stance crossing many levels of abstraction and object- oriented dispatch. Additionally, since each process has its own runtime system and garbage collector, pro- cesses do not have to agree on common object layouts and GC algorithms. Each process can be compiled with the object layout (including the removal of unsed fields) and GC algorithm best suited to its needs.
The Singularity operating system prototype consists of roughly 300K lines of commented Sing# code. It runs on x86 hardware and contains a number of drivers for network cards, IDE disks, sound and keyboard devices, a TCP/IP network stack, and a file system. All drivers and services are separate processes communicating via channels. Thus, even network packets and disk blocks are transmitted between drivers, the network stack, and the file systems as messages.
A channel is a bi-directional message conduit consisting of exactly two endpoints, called the channel peers. A channel is loss-less, messages are delivered in order, and they can only be retrieved in the order they were sent. Semantically, each endpoint has a receive queue, and sending on an endpoint enqueues a message on the peer’s queue.
Channels are described by channel contracts (Section 2.3). The two ends of a channel are not symmetric. We call one endpoint the importing end (Imp) and the other the export- ing end (Exp). They are distinguished at the type level with types C.Imp and C.Exp respectively, where C is the channel contract governing the interaction. The next sections de- scribe in more detail what data is exchanged through chan- nels, how channel contracts govern the conversation on a channel, and what static properties are enforced by verifica- tion.
2.1 The Exchange Heap
Processes in Singularity maintain independent heaps and share no memory with each other. If we are to pass data from one process to another, that data cannot come from a process’ private heap. Instead, we use a separate heap,