Literatur/Dokumentation über zwei kooperierende Prozesse, die ein Flag für sperrfreien gemeinsamen Speicher verwenden

Question

Gibt es irgendeine andere Dokumentation/Diskussion über das folgende Entwurfsmuster (ich bin mir nicht sicher, wie es genannt wird) aus einer bekannten Quelle? Ich bin mir fast zu 100% sicher, dass die folgenden Daten sicher zwischen zwei (nicht mehr als zwei) Prozessen verwaltet werden, aber ich würde mich viel besser fühlen, wenn ich einige detailliertere Informationen darüber, warum es funktioniert, aus einer seriösen Quelle finden könnte.

---

Angenommen, ich habe zwei Prozesse A und B, die parallel ausgeführt werden. Sie teilen sich die folgende Datenstruktur (in Pseudo-C-Code):

struct Shared
{
    bool ownedByA
    Otherstuff otherstuff;
}

Ich kann das folgende Paar von Zustandsautomaten verwenden, um diese gemeinsamen Daten sicher zu verwalten:

A:

state A.A (data is owned by A), entered on startup:
    read/modify/write "otherstuff"
    when done, goto A.Adone

state A.Adone
    set ownedByA to false
    goto state A.B

state A.B (data is owned by B):
    if ownedByA is true, goto state A.A
    otherwise stay in state A.B

B:

state B.A (data is owned by A), entered on startup:
    if ownedByA is false, goto state B.B
    otherwise stay in state B.A

state B.B (data is owned by B):
    read/modify/write "otherstuff"
    when done, go to B.Bdone

state B.Bdone:
    set ownedByA to true
    goto state B.A

Wir müssen sicherstellen, dass die Schreibvorgänge von A.A in "otherstuff" und von A.Adone in "ownedByA" in einer strikten Reihenfolge in Bezug auf die Speichersichtbarkeit erfolgen. Ähnliches gilt für B.B und B.Bdone.

beim Starten:

1. Initialize ownedByA to true, A to the A.A state, B to the B.A state
2. start running state machines 
(ensure that 1. happens-before 2.)

Answer 1

Vielleicht ist das ein Problem der Essensphilosophen mit nur zwei Philosophen und einer Gabel.

http://en.wikipedia.org/wiki/Dining_philosophers_problem

Answer 2

Sie können versuchen Th. J. Dekkers Lösung erwähnt von E. W. Dijkstra in seinem EWD1303 Papier .

Und dann geschah etwas Tiefgreifendes und Schönes. Indem ich analysierte, durch welche Struktur der Argumente die Beweispflichten erfüllt werden könnten, wurde die numerische Mathematiker Th.J. Dekker innerhalb weniger Stunden
die obige Lösung zusammen mit ihrem Korrektheitsargument, und damit war die Wettbewerb.
In der obigen Lösung implementiert das Paar "c1,c2" den gegenseitigen Ausschluss, während "turn" eingeführt wurde, um den Gleichstand aufzulösen, wenn die zwei Prozesse gleichzeitig versuchen, ihre kritischen Abschnitte zu betreten.