Wie kann ich Lock-Free-Algorithmen überprüfen?

Question

In der Theorie sollte es möglich sein, zumindest eine Brute-Force-Verifikation eines Lock-Free-Algorithmus (es gibt nur so viele Kombinationen von Funktionsaufrufe sind sich kreuz). Gibt es irgendwelche Werkzeuge oder formale Argumentation Prozesse zur Verfügung, um tatsächlich zu beweisen, dass ein Lock-Free-Algorithmus korrekt ist (idealerweise sollte er auch in der Lage sein, für Rennbedingungen und die ABA Problem zu überprüfen, wie gut)?

Hinweis: Wenn Sie eine Möglichkeit kennen nur einen Punkt zu beweisen (zum Beispiel nur beweisen, dass es von dem ABA Problem sicher ist) oder ein Problem, das ich nicht die Lösung dann schreibt ohnehin erwähnt habe. Im schlimmsten Fall kann jedes Verfahren wiederum voll es überprüft durchgeführt werden.

Answer 1

Sie sollten auf jeden Fall versuchen, das Spin Model Checker .

Sie schreiben eine Programm-ähnliches Modell in einer einfachen C-ähnlichen Sprache Promela genannt, die Spin intern in eine Zustandsmaschine übersetzt. Ein Modell kann mehrere parallele Prozesse enthalten.

Was Spin dann tut, ist Check jede mögliche Verschachtelung von Anweisungen von jedem Prozess für Was die Bedingungen, die Sie testen mögen - in der Regel, das Fehlen von Rennbedingungen, die Freiheit von Deadlocks usw. Die meisten dieser Tests leicht geschrieben assert()-Anweisungen werden kann. Wenn es irgendeine mögliche Ausführungssequenz ist, die eine Behauptung verletzt, wird die Sequenz ausgedruckt, sonst werden Sie die „Entwarnung“ gegeben.

(Na ja, in der Tat verwendet es einen viel schicker und schneller Algorithmus, dies zu erreichen, aber das ist der Effekt. Standardmäßig werden alle erreichbaren Programmzustände überprüft werden.)

Dies ist ein unglaublich Programm, es gewann 2001 ACM-System-Software-Preis (andere Gewinner gehören Unix, Postscript, Apache, TeX). Ich habe mit ihm sehr schnell, und in ein paar Tagen war in der Lage zu implementieren Modellen der MPI-Funktionen MPI_Isend() und MPI_Irecv() in Promela gestartet. Spin fand ein paar heikel Rennbedingungen in einem Segment von parallelem Code, den ich über zu Promela konvertierte zum Testen.

Answer 2

Der Spin ist zwar ausgezeichnet, aber auch überlegen, Relacy Rennen Detector von Dmitriy V'jukov . Es ist speziell für die gleichzeitige Algorithmen einschließlich Non-Blocking (WAIT / lock-frei) Algorithmen zu verifizieren. Es ist Open-Source und liberal lizenziert.

Relacy bietet POSIX und Windows Synchronisierungsgrund (mutexes, Bedingungsvariablen, Semaphore, CriticalSections, win32 Ereignisse, Verzahnt *, etc.), so dass Ihre tatsächliche C ++ Implementierung Relacy zur Überprüfung zugeführt werden kann. Keine Notwendigkeit für ein eigenes Modell des Algorithmus wie bei Promela und Spin zu entwickeln.

Relacy bietet C ++ 0x std::atomic (explizites Gedächtnis Bestellung für den Gewinn!), So dass Sie Pre-Prozessor #defines können zwischen Relacy Implementierung und Ihrer eigenen Plattform-spezifischen Atom Umsetzung ( TBB :: Atom ,

Daten Rennen Erkennung ist ein NP hartes Problem [Netzer & Miller 1990]

Ich habe gehört, über die Werkzeuge Lockset und DJit + (sie lehrt es im CDP-Kurs ). Versuchen Sie, die Folien zu lesen, und googeln, was sie verweisen. Es enthält einige interessante Informationen.

Ich weiß nicht, was Plattform oder Sprache Sie verwenden - aber auf der .NET-Plattform gibt es ein Microsoft Research Projekt namens Schach , die sehr viel versprechend suchen diejenigen von uns tun multithreaded Komponenten zu helfen -. einschließlich Lock-frei

Ich habe es nicht eine riesige Menge verwendet, Geist.

Es funktioniert (Roh-Erklärung) durch explizite Faden in engster Möglichkeiten Verschachtelung, um tatsächlich Ihre Bugs in die wilden Kraft aus. Es analysiert auch Code häufige Fehler und schlechte Muster zu finden -. Ähnlich wie Code-Analyse

In der Vergangenheit habe ich auch spezielle Versionen des Codes in Frage (durch #if Blöcke usw.) aufgebaut, die zusätzliche state-Tracking-Informationen hinzuzufügen; zählt, Versionen usw., dass ich kann, dann tauchen Sie ein in innerhalb eines Unit-Tests.

Das Problem mit dieser ist, dass es viel mehr Zeit in Anspruch nimmt, Ihren Code zu schreiben, und Sie können diese Art von Sachen nicht immer hinzufügen, ohne die zugrunde liegende Struktur des Codes zu ändern, die bereits vorhanden ist.

Wenn Sie wirklich wollen Lock-Free-Code überprüfen (im Gegensatz zu erschöpfend ein kleines Beispiel zu testen), können Sie VCC verwenden ( http://vcc.codeplex.com ), eine deduktive Verifizierer für die gleichzeitige C-Code, der verwendet wurde, einige interessante Lock-Free-Algorithmen (zB Lock-freien Listen und veränderbare Hashtables mit Gefahren Zeiger, optimistisch multiversion Transaktion zu überprüfen Verarbeitung, MMU-Virtualisierung, verschiedene Synchronisations Primitiven, etc.). Es tut modulare Verifikation und wird verwendet, um nicht-triviale Stücke von Industrie Code zu überprüfen (bis zu etwa 20KLOC).

Beachten Sie jedoch, dass VCC ist ein Prüfer, kein Bug Jagd-Werkzeug; Sie haben erhebliche Anmerkung auf Ihrem Code zu tun, um es zu überprüfen zu erhalten, und die Lernkurve ein wenig steil sein kann. Beachten Sie auch, dass es übernimmt sequentielle Konsistenz (wie die meisten Werkzeuge).

BTW, Peer-Review ist kein guter Weg, um einen gleichzeitigen Algorithmus (oder sogar eine sequentielles eins) zu überprüfen. Es gibt eine lange Geschichte von berühmten Persönlichkeiten veröffentlichen gleichzeitig Algorithmen in wichtigen Zeitschriften, nur Bugs Jahre später entdeckt zu haben.

Answer 3

Answer 4

Answer 5

Answer 6

Daten Rennen Erkennung ist ein NP hartes Problem [Netzer & Miller 1990]

Answer 7

Ich habe gehört, über die Werkzeuge Lockset und DJit + (sie

Answer 8

Ich weiß nicht, was Plattform oder Sprache Sie verwenden - aber auf der .NET-Plattform gibt es ein Microsoft Research Projekt namens Schach , die sehr viel versprechend suchen diejenigen von uns tun multithreaded Komponenten zu helfen -. einschließlich Lock-frei

Ich habe es nicht eine riesige Menge verwendet, Geist.

Es funktioniert (Roh-Erklärung) durch explizite Faden in engster Möglichkeiten Verschachtelung, um tatsächlich Ihre Bugs in die wilden Kraft aus. Es analysiert auch Code häufige Fehler und schlechte Muster zu finden -. Ähnlich wie Code-Analyse

In der Vergangenheit habe ich auch spezielle Versionen des Codes in Frage (durch #if Blöcke usw.) aufgebaut, die zusätzliche state-Tracking-Informationen hinzuzufügen; zählt, Versionen usw., dass ich kann, dann tauchen Sie ein in innerhalb eines Unit-Tests.

Das Problem mit dieser ist, dass es viel mehr Zeit in Anspruch nimmt, Ihren Code zu schreiben, und Sie können diese Art von Sachen nicht immer hinzufügen, ohne die zugrunde liegende Struktur des Codes zu ändern, die bereits vorhanden ist.

Answer 9

Wenn Sie wirklich wollen Lock-Free-Code überprüfen (im Gegensatz zu erschöpfend ein kleines Beispiel zu testen), können Sie VCC verwenden ( http://vcc.codeplex.com ), eine deduktive Verifizierer für die gleichzeitige C-Code, der verwendet wurde, einige interessante Lock-Free-Algorithmen (zB Lock-freien Listen und veränderbare Hashtables mit Gefahren Zeiger, optimistisch multiversion Transaktion zu überprüfen Verarbeitung, MMU-Virtualisierung, verschiedene Synchronisations Primitiven, etc.). Es tut modulare Verifikation und wird verwendet, um nicht-triviale Stücke von Industrie Code zu überprüfen (bis zu etwa 20KLOC).

Beachten Sie jedoch, dass VCC ist ein Prüfer, kein Bug Jagd-Werkzeug; Sie haben erhebliche Anmerkung auf Ihrem Code zu tun, um es zu überprüfen zu erhalten, und die Lernkurve ein wenig steil sein kann. Beachten Sie auch, dass es übernimmt sequentielle Konsistenz (wie die meisten Werkzeuge).

BTW, Peer-Review ist kein guter Weg, um einen gleichzeitigen Algorithmus (oder sogar eine sequentielles eins) zu überprüfen. Es gibt eine lange Geschichte von berühmten Persönlichkeiten veröffentlichen gleichzeitig Algorithmen in wichtigen Zeitschriften, nur Bugs Jahre später entdeckt zu haben.