An Overview of the Singularity Project:
Abstract.
Singularity is a research project in Microsoft Research that started with the question: what would a software platform look like if it was designed from scratch with the primary goal of dependability? Singularity is working to answer this question by building on advances in programming languages and tools to develop a new system architecture and operating system (named
Singularity), with the aim of producing a more robust and dependable software platform. Singularity demonstrates the practicality of new technologies and
architectural decisions, which should lead to the construction of more robust and dependable systems.
1 Introduction
Software runs on a platform that has evolved over the past 40 years and is increasingly showing its age. This platform is the vast collection of code—operating systems, programming languages, compilers, libraries, run-time systems, middleware, etc.—and hardware that enables a program to execute. On one hand, this platform is an enormous success in both financial and practical terms. The platform forms the foundation of the $179 billion dollar packaged software industry [3] and has enabled revolutionary innovations such as the Internet. On the other hand, the platform and software running on it are less robust, reliable, and secure than most users (and developers!) would wish.
Part of the problem is that our current platform has not evolved far beyond the computer architectures, operating systems, and programming languages of the 1960’s and 1970’s. The
computing environment of that period was very different from today’s milieu. Computers were
extremely limited in speed and memory capacity; used only by a small group of technically literate and non-malicious users; and were rarely networked or connected to physical devices. None of these characteristics remains true, but modern computer architectures, operating systems, and programming languages have not evolved to accommodate a fundamental shift in computers
and their use.
Singularity is a research project in Microsoft Research that started with the question: what would a software platform look like if it was designed from scratch with the primary goal of dependability, instead of the more common goal of performance?
Singularity is working to answer this question by building on advances in programming languages and programming tools to develop and build a new system architecture and operating system (named Singularity), with the aim of producing a more robust and dependable software platform. Although dependability is difficult to measure in a research prototype, Singularity shows the practicality of new
technologies and architectural decisions, which should lead to more robust and dependable
systems in the future.
With its exponential rate of progress, hardware evolution commonly appears to drive fundamental changes in systems and applications. Software, with its more glacial progress, rarely creates opportunities for fundamental improvements. However, software does evolve, and its change makes it possible—and necessary—to rethink old assumptions and practices. Advances in programming languages, run-time systems, and program analysis tools provide the building blocks to construct architectures and systems that are more dependable and robust than existing systems:
Expressive, safe programming languages, such as Java and C#. Type safety ensures a value or object is always correctly interpreted and manipulated. Memory safety ensures a program references memory only within the bounds of valid, live objects.
Optimizing compilers and high performance run-time systems generate safe code that runs at speeds comparable to unsafe code [20]. These compilers, unlike the more common just-in-time (JIT) compilers, perform global optimizations that mitigate safetyrelated overhead. Garbage collectors in these systems reclaim memory with overhead comparable to that of explicit de-allocation.
Validation techniques ensure the end-to-end type safety of the compiler, compiled code, and run-time system. Typed intermediate and assembly language validate the proper operations of system components and ensure the language safety guarantees that underlie system correctness.
Sound, specification-driven defect detection tools ensure the correctness of many aspects of the system. A sound tool finds all occurrences of an error—along with false positives—and consequently can reliably indicate when a particular defect has been eliminated. Specification-driven tools do not look for a hardwired collection of defects.
They are extensible and can be adapted to check that many program or library-specific abstractions are used correctly.
Languages and tools based on these advances are in use detecting and preventing programming errors. Less well explored is how these mechanisms enable deep changes in system architecture, which in turn might advance the ultimate goal of preventing and mitigating software defects [28].
The rest of this paper describes the Singularity system in detail. Section 2 contains an overview of the system and its novel aspects. Section 3 describes the Singularity system architecture, focusing on the kernel, processes, and the language run-time system.
Section 4
describes the programming language support for the system. Section 5 describes the I/O and
security system. Section 6 provides some performance benchmarks. Section 7 surveys related
work. Appendix A contains a list of the kernel ABI calls.
2 Singularity
Singularity is a new operating system being developed as a basis for more dependable
system and application software [28]. Singularity exploits advances in programming languages
and tools to create an environment in which software is more likely to be built correctly, program
behavior is easier to verify, and run-time failures can be contained.
A key aspect of Singularity is an extension model based on Software-Isolated Processes
(SIPs), which encapsulate pieces of an application or a system and provide information hiding,
failure isolation, and strong interfaces. SIPs are used throughout the operating system and
application software. We believe that building a system on this abstraction will lead to more
dependable software.
SIPs are the OS processes on Singularity. All code outside the kernel executes in a SIP. SIPs
differ from conventional operating system processes in a number of ways:
SIPs are closed object spaces, not address spaces. Two Singularity processes cannot simultaneously access an object. Communications between processes transfers exclusive ownership of data.
SIPs are closed code spaces. A process cannot dynamically load or generate code.
SIPs do not rely on memory management hardware for isolation. Multiple SIPs can reside
in a physical or virtual address space.
Communications between SIPs is through bidirectional, strongly typed, higher-order channels. A channel specifies its communications protocol as well as the values transferred, and both aspects are verified.
SIPs are inexpensive to create and communication between SIPs incurs low overhead.
Low cost makes it practical to use SIPs as a fine-grain isolation and extension mechanism.
SIPs are created and terminated by the operating system, so that on termination, a SIP’s resources can be efficiently reclaimed. SIPs executed independently, even to the extent of having different data layouts, run-time systems, and garbage collectors.
SIPs are not just used to encapsulate application extensions. Singularity uses a single
mechanism for both protection and extensibility, instead of the conventional dual mechanisms of
processes and dynamic code loading. As a consequence, Singularity needs only one error
recovery model, one communication mechanism, one security policy, and one programming
model, rather than the layers of partially redundant mechanisms and policies in current systems.
A key experiment in Singularity is to construct an entire operating system using SIPs and
demonstrate that the resulting system is more dependable than a conventional system.
The Singularity kernel consists almost entirely of safe code and the rest of the system, which
executes in SIPs, consists of only verifiably safe code, including all device drivers, system
processes, and applications. While all untrusted code must
be verifiably safe, parts of the
Singularity kernel and run-time system, called the trusted base, are not verifiably safe. Language
safety protects this trusted base from untrusted code.
The integrity of the SIPs depends on language safety and on a system-wide invariant that a
process does not hold a reference into another process’s object space.
Ensuring code safety is obviously essential. In the short term, Singularity relies on compiler
verification of source and intermediate code. In the future, typed assembly language (TAL) will
allow Singularity to verify the safety of compiled code [36, 38]. TAL requires that a program
executable supply a proof of its type safety (which can be produced automatically by a compiler
for a safe language). Verifying that a proof is correct and applicable to the instructions in an
executable is a straightforward task for a simple verifier of a few thousand lines of code. This
end-to-end verification strategy eliminates a compiler—a large, complex program—from
Singularity’s trusted base. The verifier must be carefully designed, implemented, and checked,
but these tasks are feasible because of its size and simplicity.
The memory independence invariant that prohibits cross-object space pointers serves several
purposes. First, it enhances the data abstraction and failure isolation of a process by hiding
implementation details and preventing dangling pointers into terminated processes. Second, it
relaxes implementation constraints by allowing processes to have different run-time systems and
their garbage collectors to run without coordination. Third, it clarifies resource accounting and
reclamation by making unambiguous a process’s ownership of a particular piece of memory.
Finally, it simplifies the kernel interface by eliminating the need to manipulate multiple types of
pointers and address spaces.
A major objection to this architecture is the difficulty of communicating through message
passing, as compared with the flexibility of directly sharing data. Singularity is addressing this
problem through an efficient messaging system, programming language extensions that concisely
specify communication over channels, and verification tools [19].
Abstract.
Singularity is a research project in Microsoft Research that started with the question: what would a software platform look like if it was designed from scratch with the primary goal of dependability? Singularity is working to answer this question by building on advances in programming languages and tools to develop a new system architecture and operating system (named
Singularity), with the aim of producing a more robust and dependable software platform. Singularity demonstrates the practicality of new technologies and
architectural decisions, which should lead to the construction of more robust and dependable systems.
1 Introduction
Software runs on a platform that has evolved over the past 40 years and is increasingly showing its age. This platform is the vast collection of code—operating systems, programming languages, compilers, libraries, run-time systems, middleware, etc.—and hardware that enables a program to execute. On one hand, this platform is an enormous success in both financial and practical terms. The platform forms the foundation of the $179 billion dollar packaged software industry [3] and has enabled revolutionary innovations such as the Internet. On the other hand, the platform and software running on it are less robust, reliable, and secure than most users (and developers!) would wish.
Part of the problem is that our current platform has not evolved far beyond the computer architectures, operating systems, and programming languages of the 1960’s and 1970’s. The
computing environment of that period was very different from today’s milieu. Computers were
extremely limited in speed and memory capacity; used only by a small group of technically literate and non-malicious users; and were rarely networked or connected to physical devices. None of these characteristics remains true, but modern computer architectures, operating systems, and programming languages have not evolved to accommodate a fundamental shift in computers
and their use.
Singularity is a research project in Microsoft Research that started with the question: what would a software platform look like if it was designed from scratch with the primary goal of dependability, instead of the more common goal of performance?
Singularity is working to answer this question by building on advances in programming languages and programming tools to develop and build a new system architecture and operating system (named Singularity), with the aim of producing a more robust and dependable software platform. Although dependability is difficult to measure in a research prototype, Singularity shows the practicality of new
technologies and architectural decisions, which should lead to more robust and dependable
systems in the future.
With its exponential rate of progress, hardware evolution commonly appears to drive fundamental changes in systems and applications. Software, with its more glacial progress, rarely creates opportunities for fundamental improvements. However, software does evolve, and its change makes it possible—and necessary—to rethink old assumptions and practices. Advances in programming languages, run-time systems, and program analysis tools provide the building blocks to construct architectures and systems that are more dependable and robust than existing systems:
Expressive, safe programming languages, such as Java and C#. Type safety ensures a value or object is always correctly interpreted and manipulated. Memory safety ensures a program references memory only within the bounds of valid, live objects.
Optimizing compilers and high performance run-time systems generate safe code that runs at speeds comparable to unsafe code [20]. These compilers, unlike the more common just-in-time (JIT) compilers, perform global optimizations that mitigate safetyrelated overhead. Garbage collectors in these systems reclaim memory with overhead comparable to that of explicit de-allocation.
Validation techniques ensure the end-to-end type safety of the compiler, compiled code, and run-time system. Typed intermediate and assembly language validate the proper operations of system components and ensure the language safety guarantees that underlie system correctness.
Sound, specification-driven defect detection tools ensure the correctness of many aspects of the system. A sound tool finds all occurrences of an error—along with false positives—and consequently can reliably indicate when a particular defect has been eliminated. Specification-driven tools do not look for a hardwired collection of defects.
They are extensible and can be adapted to check that many program or library-specific abstractions are used correctly.
Languages and tools based on these advances are in use detecting and preventing programming errors. Less well explored is how these mechanisms enable deep changes in system architecture, which in turn might advance the ultimate goal of preventing and mitigating software defects [28].
The rest of this paper describes the Singularity system in detail. Section 2 contains an overview of the system and its novel aspects. Section 3 describes the Singularity system architecture, focusing on the kernel, processes, and the language run-time system.
Section 4
describes the programming language support for the system. Section 5 describes the I/O and
security system. Section 6 provides some performance benchmarks. Section 7 surveys related
work. Appendix A contains a list of the kernel ABI calls.
2 Singularity
Singularity is a new operating system being developed as a basis for more dependable
system and application software [28]. Singularity exploits advances in programming languages
and tools to create an environment in which software is more likely to be built correctly, program
behavior is easier to verify, and run-time failures can be contained.
A key aspect of Singularity is an extension model based on Software-Isolated Processes
(SIPs), which encapsulate pieces of an application or a system and provide information hiding,
failure isolation, and strong interfaces. SIPs are used throughout the operating system and
application software. We believe that building a system on this abstraction will lead to more
dependable software.
SIPs are the OS processes on Singularity. All code outside the kernel executes in a SIP. SIPs
differ from conventional operating system processes in a number of ways:
SIPs are closed object spaces, not address spaces. Two Singularity processes cannot simultaneously access an object. Communications between processes transfers exclusive ownership of data.
SIPs are closed code spaces. A process cannot dynamically load or generate code.
SIPs do not rely on memory management hardware for isolation. Multiple SIPs can reside
in a physical or virtual address space.
Communications between SIPs is through bidirectional, strongly typed, higher-order channels. A channel specifies its communications protocol as well as the values transferred, and both aspects are verified.
SIPs are inexpensive to create and communication between SIPs incurs low overhead.
Low cost makes it practical to use SIPs as a fine-grain isolation and extension mechanism.
SIPs are created and terminated by the operating system, so that on termination, a SIP’s resources can be efficiently reclaimed. SIPs executed independently, even to the extent of having different data layouts, run-time systems, and garbage collectors.
SIPs are not just used to encapsulate application extensions. Singularity uses a single
mechanism for both protection and extensibility, instead of the conventional dual mechanisms of
processes and dynamic code loading. As a consequence, Singularity needs only one error
recovery model, one communication mechanism, one security policy, and one programming
model, rather than the layers of partially redundant mechanisms and policies in current systems.
A key experiment in Singularity is to construct an entire operating system using SIPs and
demonstrate that the resulting system is more dependable than a conventional system.
The Singularity kernel consists almost entirely of safe code and the rest of the system, which
executes in SIPs, consists of only verifiably safe code, including all device drivers, system
processes, and applications. While all untrusted code must
be verifiably safe, parts of the
Singularity kernel and run-time system, called the trusted base, are not verifiably safe. Language
safety protects this trusted base from untrusted code.
The integrity of the SIPs depends on language safety and on a system-wide invariant that a
process does not hold a reference into another process’s object space.
Ensuring code safety is obviously essential. In the short term, Singularity relies on compiler
verification of source and intermediate code. In the future, typed assembly language (TAL) will
allow Singularity to verify the safety of compiled code [36, 38]. TAL requires that a program
executable supply a proof of its type safety (which can be produced automatically by a compiler
for a safe language). Verifying that a proof is correct and applicable to the instructions in an
executable is a straightforward task for a simple verifier of a few thousand lines of code. This
end-to-end verification strategy eliminates a compiler—a large, complex program—from
Singularity’s trusted base. The verifier must be carefully designed, implemented, and checked,
but these tasks are feasible because of its size and simplicity.
The memory independence invariant that prohibits cross-object space pointers serves several
purposes. First, it enhances the data abstraction and failure isolation of a process by hiding
implementation details and preventing dangling pointers into terminated processes. Second, it
relaxes implementation constraints by allowing processes to have different run-time systems and
their garbage collectors to run without coordination. Third, it clarifies resource accounting and
reclamation by making unambiguous a process’s ownership of a particular piece of memory.
Finally, it simplifies the kernel interface by eliminating the need to manipulate multiple types of
pointers and address spaces.
A major objection to this architecture is the difficulty of communicating through message
passing, as compared with the flexibility of directly sharing data. Singularity is addressing this
problem through an efficient messaging system, programming language extensions that concisely
specify communication over channels, and verification tools [19].
DOWNLOAD LINK:
No comments:
Post a Comment