Eine Budgetinvariante gegen konkurrierende Zugriffe formulieren.
Für ein unveränderliches, nicht negatives Limit lautet die Invariante einer Budgetinstanz: 0 ≤ used ≤ limit. Die Prüfung auf einen freien Platz und die Erhöhung müssen gemeinsam unter der Sperre liegen. Sonst könnten zwei Threads denselben letzten Platz sehen und ihn beide verbrauchen. Ein geschützter Lesezugriff liefert einen konsistent gelesenen Wert, reserviert aber noch keinen Platz für eine spätere Handlung. Der passende Konkurrenztest lässt viele Arbeiter dieselbe Instanz benutzen; er prüft sowohl die Zahl der erfolgreichen Verbräuche als auch den Endstand. Getrennte Instanzen gehören in einen getrennten Testfall.
Ein Beispiel
20 Arbeiter versuchen an einem frischen Budget mit Grenze 5 jeweils genau einen Verbrauch. Ohne Rückgaben sollen exakt 5 succeed-Meldungen entstehen und used soll 5 sein. Ein Test nur auf 'keine Ausnahme' würde ein unbemerktes Überschreiten nicht erkennen. Das kurze Modell zeigt die gemeinsame Entscheidung; es startet selbst keine Threads.
Python 3.11 · Lehrbeispiel
def consume(used, limit):
# Reines Modell einer Entscheidung unter einer gemeinsamen Sperre.
if used >= limit:
return used, False
return used + 1, True
print(consume(4, 5))
print(consume(5, 5))
Erwartete Ausgabe
(5, True)
(5, False)