Language Support for Fast and Reliable Message-based Communication in Singularity OS
Manuel Fa¨hndrich, Mark Aiken, Chris Hawblitzel, Orion Hodson, Galen Hunt, James R. Larus, and Steven Levi
Message-based communication offers the potential benefits of providing stronger specification and cleaner separation between components. Compared with shared-memory in- teractions, message passing has the potential disadvantages of more expensive data exchange (no direct sharing) and more complicated programming.
In this paper we report on the language, verification, and run-time system features that make messages practical as the sole means of communication between processes in the Singularity operating system. We show that using advanced programming language and verification techniques, it is pos- sible to provide and enforce strong system-wide invariants that enable efficient communication and low-overhead soft- ware-based process isolation. Furthermore, specifications on communication channels help in detecting programmer mis- takes early—namely at compile-time—thereby reducing the difficulty of the message-based programming model.
The paper describes our communication invariants, the language and verification features that support them, as well as implementation details of the infrastructure. A number of benchmarks show the competitiveness of this approach.
Categories and Subject Descriptors
D.4.4 [Operating Systems]: Communications Manage- ment; D.3.3 [Programming Languages]: Language Con- structs and Features
Process isolation and inter-process communication are among the central services that operating systems provide. Isola- tion guarantees that a process cannot access or corrupt data or code of another process. In addition, isolation provides clear boundaries for shutting down a process and reclaim- ing its recources without cooperation from other processes. Inter-process communication allows processes to exchange data and signal events.
There is a tension between isolation and communication, in that the more isolated processes are, the more compli- cated and potentially expensive it may be for them to com- municate. For example, if processes are allowed to share memory (low isolation), they can communicate in appar- ently simple ways just by writing and reading memory. If, on the other hand, processes cannot share memory, the op- erating system must provide some form of communication channels, which typically allow transmission of streams of scalar values.
In deference to performance considerations, these trade- offs are often resolved in the direction of shared memory, even going as far as to co-locate components within the same process. Examples of such co-location are device drivers, browser extensions, and web service plug-ins. Eschewing process isolation for such components makes it difficult to provide failure isolation and clear resource management. When one component fails, it leaves shared memory in in- consistent or corrupted states that may render the remaining components inoperable.
General Terms Languages, Performance, Reliability
At the other end of the spectrum, truly isolated processes communicating solely via messages have the advantage of independent failure, but at the costs of 1) a more compli- cated programming model (message passing or RPC) and 2) the overhead of copying data.
channels, asynchronous communication, static checking, protocols, data ownership
This paper describes how we overcome these costs in the Singularity OS [22, 23] through the use of strong system- wide invariants that are enforced by the compiler and run- time system. The main features of the communication in- frastructure are:
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. To copy otherwise, to republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. EuroSys’06, April 18–21, 2006, Leuven, Belgium. Copyright 2006 ACM 1-59593-322-0/06/0004 ..$5.00.
Data is exchanged over bidirectional channels, where each channel consists of exactly two endpoints (called Imp and Exp). At any point in time, each channel endpoint is owned by a single thread.
Buffers and other memory data structures can be trans- ferred by pointer, rather than by copying. These trans- fers pass ownership of blocks of memory. Such trans-