Singularity

Achtung: Dies ist alles noch eine riesige Baustelle!

Singularity ist die Bezeichnung für den Prototyp eines neuartigen Betriebssystems, dass gegenwärtig bei Microsoft Research entwickelt wird und vor allem für den Einsatz auf x86-Plattformen konzipiert ist.

Die Besonderheit des Systems gegenüber etablierten Betriebssystemen, wie etwa Windows, Linux oder Solaris, besteht darin, dass Singularity den Schutz von Systemressourcen, insbesondere die Isolation einzelner Prozesse, ausschließlich mithilfe von Softwaremechanismen realisiert und sich dabei nicht auf die Unterscheidung verschiedener CPU-Betriebsmodi (x86-Privilege-Rings) stützt.

Motivation

Ziel der Entwicklung von Singularity ist es, ein Betriebssystem zu schaffen, dass sich zum einen durch Robustheit, Stabilität, Zuverlässigkeit und Sicherheit auszeichnet und zum anderen ausreichend leistungsfähig ist, um sich auch für den praktischen Einsatz im Alltag zu eignen.

Schutz von Ressourcen und Prozessisolation

Zu den wünschenswerten Eigenschaften eines Betriebssystems gehören unter anderem Robustheit, Sicherheit und Zuverlässigkeit. Um diese Eigenschaften zu gewährleisten, muss das OS Mechanismen bereitstellen, die das System und die zugrundeliegenden Hardwareressourcen vor Fehlern oder Schäden durch unsachgemäßen oder gar böswilligen Zugriff schützen. Eine zentrale Rolle kommt dabei der Prozessisolation zu: Das OS stellt jedem Prozess einen privaten (Speicher-)Adressraum zur Verfügung, den nur er selbst zu modifizieren berechtigt ist. Diese Vorgehensweise schafft eine Barriere, die die Entstehung von Fehlern durch direkte Wechselwirkungen zwischen den einzelnen Prozessen und deren unkontrollierte, möglicherweise mit irreparablen Schäden verbundene Mulitplikation im System verhindert.

Hardwareunterstützung

Handelsübliche Betriebssysteme stützen sich im wesentlichen auf zwei Hardware-Features moderner Prozessoren, um einen willkürlichen Zugriff einzelner Prozesse auf beliebige Speicheradressen zu verhindern:

1. Memory Management Unit (MMU)
   Sie überprüft die Zugriffsberechtigung eines Prozesses bei der Übersetzung von virtueller in physische Speicheradresse anhand der Pagetable.
2. CPU-Betriebsmodi ("x86-Privilege-Rings")
   Die Verwendung unterschiedlicher CPU-Betriebsmodi beschränkt die Ausführung bestimmter, als privilegiert gekennzeichneter Instruktionen auf den Kernel. Dazu gehören insbesondere diejenigen Instruktionen, die den Betrieb der MMU und die Adressüberprüfung betreffen, aber auch solche die bspw. für einen Zugriff auf die I/O-Controller des Systems benötigt werden. Als Konsequenz dieses Mechanismus ist ein Zugriff auf geschützte Ressourcen aus dem User-Modus nur mit Unterstützung des Kernels über entsprechende Systemrufe möglich.

Der große Nachteil dieser Vorgehensweise besteht in der Kostspieligkeit des Übergangs vom User- (Ring 3) in den Kernel-Modus (Ring 0). Dabei fallen im wesentlichen dieselben Arbeitsschritte an, wie sie auch bei einem Context-Switch durchzuführen sind:

• Wechsel des CPU-Kontextes (Austausch von Instruction-Pointer und CPU-Registern, Fortführung der Abarbeitung auf dem Kernelstack.)
• Wechsel des Speicherkontextes (Laden der Pagetabelle für den Kernel. Flush des TLB auf x86-Architekturen.)
• Kopieren von Argumenten zwischen User- und Kernelspace.

Dieselbe Arbeit ist noch einmal bei der Rückkehr aus dem Kernel zum Userprozess zu leisten.

Ein solch rigider, hardware-gestützter Prozessisolationsmechanismus benachteiligt vor allem diejenigen Prozesse, die häufig I/O-Operationen durchführen oder intensiv mit anderen Prozessen kommunizieren, da hierzu ständig Systemrufe auszuführen sind. Als Konsequenz daraus wird die strikte Isolierung von Prozessen in den heute verbreiteten Betriebssystemen an vielen Stellen zugunsten gesteigerter Performance und Flexibilität aufgeweicht.

Offene Prozessarchitektur

Bekannte Betriebssystemvertreter wie etwa Linux, Windows oder Solaris basieren auf einer offenen Prozessarchitektur. Die einzelnen Adressräume sind zwar prinzipiell durch die obig beschriebenen Hardwaremechanismen voneinander getrennt, allerdings wird dies zwecks Kostenersparnis und Flexibilität nicht an allen Stellen konsequent durchgehalten.

Die Merkmale einer offenen Prozessarchitektur lassen sich wie folgt zusammenfassen:

• Verwendung von Shared Memory
• Unterstützung für dynamisches Generieren und Nachladen von Programmcode
• Durch Reflektionsmechanismen ist es Prozessen möglich, ihren eigenen Programmcode zur Laufzeit zu analysieren und modifizieren (Bsp.: Just-In-Time Compilation von Programmcode durch die Java Virtual Machine). Ebenso lassen sich Programmerweiterungen und Plug-Ins zur Laufzeit direkt in den Adressraum eines Prozesses laden. So ist bspw. eine Vielzahl an Treibern heutzutage von vorne herein als Modul realisiert, das dynamisch in den Kernel eingebunden werden kann.
• Bereitstellung einer universellen API, die die direkte Modifikation der Daten eines Prozesses ermöglicht (Bsp.: Debugging APIs für unprivilegierte Prozesse).

Die Nachteile einer solchen Architektur liegen auf der Hand:

• Shared Memory stellt zwar einen effektiven Kommunikationsmechanismus dar, ist aber aufgrund der erforderlichen Zugriffssynchronisation recht fehleranfällig und geht mit der Kopplung des Fehlerverhaltens aller beteiligten Prozesse einher.
• Dynamisch nachladbare Softwarekomponenten enthalten potentiell fehlerhaften oder gar böswilligen Code. Trotzdem werden sie ohne weitere Sicherheitsvorkehrungen direkt in den privaten Adressraum eines Prozesses, ja häufig sogar direkt in den Kernel eingebunden. So wird bspw. berichtet [47], dass bis zu 85% aller diagnostizierten Windows- Abstürze auf fehlerhafte Treiber zurückzuführen sind.
• Die Implementation solcher Erweiterungen geschieht häufig unter Verwendung privater Details des Hostcodes, d.h.: ohne die Verwendung klar definierter Interfaces. Diese Verquickung von Host und Erweiterung erschwert zum einen die Wartbarkeit und verursacht zum anderen leicht Kompatibilitätsprobleme, falls sich der Hostcode an entscheidenden Stellen ändert.
• Die Möglichkeit Code zur Laufzeit einzubinden, stellt eine erhebliche Einschränkung für die Optimierung und Verifikation der Korrektheit des Programmcodes durch den Compiler oder andere statische Werkzeuge dar. Diese können in der Regel nicht davon ausgehen, dass sich der bestehende Code zwischen zwei Instruktionen zur Laufzeit nicht ändert. So ist es vorab bspw. unmöglich vorherzusagen, ob ein bestimmter Programmteil zur Laufzeit überhaupt Verwendung finden wird oder nicht. Folglich kann ein Compiler diesen auch nicht von vorneherein als toten Code einstufen und von der Übersetzung ausnehmen. Die Optimierung des Programmcodes muss also zu großen Teilen zur Laufzeit erfolgen, was sich negativ auf die Performance auswirken kann.

Das Hauptziel der Entwicklung von Singularity bestand in der Beseitigung der Schwächen einer offenen Prozessarchitektur, die durch die Aufweichung der Prozessisolation entstehen, wobei es Mechanismen zu entwickeln galt, die effektive Systemrufe sowie eine performante Interprozesskommunikation ermöglichen.

Architektur des Singularity-Prototyps

Singularity verfolgt das Konzept einer geschlossenen Prozessarchitektur ("Sealed Process Architecture"). Ein spezielles Prozessmodell, der softwareisolierte Prozess ("Software Isolated Process" oder SIP), kombiniert mit einem eigens entwickelten Kommunikationsmechanismus, dem so gennannten Channel, sorgt dafür, dass das System eine akzeptable Performance erreicht.

Geschlossene Prozessarchitektur

Eine geschlossene Prozessarchitektur zeichnet sich durch die vier folgenden Invarianten aus:

1. "Fixed Code Invariant"
   Ist ein Prozess einmal gestartet, so kann sein Programmcode nachträglich nicht mehr verändert werden. Dynamisches Generieren oder Nachladen von Code werden durch das System nicht unterstützt. Module sowie Programmerweiterungen werden jeweils als eigenständiger Prozess gestartet, der mit der Host-Applikation auf gesondertem Wege kommuniziert.
2. "State Isolation Invariant"
   Der direkte Zugriff auf die Daten eines Prozesses ist nur ihm selbst und keinem anderen Prozess gestattet. Es ist einem Prozess demnach strikt untersagt, einen gültigen Verweis auf Daten eines anderen Prozesses zu besitzen.
3. "Explicit Communication Invariant"
   Die gesamte Interprozesskommunikation erfolgt über explizite (verbose) Mechanismen. Der Sender einer Nachricht identifiziert sich explizit gegenüber dem Adressaten, sodass dieser die Möglichkeit erhält, den Empfang oder die Weiterleitung von Mitteilungen eines speziellen Senders abzulehnen. Eine Kommunikationsmöglichkeit über Shared Memory besteht nicht.
4. "Closed API Invariant"
   Die System-API darf keinem unprivilegierten Prozess Funktionalitäten bereitstellen, die es ihm erlauben, eine der drei anderen Invarianten zu verletzen.
   Beispiel: Export einer universellen Debugging-API, die einen lesenden und schreibenden Zugriff auf Daten eines beliebigen Prozesses ohne dessen Einwilligung ermöglicht.
   Allgemein: Direkte Verwendung privilegierter CPU-Assemblerinstruktionen durch unprivilegierte Prozesse.

Obwohl dieses Systemdesign offensichtlich wesentliche Schwächen einer offenen Prozessarchitektur beseitigt, tut sich bei der konkreten Umsetzung doch vor allem eine gewichtige Schwierigkeit auf:

Um die Zustandsisolation (Invariante 2) der einzelnen Prozesse zu gewährleisten, sind die herkömmlichen, hardwaregestützten Mechanismen (CPU-Betriebsmodi und MMU) offensichtlich ungeeignet, da bei ihrer Verwendung vor allem der Übergang vom User- in den Kernelmodus zu kostspielig ausfiele. Im Falle der Nachrichtenübermittlung wäre zusätzlich ein erheblicher Kopieraufwand zu betreiben. Die auszutauschenden Daten müssten jeweils über den Kernel vom Adressraum des Senders vollständig in denjenigen des Empfängers kopiert werden.

Singularity begegenet diesem Problem wie folgt:

Der bekannte Hardwaremechanismus zur Zugriffskontrolle wird durch eine größtenteils statisch durchführbare, softwarebasierte Überprüfung der Zustandsisolation ersetzt, was sich äußerst günstig auf die Systemperformance auswirkt. Das zur Implementation des Systems verwendete C#-Derivat Sing# verfügt über eine erweiterte Syntax, die eine explizite Spezifikation des Kommunikationsverhaltens von Prozessen unterstützt, wie sie die Kommunikationsinvariante der geschlossenen Prozessarchitektur fordert. Hierdurch wird die Einhaltung der Zustandsisolation selbst im kritischen Fall der Interprozesskommunikation, während der zwangsläufig Daten zwischen Prozessen ausgetauscht werden, bereits zur Installationszeit möglich. Aufgrund der Verwendung von Softwaretools zur Sicherung der Isolation werden Prozesse in Singularity auch als softwareisolierte Prozesse ("Software Isolated Processes" oder SIPs) bezeichnet. Der zur Kommunikation verwendete Channel-Mechanismus bietet zudem die Möglichkeit selbst große Datenmengen ohne Kopieraufwand zwischen einzelnen SIPs zu versenden.

Typ- und Speichersicherheit

Typ- und Speichersicherheit sind eng miteinander verwobene Eigenschaften einer Programmiersprache. Sie bilden die Grundlage der Prozessisolation in Singularity.

Typsicherheit garantiert, dass der Inhalt einer variablen eines bestimmten Typs immer korrekt interpretiert und manipuliert wird, d.h. keine Operationen auf einem Datenobjekt ausgeführt werden, die für den speziellen Objekttyp nicht definiert sind und daher zumeist zu nicht vorhersehbaren Fehlern führen. Cast-Operationen zu nicht verwandten Typen sind somit in jedem Fall untersagt.

Speichersicherheit unterbindet den willkürlichen Zugriff auf beliebige Speicheradressen, stellt sicher, dass vorhandene Referenzen innerhalb eines Programms stets auf Speicherbereiche verweisen, die mit einem gültigen Datenobjekt belegt sind und beseitigt somit weitere typische Quellen für Programmfehler. Dazu wird in der Regel eine manuelle Speicherverwaltung mithilfe von Pointern und Pointerarithmetik gänzlich ausgeschlossen. Garbage Collectoren übernehmen die Deallokation von Heapspeicher und verhindern das Auftreten von dangling References.

Speichersicherheit ist ohne Typsicherheit nicht denkbar. Ohne diese wäre es problemlos möglich, bspw. einen Integer zu einem Pointer zu casten und damit - das Vorhandensein eines zusätzlichen Schutzes durch das Betriebssystem ausgeschlossen - Zugriff auf nahezu beliebige Speicheradressen zu erlangen. Ebenso bildet Speichersicherheit eine notwendige Voraussetzung für die Typsicherheit einer Sprache. Ein willkürlicher Speicherzugriff über Pointer, würde das Kopieren eines beliebigen, typfremden Datenbjekts in den Speicherbereich einer jeden Variablen erlauben.

Beispiele für sichere, objektorientierte Sprachen sind bspw. Java, Python oder C#, auf das auch die zur Implementation von Singularity verwendete Sprache Sing# aufbaut.

SIPs - Softwareisolierte Prozesse

SIPs bilden das Gegenstück zu Prozessen in handelsüblichen Betriebssystemen, zeichnen sich aber im Gegensatz zu diesen durch einige Besonderheiten aus:

• SIPs sind abgeschlossene Coderäume, d.h.: sie sind nicht befähigt zur Laufzeit Code ( Klassen, Bibliotheken, etc. ) nachzuladen ( Fixed Code Invariant ).

• SIPs sind typ- und speichersicher.
  Die Typ- und Speichersicherheit des SIP-Codes kann in Singularity zum Großteil bereits zur Compilezeit überprüft werden. In einigen Fällen, bspw. zur Überprüfung dynamischer Typen, sind allerdings weiterhin Laufzeittests erforderlich.
  Die statische Verfifikation der Typ- und Speichersicherheit läuft in mehreren Schritten ab:
  Das Compiler-Frontend übersetzt den vorliegenden Programmcode zunächst in eine Zwischenrepräsentation vergleichbar mit dem Java-Bytecode, die als Microsoft Intermediate Language (MSIL) oder Common Intermediate Language (CIL) bezeichnet wird. Dabei wird die Typsicherheit des nativen Programms überprüft.
  Das produzierte Compilat ist ebenfalls mit Typinformation ausgestattet, die ausgenutzt wird, um in einem zweiten Schritt auch dessen Typsicherheit zu verifizieren. Fehler, die mit der Übersetzung in den Zwischencode zusammenhängen, können so rechtzeitig erkannt werden.
  Im letzten Schritt wird schließlich der Zwischencode durch das Compiler-Backend in ausführbaren x86-Code überführt. Derzeit wird die Entwicklung einer Typed Assembly Language (TAL) angestrebt, die es ermöglichen soll, den an sich typlosen, ausführbaren Binärcode mithilfe eines schlanken Verifikators ein weiteres Mal auf seine Sicherheit hin zu überprüfen, um Fehler im abschließenden Compilationsschritt aufzuspüren. Solange diese Arbeit noch nicht abgeschlossen ist, kommen nur solche Sprachen für die Applikationsprogrammierung in Frage, die sich nach MSIL übersetzen lassen. Alternativ ist es möglich, bereits bestehende, in anderen Sprachen verfasste Programme in einer hardwareisolierten Domäne zur Ausführung zu bringen (siehe Paper 3).

• SIPs sind in der Lage, untereinander Nachrichten auszutauschen. Diese werden in einer speziell zu diesem Zweck vorgesehenen Hauptspeicherregion, dem Exchange Heap, verwahrt und können über so genannte Channels vesandt werden.
  Für jeden Channel existiert ein Kommunikationsvertrag (Contract), der den Typ des Channels, den Typ der versendeten Nachrichten und den Ablauf der Kommunikation explizit spezifiziert. Anhand dieser Information lässt sich wiederum bereits zur Compilezeit überprüfen, dass die geforderte Zustandsisolation nicht durch Übergabe von Objektreferenzen oder den parallelen Zugriff auf Nachrichten durch Sender und Empfänger verletzt wird, und dass Typ- sowie Speichersicherheit auch während der Kommunikation gewahrt bleiben(Explicit Communication Invariant).

• SIPs sind unprivilegierte Prozesse.
  Die Ausführung privilegierter Operationen bleibt auf den Kernel beschränkt, der eine eigene softwareisolierte Domäne bildet. Die Trennung zwischen privilegierten und unprivilegierten Prozessen erfolgt nicht wie gewohnt unter Nutzung der verschiedenen Betriebsmodi der x86-Hardware, sondern wird erneut durch eine statische Überprüfung der Programme zum Zeitpunkt der Installation vollzogen. Unprivilegierte Programme, deren Code auf privilegierte CPU-Instruktionen zurückgreift, werden vom System abgelehnt.
  Zugriff auf privilegierte Operationen erhalten SIPs - wie auch in anderen Betriebssystemen üblich - nur mittels Systemruf. Der Kernel exportiert keine Funktionalitäten, die eine Verletzung der Architekturinvarianten erlauben könnte. Systemrufe akzeptieren lediglich primitive Argumente (Closed API Invariant).

• SIPs bilden geschlossene, komplett voneinander isolierte Objekträume (State Isolation Invariant).
  Kein SIP besitzt eine direkte Referenz auf Objekte eines anderen SIPs. Nachrichten haben zu jedem Zeitpunkt einen eindeutigen Besitzer, der über ein exklusives Zugriffsrecht verfügt. Diese Isolation ergibt sich direkt aus der verifizierten Typ- und Speichersicherheit, den geschilderten Kommunikationsregeln und der Closed-API-Invariant. /* TODO: Kleine Erläuterung anfügen! */
  Konsequenzen für die Systemperformance:

• Aufgrund der für SIPs geltenden Zustandsisolation lassen sich jeweils individuelle, auf die Bedürfnisse der entsprechenden Applikation zugeschnittene Laufzeitumgebungen und Garbage-Collectoren verwenden, was sich positiv auf die Laufzeitperformance der Prozesse auswirkt.
• Alle SIPs können mitsamt dem Kernel und dem Exchange Heap in ein- und demselben virtuellen Adressraum im Privilege-Ring 0 laufen, ohne dass dabei eine Gefahr von Zugriffsverletzungen für laufende Prozesse oder die Hardware besteht. Es kann also eine systemweit einheitlich geltende Pagetabelle zur Adressübersetzung verwendet werden, was den Verwaltungsaufwand für Prozesse erheblich reduziert und die Prozesserzeugung vereinfacht. Ebenso profitiert die Performance des Kontextwechsels,bei dem nun auf einen Wechsel des Speicherkontextes und einen Flush des Translation Lookaside Buffer verzichtet werden kann.
  Systemrufe lassen sich unter diesen Voraussetzungen wie gewöhnliche Funktionsaufrufe ausführen, also ohne dass dabei ein Wechsel des Stacks, des Adressraums oder des CPU-Betriebsmodus erforderlich wäre, woraus sich ein erheblicher Geschwindigkeitszuwachs ergibt. Stackframes des Kernels sind für den Garbage-Collector entsprechend zu kennzeichnen.

Auch die Umsetzung der Softwareisolation ist noch mit ungelösten Problemen, wie bspw. den Umgang mit DMA behaftet. Auf eine genauere Betrachtung wird aber an dieser Stelle verzichtet.

Interprozesskommunikation über Channels

Channels stellen einen universellen, bidirektionalen Kommunikationsmechanismus dar, den SIPs in Singularity zur effektiven Interaktion untereinander oder mit dem Kernel nutzen. Dabei ist stets sicherzustellen, dass die Kommunikationspartner beim Austausch von Nachrichten isoliert bleiben (State Isolation Invariant!).

Exchange Heap

Der Exchange Heap repräsentiert eine speziell für die Übermittlung von Nachrichten vorgesehene Hauptspeicherregion, die sich in ein- und demselben Adressraum mit den SIPs sowie dem Singularity-Kernel befindet.
Neben den eigentlichen Nachrichten enthält der Heap auch die Endpunkte der Channels, über die die Versendung stattfindet.
Alle im Bereich des Heaps abgelegten Daten unterliegen speziellen Restriktionen, die die Zustandsisolation als Systeminvariante auch während des Nachrichtenaustauschs garantieren:

• Der Exchange Heap beinhaltet weder Objekte (Attribute + Funktionen) noch Referenzen auf Objekte, die sich im Objektraum eines SIPs befinden. Folglich handelt es sich bei Nachrichten ausnahmslos um primitive Datentypen oder Strukturen. Verweise in den Exchange Heap selber sind diesen allerdings grundsätzlich gestattet. So lassen sich auch komplexere Datenkonstrukte als Nachricht übermitteln.
• Jedes Datum innerhalb des Heaps lässt sich zu jedem Zeitpunkt einem eindeutigen Besitzer (Prozess oder Thread) zuordnen. Mit dem Versenden einer Nachricht wird gleichzeitig das zugehörige Zugriffsrecht vom Sender an den Empfänger abgetreten und kann ohne dessen Kooperation auch nicht wieder erlangt werden.

Gerade im Rahmen der Interprozesskommunikation wird die Bedeutung der Zustandsisolation für die Fehlertoleranz des Systems deutlich:
Sind verschiedene Anwendungen intensiv über geteilte Datenstrukturen miteinander verwoben, ist es im Fehlerfalle nahezu unmöglich eine saubere Fehlererholung durchzuführen, da hierzu nun nicht mehr nur der lokale Programmzustand, sondern eben auch derjenige der einzelnen Kommunikationspartner berücksichtigt werden muss. Eine Beendigung des fehlerhaften Prozesses samt Freigabe seiner Ressourcen - mit oder ohne geteilte Daten - gestaltet sich ebenfalls problematisch. Dieses Vorgehen hinterließe alle anderen Beteiligten in einem potenziell nicht konsistenten Zustand. Folglich besteht der einzige Ausweg zumeist in der vollständigen Terminierung aller Interaktionspartner (Bsp.: Java VM).
In Singularity lässt sich eine solche Situation weitaus eleganter lösen.
Da sich SIPs allgemein keinen Speicher teilen, ist es immer möglich, einen fehlerhaften Prozess zu beenden und dessen Speicherressourcen freizugeben, ohne dass dabei die Gefahr von Inkonsistenzen oder des Zugriffs auf dangling References für andere Prozesse bestünde. Diese werden über die neue Situation mit einer Exception durch den Kernel informiert, wodurch eine Fehlererholung angestoßen wird, die sich ausschließlich mit den lokalen Gegebenheiten des jeweiligen Prozesses auseinandersetzen muss.

Channels

Ein Channel stellt ein Konstrukt aus genau zwei Endpunkten dar, die über Verweise miteinander verbunden sind und zwischen denen bidirektional Nachrichten verschickt werden können. Die Endpunkte liegen als Strukturen im Exchange Heap vor und lassen sich so selbst als Nachrichten über bestehende Channels versenden. Auf diese Weise besteht die Möglichkeit, ein dynamisch wachsendes Kommunikationsnetzwerk zwischen einzelnen SIPs zu schaffen. Die Endpunkte eines Channles nehmen bei der Kommunikation verschiedene Rollen ein, die an das bekannte Client-Server-Modell angelehnt sind. Sie werden als Exporter (Exp vgl. Server) und Importer (Imp vgl. Client) bezeichnet. Endpunkte besitzen zusätzlich einen speziellen Typ, der durch den zugrundeliegenden Contract bestimmt wird (Bsp: Contract1.Imp, Contract1.Exp).

Contracts

Contracts ("Kommunikationsverträge") bilden das Fundament für den gesamten Kommunikationsvorgang, der zwischen zwei Prozessen über den dazugehörigen Channel abläuft. Sinn und Zweck eines Contracts ist es, alle Details dieses Vorgangs so explizit wie möglich zu formulieren (Explicit Communication Invariant), um anhand dieser Information vor allem die Wahrung der Zustandsisolation während des Datenaustausches in vollem Umfang überprüfen zu können. Das von den Singularity-Entwicklern entworfene C#- Derivat Sing# unterstütztdie Formulierung solcher Contracts durch eine spezielle Syntaxerweiterung.
Contracts werden grundsätzlich aus der perspektive des Exporters (Servers) verfasst. Die Angaben für den Importer (Client) ergeben sich als Komplement hierzu, weshalb sie nicht noch einmal gesondert aufgeführt werden.
Folgende Angaben sind obligatorisch:

• Nachrichtentyp und Nachrichtenargumente. Optional kann eine Richtung angegeben werden, in der eine Nachricht über einen Channel versendet werden kann. Ist diese nicht spezifiziert, wird implizit eine bidirektionale Verwendbarkeit angenommen. Hierbei sind die für Nachrichtenargumente geltenden Einschränkungen zu beachten (siehe Exchange Heap).
• Ein Kommunikationsprotokoll, das die Reihenfolge erwarteter und versendeter Nachrichten sowie daran gekoppelte Aktionen auflistet. Zur Protokollbeschreibung werden endliche Automaten verwendet.

Zusätzlich zum eigentlichen Vertragstext sind alle Methoden anzugeben, die auf den Endpunkten des durch den Contact definierten Channels ausgeführt werden können.

Abbildung x zeigt einen einfachen Contract:
Der Exp wartet in einer Endlosschleife auf eine Nachricht des Typs Request und reagiert auf deren Erhalt mit einer entsprechenden Antwort oder einer Fehlermeldung. Die Methoden, die einem Entwickler zur Implementierung des angegebenen Kommunikationsprotokolls zur Verfügung stehen, sind in Abbildung y deklariert.

Die Korrektheit des Contracts sowie die Einhaltung der in ihm gemachten Angaben durch eine Applikaton, wird durch den Sing#-Compiler ("Bartok") überwacht. Dieser bricht den Compilationsprozess ab, falls der Vertrag einen erkennbaren Fehler enthält oder der Applikationscode in irgendeinem Punkt vom diesem abweicht. Durch die explizite Regelung der Kommunikation im Contract und dessen strikte Durchsetzung durch den Compiler, wird der Rahmen für die Interprozesskommunikation so eng abgesteckt, dass eine Verfikation der Zustandsisolation (Typsicherheit der Nachrichten, korrekte Übertragung von Zugriffsrechten) ebenfalls nahezu vollständig zur Compilezeit vollzogen werden kann.