Amazon Web Services'in sistem doğruluğu uygulama örnekleri
(cacm.acm.org)- Amazon Web Services (AWS), hizmetlerinde doğruluğu temel bir değer olarak konumlandırıyor ve çeşitli biçimsel yöntemleri geliştirme sürecine entegre ediyor
- TLA+ ve P dili gibi biçimsel belirtim araçları sayesinde ince hatalar erken aşamada bulunabiliyor ve iddialı optimizasyonlarda da güvenilirlik korunabiliyor
- AWS, hafif biçimsel yöntemler kapsamında özellik tabanlı test, deterministik simülasyon ve sürekli fuzzing'i de geniş ölçekte kullanıyor
- Fault Injection Service gibi hata enjeksiyonu araçları ile arıza anlarını da kapsayan güvenilirlik doğrulamasını otomatikleştiriyor
- Eğitsel bariyerler ve araç karmaşıklığı sürse de, yapay zeka ve otomasyon araçlarının yaygınlaşmasının benimsenmeyi artırması bekleniyor
AWS'nin sistem doğruluğunu sağlama stratejisi
Amazon Web Services (AWS), müşterilerin tamamen güvenebileceği yüksek güvenilirlikli hizmetler sunmayı hedefliyor.
Bunun için güvenlik, dayanıklılık, bütünlük ve erişilebilirlik standartlarını korumaya çalışıyor ve bunun merkezine sistem doğruluğu kavramını yerleştiriyor.
2015'te Communications of the ACM'de tanıtılan AWS'nin biçimsel yöntem uygulama örneklerinden bu yana, bu yaklaşım temel hizmetlerin başarılı işletiminde önemli bir rol oynuyor.
Merkezde, Leslie Lamport tarafından geliştirilen biçimsel belirtim dili TLA+ bulunuyor.
AWS'nin TLA+ kullanma deneyimi, geliştirme sürecinin erken aşamalarında klasik testlerle yakalanamayan ince hataların saptanmasını sağladı.
Ayrıca cesur performans optimizasyonları yapılırken de biçimsel doğrulama sayesinde kararlılık ve güvenilirlik korunabildi.
15 yıl önce AWS, derleme anı birim testleri ve sınırlı entegrasyon testleri gibi temel bir düzeydeydi; sonrasında ise biçimsel ve yarı biçimsel yaklaşımları kapsamlı biçimde benimsedi.
Bu değişim yalnızca doğruluğa değil, yüksek ve düşük seviye optimizasyonların doğrulanmasına, geliştirme hızının artmasına ve maliyetlerin düşmesine de katkı sağladı.
AWS'de yalnızca klasik biçimsel ispat ve model denetimi değil, özellik tabanlı test, fuzzing ve çalışma zamanı izleme gibi teknikler de biçimsel yöntemler kapsamına alınıyor.
P programlama dilinin ortaya çıkışı
İlk dönemde TLA+ güçlü bir soyut ifade aracı olma avantajına sahipti, ancak çok sayıda geliştirici için matematiksel gösterim kullanımı ciddi bir giriş engeli oluşturuyordu.
Bu nedenle AWS, geliştiricilere daha tanıdık gelen durum makinesi tabanlı bir yaklaşım sunan P dilini benimsedi.
P dili, dağıtık sistemlerin tasarımı ve analizi için durum makinesi modelleme yaklaşımı sunuyor.
Mikroservis tabanlı SOA mimarisi kullanan Amazon geliştiricileri için bu kavram oldukça tanıdık.
2019'dan beri AWS içinde geliştiriliyor ve stratejik bir açık kaynak proje olarak yönetiliyor.
Amazon S3, EBS, DynamoDB, Aurora, EC2 ve IoT gibi başlıca hizmet ekipleri, sistem tasarımının doğruluğunu doğrulamak için P'den yararlanıyor.
S3, güçlü read-after-write tutarlılığına geçirilirken protokol P ile modellenip doğrulandı; böylece hatalar tasarımın erken safhasında temizlendi ve optimizasyonlar da güvenli biçimde yansıtıldı.
2023'te AWS P ekibi, dağıtık sistemlerin doğruluğunu hem testte hem de gerçek üretim ortamında doğrulayabilmek için PObserve aracını geliştirdi.
PObserve, yürütme günlüklerini çıkararak belirtime göre doğru davranışın gerçekleşip gerçekleşmediğini sonradan doğrulayabiliyor ve tasarım aşamasındaki belirtim ile gerçek kod uygulaması arasında etkili bir bağ kuruyor.
Hafif biçimsel yöntemlerin genişlemesi
Özellik tabanlı test
En temsilî hafif biçimsel tekniklerden biri özellik tabanlı testtir.
Örneğin S3'ün ShardStore geliştirme ekibi, geliştirme döngüsünün tamamında özellik tabanlı test, kod kapsamı tabanlı fuzzing, hata enjeksiyonu ve karşı örnek küçültme gibi yöntemleri birlikte kullanıyor.
Bu yaklaşım, geliştiricilerin doğrudan yazdığı doğruluk belirtimleriyle bağlantılı çalışıyor ve sorunların debug edilme verimliliğini de ciddi biçimde artırıyor.
Deterministik simülasyon
Deterministik simülasyon testleri, dağıtık sistemi tek iş parçacıklı bir simülatörde çalıştırarak rastlantısal tüm unsurların (zamanlama, süreleme, mesaj sırası vb.) kontrol edilmesini sağlıyor.
Belirli hata ve başarı senaryolarının test edilmesi, hataya yol açan sıralamanın ayarlanması ve fuzzing'in genişletilmesi gibi çeşitli şekillerde uygulanabiliyor.
Bu sayede sistemin gecikme ve hata gibi davranışlarının doğrulaması derleme aşamasında daha erken yapılabiliyor ve test kapsamı genişliyor.
AWS, bu derleme zamanı test kodlarını shuttle ve turmoil açık kaynak projeleri olarak yayımladı.
Sürekli fuzzing
Sürekli fuzzing, özellikle kod kapsamı tabanlı büyük ölçekli girdi üretimi, entegrasyon testi aşamasında sistem doğruluğunu doğrulamak için etkili.
Örneğin Aurora Limitless Database geliştirilirken SQL sorguları ve işlemler fuzz edilerek bölümleme mantığının doğruluğu, çok sayıda rastgele şema, veri kümesi ve sorgu üretilerek doğrulanıyor.
Sonuçlar, non-sharded motorun davranışıyla veya SQLancer gibi yöntemlerle karşılaştırılıyor.
Fuzzing ile hata enjeksiyonunun birleşimi, veritabanlarının temel özellikleri olan atomiklik, tutarlılık ve izolasyonun doğrulanmasını sağlıyor.
Otomatik üretilen işlemler ve izolasyon gibi bazı özellikler ise yürütme geçmişi tabanlı sonradan doğrulama ile güvence altına alınıyor.
Fault Injection Service ile arıza enjeksiyonu
2021'de AWS, Fault Injection Service (FIS) hizmetini kullanıma sundu; böylece müşteriler API hataları, I/O kesintileri ve instance arızaları gibi çeşitli kusur senaryolarını gerçek ya da test ortamlarında hızlıca deneyebiliyor.
Bunun sonucunda mimarinin erişilebilirliğini sağlama ve arıza dayanıklılığını denetleme, hata senaryolarındaki yüksek bug yoğunluğunu azaltma ve olası kritik sorunları önceden keşfetme gibi faydalar elde ediliyor.
FIS, yalnızca AWS müşterileri tarafından değil, Amazon içinde de geniş ölçekte kullanılıyor; örneğin yalnızca Prime Day hazırlık sürecinde 733 deney gerçekleştirildi.
Hata enjeksiyonu, biçimsel belirtimlerle birleştirildiğinde daha etkili oluyor.
Beklenen davranış biçimsel belirtim olarak yazıldıktan sonra, gerçek kusur tetikleme sonuçları bununla karşılaştırılıyor; böylece yalnızca log ve metrik incelemeye göre daha fazla hata yakalanabiliyor.
Metakararlılık ve sistemin ortaya çıkan davranışları
Dağıtık sistemlerde aşırı yük veya cache tükenmesi gibi nedenlerle, sistemin kendi kendine toparlanamadığı anormal durumlara, yani metakararlı hâllere düşme örnekleri artıyor.
Bu durumda yalnızca yükün azaltılmasıyla sistem normale dönmüyor ve müdahalesi sıradan hata senaryolarından daha zor oluyor.
Çoğu yeniden deneme-zaman aşımı mantığı da bu tür olguların nedenlerinden biri hâline geliyor.
Mevcut biçimsel belirtimler çoğunlukla güvenlik ve ilerleme özelliklerine odaklansa da, metakararlılık bunların dışındaki çeşitli ortaya çıkan davranışların da hesaba katılmasını gerektiriyor.
AWS, TLA+ ve P gibi belirtim modellerine dayanarak ayrık olay simülasyonu yürütüyor; performans SLA'sının karşılanma olasılığı ve gecikme dağılımlarının hesaplanması gibi olasılıksal özellikleri de sistematik biçimde analiz ediyor.
Biçimsel ispatın gerekliliği
Bazı güvenlik sınırlarında (yetkilendirme, sanallaştırma vb.) basit testlerin ötesinde, matematiksel düzeyde ispat zorunlu oluyor.
Örneğin AWS'nin 2023'te devreye aldığı Cedar yetki politikası dili, Dafny tabanıyla otomatik ispat ve biçimsel doğrulamaya uygun biçimde tasarlandı; açık kod ve düzeltme süreçleri sayesinde kullanıcılar da bunu doğrudan doğrulayabiliyor.
Ayrıca Firecracker VMM'in güvenlik sınırına ilişkin temel özellikler, Kani gibi Rust kod analiz araçları ile ispatlanıyor.
Bu şekilde biçimsel modeller ve belirtimler; tasarım, uygulama, işletim ve ispat gibi farklı aşamalarda geniş biçimde kullanılarak yazılım doğruluğunu güvence altına almak ve şirket ile müşteri değerini büyütmek için değerlendiriliyor.
Doğruluğun ötesindeki ek etkiler
Biçimsel yöntemler, hem güvenilirliğin hem de performans iyileştirmelerinin merkezinde önemli bir rol oynuyor.
Örneğin Aurora'nın commit protokolü P ve TLA+ ile doğrulanarak ağ round-trip sayısı azaltılırken güvenlik de korunabildi.
RSA şifreleme algoritmasının ARM Graviton 2 için optimize edilmesi sırasında, HOL Light üzerinde dönüşümlerin matematiksel doğruluğu ispatlandı ve bunun sonucunda performans ile altyapı maliyetinde aynı anda iyileşme elde edildi.
Geleceğin zorlukları ve fırsatları
AWS son 15 yılda biçimsel ve yarı biçimsel yöntemlerin endüstriyel kullanımını büyük ölçüde genişletmiş olsa da, öğrenme eğrisi, uzman gereksinimi ve araçların akademik karakteri gibi somut benimseme engelleri hâlâ sürüyor.
Özellik tabanlı test ve deterministik simülasyon gibi yöntemler de birçok geliştirici için hâlâ yabancı.
Eğitsel giriş engeli lisans düzeyinden itibaren bulunduğu için, araç ve yöntemlerin yaygınlaşması ile pratikte uygulanması yavaş ilerliyor.
Metakararlılık gibi büyük ölçekli sistemlerin ortaya çıkan özellikleri de henüz araştırmanın erken aşamasında.
Gelecekte yapay zeka / büyük dil modellerinin, biçimsel model ve belirtim yazımını destekleyerek uygulayıcıların erişilebilirliğini kısa sürede çarpıcı biçimde artırması bekleniyor.
Sonuç
Sağlam ve güvenli yazılım geliştirmek için sistem doğruluğunu sağlamaya yönelik çeşitli araçlara ihtiyaç var.
AWS, standart test tekniklerinin ötesine geçerek model checking, fuzzing, özellik tabanlı test, arıza enjeksiyon testi, deterministik/olay tabanlı simülasyon ve yürütme geçmişi doğrulaması gibi yöntemleri kapsamlı biçimde benimsiyor.
Biçimsel belirtimler ve yöntemler, AWS'nin geliştirme sürecinde önemli bir test oracle işlevi görüyor ve pratik ile ekonomik etkileri kanıtlandığı için artık yatırım yapılan alanlardan biri olarak konumlanıyor.
1 yorum
Hacker News görüşleri
Deterministik simülasyon testi yaklaşımından söz etmek istiyorum. AWS'de dağıtık sistemler tek iş parçacıklı bir simülatörde çalıştırılırken iş parçacığı zamanlaması, zamanlama farkları, mesaj iletim sırası gibi tüm deterministik olmayan unsurlar kontrol ediliyor. Ardından belirli başarısızlık ya da başarı senaryolarına uygun testler yazılıyor ve sistem içindeki determinizm dışı davranış test çerçevesi tarafından kontrol ediliyor. Geliştirici, geçmişte hataya yol açmış belirli sıralamaları tanımlayabiliyor. Zamanlayıcı, sıra üzerinde fuzzing yapmaya ya da mümkün olan tüm sıralamaları keşfetmeye kadar genişletilebiliyor. Bunu dilden bağımsız şekilde açık kaynak olarak uygulayan bir kütüphane olup olmadığını merak ediyorum. Fikir, konteyner içinde ağ, depolama vb. şeyleri de test anında "deterministik" hale getiren bir ara katman aracı gerektiği yönünde. antithesis neredeyse tam olarak bunu yapıyor, ancak henüz açık kaynakta görmedim. Testler iyi yazılırsa I/O gibi şeyleri stub'layarak bir ölçüde çözülebilir, ama herkesin testleri iyi yazdığının garantisi yok. Uygulamanın üstünde daha yüksek bir katmanda determinizm sağlamak iyi olurdu diye düşünüyorum. Öte yandan yapay zekanın testte gerçekten parlayabileceğini umuyorum. Prompt (gereksinim)-test uygulaması-yapay zeka-çalışan kod bu üç eksen ideal olarak birbirine oturabilir. Yapay zekanın biçimsel doğrulamayı daha erişilebilir hale getirip yazılım dünyasını daha sıkı hale getirmesini umuyorum
Deterministik simülasyon testinin (DST) yaygınlaşmasının önünde iki zorluk var. Birincisi, geçmişte tüm sistemlerin belirli bir simülasyon çerçevesi üzerine doğrudan kurulması ve başka bağımlılıklarının olmaması gerekiyordu. İkincisi, girdi üretimi ve keşif zayıfsa testler sanki hepsi başarılıymış gibi görünüp gerçekte anlamlı doğrulama yapmıyor. antithesis bu ikisini de çözmeye çalışıyor ama hâlâ çok zor. Determinizmi herhangi bir yazılıma güvenilir biçimde uygulayabilen pek yer yok. Facebook'un Hermit projesi de deterministik Linux userspace ile bunu denemişti ama sonunda durduruldu. Deterministik bilgisayarlar test dışında da çok yararlı bir teknik temel ve bir gün birilerinin bunu açık kaynak olarak yayımlayacağını düşünüyorum
QEMU'yu %100 emülasyon modunda tek iş parçacıklı çalıştırarak deterministik bir makine elde etmenin nispeten kolay olduğunu düşünüyorum. Ama gerçekten istenen şey 'kontrollü' deterministik yürütme ve bu çok daha zor. Birden fazla süreci belirlenmiş bir senaryoya göre çalıştırmak istiyorsanız özellikle CPU ve OS zamanlayıcısı seviyesinde zorluk çok yüksek. Dilden bağımsız bir ortamın kendisini yapmak da zor ve ayrıntıların kurbanı olmak kolay. Ben de birkaç JVM iş parçacığını belirli davranış anlarında lockstep olarak çalıştıran basit bir sistem yapmıştım; I/O ve sistem zamanını stub'lar ve kontrol ile ele alıyordum. Bu sayede asenkron bileşenler arasındaki çeşitli etkileşimleri, I/O arızalarını, yeniden denemeleri vb. test edip production'a gitmeden önce can sıkıcı hataları yakalıyorduk. Ancak bu, tüm sistemi kontrol etmekten ziyade yalnızca belirli senkronizasyon noktalarını basitleştirerek mümkün oluyordu. Senkronizasyon hatalarından kaynaklanan genel veri yarışlarını bu yöntemle yakalamak zor
FoundationDB'nin test yöntemi resmi dokümantasyonu ve YouTube sunum videosu paylaşılıyor
gdb ile hata ayıklanabilen bir dilse https://rr-project.org/ projesini öneririm
Joe Armstrong'un property testing kullanarak Dropbox'ı test ettiği bir sunumu eskiden izlediğimi hatırlıyorum
S3'ün şimdiye kadar gördüğüm en havalı yazılımlardan biri olduğunu düşünüyorum. Birkaç yıl önce tüm S3 sistemine güçlü read-after-write tutarlılığı eklemeleri de gerçek yazılım mühendisliğinin zirvesiydi diye düşünüyorum blog yazısı bağlantısı
S3'ün lifecycle kısmında bizzat çalışmıştım ve bu dönem, indeks ekibinin bu tutarlılığı sağlamak için yapıyı yeniden tasarladığı zamana denk geliyordu. Dışarıdan bakınca da S3 etkileyici ama içeride hem uygulama hem de organizasyon yapısı hayal ettiğinizin ötesinde etkileyici
Google Cloud Storage ise aslında S3'ten çok daha önce bu özelliğe (güçlü tutarlılık) sahipti. Genel olarak GCS'nin biraz daha sistematik ve daha iyi inşa edilmiş bir ürün olduğu izlenimine sahibim
%92 sayısına (küme arızalarının çoğunun küçük başarısızlıklardan başlaması) katılıyorum. Gösterişli büyük kazalar değil, "önemsiz" görünen yeniden denemelerin durum birikimine yol açıp sonunda sabah 2'de büyük kesintiye dönüştüğü durumlar daha yaygın. Göze görünmeyen arızalara daha fazla mühendislik zamanı ayırmak önemli
Gerçekten ilginç bir yazı olduğunu düşünüyorum. Altyapı control plane'i kurarken durum makineleri kullanmak şart. P'nin mutlaka gerekli olup olmadığından emin değilim. Biz de 13 yıldan uzun süre Ruby ile altyapı control plane'leri kurduk ve çok iyi çalıştı ilgili deneyim paylaşımı blogu
P dili hakkında merak ettiğim bir nokta vardı. Eskiden Microsoft'un Windows USB stack runtime'ı için P ile C kodu üretip bunu gerçekten kullandığını sanıyordum, ama şimdi artık üretim kodu üretmek için kullanmıyor gibi görünüyor. Bununla ilgili Hacker News'e de soru bırakmıştım soru bağlantısı. Eğer üretilen kod çekirdeğe kadar girebiliyorsa çok daha gevşek koşullardaki bulut ortamlarında da kesinlikle kullanılabilir gibi görünüyor
AWS kökenli olmayan ve TLA+ ya da P'ye aşina olmayan biri olarak en azından bir "hello world" düzeyinde örnek olsaydı anlamak daha kolay olurdu diye düşünüyorum. Yazıyı okuyunca süreç sadece acı vericiymiş gibi de hissediliyor ve iyi tasarım ile testin zaten yeterli olmayacağı bir sorun mu diye düşündürtüyor. Basit bir örnek olsaydı gerçekte ne yapıldığını değerlendirmeye daha çok yardımcı olurdu
Sevdiğim hızlı bir TLA+ demo örneği var gist bağlantısı. Birden fazla iş parçacığının paylaşılan bir sayacı atomik olmayan şekilde artırdığı bir model ve özellik doğrulaması sırasında race condition yakalanıyor. Gerçekte bu tür hataları yalnızca testle bulmak çok zor. TLA+ özelliklerinin çoğu çok daha karmaşık, ama bu örnek basit hataları yakalamak için iyi
TLA'yı bizzat denedim ama grafik aracının öğreticilerle iyi uyuşmaması nedeniyle hayal kırıklığı yaşamıştım. TLA'nın kendisini kullanmak istiyordum ve Lamport'un çalışmalarını (LaTeX'ten makalelere kadar) uzun zamandır seviyordum
Biçimsel yöntemleri kullanmanın temel varsayımı, yalnızca testle tüm sorunların asla yakalanamayacağıdır
Resmî TLA+ Examples GitHub deposunu öneririm. DieHard gibi basit şeylerle başlamayı tavsiye ederim
Test, belirli problem örnekleri için uygulamanın doğruluğunu gösterir; biçimsel doğrulama ise tüm kategori için kanıt sunar. Örneğin anagram döndüren bir fonksiyonda test, yalnızca bazı kelime çiftleriyle doğrulama yapar; ama tüm kelime çiftleri için doğruluğu kanıtlamak istiyorsanız formal verification gerekir. undefined behavior ya da kütüphane hataları gibi durumlar da çoğu zaman ancak formal verification sürecinde yakalanır
"Property-based testing, fuzzing, runtime monitoring gibi hafif yarı-biçimsel teknikler" ifadesine dair, property-based testing ve fuzzing'in biçimsel yöntemlerin bir alt kümesi olduğu doğru olabilir ama runtime monitoring'i de yarı-biçimsel tekniklere katmak biraz fazla geliyor
Eskiden Leslie Lamport ile Buridan's Principle üzerine bir makale dâhil bazı konularda yazışmıştım. Bugün onun ana sayfasında TLA+ ve PlusCal hakkında çok şey öğrendim Peterson örneği sayfası. Matematiği programlamaya getiren ve eşzamanlı sistemler alanının öncülerinden biri olan kişinin bir sistem tasarım dili (TLA+) yapmış olması ve bunun AWS gibi yerlerde kullanılması son derece doğal geliyor. Dağıtık sistem kuran insanların Lamport'un yaptıklarını daha çok kullanmasını isterim. Büyük ölçekli sistemlerde doğruluğu kanıtlamak çok önemli
Mevcut koddan TLA+ spesifikasyonu dönüştürmek için Claude Opus'un (Extended Thinking) oldukça işe yaradığını söyleyebilirim. Rust projelerinde ya da C++ çekirdek bileşenlerini doğrularken birçok hata bulduğum oldu. Diğer modeller sözdizimi ve spesifikasyon mantığında sık sık tökezlerken Opus çok daha akıcı çalışıyor
Yalnızca büyük sistemlerde değil, SSH, terminal gibi küçük ama kritik (dünya çapında çok kullanılan) yardımcı araçlarda da doğruluğu kanıtlamak son derece faydalı
"Sistemin doğruluğunu kanıtlamak" ifadesi için, gerçekte her şeyi kanıtlamak mümkün değil. Bir model checker yalnızca sınırlı bir durum uzayında yazdığınız spesifikasyonun özellikleri sağladığını söyleyebilir
Kişisel olarak FIS'i dağıtık hizmet deneyleri için kullanmış olan var mı merak ediyorum. Kullanmayı değerlendiriyorum ama doğrudan büyük ölçekli deney yapmışlığım yok
Promela ve SPIN'in yazıda ele alınandan daha üst seviye diller olup olmadığını merak ediyorum