Eine neue Episode mit Impressionen aus Foliensätzen. Zwei Bilder und eine Formel aus einem Foliensatz über Zeitlogik zum Zwecke einer Überprüfung der Fairness-Eigenschaft, das ist der “gleichberechtigte und gleichmäßige Zugriff aller Teilnehmer eines Netzwerks auf die vorhandenen Netzwerkressourcen”.
Die beiden Bilder scheinen auf den ersten Blick recht ähnlich, doch die Suche nach dem Unterschied hat mich zu einem unerwarteten Gedankensprung geführt. Genauer geschah das, als ich um eine Interpretation der folgenden Formel rang:
Nach dem Break wird irgendwie zu rekonstruieren versucht, wohin der Sprung geführt hat, nämlich in poststrukturalistisches Gelände: Geisel, Alterität und Derrida’sche Gerechtigkeit. Ob das gelingt?
1. Erläuterung des Kontextes
Es geht um zwei nebenläufige (d.h. weitgehened kausal unabhängige) Prozesse, die auf eine gemeinsam genutzte Ressource zugreifen möchten, die jedoch immer nur ein Prozess gleichzeitig benutzen kann, man denke etwa an einen Hörsaal, in dem maximal eine Vorlesung gleichzeitig abgehalten werden kann. (diese Thematik wird manchmal durch das sogenannte Philosophen-Problem erläutert). Man möchte keinen der Prozesse prinzipiell und endgültig den Zugriff verwehren, darum muss man die Dimension der Zeit berücksichtigen (einmal bekommt Prozess 1, einmal Prozess 2 Zugriff).
Doch bei Computersystemen möchte man oft auf formale Verifikation nicht verzichten, um beispielsweise zu beweisen, dass Prozess 1 und Prozess zwei niemals zur selben Zeit auf die Ressource zugreifen können (bei hochkomplexen Systemen kann man nicht jeden Einzelfall durchtesten sondern beweist für alle unendlich vielen Fälle, dass dies nicht eintreten kann). Daher führt man eine Art von Zeit in der Logik ein, um Abläufe modellieren zu können. Jene in der Formel verwendete Variante einer temporalen Logik nennt sich Computational Tree Logic. Die stark verschachtelte obige Formel definiert in etwa die Möglichkeit, dass Prozess1 öfter nacheinander auf die Ressource zugreifen kann, ohne dass dazwischen Prozess2 drankommt.
Die beiden Modelle zeigen Protokolle, die das Konzept des “Mutual Exclusion” auf ihre je eigene Weise implementieren. Zu prüfen ist, ob bei beiden u.A. Fairness erfüllt ist, d.h. dass jeder Prozess, der sich ankündigt die Ressource nutzen zu wollen, sie irgendwann im Laufe der Zeit nutzen darf.
2. Vorkommende Kürzel
Der Fairness wegen noch eine Erklärung der Kürzel, die in den Modellen vorkommen:
- n… non-blocking state: Hier arbeitet der Prozess ruhig vor sich hin, ohne die gemeinsame Ressource zu benötigen.
- t… trying state: Der Prozess möchte gerne auf die gemeinsam genutzte Ressource zugreifen. Er äußert quasi den Wunsch, der sich durch einen Zustandsübergang von n zu t ausdrückt.
- c… critical state: Der Prozess greift momentan auf die Ressource zu.
- Die Indizes 1 und 2 zeigen an, um welchen Prozess es sich jeweils handelt.
- s… steht für state. Die Indizes benennen die Zustände.
3. Die Modelle:
Beim ersten Modell ist aufgrund von Zustand s3 ein interessanter Nicht-Determinismus vorhanden. Wenn beide Prozesse die Ressource benutzen möchten, landet das System in s3. Von dort führt ein Pfeil zu s4, was bedeutet dass Prozess1 die Ressource benutzen darf und ein Pfeil zu s7, der Prozess 2 dieses Recht einräumt. Für einen deterministischen Computer wäre das fatal. Es gibt kein Entscheidungsverfahren, das ihm einen Weg vorschlägt.Das Protokoll definiert nicht, welcher Prozess zuerst auf die Ressource zugreifen darf, wenn das System in der Situation ist, dass beide zugreifen wollen. Damit ist jedoch die Eigenschaft der Fairness nicht erfüllt:
(Für alle zeitlichen Abfolgen (Pfade) gilt in jedem Zustand: Wenn Prozess 1 auf die Ressource zugreifen möchte, dann soll er irgendwann in der Zukunft auch zugreifen können. Diese Eigenschaft ist nicht erfüllt.)
Und zwar deswegen weil nicht ausgeschlossen (möglich) ist, dass ein Prozess die Nicht-determiniertheit ausnützt um bis ans Ende aller Zeiten (da es sich in CTL um unendliche Pfade handelt, die baumartig aufspreizen können, muss man Zeit ins Plural setzen) die Ressource für sich zu beanspruchen. Beispielsweise wenn das System die Zustände s3,s4,s5 unendlich iteriert.
Man kann sich aufgrund des bisher Gesagten im zweiten Modell davon überzeugen, wie man die Nicht-Determiniertheit an dieser Stelle auflöst: Der frühere Zustand s3 wird kontextualisiert zugunsten des “Wer zuerst kommt..”. Man hat zwar trotzdem Nicht-Determinismus-Zustände im Modell, diese sind jedoch nicht gefährlich für die Fairness-Eigenschaft.
4. Zum Sprung ansetzen
Irgendwann fand ich mich selbst in eine Art Zustand, der dem Zustand s3 ähnelt: “Da spießt sich etwas mit dem, was ich am Begriff Gerechtigkeit verstehe”. S3 repreäsentiert doch das typische Muster einer Situation, in der Gerechtigkeit möglich ist, und zwar gerade weil nicht ausgeschlossen ist, dass einer der beiden Prozesse das System dominiert. Sobald sich S3 auflöst in ein striktes Entscheidungsverfahren, wo, wenn beide Kräfte schlagend werden, noch immer eine klare Kategorisierung erfolgt, dann entsteht keine Irritation und ich bin nicht genötigt, irgend etwas außergewöhnliches zu unternehmen. Ich bin vollkommen (fremd)bestimmt. Das Verfahren funktioniert (das ist für Computersysteme nötig) und es gibt kein Problem mehr.
5. Sprung
Indem ich nicht bloß mit einer einzigen Kraft, sondern mit einer Mannigfaltigkeit von Kräften zu tun habe, bin ich nicht völlig fremdbestimmt, so wie ich nicht völlig frei bin. Die Kräfte beanspruchen jenen Platz für sich allein, der prinzipiell nur von einer Kraft erfüllt werden kann. Durch diese Spannung komme ich unter Druck und bin genötigt, zu antworten und das Gewirr von Kräften angemessen zu repräsentieren, ihm gerecht zu werden.
“Man muss hier vom unmöglichen Ereignis sprechen. Von einem Un-Möglichen, das nicht nur unmöglich, nicht nur das Gegenteil des Möglichen ist, sondern gleichermaßen die Bedingung oder die Chance des Möglichen.” (Derrida: “Eine gewisse unmögliche Möglichkeit, vom Ereignis zu sprechen”, Merve 2003, S.41)