Warum ist Linearisierbarkeit eine Sicherheitseigenschaft und warum sind Sicherheitseigenschaften geschlossene Mengen?

10

In Kapitel 13 "Atomic Objects" des Buches "Distributed Algorithms" von Nancy Lynch wird die Linearisierbarkeit (auch als Atomizität bezeichnet) als Sicherheitseigenschaft nachgewiesen. Das heißt, die entsprechende Trace-Eigenschaft ist nicht leer, mit Präfix geschlossen und mit Limit geschlossen , wie in Abschnitt 8.5.3 definiert. Informell wird eine Sicherheitseigenschaft oft so interpretiert, dass eine bestimmte "schlechte" Sache niemals passiert.

Auf dieser Grundlage ist mein erstes Problem wie folgt:

Was sind die Vorteile der Linearisierbarkeit als Sicherheitseigenschaft? Gibt es in der Literatur einige Ergebnisse, die auf dieser Tatsache beruhen?

Bei der Untersuchung der Klassifizierung von Sicherheitseigenschaften und Lebendigkeitseigenschaften ist bekannt, dass Sicherheitseigenschaften als geschlossene Menge in einer geeigneten Topologie charakterisiert werden können. In der Veröffentlichung "The Safety-Progress Classification" von Amir Pnueli et al. wird eine metrische Topologie übernommen. ist eine Eigenschaft Φ eine Menge von (endlichen oder unendlichen) Wörtern über dem Alphabet Σ . Die Eigenschaft besteht aus allen unendlichen Wörtern so dass alle Präfixe von zu . Wenn zum Beispiel , dann istΦΣA(Φ)σσΦΦ=a+bA(Φ)=aω+a+bω. Eine unendliche Eigenschaft wird als Sicherheitseigenschaft definiert, wenn für eine endliche Eigenschaft . Die Metrik zwischen den unendlichen Wörtern und wird als 0 definiert, wenn sie identisch sind, und ansonsten, wo ist die Länge des längsten gemeinsamen Präfixes, auf das sie sich einigen. Mit dieser Metrik kann die Sicherheitseigenschaft topologisch als geschlossene Mengen charakterisiert werden.ΠΠ=A(Φ)Φd(σ,σ)σσd(σ,σ)=2jj

Hier kommt mein zweites Problem:

Wie kann man Linearisierbarkeit topologisch als geschlossene Mengen charakterisieren? Was ist insbesondere die zugrunde liegende Menge und wie ist die Topologie?

Hengxin
quelle

Antworten:

8

Was sind die Vorteile der Linearisierbarkeit als Sicherheitseigenschaft? Gibt es in der Literatur einige Ergebnisse, die auf dieser Tatsache beruhen?

Angenommen, Sie haben eine gemeinsam genutzte Speichermaschine implementiert , die nur die eventuelle Linearisierung erfüllt , die wie folgt definiert ist: In jedem Lauf von gibt es einen ZeitpunktMαMTα , so dass die Linearisierung ab dem Zeitpunkt . Beachten Sie, dass es für keine Obergrenze gibt . (*) (Dies ist ein Gegenstück zur künstlichen Lebendigkeit der Standarddefinition der Sicherheitseigenschaften der Linearisierbarkeit.)TαT

Eine solche Implementierung des gemeinsam genutzten Speichers wäre für den Programmierer nicht sehr nützlich: Beachten Sie, dass, wenn nur eine eventuelle Linearisierbarkeit gilt, keinerlei Garantie für die Konsistenz von Lese- / Schreibvorgängen in einem "frühen" Präfix eines Laufs (vor dem unbekannten Zeitpunkt) besteht ). Mit anderen Worten, was auch immer bisher passiert ist, Sie können das aktuelle Präfix eines Laufs immer noch auf ein Präfix erweitern, das die eventuelle Linearisierbarkeit erfüllt. T

(*) Wenn es eine solche Obergrenze gab, dann gäbe, würde eine eventuelle Linearisierbarkeit zu einer Sicherheitseigenschaft.

Wie kann man Linearisierbarkeit topologisch als geschlossene Mengen charakterisieren? Was ist insbesondere die zugrunde liegende Menge und wie ist die Topologie?

Wir können eine für die Menge , die die Menge aller möglichen Läufe eines verteilten Algorithmus ist. Beachten Sie, dass jeder Lauf einer unendlichen Folge von Zustandsübergängen entspricht. Für , definieren wir wobei der früheste Index ist, bei dem der Zustand in und unterscheiden sich; Andernfalls definieren wir , wenn , .ASYNCαASYNCα,βASYNCαβ

d(α,β):=2N
Nαβα=βd(α,β)=0

Wir argumentieren zunächst, dass eine Metrik für . Per Definition ist unddASYNCd wir haben d ( α , β ) = d ( β , α ) . Für α , β , γ A S Y N C ist die Dreiecksungleichung d ( α , β ) d (α,βASYNCd(α,β)=d(β,α)α,β,γASYNC trivial, wenn γ = α oder γ = β . Betrachten Sie nun den Fall, dass d ( α , γ ) d ( γ , β ) > 0 ist , dh d ( α , γ ) = 2 - n 1 und d ( γ , β ) = 2 -d(α,β)d(α,γ)+d(γ,β)γ=αγ=βd(α,γ)d(γ,β)>0d(α,γ)=2n1 , für einige Indizes n1n2. Daγein gemeinsames Präfix der Längen2-1mitβteilt,aber nur ein Präfix der Längen1-1mitα, folgt, dass sichαund βam Indexn1unterscheiden und somitd(α,β)=d(α,γ)und die Dreiecksungleichung folgt. Der Fall, in dem0d(γ,β)=2n2n1n2γn21βn11ααβn1d(α,β)=d(α,γ) folgt analog.0<d(α,γ)<d(γ,β)

dϵBε(α)={βASYNCd(α,β)<ε}αSASYNCαSNβNαSαSN0βASYNCd(α,β)<2N,αβNβSS

[1] James Munkres. Topologie.

Peter
quelle
Danke für deine Antwort. Ich muss darüber nachdenken. Beziehen Sie sich übrigens auf das Buch "Topology" von James R. Munkres, wenn Sie das sagen The metric d induces a topology (e.g., page~119 of [1]) where the ϵ-balls...?
Hengxin
Ja, ich habe die Referenz hinzugefügt.
Peter
Ich habe festgestellt, dass Sie eine Änderung des Titels dieses Beitrags vorgeschlagen haben (wenn ich einen Fehler gemacht habe, ignorieren Sie diesen Kommentar bitte). Zunächst stimme ich zu, dass sich die beiden Teilprobleme im Titel widerspiegeln sollten. Ich frage jedoch nicht nach " Warum ist Linearisierbarkeit eine Sicherheitseigenschaft?". Ich frage nach den Konsequenzen dieser Tatsache. Ich bin nicht sicher, wie ich den Titel entsprechend ändern soll, und habe diese Änderung übersprungen. Bitte lassen Sie mich wissen, wenn Sie andere Kommentare oder Ideen haben.
Hengxin
Mir wurde klar, dass die Charakterisierung (Beweis) der Linearisierbarkeit als geschlossene Menge im Grunde nichts mit dem Begriff der Linearisierungspunkte zu tun hat. Es scheint ein allgemeinerer Beweis zu sein, der jede Sicherheitseigenschaft als geschlossene Menge charakterisiert . Habe ich etwas verpasst?
Hengxin
Ja, alle Sicherheitseigenschaften sind geschlossene Mengen, während die Lebendigkeitseigenschaften in dieser Topologie dichte Mengen sind. Tatsächlich kann jede Eigenschaft (dh eine Reihe von Läufen) als Konjunktion (dh Schnittpunkt) von Sicherheits- und Lebendigkeitseigenschaften ausgedrückt werden.
Peter
6

In Bezug auf Ihre erste Frage: Sicherheitseigenschaften sind in gewisser Weise die "am einfachsten zu handhabenden Eigenschaften" in Bezug auf Probleme wie Modellprüfung und Synthese.

Der Hauptgrund dafür ist, dass sich im automatentheoretischen Ansatz für formale Methoden das Denken über Sicherheitseigenschaften auf das Denken über endliche Spuren reduziert, was einfacher ist als die Standardeinstellung für unendliche Spuren.

Sehen Sie hier die Arbeit von Orna Kupferman als Ausgangspunkt.

Shaull
quelle
u¨
Ich bin mir ziemlich sicher, dass ich Artikel gesehen habe, die sich zumindest in bestimmten Fällen mit Linearisierbarkeit über LTL befassen. Wenn ich sie finde, werde ich kommentieren.
Shaull
Das wird toll. Ich bin immer gespannt, wie ich mit Linearisierbarkeit über LTL umgehen soll, insbesondere mit dem Begriff der Linearisierungspunkte. Ich folge Ihrem Hinweis und finde das Papier Beweisen der Linearisierbarkeit mit zeitlicher Logik . Ich werde versuchen, es in diesen Tagen zu lesen. Ich bin mir jedoch nicht sicher über die Qualität. Ich freue mich auf Eure Kommentare.
Hengxin
Vielleicht ist dies von Nutzen. Nach Ansicht der Autoren ist dies ein ernstes Papier. Ich bin mir jedoch nicht sicher, wie eng die Verbindung zu LTL ist.
Shaull