Mimari, işlemleri fiziksel zaman yerine Hibrit Mantıksal Saatler kullanarak sıralayan deterministik bir işlem sıralayıcısına merkezlenmiştir; bu, TrueTime tabanlı sistemlerdeki saat kayması bağımlılıklarını ortadan kaldırır. Koordinatör, işlem niyetlerinin yürütmeden önce çoğunluk kesim liderlerine çoğaltıldığı Calvin protokolünün bir varyantını uygular; böylece dağıtılmış kilitleme yerine deterministik zamanlama ile serileştirme sağlanır. TLA+ spesifikasyonları, koordinatörün durum geçişlerini modeller, sistemin güvenliği (katı serileştirme) ve canlılığı (tüm taahhüt edilen işlemler nihayetinde tamamlanır) sağladığını resmi olarak doğrular, hatta kısmi ağ bölünmeleri sırasında bile.
Koordinatör, dayanıklılık için Paxos mutabakatı kullanarak işlem günlüklerini WAL (Ön Yazma Günlüğü) olarak kalıcı hale getirir. Kesim proxy'leri, atanmış depolama motorlarını—PostgreSQL, MongoDB veya Cassandra—abstre eder ve yürütme motoru için birleşik bir arayüz sunar. Çatışma tespiti, sıralama aşamasında oluşturulan bir bağımlılık grafiği kullanarak gerçekleştirilir, bu da çelişmeyen işlemlerin eşzamanlı yürütülmesine izin verirken, serisel bir sıraya eşdeğerlik sağlar.
Küresel bir yatırım bankası, ticaret uzlaşı sistemlerini monolitik Oracle veritabanından, AWS ve Azure bölgelerini kapsayan bir kesim mimarisine taşımak için ihtiyaç duydu. Kritik zorluk, farklı veritabanı teknolojilerini kullanan birden fazla varlık sınıfını kapsayan ticaretlerin atomik uzlaşmasını sağlamaktı—PostgreSQL'de hisse senetleri ve ScyllaDB'de türevler—atomik saatler veya GPS zaman kaynakları kullanmadan senkronizasyon sağlamaktı.
Önerilen bir çözüm, bir Narayana işlem yöneticisi tarafından yönetilen iki aşamalı taahhüt (2PC) protokolü ile standart XA işlemlerini kullandı. Bu yaklaşım güçlü tutarlılık ve olgun ekosistem desteği sundu, ancak hazırlık aşamasında bir koordinatör hatası, kesimlerin kilitleri sonsuz bir süre tutmasına neden olduğundan, dağılmış bulut ağ kararsızlığında canlılık gereksinimlerini ihlal ederek bloke olma davranışını tanıttı.
Başka bir alternatif, Axon Framework aracılığıyla uygulanan Saga desenini düşündü ve geri alma senaryoları için telafi işlemleri kullandı. Bu yaklaşım yüksek kullanılabilirlik sağladı ve dağıtılmış kilitlemeyi önledi, ancak katı serileştirmeyi feda etti—bu finansal uzlaşmalarda ara durumların asla gözlemlenmaması gerektiği için kabul edilemezdi ve geri ödeme mantığı geri alınamaz dış piyasa işlemleri için aşırı karmaşık hale geldi.
Seçilen mimari, TLA+ resmi doğrulaması ile Calvin esinlenmeli deterministik bir koordinatör uyguladı. Sistem, koordinasyon günlüğü için Raft kullanarak çoğaltılmış bir durum makinesi aracılığıyla tüm uzlaşma işlemlerini sıraladı, ardından bunları idempotent saklama prosedürleri kullanarak tüm kesimlerde aynı sırada yürüttü. Bu, yürütme sırasında dağıtılmış kilitleme ihtiyacını ortadan kaldırdı ve TLA+ model kontrolü sayesinde sistemin ölü kilitlenmeye ya da işlem kaybına uğrayamayacağını matematiksel olarak kanıtladı.
Dağıtım, miras alınan Oracle sistemine göre uzlaşma gecikmesinde %40'lık bir azalma ile sonuçlandı ve bulutlar arasında tam ACID garantileri sağlandı. Ardından gelen bir bölge genelindeki AWS kesintisi sırasında, sistem manuel müdahale olmadan işlemleri işlemeye devam etti ve resmi olarak kanıtlanmış canlılık özelliklerini doğruladı.
Katı serileştirilebilirlik ile lineerleştirilebilirlik arasındaki temel fark nedir ve neden dağıtılmış bir işlem koordinatörü genellikle birincisini hedef alır?
Katı serileştirilebilirlik, serileştirmeyi (işlemler belirli bir sıralı sıradaki gibi görünüyor) ve lineerleştirilebilirliğin gerçek zamanlı kısıtlamasını (işlemler, sonrakiler başlamadan önce tamamlanır) birleştirir. Lineerleştirilebilirlik, tek nesne işlemleri için geçerli iken, katı serileştirilebilirlik bunu çok nesne işlemlerine genişletir. Adaylar genellikle bunları birbirine karıştırır; tek anahtar lineerleştirilebilirliğini sağlayan sistemler tasarlarlar ancak birden fazla anahtar arasında yazma kaymasını önlemekte başarısız olurlar. Bir koordinatör, genellikle bir sıralama katmanı veya zaman damgası oracle’ı aracılığıyla işlemler için küresel bir sıralama oluşturarak katı serileştirilebilirlik başarır; oysa yalnızca lineerleştirilebilirlik, kesimler arasında sıralama garantileri olmaksızın her bir kesim için karşılanabilir.
İki aşamalı taahhüt (2PC) protokolü neden koordinatör hatası sırasında sonsuz bir şekilde bloke olur ve üç aşamalı taahhüt (3PC) ağ bölünmeleri altında bunu çözmeyi neden başaramaz?
2PC'de, bir katılımcı hazırlık aşamasında "evet" oyu verince, koordinatörden global taahhüt/iptal kararını alana kadar kilitleri tutar. Koordinatör, tüm oyları aldıktan sonra ama karar yaymadan önce başarısız olursa, katılımcılar belirsiz ve kilitli kalır, bu da kullanılabilirliği ihlal eder. 3PC, bir ön taahhüt aşaması ve zaman aşımına dayalı ilerleme ekleyerek bunu çözmeye çalışır, ancak ağ bölünmeleri altında bir katılımcı, başarısız bir koordinatör ile bölünmüş bir koordinatör arasında ayırt edemez. Bu, çelişkili kararlar veren farklı bölünmelerin ortaya çıktığı split-brain senaryolarına yol açar ve tutarlılığı ihlal eder. Temel sorun, FLP imkansızlığının, belirli bir hatalı süreç ile birlikte asenkron sistemlerde deterministik mutabakatın imkansız olduğunu kanıtlamasıdır. Bu da herhangi bir taahhüt protokolünün bazı hata modları sırasında bloke olma (güvenlik) ve potansiyel tutarsızlık (canlılık) arasında seçim yapması gerektiği anlamına gelir.
TLA+ bir işlem koordinatöründe canlılık niteliklerini nasıl doğrular ve "nihayetinde taahhütler" ile "asla veri kaybı yaşamaz"'ı ifade eden belirli zamansal mantık operatörleri nelerdir?
TLA+, iyi şeylerin nihayetinde gerçekleştiğini (canlılık) ve kötü şeylerin asla gerçekleşmediğini (güvenlik) belirtmek için zamansal mantık kullanır. Başlatılan tüm işlemlerin nihayetinde tamamlanacağına dair canlılık niteliği nihayetinde operatörü (◇) ile ifade edilir; tipik olarak Başlatılan(t) ~> Taahhüt(t) (yol açma) biçiminde yazılır, yani işlem t başlatılırsa, nihayetinde taahhüt ya da iptal edilecektir. "Asla veri kaybı yaşamaz" gibi güvenlik nitelikleri her zaman operatörünü (□) kullanır; □(Taahhüt(t) ⇒ ◇(Sorgu(t) = Değer)) biçiminde yazılır, yani bir kez taahhüt edildiğinde değer her zaman nihayetinde okunabilir. Adaylar genellikle canlılık denetiminin adalet varsayımlarını gerektirdiğini gözden kaçırır—zayıf adalet (WF_vars(Action)) eylemin etkin kalması durumunda nihayetinde gerçekleşmesini sağlamalıdır; böylece koordinatör sonsuza dek duramaz. Bu adalet kısıtlamaları olmadan, TLA+ modelleri, hiçbir şey yapmadan canlılık niteliklerini sıradan bir şekilde tatmin edebilir.