Concurrency Modelleri ve Concurrent Kodu Doğrulamak: Shared Memory, Actor, CSP ve Model Checking

Sürüm notu: Bu yazıdaki kodlar .NET 10 (C# 14) ile derlenip denenmiştir; testler xUnit v3 4.0.3 ile yazıldı. Model checking örnekleri tla2tools.jar 1.7.4 ve Java 21 ile çalıştırıldı. Çıktılar ARM64 (Arm'ın 64-bit işlemci mimarisi) üzerinde alınmıştır.

Önce Tahmin Et

Sitedeki serilerin ortak örnek uygulaması Bookstore'da (bir online kitapçı) Dune'dan 1.000 adet stok var ve sekiz istemci 500'er sipariş gönderiyor. Rezervasyonu stoğa tek bir thread'in dokunduğu bir actor yapıyor: hiçbir lock yok, stok alanına yalnız actor'ün kendi döngüsü erişiyor. İstemciler önce "stok kaç?" diye soruyor, cevap sıfırdan büyükse "stoğu şu değere ayarla" mesajı gönderiyor. Actor'ün içinde data race yok. Bu durumda kaç kitap satılır?

İkinci soru: dört thread'in her biri 10 adımlık bir iş yapıyorsa, ilk yazıdaki formülle kaç farklı interleaving vardır? Bir stress test bunların ne kadarını dener? Serinin önceki yedi yazısında shared memory modelinin içinde kaldık. Bu son yazıda iki şeye bakıyoruz: paylaşmadan haberleşen modeller ve concurrent kodun doğruluğunu testin ötesinde göstermek.

Modeller ve Shared Memory

Concurrency modeli, eşzamanlı çalışan parçaların durumu kimin tuttuğunu ve birbirleriyle nasıl haberleştiğini belirleyen çerçevedir. Aynı Bookstore problemini (sınırlı stoktan rezervasyon) dört farklı şekilde kurabilirsin:

İlk satır serinin şimdiye kadarki konusuydu. Laboratuvar projesine eklediğim Models/ klasöründe aynı rezervasyon üç modelle yazıldı. Shared memory sürümü kısa:

// Model 1: shared memory + lock. Kontrol ve eylem kilit içinde tek adım
public sealed class LockedOrderDesk(int stock) : IOrderDesk
{
    private readonly Lock _gate = new();
    private int _stock = stock;

    public Task<bool> ReserveAsync(int quantity)
    {
        lock (_gate)
        {
            if (_stock < quantity)
                return Task.FromResult(false);
            _stock -= quantity;
            return Task.FromResult(true);
        }
    }
}

Bu modelin gücü doğrudanlığı; zayıflığı ise doğruluğun her erişimde disipline bağlı olması. Stoğa dokunan her yeni method doğru kilidi almak zorunda; ikinci yazıdaki race'ler, dördüncü yazıdaki deadlock'lar ve beşinci ile altıncı yazılardaki memory model incelikleri bu modelin bedeli.

Actor Modeli

Actor modeli Carl Hewitt, Peter Bishop ve Richard Steiger'in 1973'teki çalışmasından gelir. Fikir şu: her actor kendi durumunu tutar ve kimseyle paylaşmaz. Dışarıdan yalnız mesaj alır; mesajlar actor'ün mailbox'ında birikir ve actor onları birer birer işler. Bir mesajı işlerken başka actor'lere mesaj gönderebilir, yeni actor'ler oluşturabilir ve bir sonraki mesaj için kendi durumunu değiştirebilir.

// Model 2: actor. Stoğa yalnız actor'ün kendi döngüsü dokunur; çağıranlar mailbox'a mesaj gönderir
private async Task LoopAsync()
{
    // her seferinde tek mesaj: bir handler çalışırken _stock'a başka hiçbir şey dokunamaz
    await foreach (Message message in _mailbox.Reader.ReadAllAsync())
    {
        switch (message)
        {
            case ReserveMessage r when _stock >= r.Quantity:
                _stock -= r.Quantity;
                r.Reply.SetResult(true);
                break;
            case ReserveMessage r:
                r.Reply.SetResult(false);
                break;
            case GetStockMessage g:
                g.Reply.SetResult(_stock);
                break;
            case SetStockMessage s:
                _stock = s.Value;
                break;
        }
    }
}

Mailbox burada tek okuyuculu bir Channel<T>; cevaplar TaskCompletionSource ile dönüyor. _stock alanında hiç kilit yok, çünkü ona yalnız bu döngü dokunuyor. Gerçek projede bu altyapıyı kendin yazmazsın. Microsoft Orleans, actor'leri cluster'a dağıtılmış "grain"ler olarak sunar; Akka.NET ise Scala dünyasındaki Akka'nın .NET karşılığıdır.

Actor modeli data race'i ortadan kaldırır ama race condition'ı kaldırmaz. Orleans dokümanı iki örnek veriyor. Varsayılan modda bir grain, bir isteği sonuna kadar işlemeden yenisine başlamaz; bu yüzden birbirini aynı anda çağıran iki grain, birbirinin cevabını bekleyerek takılabilir ve çağrılar timeout ile biter. Dördüncü yazıdaki circular wait, bu kez mesajlarla. Grain'i reentrant işaretlersen bu kilitlenme kalkar ama bir isteğin await ettiği noktada başka bir isteğin adımları araya girebilir; yani check-then-act, await'in iki yanına bölünürse yine bozulur.

CSP: Channel ile Haberleşen Süreçler

CSP, yani kendi içinde sıralı çalışan ve birbirleriyle yalnız channel üzerinden haberleşen süreçler, Tony Hoare'un 1978'deki makalesinden gelir. Actor'e benzer ama vurgu farklı: actor'lerin bir kimliği vardır ve mesaj o kimliğe gönderilir; CSP'de süreçler adsızdır, haberleşme isimli channel'lar üzerinden olur. Go'nun goroutine ve channel'ları bu fikrin en bilinen uygulaması; ilerideki Go ile Backend serisinde ayrıntısıyla görülecek. .NET'teki karşılığı System.Threading.Channels; kullanımını C# Asenkron Programlama serisinin Channels yazısında anlatmıştık.

// Model 3: CSP. Channel'larla bağlı adsız aşamalar; stoğun tek sahibi reserve aşaması
private async Task ValidateAsync()
{
    await foreach (OrderRequest request in _incoming.Reader.ReadAllAsync())
    {
        if (request.Quantity is < 1 or > 20)
            request.Reply.SetResult(false);
        else
            await _validated.Writer.WriteAsync(request);
    }
}

private async Task ReserveStageAsync(int stock)
{
    await foreach (OrderRequest request in _validated.Reader.ReadAllAsync())
    {
        bool ok = stock >= request.Quantity;
        if (ok)
            stock -= request.Quantity;
        request.Reply.SetResult(ok);
    }
}

Doğrulama aşaması stoğu hiç görmüyor; stok, reserve aşamasının local değişkeni. Bounded channel'lar sayesinde bir aşama yavaşlarsa önceki aşama beklemeye başlar, yani backpressure modelin kendisinden gelir. Üç modeli aynı yükle çalıştırdım: 1.000 stok, 8 istemci, toplam 4.000 tek adetlik sipariş:

dotnet run -c Release --project src/Bookstore.ConcurrencyLab -- models

shared memory + lock  stock=1,000 orders=4,000 accepted=1,000 (4 ms)
actor (mailbox)       stock=1,000 orders=4,000 accepted=1,000 (4 ms)
CSP pipeline          stock=1,000 orders=4,000 accepted=1,000 (4 ms)

Üçü de tam 1.000 sipariş kabul etti. Fark doğrulukta değil, doğruluğun nereden geldiğinde: ilkinde her erişimdeki disiplinden, diğer ikisinde durumun tek bir sahibi olmasından.

Immutable Veri, Event Loop ve STM

Paylaşmanın bir başka yolu, paylaşılan şeyi değiştirilemez yapmak. Immutable bir fiyat listesini istediğin kadar thread okuyabilir; güncelleme yeni bir liste oluşturup referansı yayınlamaktır. Altıncı yazıda gördüğümüz gibi .NET'te referans yayınlamak güvenli ve ImmutableDictionary gibi tipler bu modeli doğrudan destekler. Yazmalar seyrek, okumalar sıksa en ucuz model genellikle budur.

Single-threaded event loop ise concurrency'yi tek bir thread'de yaşatır: Node.js ve tarayıcıdaki JavaScript her callback'i sonuna kadar çalıştırır, sonra queue'daki bir sonrakine geçer. Data race yoktur, ama await noktaları arasında durum yine değişebilir; JavaScript İleri serisinin event loop yazısında bu sırayı ayrıntılı görmüştük.

STM (Software Transactional Memory; bellek erişimlerini veritabanı transaction'ı gibi gruplayan model), paylaşılan bellekteki değişiklikleri transaction'lar içinde yapıp çakışmada otomatik retry'ı önerir. Haskell'de GHC (Glasgow Haskell Compiler; Haskell'in en yaygın derleyicisi) ile ve Clojure'da yerleşik olarak destekleniyor; .NET'te ise Microsoft'un deneysel STM.NET çalışması ürüne dönüşmedi.

Neden Test Yetmez

Baştaki ilk sorunun cevabı:

dotnet run -c Release --project src/Bookstore.ConcurrencyLab -- actor-protocol

run 1: stock=1,000 sold with GetStock+SetStock=4,000 stock left=425
run 2: stock=1,000 sold with GetStock+SetStock=4,000 stock left=392
run 3: stock=1,000 sold with GetStock+SetStock=4,000 stock left=457

1.000 adet stoktan 4.000 kitap satıldı ve sonunda stokta hâlâ 400 civarı kitap görünüyor. Actor'ün içinde hiçbir hata yok; her mesaj tek başına doğru işleniyor. Hata protokolde: "oku" ve "yaz" iki ayrı mesaj, ve iki mesaj arasında başka istemcilerin mesajları araya giriyor. Bu, ikinci yazıdaki check-then-act'in mesajlarla yazılmış hâli. Düzeltme, kararı actor'e taşımak: istemci "1 adet rezerve et" der, kontrolü ve azaltmayı actor tek mesajda yapar. Model değiştirmek, düşünmeyi bırakmak anlamına gelmiyor.

Bu tür hataları test neden kaçırır? İlk yazıda iki thread'in üçer adımlık işinin 20 farklı sırayla çalışabileceğini hesaplamıştık. Aynı formülle dört thread'in onar adımlık işi yaklaşık 4,7 × 10^21 farklı interleaving demek. Stress test bunların içinden işletim sisteminin zamanlamasının seçtiği küçük bir örneklemi dener ve yedinci yazıdaki gibi bozuk bir stack'i 20.000 geçmişin yalnız 63'ünde yakalar.

Stress testi daha etkili hâle getirmenin yolları var. Birincisi invariant assertion'ları: "satılan + stok = başlangıç stoğu" gibi bir kuralı kodun içine koyup her işlemden sonra kontrol etmek, hatayı sonucunda değil oluştuğu anda yakalar. İkincisi deterministic scheduling: test sırasında thread'lerin ve task'ların sırasını bir test aracının kontrol etmesi, farklı sıraları sistematik olarak denemesi ve hata bulunca aynı sırayı tekrar oynatabilmesi. .NET'te bu yaklaşımın bilinen aracı Microsoft Coyote. GitHub'daki durumunu kontrol ettim: depo aktif, Kasım 2026'da .NET 10 ve .NET 11 desteği eklendi; ama NuGet'teki son sürüm Mart 2024'teki 1.7.11 ve en yeni hedefi net8.0. Bu yüzden bu yazıda Coyote'yi çalıştırmadım; .NET 10 projesinde kullanmadan önce yeni bir sürümün yayınlanıp yayınlanmadığına bak.

Model Checking: TLA+ ile Stok Rezervasyonu

Model checking, sistemin küçük bir modelini yazıp bütün olası davranışlarını bir aracın denemesidir. Leslie Lamport'un TLA (Temporal Logic of Actions; sistemin durumlarını ve adımlarını mantık formülleriyle tanımlayan dil) üzerine kurduğu TLA+ bu iş için en yaygın dillerden biri; spec'ler TLC (TLA+ ile gelen model checker) ile çalıştırılır, ben 2.19 sürümünü kullandım. İkinci yazıdaki if (stock > 0) stock-- kodunun modeli, projede yeni açtığım specs/ klasöründe:

------------------------- MODULE StockReservation -------------------------
EXTENDS Integers

CONSTANTS Buyers, InitialStock

VARIABLES stock, sold, pc

vars == <<stock, sold, pc>>

Init ==
    /\ stock = InitialStock
    /\ sold = 0
    /\ pc = [b \in Buyers |-> "check"]

\* if (stock > 0) ...
Check(b) ==
    /\ pc[b] = "check"
    /\ pc' = [pc EXCEPT ![b] = IF stock > 0 THEN "reserve" ELSE "done"]
    /\ UNCHANGED <<stock, sold>>

\* ... stock--;
Reserve(b) ==
    /\ pc[b] = "reserve"
    /\ stock' = stock - 1
    /\ sold' = sold + 1
    /\ pc' = [pc EXCEPT ![b] = "done"]

Finished ==
    /\ \A b \in Buyers : pc[b] = "done"
    /\ UNCHANGED vars

Next == (\E b \in Buyers : Check(b) \/ Reserve(b)) \/ Finished

Spec == Init /\ [][Next]_vars

NoOversell == sold <= InitialStock
=============================================================================

Okuması şöyle: pc her alıcının kodda nerede olduğunu tutuyor. Check adımı yalnız stoğa bakıp alıcıyı "reserve" ya da "done" durumuna geçiriyor; Reserve adımı stoğu azaltıyor. Next, her adımda herhangi bir alıcının herhangi bir adımı atabileceğini söylüyor; interleaving'leri biz yazmıyoruz, TLC hepsini kendisi üretiyor. NoOversell her durumda doğru olması gereken invariant. Aynı adlı .cfg dosyası iki alıcı ("ada", "alan") ve 1 adet stok veriyor. tla2tools.jar'ı TLA+ deposunun GitHub release sayfasından (v1.7.4) indirip specs/ klasörüne koyduktan sonra komut her işletim sisteminde aynı:

java -XX:+UseParallelGC -cp tla2tools.jar tlc2.TLC StockReservation

Error: Invariant NoOversell is violated.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ sold = 0
/\ pc = [ada |-> "check", alan |-> "check"]
/\ stock = 1

State 2: <Check line 17, col 5 to line 19, col 32 of module StockReservation>
/\ sold = 0
/\ pc = [ada |-> "reserve", alan |-> "check"]
/\ stock = 1

State 3: <Check line 17, col 5 to line 19, col 32 of module StockReservation>
/\ sold = 0
/\ pc = [ada |-> "reserve", alan |-> "reserve"]
/\ stock = 1

State 4: <Reserve line 23, col 5 to line 26, col 38 of module StockReservation>
/\ sold = 1
/\ pc = [ada |-> "done", alan |-> "reserve"]
/\ stock = 0

State 5: <Reserve line 23, col 5 to line 26, col 38 of module StockReservation>
/\ sold = 2
/\ pc = [ada |-> "done", alan |-> "done"]
/\ stock = -1

13 states generated, 10 distinct states found, 1 states left on queue.

Başlıktaki sürüm ve ortam satırlarını çıkardım; gerisi TLC'nin çıktısı. TLC, invariant'ı bozan en kısa yolu adım adım veriyor: iki alıcı da stoğu 1 görüyor, ikisi de azaltıyor, stok -1'e düşüyor ve 1 kitaplık stoktan 2 kitap satılıyor. İkinci yazıda 2.000 turun 372'sinde gördüğümüz fazla satışın kâğıt üzerindeki kanıtı bu. Kontrol ve azaltmayı tek atomik adımda yapan sürüm (StockReservationLocked, kilit içindeki kodun modeli) için çıktı farklı:

java -XX:+UseParallelGC -cp tla2tools.jar tlc2.TLC StockReservationLocked

Model checking completed. No error has been found.
  Estimates of the probability that TLC did not check all reachable states
  because two distinct states had the same fingerprint:
  calculated (optimistic):  val = 4.3E-19
6 states generated, 4 distinct states found, 0 states left on queue.

"Hata bulunamadı" burada "denediklerimde görmedim" değil, "bu modelin bütün erişilebilir durumlarına baktım" demek. Üç alıcı ve 2 adet stokla (ThreeBuyers.cfg) aynı sonuç 8 farklı durumla geliyor; bozuk sürüm ise 7 durumluk bir karşı örnekle yine yakalanıyor. TLC interleaving'leri tek tek denemiyor, aynı duruma çıkan farklı yolları birleştiriyor; bu yüzden durum sayısı interleaving sayısından çok daha yavaş büyür.

Modelin sınırını da unutma: TLC, C# kodunu değil senin yazdığın modeli kontrol eder. Model koddan farklıysa (örneğin stock--'ı atomik varsaydıysan) kanıt da o farka kadar geçerlidir. Bu yüzden model checking en çok protokoller ve algoritmalar için kullanılır: kilit sırası, iki aşamalı onay, cache invalidation, bir dağıtık sistemdeki mesaj akışı.

Karar Rehberi: Hangi Problemde Hangi Model

Serinin sonunda vardığım kurallar şunlar:

• Önce paylaşmamayı dene: her isteğin kendi verisi, her thread'in kendi sonucu, en sonda birleştirme. Paylaşılmayan durum için bu serideki hiçbir kural gerekmez.
• Okuma çok, yazma azsa immutable veri ve referans yayınlama.
• Birkaç alanı birlikte koruyan kısa critical section'lar için lock; tek bir sayaç ya da bayrak için Interlocked.
• Bir varlığın (bir sepet, bir stok kalemi, bir kurumsal sipariş) uzun ömürlü durumu ve ona gelen sıralı istekler varsa actor; özellikle durum birden çok sunucuya dağılacaksa Orleans gibi bir altyapı.
• Veri bir aşamadan diğerine akıyorsa (sipariş doğrulama, rezervasyon, kargo etiketi) CSP tarzı bir channel pipeline'ı.
• Protokol karmaşıksa ve hatanın maliyeti yüksekse, kodu yazmadan önce TLA+ ile küçük bir model.

Üretimde Dikkat

Modeli ekipçe seç ve sınırlarını yaz. Aynı serviste bir kısmı kilitle, bir kısmı actor ile, bir kısmı kilitsiz yazılmış durum, her modelin kurallarının başka bir modelin içinde ihlal edilmesine yol açar. Örneğin bir actor'ün içinden paylaşılan bir dictionary'ye dokunmak, actor modelinin bütün garantisini siler.

Mesaj protokolünü API gibi tasarla. Actor ve channel'larda race, mesajların sırasında ve parçalanmasında saklanır. "Oku, sonra yaz" yerine "niyetini söyle" mesajları (rezerve et, iptal et) kullan; kararı durumun sahibine bırak. Kullandığın altyapının mesaj sırası için neyi garanti ettiğini dokümanından kontrol et; farklı istemcilerden gelen mesajların birbirine göre sırası hakkında hiçbir varsayım yapma.

Doğrulamayı katmanlara böl. Algoritmanın kendisi için model checking ya da kâğıt üzerinde linearization point argümanı; implementasyon için invariant assertion'larla stress test; dağıtık davranış için Distributed Systems Temelleri serisinde anlattığımız fencing token ve idempotency gibi kalıplar. Hiçbiri tek başına yetmez.

Sık Düşülen Tuzaklar

Actor modelinde race olmayacağını sanmak. Deneyde actor'ün içi hatasızdı ve yine 1.000 stoktan 4.000 kitap satıldı. Data race yok, race condition var.

Reentrancy'yi hafife almak. Bir actor'ü ya da grain'i reentrant yapmak deadlock'u çözer ama her await'i bir interleaving noktasına çevirir. Check-then-act'in iki adımı arasında await varsa, kilitsiz koddaki aynı hatayı yaşarsın.

Model checker'ı bütün sisteme uygulamaya çalışmak. TLA+ ile bir mikroservis mimarisini uçtan uca modellemeye çalışan ekip, durum patlamasına ve hiç bitmeyen bir spec'e ulaşır. Modeli en riskli protokolle sınırla, sabitleri küçük tut (iki alıcı, bir kitap) ve büyütmeyi TLC hızlı kaldıkça yap.

Yeşil testi kanıt saymak. 4,7 × 10^21 interleaving'in birkaç bin tanesini denemek, kalanlar hakkında bir şey söylemez. Test, "bu hata yok" demez; yalnız "bu çalıştırmalarda görmedim" der.

Küçük Bir Deneme

★☆☆ actor-protocol komutundaki istemciyi düzelt: GetStockAsync ve SetStock yerine ReserveAsync(1) kullan ve satılan kitap sayısının tam 1.000 olduğunu doğrula. Düzeltmenin neden actor'ün içine kod eklemeden çalıştığını açıkla.

★★☆ StockReservation.tla'ya bir Cancel(b) adımı ekle: rezervasyon yapmış bir alıcı iptal edip stoğu geri artırabilsin. NoOversell invariant'ı bozuk sürümde yine yakalanıyor mu, kilitli sürümde hâlâ geçiyor mu? sold değişkeninin anlamını iptalle birlikte nasıl güncellemen gerektiğini tartış.

★★★ Dördüncü yazıdaki iki depolu stok transferini TLA+ ile modelle: her transfer önce kaynak, sonra hedef deponun kilidini alsın. Deadlock'u TLC'nin varsayılan deadlock kontrolüyle bulan bir spec yaz, sonra kilitleri Id sırasıyla alan sürümün deadlock'suz olduğunu göster.

Bu yazıyla Concurrency Teorisi serisi bitiyor. İlk yazıda interleaving ve Amdahl ile başladık, race ve data race ayrımını yaptık, mutual exclusion'ın ve deadlock'un teorisine, donanımın ve .NET'in memory model'ine, kilitsiz algoritmalara ve son olarak modellere ve doğrulamaya baktık. Aynı soruların birden çok makineye yayıldığı hâli, yani mesaj kaybı, saat farkı ve ağ bölünmesi altında tutarlılık, Distributed Systems Temelleri serisinin konusu; bu serideki happens-before, linearizability ve deadlock kavramlarını orada dağıtık bağlamda yeniden göreceksin.