{"id":629,"date":"2010-01-07T23:17:42","date_gmt":"2010-01-07T22:17:42","guid":{"rendered":"http:\/\/phaidon.philo.at\/qu\/?p=629"},"modified":"2010-01-07T23:17:42","modified_gmt":"2010-01-07T22:17:42","slug":"gerechtigkeit-ist-unfair-temporallogische-abfahrt","status":"publish","type":"post","link":"https:\/\/quatsch.philo.at\/?p=629","title":{"rendered":"Gerechtigkeit ist unfair. Temporallogische Abfahrt"},"content":{"rendered":"<p>Eine neue Episode mit Impressionen aus Foliens\u00e4tzen. Zwei Bilder und eine Formel aus einem Foliensatz \u00fcber Zeitlogik zum Zwecke einer \u00dcberpr\u00fcfung der <a href=\"http:\/\/de.wikipedia.org\/wiki\/Fairness#Informatik\">Fairness<\/a>-Eigenschaft, das ist der &#8220;gleichberechtigte und gleichm\u00e4\u00dfige Zugriff aller Teilnehmer eines Netzwerks auf die vorhandenen Netzwerkressourcen&#8221;.<\/p>\n<p><a href=\".\/wp-content\/uploads\/2010\/01\/non-determinism.jpg\"><img loading=\"lazy\" decoding=\"async\" title=\"non-determinism\" src=\".\/wp-content\/uploads\/2010\/01\/non-determinism-300x192.jpg\" alt=\"\" width=\"277\" height=\"177\" \/><\/a><a href=\".\/wp-content\/uploads\/2010\/01\/die_Geisel.jpg\"><img loading=\"lazy\" decoding=\"async\" title=\"die_Geisel\" src=\".\/wp-content\/uploads\/2010\/01\/die_Geisel-300x195.jpg\" alt=\"\" width=\"279\" height=\"181\" \/><\/a><\/p>\n<p>Die beiden Bilder scheinen auf den ersten Blick recht \u00e4hnlich, doch die Suche nach dem Unterschied hat mich zu einem unerwarteten Gedankensprung gef\u00fchrt. Genauer geschah das, als ich um eine Interpretation der folgenden Formel rang:<\/p>\n<p><a href=\".\/wp-content\/uploads\/2010\/01\/Ich_darf_zweimal.jpg\"><img loading=\"lazy\" decoding=\"async\" title=\"Ich_darf_zweimal\" src=\".\/wp-content\/uploads\/2010\/01\/Ich_darf_zweimal-300x17.jpg\" alt=\"\" width=\"378\" height=\"21\" \/><\/a><\/p>\n<p>Nach dem Break wird irgendwie zu rekonstruieren versucht, wohin der Sprung gef\u00fchrt hat, n\u00e4mlich in poststrukturalistisches Gel\u00e4nde: Geisel, Alterit\u00e4t und Derrida&#8217;sche Gerechtigkeit.\u00a0 Ob das gelingt?<\/p>\n<p><!--more--><\/p>\n<p><strong>1. Erl\u00e4uterung des Kontextes<\/strong><\/p>\n<p>Es geht um zwei nebenl\u00e4ufige (d.h. weitgehened kausal unabh\u00e4ngige) Prozesse, die auf eine gemeinsam genutzte Ressource zugreifen m\u00f6chten, die jedoch immer nur ein Prozess gleichzeitig benutzen kann, man denke etwa an einen H\u00f6rsaal, in dem maximal eine Vorlesung gleichzeitig abgehalten werden kann. (diese Thematik wird manchmal durch das sogenannte <a href=\"http:\/\/de.wikipedia.org\/wiki\/Philosophenproblem\">Philosophen-Problem<\/a> erl\u00e4utert). Man m\u00f6chte keinen der Prozesse prinzipiell und endg\u00fcltig den Zugriff verwehren, darum muss man die Dimension der Zeit ber\u00fccksichtigen (einmal bekommt Prozess 1, einmal Prozess 2 Zugriff).<\/p>\n<p>Doch bei Computersystemen m\u00f6chte 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\u00f6nnen (bei hochkomplexen Systemen kann man nicht jeden Einzelfall durchtesten sondern beweist f\u00fcr alle unendlich vielen F\u00e4lle, dass dies nicht eintreten kann). Daher f\u00fchrt man eine Art von Zeit in der Logik ein, um Abl\u00e4ufe modellieren zu k\u00f6nnen. Jene in der Formel\u00a0 verwendete Variante einer temporalen Logik nennt sich Computational Tree Logic. Die stark verschachtelte obige Formel definiert in etwa die M\u00f6glichkeit, dass Prozess1 \u00f6fter nacheinander auf die Ressource zugreifen kann, ohne dass dazwischen Prozess2 drankommt.<\/p>\n<p>Die beiden Modelle zeigen Protokolle, die das Konzept des &#8220;Mutual Exclusion&#8221; auf ihre je eigene Weise implementieren. Zu pr\u00fcfen ist, ob bei beiden u.A. Fairness erf\u00fcllt ist, d.h. dass jeder Prozess, der sich ank\u00fcndigt die Ressource nutzen zu wollen, sie irgendwann im Laufe der Zeit nutzen darf.<\/p>\n<p><strong>2. Vorkommende K\u00fcrzel<\/strong><\/p>\n<p>Der<em> Fairness <\/em>wegen noch eine Erkl\u00e4rung der K\u00fcrzel, die in den Modellen vorkommen:<\/p>\n<ul>\n<li> n&#8230; non-blocking state: Hier arbeitet der Prozess ruhig vor sich hin, ohne die gemeinsame Ressource zu ben\u00f6tigen.<\/li>\n<li>t&#8230; trying state: Der Prozess m\u00f6chte gerne auf die gemeinsam genutzte Ressource zugreifen. Er \u00e4u\u00dfert quasi den Wunsch, der sich durch einen Zustands\u00fcbergang von n zu t ausdr\u00fcckt.<\/li>\n<li>c&#8230; critical state: Der Prozess greift momentan auf die Ressource zu.<\/li>\n<li>Die Indizes 1 und 2 zeigen an, um welchen Prozess es sich jeweils handelt.<\/li>\n<li>s&#8230; steht f\u00fcr state. Die Indizes benennen die Zust\u00e4nde.<\/li>\n<\/ul>\n<p><strong>3. Die Modelle: <\/strong><\/p>\n<p>Beim ersten Modell ist aufgrund von <strong><em>Zustand s3<\/em><\/strong> ein interessanter Nicht-Determinismus vorhanden. Wenn beide Prozesse die Ressource benutzen m\u00f6chten, landet das System in s3. Von dort f\u00fchrt ein<strong> Pfeil zu s4<\/strong>, was bedeutet dass Prozess1 die Ressource benutzen darf und ein <strong>Pfeil zu s7<\/strong>, der Prozess 2 dieses Recht einr\u00e4umt. F\u00fcr einen deterministischen Computer w\u00e4re das fatal. Es gibt kein Entscheidungsverfahren, das ihm einen Weg vorschl\u00e4gt.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\u00fcllt:<\/p>\n<p><a href=\"http:\/\/phaidon.philo.at\/qu\/wp-content\/uploads\/2010\/01\/Ich_k\u00f6nnte_dich_nicht_ranlassen.jpg\"><img loading=\"lazy\" decoding=\"async\" class=\"aligncenter size-full wp-image-633\" title=\"Ich_k\u00f6nnte_dich_nicht_ranlassen\" src=\"http:\/\/phaidon.philo.at\/qu\/wp-content\/uploads\/2010\/01\/Ich_k\u00f6nnte_dich_nicht_ranlassen.jpg\" alt=\"\" width=\"597\" height=\"32\" \/><\/a> (F\u00fcr alle zeitlichen Abfolgen (Pfade) gilt in jedem Zustand: Wenn Prozess 1 auf die Ressource zugreifen m\u00f6chte, dann soll er irgendwann in der Zukunft auch zugreifen k\u00f6nnen. Diese Eigenschaft ist nicht erf\u00fcllt.)<\/p>\n<p>Und zwar deswegen weil <em>nicht ausgeschlossen<\/em> (m\u00f6glich) ist, dass ein Prozess die Nicht-determiniertheit ausn\u00fctzt um bis ans Ende aller Zeiten (da es sich in CTL um unendliche Pfade handelt, die baumartig aufspreizen k\u00f6nnen, muss man Zeit ins Plural setzen) die Ressource f\u00fcr sich zu beanspruchen. Beispielsweise wenn das System die Zust\u00e4nde s3,s4,s5 unendlich iteriert.<\/p>\n<p>Man kann sich aufgrund des bisher Gesagten im zweiten Modell davon \u00fcberzeugen, wie man die Nicht-Determiniertheit an dieser Stelle aufl\u00f6st: Der fr\u00fchere Zustand s3 wird kontextualisiert zugunsten des &#8220;Wer zuerst kommt..&#8221;. Man hat zwar trotzdem Nicht-Determinismus-Zust\u00e4nde im Modell, diese sind jedoch nicht gef\u00e4hrlich f\u00fcr die Fairness-Eigenschaft.<\/p>\n<p><strong>4. Zum Sprung ansetzen<\/strong><\/p>\n<p>Irgendwann fand ich mich selbst in eine Art Zustand, der dem Zustand s3 \u00e4hnelt: &#8220;Da spie\u00dft sich etwas mit dem, was ich am Begriff Gerechtigkeit verstehe&#8221;. S3 repre\u00e4sentiert doch das typische Muster einer Situation, in der Gerechtigkeit m\u00f6glich ist, und zwar gerade weil nicht ausgeschlossen ist, dass einer der beiden Prozesse das System dominiert. Sobald sich S3 aufl\u00f6st in ein striktes Entscheidungsverfahren, wo, wenn beide Kr\u00e4fte schlagend werden, noch immer eine klare Kategorisierung erfolgt, dann entsteht keine Irritation und ich bin nicht gen\u00f6tigt, irgend etwas au\u00dfergew\u00f6hnliches zu unternehmen. Ich bin vollkommen (fremd)bestimmt. Das Verfahren funktioniert (das ist f\u00fcr Computersysteme n\u00f6tig) und es gibt kein Problem mehr.<\/p>\n<p><strong>5. Sprung<\/strong><\/p>\n<p>Indem ich nicht blo\u00df mit einer einzigen Kraft, sondern mit einer Mannigfaltigkeit von Kr\u00e4ften zu tun habe, bin ich nicht v\u00f6llig fremdbestimmt, so wie ich nicht v\u00f6llig frei bin. Die Kr\u00e4fte beanspruchen jenen Platz f\u00fcr sich allein, der prinzipiell nur von einer Kraft erf\u00fcllt werden kann. Durch diese Spannung komme ich unter Druck und bin gen\u00f6tigt, zu antworten und das Gewirr von Kr\u00e4ften angemessen zu repr\u00e4sentieren, ihm gerecht zu werden.<\/p>\n<p>&#8220;Man muss hier vom unm\u00f6glichen Ereignis sprechen. Von einem Un-M\u00f6glichen, das nicht nur unm\u00f6glich, nicht nur das Gegenteil des M\u00f6glichen ist, sondern gleicherma\u00dfen die Bedingung oder die Chance des M\u00f6glichen.&#8221; (Derrida: &#8220;Eine gewisse unm\u00f6gliche M\u00f6glichkeit, vom Ereignis zu sprechen&#8221;, Merve 2003, S.41)<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Eine neue Episode mit Impressionen aus Foliens\u00e4tzen. Zwei Bilder und eine Formel aus einem Foliensatz \u00fcber Zeitlogik zum Zwecke einer \u00dcberpr\u00fcfung der Fairness-Eigenschaft, das ist der &#8220;gleichberechtigte und gleichm\u00e4\u00dfige Zugriff aller Teilnehmer eines Netzwerks auf die vorhandenen Netzwerkressourcen&#8221;. Die beiden Bilder scheinen auf den ersten Blick recht \u00e4hnlich, doch die Suche nach dem Unterschied hat<a class=\"more-link\" href=\"https:\/\/quatsch.philo.at\/?p=629\">Read more<\/a><\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[3,11],"tags":[99,106,144,186],"class_list":["post-629","post","type-post","status-publish","format-standard","hentry","category-bric-a-brac","category-philosophie-klassisch","tag-informatisch","tag-irritation","tag-poststrukturalismus","tag-umstritten"],"_links":{"self":[{"href":"https:\/\/quatsch.philo.at\/index.php?rest_route=\/wp\/v2\/posts\/629","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/quatsch.philo.at\/index.php?rest_route=\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/quatsch.philo.at\/index.php?rest_route=\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/quatsch.philo.at\/index.php?rest_route=\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/quatsch.philo.at\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=629"}],"version-history":[{"count":0,"href":"https:\/\/quatsch.philo.at\/index.php?rest_route=\/wp\/v2\/posts\/629\/revisions"}],"wp:attachment":[{"href":"https:\/\/quatsch.philo.at\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=629"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/quatsch.philo.at\/index.php?rest_route=%2Fwp%2Fv2%2Fcategories&post=629"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/quatsch.philo.at\/index.php?rest_route=%2Fwp%2Fv2%2Ftags&post=629"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}