TLA+ ve biçimsel yöntemler: Kodu yazmadan önce tasarımı test etmek

Kodu değil, tasarımı kontrol etmek

Hillel Wayne, biçimsel yöntemler (formal methods) üzerine danışmanlık yapan bir eğitmen ve yazar. TLA+ için ücretsiz rehber learntla.com’u o yazdı. The Pragmatic Engineer’daki uzun söyleşinin en somut kısmı, bu yöntemlerin gerçekte ne işe yaradığı.

“Biçimsel” denince akla genelde kodun doğruluğunu matematikle kanıtlamak gelir. Bu mümkün ama pahalı. Daha pratik bir yol da var: biçimsel spesifikasyon. Burada kodu değil, sistemin tasarımını kesin bir dille yazıyorsun. Sonra bir araç, tasarımın kurallarını bozan bir senaryo arıyor.

TLA+ bunun en bilinen dili. Leslie Lamport geliştirdi, özellikle eşzamanlı (concurrent) ve dağıtık sistemler için. Sistemi bir durum makinesi gibi tanımlıyorsun: Başlangıç nasıl, her adımda ne değişebilir, hangi kural asla bozulmamalı. Model denetleyici TLC, ulaşılabilen bütün durumları geziyor. Kuralı bozan bir durum bulursa oraya giden adımları sana gösteriyor. Bir test tek bir yolu dener, TLC modelin sınırları içinde hepsini.

Örnek: Aynı anda iki havale

Bir havale servisi düşün. Kural: Hiçbir hesap eksiye düşmesin. Havale önce bakiyeye bakıyor, sonra parayı çekiyor. Ayşe’nin 100 lirası var ve aynı anda iki ayrı 70 liralık havale başlatıyor. İki işlem de bakiyeye bakıyor: 100 lira, yeterli. Sonra ikisi de çekiyor. Ayşe -40’ta.

Bu klasik bir yarış durumu (race condition). Testte nadiren çıkar, çünkü zamanlamanın tam tutması gerekir. TLC ise adımların bütün sıralamalarını denediği için hemen bulur. Learn TLA+’nın giriş bölümü de benzer bir havale örneğiyle başlıyor. Söyleşide Wayne bunu geri bildirim hızıyla anlatıyor: Kodundaki bir yarış durumu aylar sonra çıkabilir, hatta hiç çıkmayabilir. Model ise araç çalışır çalışmaz gösterir.

Dağıtık sistemler bunun büyük hâli. Mesajlar gecikiyor, kayboluyor, sırası değişiyor. Makineler yarı yolda çöküp geri geliyor. Olası sıralamaların sayısı kafada tutulamayacak kadar çok.

AWS’nin deneyimi

Amazon mühendislerinin 2015’te Communications of the ACM’de yayımladığı makale bu alanın en çok anılan örneği. AWS 2011’den beri TLA+ kullanıyor. Makaleye göre S3, DynamoDB ve EBS dahil 10 büyük sistemde ya ciddi hatalar buldu ya da performans iyileştirmelerini güvenle yapmayı sağladı. DynamoDB’nin çoğaltma (replication) tasarımındaki bir hata, belirli bir çökme ve kurtarma sırasında veri kaybına yol açabiliyordu. Hatayı gösteren en kısa senaryo 35 adımdı. Tasarım incelemelerinden, kod incelemelerinden ve kapsamlı testlerden geçmişti. Mühendisler TLA+’yı sıfırdan 2–3 haftada öğrenip işe yarar sonuç almış.

Neye yarar, neye yaramaz?

TLA+ tasarımı kontrol eder, kodu değil. Makaledeki en sık soru da bu: Kod, doğrulanan tasarıma uyuyor mu? Cevapları dürüst: Bilmiyoruz. Ama tasarım bozuksa kod da neredeyse kesin bozuktur. Makale bir sınır daha sayıyor: Mantık hatası olmadan çöken sistemler. Örneğin yavaşlayan sunucuya istemcilerin tekrar tekrar istek atıp yükü artırması.

Söyleşide Wayne’in tavsiyesi ölçülü: Çoğu mühendis için biçimsel yöntemler, nadir durumlar için fazladan emek. Çoğu kişi özellik tabanlı testi (property-based testing) öğrenip orada durabilir. Tek tek örnek yazmak yerine “çıktı hep sıralı olmalı” gibi bir kural yazıyorsun, araç da binlerce rastgele girdiyle onu bozmaya çalışıyor.

Yapay zekâ bunu yaygınlaştıracak mı?

Bölümün çıkış sorusu bu: Kodu makineler yazınca doğruluğu matematikle göstermek zorunlu hâle gelir mi? Söyleşide Wayne’in cevabı: Ana akım olmayacak, ama kullanım artacak. Sektördeki payı binde birden binde üçe çıksa bile bunu büyük bir gelişme sayıyor. Bir gözlemi de var: Yapay zekâyla spesifikasyon üretmeyi başaranlar genelde zaten bu işin uzmanları.

Matematikte de tablo benzer. Lean, yapay zekânın kanıtlarını kontrol edebiliyor ama yalnızca senin yazdığın ifadeyi (yapay zekâ ve matematik yazısı). TLA+ için de aynısı geçerli: Yanlış kuralı yazarsan TLC sana boş bir “hata yok” verir. Ajan çağında darboğazın doğrulamaya kaydığını Charity Majors söyleşisinde de görmüştük.

Düşün

• Sistemindeki “bu asla olmamalı” kurallarını yazsan kaç tane çıkar? Hangisini bugün hiçbir test kontrol etmiyor?
• Kodunda “önce kontrol et, sonra yap” adımları arasına başka bir işlem girebilir mi?

Kendi cümlelerimizle yazılmış bir özettir, çeviri değildir. Tüm kaynaklar yukarıda.