Der Schlüssel zum Kopierraum
Eine Sperre (englisch Lock) sorgt dafür, dass immer nur ein Prozess in einem bestimmten Abschnitt arbeitet. Das nennt man gegenseitigen Ausschluss. Eine Sperre, die nur meistens hält, ist gefährlich.
Im Kopierraum einer Hochschule darf immer nur eine Person sein, und der Schlüssel hängt an einem Haken. SPIN prüft für jede Reihenfolge, ob eine Sperre das wirklich garantiert.
Am Ende dieser Lektion
Notiz
Ich kann eine Sperre schreiben, bei der SPIN keinen Fehler meldet.
Schlüsselwörter
| Begriff | Was er bedeutet | Beispiel |
|---|---|---|
| Sperre (Lock) | ein Zeichen, dass ein Abschnitt besetzt ist | |
| Gegenseitiger Ausschluss | höchstens ein Prozess ist im Abschnitt | |
| Kritischer Abschnitt | der Teil eines Prozesses, der allein laufen muss | |
| Unteilbar (atomic) | ein Schritt, in den kein anderer Prozess eingreift | atomic { ... } |
| Verklemmung (Deadlock) | kein Prozess kann mehr weiter | |
| Modellprüfung | ein Werkzeug probiert alle Abläufe eines Modells durch | SPIN |
Die Zellen, die Lernende ausfüllen, bleiben in dieser Vorschau leer.
Eine Sperre aus einem Zeichen reicht nicht
Der Schlüssel am Haken ist eine Variable: schluessel ist 0, wenn er hängt, und 1, wenn jemand ihn hat. Wer den Raum betreten will, wartet, bis schluessel gleich 0 ist, und setzt ihn dann auf 1.
In Promela ist eine Bedingung wie schluessel == 0 ein Schritt, der erst ausführbar wird, wenn sie wahr ist. Das Warten und das Setzen sind aber zwei getrennte Schritte.
Die Sperre mit zwei getrennten Schritten
bit schluessel = 0
byte drin = 0
active [2] proctype student() {
schluessel == 0 -> schluessel = 1
drin++ -> assert(drin == 1) -> drin--
schluessel = 0
}
Das Modell schreiben und von SPIN prüfen lassen
Die Zusicherung assert(drin == 1) hält fest, dass nie zwei Personen zugleich im Raum sind. drin++ und drin-- zählen sie.
Der erste Befehl legt den Ordner an, falls er fehlt. Der zweite schreibt das Modell, der dritte lässt SPIN alle Abläufe prüfen.
Den Ordner anlegen, falls er fehlt
mkdir -p ~/werkstattHier angezeigt, nicht ausgeführt. Erstellen Sie ein kostenloses Konto, um „Ausführen“ zu drücken und ihn im Terminal Ihres eigenen Labs einzugeben.
Das Modell mit zwei Schritten schreiben
printf '%s\n' 'bit schluessel = 0' 'byte drin = 0' 'active [2] proctype student() {' ' schluessel == 0 -> schluessel = 1' ' drin++ -> assert(drin == 1) -> drin--' ' schluessel = 0' '}' > ~/werkstatt/kopierraum.pmlHier angezeigt, nicht ausgeführt. Erstellen Sie ein kostenloses Konto, um „Ausführen“ zu drücken und ihn im Terminal Ihres eigenen Labs einzugeben.
Hält diese Sperre?
spinrun ~/werkstatt/kopierraum.pml | grep -o "errors: [0-9]*"Hier angezeigt, nicht ausgeführt. Erstellen Sie ein kostenloses Konto, um „Ausführen“ zu drücken und ihn im Terminal Ihres eigenen Labs einzugeben.
Ein unteilbarer Schritt macht die Sperre dicht
Die Lösung ist, Warten und Setzen zu einem einzigen Schritt zu machen. In Promela setzt man sie in einen atomic-Block: Kein anderer Prozess läuft dazwischen.
Nun kann nur noch einer den Schlüssel nehmen, denn der Zweite sieht ihn erst wieder frei, wenn der Erste ihn zurückgehängt hat.
Die Sperre mit einem unteilbaren Schritt
bit schluessel = 0
byte drin = 0
active [2] proctype student() {
atomic { schluessel == 0 -> schluessel = 1 }
drin++ -> assert(drin == 1) -> drin--
schluessel = 0
}
Das bessere Modell schreiben
printf '%s\n' 'bit schluessel = 0' 'byte drin = 0' 'active [2] proctype student() {' ' atomic { schluessel == 0 -> schluessel = 1 }' ' drin++ -> assert(drin == 1) -> drin--' ' schluessel = 0' '}' > ~/werkstatt/kopierraum2.pmlHier angezeigt, nicht ausgeführt. Erstellen Sie ein kostenloses Konto, um „Ausführen“ zu drücken und ihn im Terminal Ihres eigenen Labs einzugeben.
Hält diese Sperre?
spinrun ~/werkstatt/kopierraum2.pml | grep -o "errors: [0-9]*"Hier angezeigt, nicht ausgeführt. Erstellen Sie ein kostenloses Konto, um „Ausführen“ zu drücken und ihn im Terminal Ihres eigenen Labs einzugeben.
Ein häufiger Fehler
Warnung
Viele denken: Wenn SPIN keinen Fehler findet, ist die Sperre richtig. Das gilt nur für das, was geprüft wird. Die Zusicherung sagt nichts darüber, ob alle Prozesse fertig werden. Auch eine Sperre, die nie öffnet, hält den Ausschluss ein.
Wer den Schlüssel nie zurückhängt, verklemmt alle
Vergisst ein Prozess den Schlüssel zurückzugeben, wartet der andere für immer. SPIN meldet das als ungültigen Endzustand: Ein Prozess steht still, obwohl er nicht fertig ist. Das ist eine Verklemmung.
Das Modell unten lässt die letzte Zeile weg. Die Zusicherung bricht nie, trotzdem gibt es einen Fehler.
Das Modell ohne Zurückhängen schreiben
printf '%s\n' 'bit schluessel = 0' 'byte drin = 0' 'active [2] proctype student() {' ' atomic { schluessel == 0 -> schluessel = 1 }' ' drin++ -> assert(drin == 1) -> drin--' '}' > ~/werkstatt/kopierraum3.pmlHier angezeigt, nicht ausgeführt. Erstellen Sie ein kostenloses Konto, um „Ausführen“ zu drücken und ihn im Terminal Ihres eigenen Labs einzugeben.
Was meldet SPIN ohne Freigabe?
spinrun ~/werkstatt/kopierraum3.pml | grep -o "pan:1: invalid end state"Hier angezeigt, nicht ausgeführt. Erstellen Sie ein kostenloses Konto, um „Ausführen“ zu drücken und ihn im Terminal Ihres eigenen Labs einzugeben.
Weiterführend
Das Lab hat einen eigenen Teil mit SPIN, in dem eine Sperre in einen fertigen Rahmen gehört. Seine Prüfung gilt dem, was Sie dort schreiben.
Schreiben Sie dort Ihre eigene Sperre, und lesen Sie die Meldung von SPIN genau, bevor Sie etwas ändern.