L'architecture repose sur un séquenceur de transaction déterministe qui ordonne les opérations en utilisant des Horloges Logiques Hybrides plutôt que le temps physique, éliminant les dépendances liées à l'écart d'horloge inhérentes aux systèmes basés sur TrueTime. Le coordinateur met en œuvre une variante du protocole Calvin, où les intentions de transaction sont répliquées à une majorité de leaders de shard avant l'exécution, garantissant la sérialisation par un ordonnancement déterministe plutôt que par un verrouillage distribué. Les spécifications TLA+ modélisent les transitions d'état du coordinateur, vérifiant formellement que le système maintient la sécurité (sérialisation stricte) et la vivacité (toutes les transactions engagées se terminent finalement) même pendant les partitions réseau partielles.
Le coordinateur persiste les journaux de transaction dans un WAL (Write-Ahead Log) en utilisant le consensus Paxos pour la durabilité à travers les zones de disponibilité. Les proxys de shard abstraient les moteurs de stockage sous-jacents—qu'il s'agisse de PostgreSQL, MongoDB ou Cassandra—présentant une interface unifiée pour le moteur d'exécution. La détection de conflit utilise un graphe de dépendance construit lors de la phase de séquençage, permettant l'exécution concurrente des transactions non conflictuelles tout en maintenant l'équivalence avec un ordre sériel.
Une banque d'investissement mondiale a dû migrer son système de règlement des transactions d'une base de données Oracle monolithique à une architecture sharded s'étendant sur les régions AWS et Azure. Le défi critique était d'assurer le règlement atomique des transactions touchant plusieurs classes d'actifs stockées dans différentes technologies de base de données—actions dans PostgreSQL et dérivés dans ScyllaDB—sans déployer des horloges atomiques ou des sources de temps GPS pour la synchronisation.
Une solution proposée a utilisé des transactions standard XA avec un protocole de validation en deux phases (2PC) géré par un gestionnaire de transactions Narayana. Cette approche offrait une forte cohérence et un support écosystémique mûr, mais introduisait un comportement bloquant où un échec du coordinateur pendant la phase de préparation laissait les shards détenant des verrous indéfiniment, violant les exigences de vivacité pendant l'instabilité du réseau inter-clouds.
Une autre alternative a considéré le modèle Saga implémenté via Axon Framework, utilisant des transactions compensatoires pour des scénarios de retour en arrière. Bien que cela ait fourni une haute disponibilité et évité le verrouillage distribué, cela a sacrifié la sérialisation stricte—inacceptable pour le règlement financier où les états intermédiaires ne doivent jamais être observables, et la logique de compensation pour les opérations de marché externes irréversibles s'est avérée prohibitivement complexe.
L'architecture sélectionnée a mis en œuvre un coordinateur déterministe inspiré par Calvin avec vérification formelle TLA+. Le système a séquencé toutes les transactions de règlement via une machine d'état répliquée utilisant Raft pour le journal de coordination, puis les a exécutées dans le même ordre sur tous les shards en utilisant des procédures stockées idempotentes. Cela a éliminé le besoin de verrouillage distribué pendant l'exécution et a permis à la vérification de modèle TLA+ de prouver mathématiquement que le système ne pouvait pas avoir de blocage ou perdre des règlements pendant des partitions réseau arbitraires.
Le déploiement a entraîné une réduction de 40 % de la latence de règlement par rapport au système Oracle hérité, tout en maintenant des garanties ACID complètes à travers les clouds. Lors d'une panne régionale ultérieure AWS, le système a continué de traiter des transactions sans intervention manuelle, validant les propriétés de vivacité formellement prouvées.
Quelle est la différence fondamentale entre la sérialisation stricte et la linéarisation, et pourquoi un coordinateur de transaction distribué cible-t-il généralement la première plutôt que la seconde ?
La sérialisation stricte combine la sérialisation (les transactions semblent s'exécuter dans un certain ordre séquentiel) avec la contrainte de temps réel de la linéarisation (les transactions se terminent avant que les suivantes ne commencent). Alors que la linéarisation s'applique aux opérations sur un seul objet, la sérialisation stricte étend cela à des transactions sur plusieurs objets. Les candidats confondent souvent ces deux concepts, concevant des systèmes qui garantissent la linéarisation sur une seule clé mais échouent à prévenir des anomalies comme l'écart d'écriture sur plusieurs clés. Un coordinateur atteint la sérialisation stricte en établissant un ordre global des transactions—souvent par le biais d'une couche de séquençage ou d'un oracle de timestamp—tandis que la linéarisation seule peut être satisfaite par shard sans garanties d'ordre inter-shard.
Pourquoi le protocole de validation en deux phases (2PC) bloque-t-il indéfiniment lors d'une panne de coordinateur, et comment le protocole de validation en trois phases (3PC) échoue-t-il à résoudre cela lors de partitions réseau ?
Dans 2PC, une fois qu'un participant vote "oui" lors de la phase de préparation, il conserve des verrous jusqu'à recevoir la décision de validation/abort globale du coordinateur. Si le coordinateur échoue après avoir reçu tous les votes mais avant de diffuser la décision, les participants restent incertains et bloqués, violant la disponibilité. 3PC tente de résoudre cela en ajoutant une phase de pré-validation et des progrès basés sur des délais, mais lors de partitions réseau, un participant ne peut pas distinguer entre un coordinateur échoué et un coordinateur partitionné. Cela conduit à des scénarios de split-brain où différentes partitions prennent des décisions conflictuelles, violant la cohérence. Le problème fondamental est que l'impossibilité de FLP prouve qu'un consensus déterministe est impossible dans des systèmes asynchrones avec même un seul processus défaillant, ce qui signifie que tout protocole de validation doit choisir entre le blocage (sécurité) et l'inconsistance potentielle (vivacité) lors de certains modes de défaillance.
Comment TLA+ vérifie-t-il les propriétés de vivacité dans un coordinateur de transactions, et quels opérateurs de logique temporelle expriment "s'engager finalement" par rapport à "ne perd jamais de données" ?
TLA+ utilise la logique temporelle pour spécifier que les bonnes choses arrivent finalement (vivacité) tandis que les mauvaises choses n'arrivent jamais (sécurité). La propriété de vivacité que toutes les transactions initiées se terminent finalement est exprimée à l'aide de l'opérateur finalement (◇), généralement écrit comme Initiated(t) ~> Committed(t) (mène à), signifiant que si la transaction t est initiée, elle s'engagera ou s'abandonnera finalement. Les propriétés de sécurité comme "ne perd jamais de données" utilisent l'opérateur toujours (□), écrit comme □(Committed(t) ⇒ ◇(Query(t) = Value)), signifiant qu'une fois engagée, la valeur est toujours lisible à un moment donné. Les candidats manquent souvent que la vérification de la vivacité nécessite des hypothèses d'équité—l'équité faible (WF_vars(Action)) garantit que si une action reste activée, elle doit finir par se produire, empêchant les stagnations infinies où le coordinateur cesse simplement de faire des étapes. Sans ces contraintes d'équité, les modèles TLA+ satisferaient trivialement les propriétés de vivacité en ne faisant rien.