Consistency Model'leri: Linearizability, Sequential, Causal ve Eventual Consistency

Sürüm notu: Bu yazıdaki kodlar C# 14 ve .NET 10 ile derlenip denenmiştir.

Önce Tahmin Et

Bir kitabın fiyatı 400. Alice fiyatı 450'ye güncelliyor; isteği 0. milisaniyede başlıyor, 30. milisaniyede onay alıyor. Bu sırada Carol 5. ile 10. milisaniye arasında fiyatı okuyor ve 450 görüyor. Bob ise Carol'ın okuması bittikten sonra, 12. ile 15. milisaniye arasında okuyor ve 400 görüyor.

Alice'in yazması Bob okurken henüz onaylanmamıştı, o yüzden Bob'un eski değeri görmesi ilk bakışta makul. Ama Carol yeni değeri Bob'dan önce görmüştü. Bu geçmiş "doğru" mu? Cevap, sisteminin hangi consistency model'i vaat ettiğine bağlı. Bu yazının sonunda bu geçmişin hangi modelde geçerli, hangisinde geçersiz olduğunu bir programın söylediğini göreceksin.

Consistency Model Nedir?

Bir önceki yazıda replica'ların aynı anda farklı değerler gösterebildiğini gördük. "Doğru davranış"ı tartışmak için önce neyin doğru sayılacağını tanımlamak gerekir. Consistency model bu tanımdır: client'ların gözlemleyebileceği okuma ve yazma geçmişlerinden hangilerine izin verildiğini söyleyen bir sözleşme. Jepsen'in tanımıyla bir model, geçmişlerin bir kümesidir. Bir sistem bir modeli sağlıyorsa ürettiği her geçmiş o kümenin içindedir.

Bu tanımın pratik bir faydası var: sistemin içine bakmadan, yalnız client'ların gördüklerini kaydederek bir garantiyi test edebilirsin. Jepsen'in veritabanlarını test etme yöntemi de budur: işlemleri ve sonuçlarını zaman damgalarıyla kaydet, sonra bu geçmişin vaat edilen modele uyup uymadığını bir checker ile kontrol et. Bu yazıda aynı şeyi küçük ölçekte yapacağız.

Linearizability: Sanki Tek Bir Kopya Varmış Gibi

Herlihy ve Wing'in 1990'da tanımladığı linearizability, tek bir object (bizim örneğimizde bir register, yani tek bir değer) için en güçlü modeldir. Her işlem, başladığı an ile bittiği an arasında bir noktada atomik olarak gerçekleşmiş gibi görünmelidir. Bu noktalar bütün işlemleri tek bir sıraya dizer ve o sıra hem register'ın anlamına (her okuma, kendinden önceki son yazmanın değerini döndürür) hem de gerçek zamana uyar: A bittikten sonra B başladıysa, sırada A, B'den önce gelir.

Sezgisel karşılığı şu: sistem ne kadar replica'ya bölünmüş olursa olsun, client'lar onu tek bir kopya gibi görür. Bir yazma onaylandıktan sonra başlayan her okuma o yazmayı (ya da daha yenisini) görür. Bir okuma yeni değeri döndürdükten sonra başlayan hiçbir okuma eski değeri döndüremez. Kleppmann bunu "recency guarantee" diye adlandırır. Kilitler, leader seçimi, unique constraint ve "stok sıfırın altına inmesin" gibi kurallar bu garantiye ihtiyaç duyar.

Bir Geçmişi Kontrol Etmek

Geçmişi kayıt olarak modelleyelim: her işlemin client'ı, türü, değeri ve başlangıç ile bitiş zamanı. Checker, bütün olası sıralamaları deneyerek kurallara uyan bir sıra arıyor. Fark yalnız "hangi işlem hangisinden önce gelmek zorunda" kuralında: linearizability'de gerçek zaman, sequential consistency'de yalnız aynı client'ın kendi işlemleri:

namespace Bookstore.Consistency;

public enum Kind { Write, Read }

// "price" register'ı üzerinde bir işlem: kim, ne yaptı, ne zaman başladı ve bitti
public record Op(string Client, Kind Kind, int Value, int Invoked, int Completed)
{
    public override string ToString() => $"{Client}:{(Kind == Kind.Write ? "W" : "R")}({Value})[{Invoked}-{Completed}]";
}

public static class HistoryChecker
{
    public const int Initial = 400;

    // Linearizable: gerçek zamana uyan geçerli bir register sırası
    public static bool IsLinearizable(IReadOnlyList<Op> history) =>
        Search(history, (a, b) => a.Completed < b.Invoked);

    // Sequential: yalnız her client'ın kendi sırasına uyan geçerli bir register sırası
    public static bool IsSequential(IReadOnlyList<Op> history) =>
        Search(history, (a, b) => a.Client == b.Client && a.Completed < b.Invoked);

    private static bool Search(IReadOnlyList<Op> history, Func<Op, Op, bool> mustPrecede)
    {
        bool Extend(List<Op> placed, int current)
        {
            if (placed.Count == history.Count) return true;
            foreach (Op next in history.Except(placed))
            {
                // "next"ten önce gelmesi gereken her işlem zaten yerleştirildi
                bool ready = history.Except(placed).All(other => other == next || !mustPrecede(other, next));
                bool legal = next.Kind == Kind.Write || next.Value == current;
                if (ready && legal)
                {
                    placed.Add(next);
                    if (Extend(placed, next.Kind == Kind.Write ? next.Value : current)) return true;
                    placed.RemoveAt(placed.Count - 1);
                }
            }
            return false;
        }
        return Extend([], Initial);
    }
}

Bu brute-force yaklaşım beş-altı işlemlik geçmişler için yeterli; Jepsen'in Knossos ve Elle checker'ları aynı problemi binlerce işlem için çok daha akıllı algoritmalarla çözer (genel durumda linearizability kontrolü, verimli bir çözümü bilinmeyen (NP-complete) bir problemdir). Beş geçmiş:

using Bookstore.Consistency;

Dictionary<string, Op[]> histories = new()
{
    ["1 read overlaps the write"] =
        [new("Alice", Kind.Write, 450, 0, 20), new("Bob", Kind.Read, 400, 5, 8)],
    ["2 stale read after the write finished"] =
        [new("Alice", Kind.Write, 450, 0, 10), new("Bob", Kind.Read, 400, 12, 15)],
    ["3 two readers disagree"] =
        [new("Alice", Kind.Write, 450, 0, 30), new("Carol", Kind.Read, 450, 5, 10), new("Bob", Kind.Read, 400, 12, 15)],
    ["4 Alice does not see her own write"] =
        [new("Alice", Kind.Write, 450, 0, 10), new("Alice", Kind.Read, 400, 12, 14)],
    ["5 Bob sees new, then old"] =
        [new("Alice", Kind.Write, 450, 0, 10), new("Bob", Kind.Read, 450, 12, 15), new("Bob", Kind.Read, 400, 16, 18)],
};

Console.WriteLine($"{"history",-40} {"linearizable",-13} sequential");
foreach ((string name, Op[] ops) in histories)
{
    Console.WriteLine($"{name,-40} {HistoryChecker.IsLinearizable(ops),-13} {HistoryChecker.IsSequential(ops)}");
}

history                                  linearizable  sequential
1 read overlaps the write                True          True
2 stale read after the write finished    False         True
3 two readers disagree                   False         True
4 Alice does not see her own write       False         False
5 Bob sees new, then old                 False         False

Birinci geçmişte Bob'un okuması Alice'in yazmasıyla çakışıyor; okumanın yazmadan önce gerçekleştiği bir sıra mümkün, o yüzden eski değeri görmek linearizable. İkinci geçmişte Alice'in yazması 10. milisaniyede bitti, Bob 12. milisaniyede başladı ve hâlâ 400 görüyor: replication lag'ın tipik sonucu, linearizable değil. Üçüncü geçmiş açılıştaki soru: Bob'un okuması yazmayla çakışsa bile, Carol yeni değeri Bob başlamadan önce görmüştü. Yeni değer bir kez görüldükten sonra geri dönülemez; linearizable değil.

Sequential Consistency: Gerçek Zamanı Unut, Sırayı Koru

Lamport'un 1979'da çok işlemcili bilgisayarlar için tanımladığı sequential consistency, gerçek zaman şartını kaldırır: bütün işlemler tek bir sıraya dizilebilmeli ve her client'ın kendi işlemleri o sırada kendi yaptığı sırayla yer almalı. Farklı client'ların işlemleri arasındaki gerçek zaman ilişkisi önemsizdir.

Checker'ın ikinci sütunu bunu gösteriyor. İkinci ve üçüncü geçmiş sequential: Bob'un okumalarını Alice'in yazmasından önceye koyan bir sıra var ve Bob'un kendi sırası bozulmuyor. Dördüncü ve beşinci geçmiş ise sequential bile değil. Dördüncüde Alice kendi yazmasını göremiyor: Alice'in sırasında yazma okumadan önce, o yüzden okuma 450 döndürmeli. Beşincide Bob önce yeni, sonra eski değeri görüyor: Bob'un sırasında 450'yi okuduğu an yazmadan sonradır, sonraki okuması da ondan sonra gelmek zorunda, ve sonrasında 400'ü yazan kimse yok.

Sequential consistency'nin gerçek zaman şartını kaldırması teoride küçük bir fark gibi durur; pratikte "bir kullanıcının yaptığı değişikliği, telefonla haber verdiği başka bir kullanıcı henüz göremeyebilir" demektir. Sistemin dışından gelen bir iletişim kanalı (telefon, e-posta, başka bir servis) varsa sequential consistency yetmez.

Causal Consistency ve Session Guarantee'leri

Causal consistency, dördüncü yazıdaki happens-before ilişkisine uyulmasını ister: bir işlem diğerini causal olarak etkilemişse herkes onları o sırada görür. Concurrent işlemler ise farklı client'lara farklı sırada görünebilir. Bir soru ve ona yazılan cevap her yerde aynı sırada görünür; birbirinden habersiz iki yorum farklı sırada görünebilir.

Causal consistency'nin altında, tek bir client'ın oturumunu ilgilendiren daha zayıf garantiler var. Bir önceki yazıda gördüğümüz session guarantee'ler bunlar: read-your-writes (kendi yazdığını görürsün; dördüncü geçmiş bunu bozuyor), monotonic reads (bir kez gördüğün değerden geriye gitmezsin; beşinci geçmiş bunu bozuyor), monotonic writes (yazmaların yaptığın sırada uygulanır) ve writes-follow-reads (okuduğun şeye dayanarak yaptığın yazma, okuduğun şeyden sonra görünür). Causal consistency bunların hepsini içerir.

Bu garantilerin önemi, availability tarafında ortaya çıkıyor. Jepsen'in haritası modelleri bir network partition sırasında ne kadar erişilebilir kalabildiklerine göre sınıflar:

Kırmızı modeller (linearizable, sequential, serializable ve snapshot isolation dahil) asynchronous bir network'te partition sırasında bazı node'ların cevap vermeyi reddetmesini gerektirir. Sarı modeller (causal ve session guarantee'leri) client hep aynı replica'ya bağlı kaldıkça (sticky) her yerde çalışabilir. Yeşil modeller (read committed gibi) her sağlam node'un cevap vermesine izin verir. Bir sonraki yazıdaki CAP (Consistency, Availability, Partition tolerance) teoremi, bu haritanın tek bir noktasının, linearizability'nin, ispatlanmış sınırıdır.

Eventual Consistency: Yalnız "Sonunda"

Eventual consistency en çok kullanılan ve en az şey vaat eden terimdir: yeni yazma gelmezse, bütün replica'lar sonunda aynı değere varır. Ne zaman varacakları, o sırada okumaların ne döndüreceği, hangi değere varacakları tanımın parçası değildir. İkinci yazının diliyle bu bir liveness garantisidir; hiçbir safety garantisi içermez. Üçüncü yazıdaki LWW (last-write-wins) örneği eventual consistency'yi sağlıyordu: iki replica da sonunda aynı değere vardı. Sadece o değer yanlıştı.

Daha kullanışlı bir varyantı strong eventual consistency: aynı yazmaları (hangi sırayla olursa olsun) almış iki replica aynı durumdadır. Bu, CRDT'lerin (Conflict-free Replicated Data Type) verdiği garantidir ve on birinci yazının konusu. Microservices serisinin "Microservice'lerde Transaction Yok: Eventual Consistency'yi Tasarımla Kabullenmek" yazısı ise eventual consistency'yi iş akışı seviyesinde ele alıyor: ara durumlar, saga'lar ve kullanıcıya gösterilen bekleme. Oradaki "eventual", buradaki replication tanımının iş kuralları seviyesindeki karşılığı.

Transaction Tarafı: Serializable, Linearizable ve Strict Serializability

Consistency kelimesi veritabanı dünyasında başka bir şey de anlatır ve karışıklık buradan doğar. Transaction isolation level'ları (read committed, repeatable read, snapshot isolation, serializable) birden fazla object'e dokunan transaction'ların birbirini nasıl gördüğünü tanımlar. Serializable, transaction'ların sonucunun onları bir sıraya dizerek tek tek çalıştırmakla aynı olmasını ister; ama o sıranın gerçek zamana uymasını istemez. Linearizable ise tek object içindir ve gerçek zamana uyar.

İkisini birleştiren model strict serializability'dir: transaction'lar bir sıraya dizilebilir ve sıra gerçek zamana uyar. Haritanın tepesindeki model budur ve Google Spanner'ın "external consistency" dediği garanti budur. Snapshot isolation ise serializable'ın altındadır: her transaction tutarlı bir snapshot okur ama write skew anomalisine izin verir. SQL (Structured Query Language) Server'da SNAPSHOT, PostgreSQL'de REPEATABLE READ bu modeldir. EF (Entity Framework) Core serisinin "EF Core'da Transaction'lar: SaveChanges, BeginTransaction ve Savepoint'ler" yazısında isolation level seçimini kod tarafından görmüştük; ayrıntılı uygulama ilerideki Veritabanı › SQL Server Derinlemesine serisinde.

Sık Düşülen Tuzaklar

"Consistent" kelimesini tanımsız kullanmak. ACID (Atomicity, Consistency, Isolation, Durability) kısaltmasındaki C (uygulamanın invariant'ları), CAP'teki C (linearizability) ve "eventually consistent"taki C üç farklı şeydir. Bir tasarım tartışmasında "tutarlı olmalı" denince hangi modelin kastedildiğini sor.

Serializable'ı linearizable sanmak. Serializable bir veritabanının replica'sından okumak, az önce commit edilmiş bir transaction'ı görmeyebilir; serializability bunu yasaklamaz.

Session guarantee'leri bedava sanmak. Read-your-writes, load balancer kullanıcıyı başka bir replica'ya gönderdiği anda bozulur. Sticky routing, versiyon token'ı ya da kullanıcının kendi verisini leader'dan okuma gibi açık bir mekanizma gerekir.

Eventual consistency'yi "birkaç milisaniye" sanmak. Tanım bir süre vermez. Bir replica bir saat boyunca partition'da kalırsa "sonunda" bir saat sonradır; iş akışını buna göre tasarla.

Dokümantasyondaki garantiye kör güvenmek. Jepsen'in yıllar içinde test ettiği pek çok veritabanı, vaat ettiği modeli belirli failure'larda sağlamadı. On birinci yazıda bu derse döneceğiz.

Küçük Bir Deneme

★☆☆ Birinci geçmişte Bob'un okumasını 21. ile 25. milisaniye arasına taşı. Checker ne diyor? Neden?

★★☆ HistoryChecker'a IsReadYourWrites ekle: aynı client'ın bir yazmasından sonra başlayan okumalarının o değeri ya da daha yenisini döndürmesini kontrol etsin. Beş geçmişi bu kontrolle de çalıştır. Hangi geçmiş sequential değil ama read-your-writes'ı sağlıyor?

★★★ Checker'ı iki register'a (price ve stock) genişlet ve şu geçmişi kur: Alice önce price'ı, sonra stock'u yazıyor; Bob önce yeni stock'u, sonra eski price'ı okuyor. Her register'ın kendi alt geçmişi ayrı ayrı sequential mi? İki register birlikte? Aynı soruyu linearizability için sor. Cevaplar, linearizability'nin neden "local" (object object kontrol edilebilir) bir property olduğunu ve sequential consistency'nin neden olmadığını gösteriyor.

Bu yazıda modelleri tanımladık ve linearizability'nin availability ile gerilimini haritada gördük. Bir sonraki yazıda bu gerilimin en ünlü ve en yanlış anlaşılan ifadesine bakıyoruz: CAP teoreminin tam olarak ne söylediği, "3'ten 2'sini seç" özetinin neden yanlış olduğu ve partition yokken bile var olan latency ile consistency arasındaki seçimi anlatan PACELC (if Partition: Availability or Consistency, Else: Latency or Consistency).