Thread-Interleaving-Explorer

Alle zulässigen Abläufe von zwei oder drei kurzen Programmen unter sequentieller Konsistenz prüfen. Beispiel wählen, Anfangswerte oder Programme bearbeiten, dann Prüfen. Änderungen löschen alte Ergebnisse. Das verlorene Update liefert 20 Abläufe: x=1 in 18, x=2 in 2. Ein Mutex macht Lesen–Erhöhen–Schreiben exklusiv.

Eine Anweisung je Zeile: r1 = x liest eine gemeinsame Variable, x = r1 schreibt ein lokales Register, x = 5 setzt eine gemeinsame Ganzzahl, r1 = r1 + 1 rechnet in einem lokalen Register. Addition, Subtraktion und Multiplikation erlauben Ganzzahlen oder Variablen-/Registernamen. lock(m) wartet auf einen freien Mutex; unlock(m) verlangt eigenen Besitz. wait(x == 1) wartet auf den Vergleich einer gemeinsamen Variablen; !=, <, >, <= und >= funktionieren ebenfalls. Namen ignorieren Großschreibung; r mit Ziffern ist thread-lokal, andere Namen sind gemeinsam. Fehlende Anfangswerte sind null. Anfangswerte: x = 0, y = 1; doppelte Namen werden abgewiesen. // beginnt einen Kommentar.

Ergebnisse enthalten gemeinsame Werte und alle lokalen Register. Ablaufanteile zählen aufgezählte Pfade, niemals reale Zeitwahrscheinlichkeiten. Thread-Reihenfolge bedeutet: Dasselbe Ergebnis ist auch bei vollständiger Ausführung eines Threads nach dem anderen möglich. Verschränkt bedeutet: Dieses Ergebnis benötigt verschränkte Anweisungen. Beide Aussagen beweisen weder Vorhandensein noch Abwesenheit eines Datenrennens. Blockiert heißt: Unfertige Threads haben keine ausführbare nächste Aktion; Ursache kann ein Lock-Deadlock oder eine unerfüllte Wartebedingung sein. Ablauf öffnet einen echten Zeugenablauf mit gemeinsamen und lokalen Zwischenwerten.

Grenzen: 18 Anweisungen insgesamt, 80.000 Abläufe vor Mutex-/Wartebeschränkungen, 4.096 Zeichen je Eingabe und 64 je Name. Ganzzahlen und Berechnungen müssen innerhalb ±9.007.199.254.740.991 bleiben. Das lokale vollständige Lehrmodell enthält keine Schleifen, echte Zeit, Compilerumordnungen, Atomics oder schwache Speichermodelle. Kaputte und korrekte Veröffentlichung vergleichen: ready vor data erlaubt das Lesen von 0; umgekehrte Schreibreihenfolge nur 42.

Die Suche läuft in einem lokalen Worker, damit die Seite bedienbar bleibt. Der Aktivitätsbalken zeigt keine Prozentzahl: Mutex und Warten können Abläufe früh beenden. Gezählt werden untersuchte Endabläufe; Abbrechen stoppt den Worker und behält die Eingaben. Bearbeiten und Verlassen stoppen ebenfalls und verwerfen verspätete Antworten. Der Filter sucht ohne Groß-/Kleinschreibung in gemeinsamen Werten und Registern; alle durch Leerzeichen getrennten Suchbegriffe müssen passen. Von keinem Thread verwendete Anfangswerte stehen einmal unter Unbenutzte Anfangswerte und entfallen in wiederholten Ergebnis-/Ablaufzellen.

Programme einschließlich verborgenem T3, Threadzahl, rohe Anfangswerte, Fehler, Ergebnisfilter und gewählter/offener Ablauf bleiben im lokalen Browserspeicher. Cache-Struktur, Zählsummen und Eingabezuordnung werden geprüft; der gewählte Zeugenablauf wird vor der Anzeige abgespielt. Das ist kein manipulationssicheres Ergebniszertifikat. Importierte fertige Ergebnisse werden immer im Worker neu berechnet, veränderte Dateizähler also nicht übernommen. Keine Serverberechnung.

Nur Eingabewerte bleiben in diesem Browser erhalten. Berechnete Ergebnisse und Versuchsverläufe werden nicht gespeichert.