adya, Jepsen tarzı izolasyon denetimini tek bir Rust binary'sinde CI'ya getiriyor

Bir geliştirici, adya adlı açık kaynak bir Rust aracını yayımladı; araç, bir veritabanının iddia ettiği transaction izolasyonunu gerçekten sağlayıp sağlamadığını, Jepsen'in Elle denetçisinin dayandığı JVM'ye gerek duymadan kontrol ediyor. dev.to'daki bir yazıda yazar, bunu black-box izolasyon doğrulamasını sıradan continuous integration içinde çalıştırılabilecek kadar ucuz ve taşınabilir hale getirme girişimi olarak tanımlıyor.

adya ne yapıyor

adya bir history — her istemcinin ne istediğinin ve veritabanının ne döndürdüğünün kaydı — alır ve hangi izolasyon garantilerinin sağlandığını raporlar. Her ihlal için, ilgili transaction'ları ve anomaliyi kanıtlayan okuma-yazma zincirini yazdırır. Gönderiye göre araç, Elle yaklaşımının (Kingsbury ve Alvaro, VLDB 2020) bağımsız bir uygulaması; aynı history formatlarını okuyor ve aynı flag'leri kabul ediyor.

Temel sorun, izolasyon hatalarının unit testlerde ortaya çıkmamasıdır. Bu hatalar, eşzamanlı transaction'ların belirli bir şekilde iç içe geçmesini gerektirir ve ortaya çıktıklarında hiçbir şey çökmez: bir bakiye sadece yanlıştır ya da iki rezervasyon aynı koltuğa düşer. Standart örnek write skew'dir — iki transaction bir koşulu kontrol eder, koşulun sağlandığını görür ve birlikte koşulu bozan değişiklikleri commit'ler. Snapshot isolation buna izin verir ve Postgres'in REPEATABLE READ'i snapshot isolation'dır; dolayısıyla daha güçlü semantikler varsayan uygulamalar bu hatayı fark etmeden yayımlayabilir.

Elle'nin katkısı, bu tür anomalilerin dışarıdan tespit edilebileceğini göstermek oldu: istemci operasyonlarını kaydet, transaction'lar arasındaki bağımlılıkları çıkar ve her izolasyon seviyesinin yasakladığı döngüleri ara. Anomali sınıfları (G0, G1c, G-single, G2), aracın adını da veren Atul Adya'nın 1999 tezinden gelir.

Neden sadece Elle kullanılmıyor

Elle bir Clojure kütüphanesidir ve onu bir Jepsen koşusunun dışında kullanmak isteyen ekipler genellikle Go veya Python harness'ten elle-cli'yi çağırır. Yazar, CI'da tam olarak bunu yapan iki açık kaynak projeden söz ediyor; bunlardan bytecaskdb'nin pull request'i yaşanan sıkıntıları belgeliyor: engellenmiş bir Clojars mirror'ü, graphviz eksikken yaşanan bir çökme ve JSON çıktısını bozan log satırları. Yazar ayrıca elle-cli 0.1.11'in Windows'ta anormal history'lerde hiç çıktı vermeden takıldığını, Linux'ta ise kırk rastgele 300 transaction'lık history'den beşinde beş dakikadan uzun sürdüğünü ve bir tanesinde 6 GB heap'i tükettiğini bildiriyor. adya'nın ise tamamını 0.2 saniyede kontrol ettiğini söylüyor.

Elle ayrıca workload'u size bırakır: transaction'ları üreten, bunları veritabanında çalıştıran ve history'yi kaydeden istemci sizin sorumluluğunuzdadır. adya her iki yarımı tek bir binary'de toplar — cargo install adya sonrası tek bir komut, canlı bir Postgres bağlantısına ya da yerleşik bir simülatöre karşı belirli bir izolasyon seviyesinde bir workload çalıştırabilir ve ortaya çıkan history'yi daha katı bir modele karşı kontrol edebilir.

Denetim nasıl çalışıyor

Varsayılan workload, Elle'den alınan list-append'dir: key'ler liste tutar, transaction'lar benzersiz değerler ekler ve tüm listeleri geri okur; böylece her okuma, veritabanına güvenmeden önceki tüm append'lerin sırasını ortaya çıkarır. adya, bu sıralamalardan Adya'nın ww, wr ve rw kenar tiplerini kullanarak bir bağımlılık graph'ı kurar; strict serializability için real-time kenarları ekler ve bir transitive reduction, graph'ı history boyutuyla kabaca doğrusal tutar.

Her anomali sınıfı kısıtlara sahip bir döngüdür — örneğin G-single tam olarak bir rw kenarına sahiptir. adya döngüleri saymak yerine, transaction ve path-state çiftleri üzerinde bir genişlik öncelikli arama çalıştırır; state, rw sayılarını ve kenar komşuluğunu izleyen yedi bittir ve istenen biçimdeki en kısa döngüyü döndürür. Daha ucuz strongly-connected-component kontrolleri önce çalıştığından, ortaya çıkması imkânsız olan anomali sınıfları tamamen atlanır. Yazar, 100.000 transaction'lık bir history'nin (30 MB JSON) dizüstü bilgisayarında yaklaşık 1.6 saniyede kontrol edildiğini bildiriyor.

Doğrulama ve veritabanı sonuçları

Yanlış bir denetçi, hiç olmayandan kötü olduğu için doğrulama çabanın büyük kısmını almış, diyor gönderi. adya, elle-cli'nin test setindeki 56 history'nin tamamıyla eşleşiyor — aynı kararlar, anomali tiplerleri ve elenen en zayıf modeller — ve CI'sı rastgele üretilmiş history'leri canlı Elle ile çapraz kontrol ediyor; ilk tam koşuda Elle 40 history'den 34'ünü tamamladı ve adya 34'ünün tamamında aynı sonucu verdi. Serializable, snapshot isolation, read committed, read uncommitted ve bilinçli olarak bozulmuş bir seviyeyi uygulayan bir simülatör, doğru koşuların kendi seviyelerinde sıfır anomali ürettiğini ve üzerindeki seviyelerde beklenen anomalileri ürettiğini doğruluyor.

Projenin CI'sı ayrıca 10 istemciden 6 hot key üzerinden 4.000 transaction'ı Postgres 17 ve MySQL 8.4'e karşı çalıştırıyor. Postgres SERIALIZABLE her modele göre doğrulanıyor; Postgres REPEATABLE READ, serializability'ye göre kontrol edildiğinde G2-item gösteriyor ve bu, snapshot isolation'ın bilinen sınırlarıyla örtüşüyor; Postgres READ COMMITTED ise G-single, G2-item, internal ve lost-update anomalileri gösteriyor. Özellikle, MySQL'in REPEATABLE READ'i yayımlanan tabloda snapshot isolation kontrolünde bile başarısız oldu ve Postgres'in aynı adlı seviyesinin sergilemediği anomaliler ortaya çıktı.

Neden önemli

Çoğu ekip izolasyon seviyelerini dokümantasyon vaatleri olarak görüyor. adya bu vaadi otomatik, tekrarlanabilir bir teste dönüştürüyor: tek bir Rust binary'si workload'u üretiyor, history'yi kaydediyor ve saniyeler içinde kontrol ediyor; Elle'yi CI pipeline'larında kullanışsız kılan JVM kırılganlığını ortadan kaldırıyor. Postgres-MySQL karşılaştırması ödülü zaten gösteriyor — aynı seviye adları, maddi olarak farklı garantiler saklayabilir. Black-box history kontrolü hâlâ bir doğruluk kanıtı değil deneysel bir yöntemdir; ama bu hataları rutin olarak aramak, hiç kontrol etmemekten önemli bir adım ötedir.