Das letzte Brot wird zweimal verkauft
Eine Race Condition (Wettlaufsituation) entsteht, wenn das Ergebnis eines Programms davon abhängt, in welcher Reihenfolge zwei Abläufe ihre Schritte ausführen. Sie ist schwer zu finden, weil sie nur manchmal auftritt.
Eine Bäckerei hat noch ein Brot. Zwei Verkäufer prüfen gleichzeitig, ob eines da ist, und verkaufen es beide. Das Modellprüfprogramm SPIN findet diese Reihenfolge, indem es alle durchprobiert.
Am Ende dieser Lektion
Notiz
Ich kann eine Race Condition in der Ablaufspur eines Programms finden.
Schlüsselwörter
| Begriff | Was er bedeutet | Beispiel |
|---|---|---|
| Prozess | ein Ablauf aus Schritten, der neben anderen läuft | |
| Nebenläufigkeit | mehrere Prozesse laufen zur selben Zeit | |
| Interleaving | eine bestimmte Mischung der Schritte mehrerer Prozesse | |
| Race Condition | das Ergebnis hängt von der Reihenfolge der Schritte ab | |
| Zusicherung (assert) | eine Bedingung, die an einer Stelle gelten muss | assert(verkauft <= 1) |
| Ablaufspur (Trace) | die Schritte, die zu einem Fehler führen |
Die Zellen, die Lernende ausfüllen, bleiben in dieser Vorschau leer.
Zwei Abläufe lassen sich beliebig mischen
Zwei Prozesse laufen nebenläufig: Der Rechner führt immer nur einen Schritt eines Prozesses aus, wechselt aber dazwischen, wann er will. Jede mögliche Folge heißt Interleaving.
Im Verkaufsbeispiel hat jeder Verkäufer vier Schritte: prüfen, zählen, Brot nehmen, nachprüfen. Die Tabelle zeigt eine Mischung, die schiefgeht.
Eine Mischung, bei der zweimal verkauft wird
| Schritt | Wer | Was | brot | verkauft |
|---|---|---|---|---|
| 1 | A | prüft: brot > 0 ist wahr | 1 | 0 |
| 2 | A | zählt: verkauft + 1 | 1 | 1 |
| 3 | B | prüft: brot > 0 ist noch wahr | 1 | 1 |
| 4 | A | nimmt das Brot | 0 | 1 |
| 5 | A | prüft: verkauft <= 1 ist wahr | 0 | 1 |
| 6 | B | zählt: verkauft + 1 | 0 | 2 |
| 7 | B | nimmt ein Brot, das es nicht gibt | 255 | 2 |
| 8 | B | prüft: verkauft <= 1 ist falsch | 255 | 2 |
Die Zellen, die Lernende ausfüllen, bleiben in dieser Vorschau leer.
Promela beschreibt die Verkäufer als Prozesse
SPIN liest Modelle in der Sprache Promela. byte legt eine kleine Zahl an. active [2] proctype verkaeufer() startet zwei Prozesse mit demselben Ablauf.
-> trennt Schritte, if :: ... fi wählt einen Fall, dessen erster Schritt ausführbar ist. assert bricht ab, wenn die Bedingung falsch ist.
Das Modell der Bäckerei
byte brot = 1
byte verkauft = 0
active [2] proctype verkaeufer() {
if
:: brot > 0 -> verkauft++ -> brot-- -> assert(verkauft <= 1)
:: else -> skip
fi
}
Das Modell in eine Datei schreiben und prüfen
Der erste Befehl legt einen Ordner an, der zweite schreibt das Modell in eine Datei. printf '%s\n' gibt jeden Text in Anführungszeichen als eigene Zeile aus. Danach prüft spinrun die Datei.
Ihre Dateien im Lab bleiben unberührt: Das Modell liegt in einem eigenen Ordner.
Einen Ordner anlegen
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 schreiben
printf '%s\n' 'byte brot = 1' 'byte verkauft = 0' 'active [2] proctype verkaeufer() {' ' if' ' :: brot > 0 -> verkauft++ -> brot-- -> assert(verkauft <= 1)' ' :: else -> skip' ' fi' '}' > ~/werkstatt/brot.pmlHier angezeigt, nicht ausgeführt. Erstellen Sie ein kostenloses Konto, um „Ausführen“ zu drücken und ihn im Terminal Ihres eigenen Labs einzugeben.
Wie viele Fehler findet SPIN?
spinrun ~/werkstatt/brot.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.
Welche Zusicherung bricht?
spinrun ~/werkstatt/brot.pml | grep "assertion violated"Hier angezeigt, nicht ausgeführt. Erstellen Sie ein kostenloses Konto, um „Ausführen“ zu drücken und ihn im Terminal Ihres eigenen Labs einzugeben.
Die Ablaufspur zeigt die schlechte Mischung
Bei einem Fehler behält spinrun die Ablaufspur in einer Datei neben dem Modell. spin -t -p spielt sie Schritt für Schritt ab.
Wer die Spur liest, sucht die Stelle, an der ein Prozess etwas prüft und ein anderer es ändert, bevor der erste handelt. Der Befehl zählt, wie oft die Prüfung brot>0 in der Spur vorkommt.
Wie oft prüft die Spur brot > 0?
spin -t -p ~/werkstatt/brot.pml | grep -c "brot>0"Hier angezeigt, nicht ausgeführt. Erstellen Sie ein kostenloses Konto, um „Ausführen“ zu drücken und ihn im Terminal Ihres eigenen Labs einzugeben.
Mischungen bei 4 und 4 Schritten zählen
python3 -c "print(__import__('math').comb(8, 4))"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: Prüfen und Handeln in einer Zeile sind ein einziger Schritt. Das stimmt nicht, denn jeder einzelne Schritt kann unterbrochen werden. Zwischen dem Prüfen und dem Nehmen darf ein anderer Prozess laufen.
Weiterführend
Ändern Sie das Modell so, dass es 3 Brote und 4 Verkäufer gibt: byte brot = 3 und active [4]. Ändern Sie auch die Zusicherung auf verkauft <= 3. Prüfen Sie es erneut und lesen Sie die Spur.
Überlegen Sie, wie man die beiden Schritte „prüfen“ und „nehmen“ zu einem einzigen machen könnte. Die nächste Lektion zeigt eine Lösung.