Jepsen: Analyse von Datomic Pro 1.0.7075

 (jepsen.io)
1 Punkte von GN⁺ 2024-05-17 | 1 Kommentare | Auf WhatsApp teilen
  • In Tests wirkte die Sicherheit zwischen Transaktionen bei Datomic Pro 1.0.7075 stärker als in der Dokumentation behauptet, aber die Semantik innerhalb von Transaktionen wich deutlich vom üblichen seriellen Ausführungsmodell ab.
  • Alle Test-Historien wirkten Serializable, eine einzelne Peer-Session war Strong Session Serializable, und Schreibvorgänge sowie d/sync-Reads kamen Strong Serializable nahe.
  • Die Add-, Retract- und Transaction-Functions von Datomic werden innerhalb einer Transaktion nicht der Reihe nach akkumulativ ausgeführt; stattdessen arbeitet jede Funktion so, dass sie nur den DB-Zustand zum Startzeitpunkt sieht.
  • Wenn man in derselben Transaktion für sich genommen sichere Transaction-Functions wie approve und deny kombiniert, kann das Gesamtergebnis eine Invariantverletzung erzeugen.
  • Wenn mehrere Transaction-Functions in eine Transaktion aufgenommen werden, sollte man die Beziehung zwischen Read Set und Write Set prüfen und zusammen mit expliziten Constraints wie Entity Predicate, Attribute Predicate und Entity Spec arbeiten.

Modell und Architektur von Datomic Pro

  • Datomic ist eine Entity-Attribute-Value-OLTP-Datenbank, die das Konzept der Zeit explizit modelliert.
    • Der Zustand der DB zu einem bestimmten Zeitpunkt wird als Menge von Datoms in der Form [entity, attribute, value] dargestellt.
    • Für jedes Datom bleibt auch erhalten, durch welche Transaktion es hinzugefügt oder zurückgezogen wurde.
    • Ein vollständiges Datom ist ein 5-Tupel der Form [entity, attribute, value, transaction, asserted-or-retracted?].
  • Datomic ist eine temporale Datenbank, daher lassen sich Snapshots nicht nur für die Gegenwart, sondern auch für vergangene logische Zeitpunkte oder Wall-Clock-Zeitpunkte anfordern.
    • Über eine vollständige History-Ansicht kann auch abgefragt werden, ob eine bestimmte Tatsache in der Vergangenheit existierte.
    • Für Abfragen stellt es eine Datalog-ähnliche API, eine API für Graph Traversal und den ODM-artigen Typ Entity bereit.
  • Datomic Pro ist die Version, die Nutzer selbst betreiben können; Datomic Cloud läuft auf AWS und hat teilweise eine andere Architektur.
  • Datomic Pro besteht aus mehreren zusammenarbeitenden Komponenten.
    • Der Transactor übernimmt die Ausführung von Schreibtransaktionen, die Pflege der Indizes und das Schreiben in den Storage.
    • Der Peer ist ein dicker Client mit eingebetteter JVM-Bibliothek, der Transaktionen einreicht, Leseabfragen gegen den Storage ausführt und Caching übernimmt.
    • Für Anwendungen in anderen Sprachen gibt es außerdem ein Thin-Client- und Peer-Server-basiertes Client-Server-Modell.
  • Intern hängt Datomic jede Transaktion an ein zeitlich geordnetes Log an und hält vier Indizes vor, die nach Kombinationen aus Entity, Attribute, Value und Time sortiert sind.
    • Log und Indizes werden als persistente, unveränderliche Bäume in einem Storage wie Cassandra oder DynamoDB gespeichert.
    • Weil die Baumknoten unveränderlich sind, muss der zugrunde liegende Storage nur Eventual Consistency garantieren.
    • Beim Commit speichert der Transactor neue unveränderliche Baumknoten und rückt dann den Root Pointer per compare-and-set (CaS) vor; dieses CaS benötigt Sequential Consistency.
  • Sequential CaS garantiert die globale Reihenfolge der Transaktionen, bindet den Schreibdurchsatz aber an die Geschwindigkeit eines einzelnen Transactors.
    • Datomic betreibt üblicherweise immer nur einen aktiven Transactor gleichzeitig und setzt für Fehlertoleranz mehrere Transactors ein.
    • Peers verbinden sich direkt mit Storage und Transactor und halten jeweils eine monoton wachsende Kopie des Root Pointers.
    • Da Reads unveränderliche Baumknoten cachen können, ist mit mehr Peers eine nahezu lineare Skalierung beim Lesen möglich.

Das Transaktionsmodell von Datomic

  • Datomic bietet keine interaktiven Transaktionen wie eine typische OLTP-Datenbank.
    • Es ist also kein Modell, bei dem man eine Transaktion startet, das Ergebnis einer Operation erhält, dann die nächste Operation einreicht und am Ende committet.
    • Es gibt zwar Stored-Procedure-ähnliche Transaction-Functions, diese können dem Aufrufer aber keine beliebigen Werte zurückgeben.
  • Lese- und Schreibpfad sind strikt getrennt.
    • db gibt den neuesten dem Peer bekannten DB-Zustand zurück.
    • d/sync synchronisiert mit dem Transactor, um den neuesten Stand aus Sicht aller Peers oder den Stand nach einem bestimmten Zeitpunkt zu erhalten.
    • d/as-of liefert den DB-Zustand zu einem vergangenen Zeitpunkt.
    • Da der DB-Zustand unveränderlich ist, laufen mehrere Abfragen auf demselben Zustand exakt zum gleichen logischen Zeitpunkt.
  • Schreibtransaktionen werden als geordnete Liste von Operationen dargestellt.
    • Beispiele sind :db/add, :db/retract, db/cas und Aufrufe benutzerdefinierter Transaction-Functions.
    • Eine Transaction-Function erhält den DB-Zustand zum Startzeitpunkt der Transaktion und ihre Argumente und gibt eine neue Menge von Operationen zurück.
    • Funktionsaufrufe werden rekursiv expandiert, bis nur noch Assertions und Retractions übrig bleiben.
  • Transaction-Functions können intern Reads ausführen, um bedingte Writes zu entscheiden, geben aber weder Leseergebnisse noch sonstige beliebige Informationen direkt an den transact-Aufrufer zurück.
    • transact gibt den DB-Zustand vor der Transaktion, den resultierenden DB-Zustand nach der Transaktion und die expandierte Menge von Datoms zurück.
    • Der Aufrufer kann anhand von Pre-State und Post-State feststellen, ob ein bedingter Write stattgefunden hat.
  • Datomic ist auf ein Modell ausgelegt, das Probleme rund um günstige und übertragbare DB-Snapshots löst.
    • Nubank ist der aktuelle Entwickler von Datomic und bietet Finanzdienstleistungen für rund 94 Millionen Nutzer an und verarbeitet im Tagesdurchschnitt 2,3 Milliarden Nutzertransaktionen.
    • Nahezu alle Produkte von Nubank verwenden Datomic als System of Record.

Konsistenzbehauptungen und Testdesign

  • Die Datomic-Dokumentation beansprucht ACID-Transaktionen und geht davon aus, dass Transaktionen als ein einzelner atomarer Write in den Storage geschrieben werden und jeder Peer alle bis zu einem bestimmten Zeitpunkt abgeschlossenen Transaktionen in einer Totalordnung beobachtet
    • Vor dem Client-Acknowledgement werden Transaktionen in den dauerhaften Storage geflusht
  • Die Dokumentation zum Zeitpunkt des Analysebeginns Anfang Januar 2024 behauptete inoffiziell, dass Write-Transaktionen serialisierbar seien
    • Die Dokumentation bezeichnete Datomic auch als „single-writer“-System, aber Jepsen hält diese Beschreibung aus zwei Gründen für ungenau
    • Zur Fehlertoleranz können mehrere Transactors betrieben werden, und da ein Failure Detector nicht perfekt sein kann, kann ein Zeitfenster entstehen, in dem mehrere Transactors gleichzeitig als aktiv gelten
    • Selbst wenn es nur einen einzelnen Transactor gibt, können sich durch Netzwerklatenz Storage-Nachrichten mit Nachrichten anderer Transactors verschachteln
  • Die Sicherheit von Datomic beruht nach dieser Einschätzung nicht auf einer „single-writer“-Logik, sondern auf der sequentiellen Konsistenz der Storage-CaS-Operation
    • Auch bei mehreren konkurrierenden Transactors muss CaS die Sicherheit gewährleisten
  • Für die Tests wurde die mit der Jepsen testing library geschriebene Datomic test suite verwendet
    • Datomic Pro 1.0.7075 wurde auf einem Cluster aus Debian-Bookworm-Nodes installiert
    • Als Storage wurde eine AWS-DynamoDB-Tabelle verwendet
    • Zwei Nodes führten den Transactor aus, die übrigen Nodes den Peer
  • Der Peer war ein kleines Clojure-Programm, das die Datomic-Peer-Library nutzte und eine HTTP-API für Testoperationen bereitstellte
    • Die Tests liefen sowohl im Modus mit möglichen Stale Reads unter Verwendung von d/db als auch im Modus mit garantierter Aktualität über d/sync
  • Fault Injection wurde sowohl auf Transactor als auch auf Peer angewendet
    • Es wurden Process Pause, Crash und Clock Error injiziert
    • Es wurden Netzwerkpartitionen zwischen Transactor und Peer sowie zwischen Nodes und Storage erzeugt
    • Auch Datomic Garbage Collection wurde angefordert
  • Wenn ein Transactor keine stabile Verbindung zum Storage halten kann, beendet er sich selbst
    • Mit dem Standard-Timeout von 5 Sekunden auf Nodes außerhalb von AWS beendete er sich selbst schon bei normalen Netzwerkschwankungen alle paar Minuten
    • Selbst in einer EC2-Testumgebung beendete er sich bei einem Timeout von 1 Sekunde alle 10 bis 20 Minuten
    • Datomic empfiehlt, dass der Operator den Transactor mit einem Supervisor-Daemon neu startet; im Test wurde ein systemd-Service mit Restart=on-failure verwendet

Vier Workloads

  • List Append

    • Der List-Append-Workload wird zusammen mit dem Elle Transaction Checker verwendet
    • Logisch arbeitet er mit Listen von Integer-Elementen, wobei jede Liste durch einen Integer-Primary-Key identifiziert wird
    • Clients führen zufällige Transaktionen aus, bestehend aus Listen-Reads oder dem Anhängen eindeutiger Elemente
    • Elle prüft auf Aborted Read, Intermediate Read, Verletzungen der internen Konsistenz und Unstimmigkeiten in der Reihenfolge der Elemente und entscheidet anhand von Zyklen im Dependency Graph über Verstöße gegen das Konsistenzmodell
    • In Datomic werden Listen als eine Entity mit zwei Attributen kodiert
    • append/key dient als Primary Key
    • append/elements speichert die Integer-Elemente der Liste als mehrwertiges Attribut
    • Da mehrwertige Attribute ungeordnete Sets sind, sortiert Jepsen die Elemente anhand des Transaktionszeitstempels jedes Datoms, damit Elle die benötigte Reihenfolge erhält
    • Die Einschränkung, dass es keine gemischten Read-Write-Transaktionen gibt, wird mit einer Transaction Function und der Berechnung des Pre-State umgangen
    • Writes werden über eine Transaction Function ausgeführt
    • Mithilfe des von transact zurückgegebenen Pre-State wird berechnet, was ein interner Read innerhalb der Transaktion gesehen hätte
    • Dieselbe Funktion wird einmal in transact und einmal im Peer ausgeführt, um auf Basis des Pre-State interne Reads zu ergänzen

  • List Append with CaS

    • Der List-Append-with-CaS-Workload verwendet das db/cas-Muster
    • Nutzer können mit d/db den aktuellen Zustand lesen und dann zum Beispiel [:db/cas 123 :counter/value 4 5] einreichen, um den Wert nur dann von 4 auf 5 zu ändern, wenn er aktuell 4 ist
    • Wenn für alle Writes db/cas verwendet wird, lässt sich über logischen „User-Transaktionen“ eine ad-hoc-Snapshot Isolation aufbauen
    • In diesem Workload wird eine Liste nicht als mehrwertiges Attribut, sondern als einzelner kommagetrennter String gespeichert
    • Zu Beginn der Transaktion wird gelesen, dann werden Reads und Writes lokal angewendet und anschließend eine CaS-Transaktion konstruiert, die sicherstellt, dass sich seit dem Read nichts geändert hat

  • Internal

    • Der Internal-Workload misst direkt die interne Konsistenz innerhalb einer Transaktion
    • Dazu gehören Fälle, in denen auf dasselbe Entity-Attribut erst 1 und dann 2 asserted wird
    • Fälle, in denen in derselben Transaktion ein Fact asserted und wieder retracted wird
    • Fälle, in denen ein Wert asserted und anschließend per CaS geändert werden soll
    • Fälle mit mehreren CaS wie 1→2 und 2→3
    • Fälle, in denen nach dem Erzeugen einer Entity über einen Lookup Ref eine Änderung erfolgt
    • Sowie Fälle, in denen eine Transaction Function versucht, einen Wert zweimal zu inkrementieren

  • Grant

    • Der Grant-Workload prüft, ob eine Transaction Function die Invarianten der Funktion bewahrt
    • Ein Grant wird als einzelne Entity mit den drei Attributen created-at, approved-at und denied-at kodiert
    • Ein Grant darf nicht gleichzeitig den Status approved und denied haben
    • Die Funktionen approve und deny prüfen zunächst, ob der Grant bereits approved oder denied ist, und brechen bei Bedarf ab
    • Es wird geprüft, ob ein Grant bei verschiedenen Kombinationen von Transaction Boundaries gleichzeitig approved und denied werden kann

Testergebnisse: Die transaktionsübergreifende Sicherheit wirkt stark

  • Jepsen fand kein Verhalten, das den zentralen Sicherheitsbehauptungen von Datomic widerspricht
    • Transaktionen schienen so angewendet zu werden, als ob sie in einer Totalordnung ausgeführt würden
    • Diese Ordnung stimmt mit der lokalen Operationsreihenfolge auf jedem Peer überein
  • Historien, die auf reine Write-Transaktionen beschränkt waren, sowie Historien, in denen bei Reads (d/sync conn) verwendet wurde, stimmten mit der Real-Time-Order überein
    • Jepsen bewertet dies als Hinweis auf Strict Serializability
  • Wenn Sessions als an einen einzelnen Peer gebunden interpretiert werden, scheint Datomic Strong Session Serializability zu garantieren
    • Die Transaktionshistorie ist nicht von einer Historie zu unterscheiden, die in irgendeiner Totalordnung ausgeführt wurde
    • Diese Ordnung stimmt mit der auf jedem Peer beobachteten Reihenfolge überein
  • d/db gibt eine asynchron aktualisierte DB-Kopie zurück, daher sind Stale Reads möglich
    • Auch die Datomic-Dokumentation weist ausdrücklich darauf hin, dass Peer-Reads möglicherweise einige kürzlich committete Transaktionen nicht beobachten
    • d/sync synchronisiert mit dem Transactor und verhindert so Stale Reads
  • Die experimentelle Verifikation hat weiterhin Grenzen
    • Die Existenz von Bugs kann bewiesen werden, ihre Abwesenheit jedoch nicht
    • Correctness Errors in den Storage-Systemen, von denen Datomic abhängt, können zu Verstößen gegen die Datomic-Garantien führen
    • Datomic auf DynamoDB ist nur so sicher wie die Compare-and-Set-Operation von DynamoDB

Semantik innerhalb von Transaktionen: keine Reihenfolge, sondern Nebenläufigkeit

  • Die meisten Datenbanken und zentrale Formalisierungen von Transaktionsisolation bieten serielle Ausführungssemantik innerhalb einer Transaktion
    • Bei set x = 1; read x; sieht der Read normalerweise 1
    • Formalisierungen von Adya, Cerone·Bernardi·Gotsman, Crooks·Alvisi·Pu·Clement u. a. machen die Reihenfolge von Operationen innerhalb einer Transaktion und die Eigenschaft explizit, dass „ein späterer Read einen früheren Write beobachtet“
  • Der Transaction Request von Datomic ist zwar eine geordnete Liste, die Ausführung erhält diese Reihenfolge jedoch nicht
    • Add, Retract und Transaction Function verhalten sich so, als würden sie gleichzeitig ausgeführt
    • Eine Transaction Function beobachtet immer den DB-Zustand zum Beginn der Transaktion
    • Sie sieht die Effekte vorheriger Assertionen, Retractions oder Transaction Functions nicht
  • Fügt man bei einer Entity mit aktuellem Wert 0 zweimal denselben CaS ein, sehen in Datomic beide den Ausgangszustand 0 und sind erfolgreich
[[:db/cas 123 :internal/value 0 1]
 [:db/cas 123 :internal/value 0 1]]
  • In einem seriellen Modell würde der erste CaS den Wert auf 1 ändern und der zweite CaS fehlschlagen
    • In Datomic erzeugen die beiden CaS doppelte Assertionen und der Endwert wird 1
  • Auch zwei Increment-Transaction-Functions liefern ein anderes Ergebnis als im seriellen Modell
[['internal/increment "x"]
 ['internal/increment "x"]]
  • Ist der Startwert 0, wäre das Ergebnis im seriellen Modell 2
  • In Datomic sehen beide Funktionen den Ausgangszustand 0 und der Endwert wird 1
  • Eine Transaction Function sieht auch vorhergehende Assertionen nicht
[[:db/add id-of-x :internal/value 1]
 ['internal/increment "x"]]
  • In Datomic wird der Endwert nicht 2, sondern 1
  • Auch Lookup-Refs verwenden den DB-Zustand zum Transaktionsbeginn
    • Fügt man in derselben Transaktion eine Entity hinzu, kann man diese Entity anschließend nicht per Lookup-Ref referenzieren
    • In diesem Fall wird mit dem Fehler Unable to resolve entity abgebrochen

Konflikterkennung und pseudo write skew

  • Datomic bricht mit :db.error/datoms-conflict ab, wenn innerhalb derselben Transaktion für ein Attribut mit einfacher Kardinalität unterschiedliche Werte asserted werden
    • Wird für den Ausgangswert 0 der Wert 2 asserted und erzeugt gleichzeitig eine Increment-Function eine Assertion für den Wert 1, entsteht ein Konflikt
    • Diese Konflikterkennung kann viele überraschende Ergebnisse verhindern, die aus der fehlerhaften Komposition von Transaction Functions entstehen
  • Wenn sich die Write Sets auf unterschiedliche [entity, attribute]-Paare beziehen, reicht Konflikterkennung allein kaum aus, um Invarianten zu wahren
    • Die Grant-Workload zeigt diese Situation
    • approve und deny prüfen jeweils, dass ein Grant weder approved noch denied ist, und fügen dann unterschiedliche Attribute hinzu
  • Ruft man approve und deny in unterschiedlichen Transaktionen auf, gewährleisten die Serializable-Transaktionen von Datomic die Invariante
    • Ruft man jedoch beide innerhalb derselben Transaktion gemeinsam auf, sehen beide den Ausgangszustand und sind erfolgreich
[['grant/approve id]
 ['grant/deny id]]
  • Das Ergebnis ist ein Grant, das sowohl approved-at als auch denied-at besitzt
    • Die Invariante „Ein Grant darf nicht gleichzeitig approved und denied sein“ wird verletzt
    • Der In-Transaction-Conflict-Checker von Datomic verhindert dies nicht, weil die beiden Funktionen Assertionen für unterschiedliche Attribute erzeugt haben
  • Dieses Phänomen ähnelt dem Write Skew aus Berenson et al.
    • Weil die beiden Funktionen die Effekte der jeweils anderen nicht sehen können, entsteht ein Read-Write-Anti-Dependency-Cycle
    • Betrachtet man Transaction Functions als Transaktionen, ähnelt dies der G2-item-Anomalie, die Repeatable Read und Serializability verbieten
  • Datomic und Nubank betrachten dieses Verhalten nicht als Bug, sondern als erwartetes Verhalten von Datomic
    • Nubank plant, die konkurrierende Intra-Transaction-Semantik von Datomic beizubehalten

Invarianten mit Entity Predicate absichern

  • Datomic bietet Constraint-Mechanismen wie Typen, Uniqueness, bestimmte Attribute Predicates und Entity Predicates
    • Ein Entity Predicate erhält den Kandidaten-DB-Zustand, auf den alle Transaktionseffekte angewendet wurden, sowie die Entity-ID und gibt true oder false zurück, je nachdem ob der Commit erlaubt ist
    • Trotz des Namens Entity Predicate kann es auf den gesamten DB-Zustand zugreifen und damit auch globale Constraints ausdrücken, die über eine einzelne Entity hinausgehen
  • Im Grant-Beispiel kann man mit dem Predicate valid-grant? verhindern, dass approved-at und denied-at gleichzeitig existieren
(defn valid-grant?
  [db eid]
  (let [{:grant/keys [approved-at denied-at]}
        (d/pull db '[:grant/approved-at
                     :grant/denied-at]
                   eid)]
   (not (and approved-at denied-at))))
  • Im Schema fügt man eine Entity Spec hinzu, die auf dieses Predicate verweist
    • Ein mit einer Entity Spec verknüpftes Entity Predicate wird nicht automatisch auf alle Transaktionen angewendet
    • Datomic betrachtet die Anwendung einer Entity Spec als Domain-Entscheidung und vertritt die Position, dass jede Transaktion sie explizit anfordern muss
  • Die Funktionen approve und deny können nach dem Hinzufügen der Attribute über das virtuelle Datom :db/ensure die Anwendung der Entity Spec anfordern
(defn approve
  [db id]
  [[:db/add id :grant/approved-at (Date.)]
   [:db/add id :db/ensure :grant/valid?]])
  • Verwendet man diese Entity Spec, tritt beim gleichzeitigen Versuch von approve und deny in derselben Transaktion ein Entity-Predicate-Fehler auf und die Invariante bleibt erhalten
    • Der Fehler enthält :db.error/entity-pred, :db.error/pred-return false

Dokumentationsänderungen und Hinweise für Nutzer

  • Datomic hat nach der Zusammenarbeit mit Jepsen seine Dokumentation umfassend überarbeitet
    • Die transaction safety documentation spiegelt die stärkeren Sicherheitsgarantien wider, die Datomic nach eigener Auffassung tatsächlich bietet
    • Globale Serialisierbarkeit, peer-spezifische Monotonie und Strict Serializability für Schreibvorgänge oder Lesevorgänge mit sync werden ausdrücklich genannt
    • Das Argument des „single-writer“ wurde aus der Sicherheitsdokumentation entfernt
  • Die Dokumentation zu transaction syntax and semantics behandelt umfassend die Struktur von Transaction Requests, die Erweiterungsregeln für Map-Form und Transaction Functions sowie den Ablauf der Anwendung einer Transaktion
  • Auch die Dokumentation zu transaction functions wurde überarbeitet
    • Sie beschreibt mehrere Mechanismen zur Gewährleistung von Konsistenz, die Erstellung und den Aufruf von Funktionen sowie das Verhalten eingebauter Funktionen
    • Formulierungen, nach denen Transaction Functions Datenbankwerte „atomically analyze and transform database values“ könnten oder „atomic read-modify-write processing“ garantierten, wurden entfernt
  • Datomic will die an d/transact übergebene Datenstruktur künftig nicht mehr „transaction“, sondern transaction request nennen
    • Deren Elemente sollen statt „statements“ oder „operations“ als „data“ bezeichnet werden
    • [:db/add ...] und [:db/retract ...] sind jeweils ein Assertion Request bzw. ein Retraction Request
    • Das hilft dabei, tatsächliche Assertion-Datoms von unvollständigen Assertion Requests innerhalb eines Transaction Requests zu unterscheiden
  • Die nötigen Vorsichtspunkte für Nutzer sind klar
    • Auf die Serialisierbarkeit zwischen Datomic-Transaktionen ist Verlass
    • Die Semantik konkurrierender Ausführung innerhalb einer Transaktion ist eine ungewöhnliche Wahl, daher ist Vorsicht geboten, wenn mehrere Transaction Functions in derselben Transaktion aufgerufen werden
    • Besonders vorsichtig sollte man sein, wenn sich Read Sets überschneiden und Write Sets getrennt sind
    • Mehrere Increments können stillschweigend zu einem einzigen Update zusammenfallen
    • Attribute Predicates und Entity Specs können verwendet werden, aber Entity Specs müssen in allen erforderlichen Transaktionen explizit angefordert werden
  • Auch aus Betriebssicht müssen Neustarts des Transactors und Netzwerkschwankungen berücksichtigt werden
    • Der Datomic-Transactor beendet sich selbst, wenn er mehrere Minuten lang nicht mit dem Storage kommunizieren kann
    • Jepsen empfiehlt, dem Transactor eine Retry-Schleife hinzuzufügen, damit er robuster gegen Netzwerkschwankungen wird

Grenzen und künftige Forschungsfragen

  • In diesem Test blieben Punkte außerhalb des Bewertungsumfangs offen
    • Excision und Historical Query wurden nicht bewertet
    • Die Datomic-Client-Bibliothek wurde ebenfalls nicht untersucht, aber Jepsen vermutet, dass ihr Verhalten dem des für den Test verwendeten Peers ähneln dürfte
    • Als Storage Engine wurde nur DynamoDB verwendet
    • Datomic Cloud wurde ebenfalls nicht bewertet und verwendet eine leicht abweichende Architektur
  • Jepsen erklärt, kaum Systeme oder Formalisierungen zu kennen, die sowohl Serialisierbarkeit zwischen Transaktionen als auch konkurrierende Semantik innerhalb einer Transaktion bereitstellen
  • Das Modell von Datomic wirft mehrere Forschungsfragen auf
    • Ob sich eine Datomic-Transaktion als Dual klassischer Transaktionen oder als Modell einer „co-transaction“ verstehen lässt
    • Ob sich Vor- und Nachteile eines solchen Modells durch Static Analysis, Runtime Checks oder API-Erweiterungen abmildern lassen
    • Wie wahrscheinlich es ist, dass reale Nutzer Transaktionen schreiben, die Invarianten verletzen
  • Als Vergleich werden das temporale Datalog-Forschungsprojekt Alvaro’s Dedalus und Fauna genannt
    • Dedalus lässt wie Datomic Transaktionen „all at once“ stattfinden
    • Fauna ist eine temporale Datenbank und unterstützt sogar Strong Serializability; anders als Datomic scheint es innerhalb von Transaktionen serielle Ausführung und inkrementelle Side Effects zu bieten
  • Auch die Ähnlichkeit zwischen Datomics End-of-Transaction-Conflict-Checker und der First-Committer-Wins-Regel von Snapshot Isolation bleibt eine Forschungsmöglichkeit
    • Welche Teile der Literatur zu Snapshot Isolation sich auf Datomic anwenden lassen
    • Durch welche Anti-Dependency-Edges Zyklen innerhalb von Datomic-Transaktionen dargestellt werden
    • Ob es interne semantische Analoga zu Phänomenen wie Lost Update, Fractured Read, Read-Only Transaction Anomaly oder Long Fork gibt, bleibt offen
  • Auch die Verbindung zum CALM-Theorem lässt sich weiter untersuchen
    • Ob logisch monotone Transaction Functions innerhalb derselben Datomic-Transaktion sicher kombiniert werden können
    • Ob sich erforschen lässt, ob Datalog-Programme ohne Negation auch in diesem Ausführungsmodell sicher sind

Verwandte Beiträge

1 Kommentare

 
GN⁺ 2024-05-17
Hacker-News-Kommentare

  • Ich habe diese Arbeit aus der Nähe mitverfolgt, und es war wirklich spannend, den Diskussionsprozess zu sehen.
    Es war auch überraschend, dass Jepsen keine kritischen Bugs gefunden hat; allein die Klarstellung der Dokumentation und des beabsichtigten ungewöhnlichen Verhaltens war ein sehr nützliches Ergebnis.
    Wenn man bedenkt, dass wir eine Bank auf Datomic betreiben, war es als Übung zum Aufbau von Vertrauen auf jeden Fall wertvoll.

    • Wenn man bedenkt, dass es eine von Rich Hickey entworfene Datenbank ist, ist das Ergebnis nicht allzu überraschend.
      Ein wirklich hervorragender Text; jedes Mal, wenn ich mich selbst für ziemlich schlau halte, ist eine Jepsen-Analyse eine gute Gelegenheit, wieder bescheiden zu werden.
    • Darf ich fragen, um welche Bank es geht?
    • Zu der Aussage „Es war auch überraschend, dass Jepsen keine kritischen Bugs gefunden hat“: Im Bericht steht, dass man zwar die Existenz von Bugs beweisen kann, aber nicht die Abwesenheit von Bugs.
    • Habt ihr eine solche Validierung nicht selbst durchgeführt, bevor ihr eine Bank darauf betrieben habt?

  • Das war das erste Mal, dass ich einen Jepsen-Bericht gründlich gelesen habe, und mir gefiel besonders, wie klar die internen Abläufe von Datomic-Transaktionen erklärt wurden.
    Mir wurde auch klar, wie wenig ich die Unterschiede zwischen Datomic-Transaktionen und Transaktionen in SQL-Datenbanken verstanden hatte.
    Besonders aufgefallen ist mir der Absatz: „Datomic bezeichnete früher die an d/transact übergebene Datenstruktur als ‚transaction‘ und ihre Elemente als ‚statements‘ oder ‚operations‘. Künftig wollen wir diese Struktur ‚transaction request‘ und ihre Elemente ‚data‘ nennen.“
    Ich frage mich, was das für d/transact-async und verwandte Funktionen im Namespace datomic.api bedeutet.
    Ich habe Datomic seit fast einem Jahr nicht mehr genutzt, und es sieht so aus, als hätte sich viel geändert.

    • Aufgrund der Jepsen-Testergebnisse waren keine Änderungen an der Datomic-Software erforderlich.
      Alle Funktionen in datomic.api bleiben unverändert.

  • Ein hervorragender, ausführlicher Bericht über eine wirklich gute Datenbank.
    Es ist auch sehr erfreulich, dass die Dokumentation klarer und aktualisiert wird.
    Nebenbei: Ich würde mir wirklich wünschen, dass Apple eine Jepsen-Analyse von FoundationDB finanziert.
    Ich weiß, dass Aphyr gesagt hat, „ihre Tests sind wahrscheinlich besser“, aber wenn Jepsen tatsächlich keine Probleme in FoundationDB findet, wäre das ein weiteres starkes Argument dafür, dass es eine hervorragende Datenbank ist.

    • Ich habe absolut nicht den Wunsch, Aphyr die Lebensgrundlage zu entziehen, aber ich frage mich, ob es einen besonderen Grund gibt, warum ein ausreichend motivierter Contributor nicht selbst Jepsen-Tests erstellen könnte, oder ob das so teuer ist, dass es selbst mit einer „GoFundMe-ähnlichen Methode“ schwer zu stemmen wäre.
      Ich kenne mich in diesem Bereich nicht besonders gut aus, aber wenn ich höre „$foo sollte die Kosten übernehmen“, werde ich hellhörig.
      Kapital gibt es im Überfluss, aber darauf zu warten, dass Apple etwas tut, dauert meiner Erfahrung nach lange.

  • Jepsen fand eine klare Situation, die zu Verletzungen von Invarianten führt, und es war auffällig, dass Datomic darauf offenbar nur mit einer Klarstellung der Dokumentation reagierte.
    Bedeutet das am Ende, dass das Datomic-Team akzeptiert, dass solche Verletzungen auftreten, es ihm aber egal ist?
    Im Artikel heißt es: „Aus Sicht von Datomic sind Verletzungen der Invarianten im Grant-Workload ein Benutzerfehler. Transaktionsfunktionen werden nicht der Reihe nach atomar ausgeführt. Wenn andere Operationen innerhalb der Transaktion ihre Vorbedingungen ungültig machen können, ist es nicht sicher, Vorbedingungen in einer Transaktionsfunktion zu prüfen.“

    • Wie Jepsen bestätigt hat, funktioniert Datomics Mechanismus zur Durchsetzung von Invarianten wie vorgesehen.
      Um zu sehen, was das aus Nutzersicht bedeutet, kann man sich etwa folgende Pseudo-Transaktionsdaten vorstellen:
      [ [Stu favorite-number 41] ;; maybe more stuff [Stu favorite-number 42] ]
      Operativ gelesen sieht es so aus, als hätte ich zu Beginn der Transaktion die 41 gemocht und später die 42.
      Nach Abschluss der Transaktion würde ein Beobachter erwarten, nur zu sehen, dass ich die 42 mag, und müsste sich fragen, unter welchen Bedingungen die 41 sichtbar sein kann.
      Eine solche operative Interpretation der Semantik innerhalb einer Transaktion ist in vielen Datenbanken üblich, setzt aber voraus, dass es innerhalb der Transaktion mehrere Zeitpunkte gibt.
      Datomic hat solche Zeitpunkte nicht, will sie auch nicht haben, und bevorzugt es, sich nicht darum kümmern zu müssen, was „mitten in der Transaktion“ passiert ist.
      In Datomic geschehen alle Fakten einer Transaktion zum selben Zeitpunkt, daher sagt diese Transaktion aus, dass ich angefangen habe, beide Zahlen gleichzeitig zu mögen.
      Wenn man Datomic-Transaktionen fälschlich als Kombination mehrerer Operationen liest, findet man natürlich alle möglichen „Invarianten-Anomalien“.
      Umgekehrt kann man auch „Invarianten-Anomalien“ finden, wenn man das Datomic-Modell fälschlich auf SQL-Transaktionen überträgt.
      Wegen dieser möglichen Missverständnisse brauchte es gute Dokumentation, und gemeinsam mit Jepsen haben wir die Dokumentation verbessert [1], unvorsichtige Formulierungen geglättet und versucht, Missverständnisse zu reduzieren.
      Außerdem haben wir eine technische Notiz ergänzt, die genau dieses Missverständnis direkt behandelt [2].
      [1] https://docs.datomic.com/transactions/transactions.html#tran...
      [2] https://docs.datomic.com/tech-notes/comparison-with-updating...
    • Kurz gesagt ist es eher „eine potenzielle Falle, aber konsistent mit der Dokumentation und funktioniert wie vorgesehen“.
      Ob das in der Praxis wichtig ist, hängt davon ab, welche Invarianten ein Nutzer mit Transaktionsfunktionen erhalten will und ob diese Funktionen die Invarianten nur dann wahren, wenn sie sequenziell und nicht gleichzeitig ausgeführt werden.
      Die Position von Datomic – oder das, was jemand von Datomic hoffentlich noch einordnen würde – ist, dass Nutzer solche Transaktionsfunktionen nicht besonders häufig schreiben.
      Diese Position lässt sich verteidigen. In der Dokumentation stand ausdrücklich, dass Transaktionsfunktionen nicht einander beobachten, sondern den Zustand zu Beginn der Transaktion.
      Andererseits gab es in der Dokumentation auch Formulierungen, die nahelegten, dass Transaktionsfunktionen zum Erhalt von Invarianten verwendet werden können: „[txn fns] can atomically analyze and transform database values. You can use them to ensure atomic read-modify-update processing, and integrity constraints...“
      Wegen dieser Formulierung und der Tatsache, dass fast alle anderen serialisierbaren Datenbanken eine sequenzielle Semantik innerhalb von Transaktionen verwenden, nahm dieses Thema im Bericht viel Raum ein.
      Es ist eine komplexe Frage ohne klare Antwort, und ich würde gern hören, wie die allgemeine Datenbank-Community und insbesondere Datomic-Nutzer diese Semantik aufnehmen.
    • Ich denke, am Ende von Abschnitt 3.1 gibt der Text die Antwort bereits: „Dieses Verhalten mag überraschend sein, ist aber im Großen und Ganzen konsistent mit der Datomic-Dokumentation. Nubank plant nicht, dieses Verhalten zu ändern, und wir betrachten es nicht als Bug.“
      Wenn man von einer „Situation, die zu Verletzungen von Invarianten führt“ spricht, klingt das wie ein Bug in Datomic, ist es aber nicht.
      Man muss verstehen, wie Datomic Transaktionen verarbeitet, und den Code entsprechend schreiben.
      Ich habe nichts mit Nubank zu tun, aber ich habe Datomic als Allzweckdatenbank genutzt und bin in keine Situation geraten, in der das ein Problem war.
    • Das klingt ähnlich wie Situationen in manchen relationalen Datenbanken, in denen man wissen muss, dass man SELECT ... FOR UPDATE braucht, wenn ein Update von einem gerade selektierten Wert abhängt.

  • Für alle, die es nicht wissen: Der Name Jepsen ist ein Wortspiel mit Carly Rae Jepsen, die „Call Me Maybe“ gesungen hat.
    Als Name für ein Forschungsprojekt zu verteilten Systemen ist das meiner Meinung nach perfekt.

  • Ich habe Datomic in der Praxis nicht lange verwendet, aber es ist so eigenwillig, dass ich mich frage, ob daran irgendetwas überraschend ist.
    Datomic-Transaktionen sind im Grunde eher Batches, und ich hatte sie immer als single-threaded verstanden, daher wirkt es erwartbar, dass es nicht viele Race Conditions gibt.
    Vom Design her ist es eher langsam und sicher.

    • Das Beispiel „Wenn man x in derselben Transaktion zweimal erhöht, wird daraus nicht x+2, sondern x+1“ wirkt ziemlich wichtig.
      Da muss man wohl ziemlich vorsichtig sein.
    • Komprimiert Datomic irgendwann das Transaktionslog?

  • Danke, Kyle.
    Es ist klar, dass unsere Dokumentation unzureichend war.
    Zusammen mit Rich habe ich versucht, eine klarere und umfassendere Dokumentation zu Datomics Transaktionsmodell zu schreiben.
    Ich hoffe, dass sie häufige Missverständnisse im Voraus verhindert, und freue mich über jedes Feedback.
    https://docs.datomic.com/transactions/model.html

  • Das Datenmodell von Datomic ist ziemlich intuitiv, wenn man mit Triple Stores oder RDF vertraut ist.
    In der Dokumentation oder in Online-Diskussionen wird diese Ähnlichkeit jedoch selten erwähnt.
    Ich frage mich, ob das daran liegt, dass die Leute mit solchen Konzepten nicht vertraut sind, ob Assoziationen mit dem Semantic Web als störend empfunden werden, oder ob es einen grundlegenden Unterschied gibt, den ich übersehe.

  • Auf diese Analyse habe ich wirklich gewartet.
    Da ich in letzter Zeit selbst einen Datomic-ähnlichen Datenspeicher baue, dürfte sie nützlich sein, und ich lese sie gerade.
    Auch die MongoDB-Analyse war interessant, und andere Analysen zu Redis, RethinkDB usw. sollte man sich unbedingt ansehen.
    Irgendwann wäre auch eine Analyse zu rqlite/dqlite oder turso/libsql schön.