Techniques for runtime monitoring and static verification of concurrent software

Veri yapılarının ve servislerin koşut-zamanlı gerçekleştirmeleri, veritabanları, Internet sunucuları ve dosya sistemleri gibi geniş kullanım alanına sahip pek çok sistemin omurgasını oluşturmaktadır. Bu yazılımlar, koşut-zamanlı olarak çalışan çok sayıda istemciye verimli şekilde cevap verebilmek için küçük parçalı kilitleme ve bloklanmayan operasyonlar gibi eşleme teknikleri kullanırlar. Bu tekniklerin yanlış kullanımı, veri bozulması ve işletim sisteminin çökmesi, ve hatta bir uçuş kontrol sisteminin arızası gibi ciddi sonuçları olan koşut-zaman hatalarına yol açar. Koşut-zaman hatalarının tespiti, yeniden oluşturulması ve düzeltilmesi aslen ardışık yazılımlar için geliştirilen tekniklerle zor olmaktadır. Bu zorluk, koşut-zamanlı yazılımları kesin olarak, ve koşularının büyük kısmını kapsayacak şekilde sınayabilecek yeni program analizlerine ihtiyaç oluşturmaktadır. Bu tezde, bu ihtiyaca cevap veren ve farklı yollar izleyen iki teknik sunulmaktadır.Yarış durumları çoğu kez yüksek seviyede hataların belirtisidir ve istenmeyen koşulara yol açmaktadır. Bu tezin ilk kısmı, programın koşularını izleyerek, bir yarış durumunun hemen öncesinde bir DataRaceException fırlatan çalıştırma ortamı olan Goldilocks'ı sunmaktadır. Böylece, yarış durumu oluşturacak veri erişimlerinin oluşması engellenmekte, ve bu yarış durumlarının, teşhisinin zor olacağı hatalara yol açmadan işlenmesine izin verilmektedir. Sunulan çalışma ortamında çok-örgülü koşuların yarışsız, ve Java Bellek Modeli'ne göre ardışık tutarlı olması garantilenmektedir. Bu teminat, programcılara kolay kullanılabilir ve net bir semantik sağlamakta, ve hata ayıklama sırasında koşut-zamanla ilişkili pek çok olasılığın ortadan kaldırılmasına yardımcı olmaktadır. Böylece DataRaceException, değerli bir hata ayıklama aracı olmakta, aynı zamanda eğer makul bir hesaplama masrafıyla desteklenirse, yazılım için dağıtımı sonrası önemli bir güvenlik mekanizması olabilecektir. Ayrıca bu tezde, DataRaceException'ı desteklemek için Goldilocks adlı dinamik ve kesin bir yarış durumu tespit algoritması gerçekleştirilmiştir. Goldilocks algoritması genel ve sezgisel olmakla birlikte, farklı eşleme desenlerini ve yazılım işlem belleğini kullanan programları aynı biçimde işleyebilmektedir. Algoritmamız ve DataRaceException, Kaffe adlı bir Java sanal makinesinde gerçeklenmiş, ve sistemimiz çeşitli açık erişimli Java programları kullanılarak değerlendirilmiştir. Deneylerimiz, bu gerçekleştirmenin makul masrafları olduğunu ve başarımının literatürdeki diğer algoritmalarla rekabetçi olduğunu göstermektedir.Goldilocks gibi çalışma-zamanı izleme teknikleri hataların yokluğunu tamamen garanti edemez. Koşut-zamanlı yazılım, örneğin bir dosya sistemi ya da standart kütüphanenin bir parçası ise, hiç bir koşusunun hataya yol açmayacağının doğrulanması gerekmektedir. Bu, programın kaynak kodu üzerinde yapılacak durağan bir biçimsel ispat ile başarılabilir. Örgülerin paylaşımlı bellek üzerindeki olan küçük parçalı etkileşimleri, biçimsel ispatların kullanıcının ek girdileri açısından pahalı olmasına yol açmaktadır. Tezin ikinci kısmında, koşut-zamanlı programların durağan doğrulanması için geliştirdiğimiz bir ispat sistemi olan QED sunulmaktadır. Yaklaşımımızın kilit noktası, atomikliğin, güvenlik özelliklerinin ispatındaki zorlukların üstesinden gelmek amacıyla merkezi ispat aracı olarak kullanılmasıdır. İddialar ve sıralanabilirlik gibi geniş çapta kabul gören iki güvenlik özelliği desteklenmektedir. İddialar, programın yerel özelliklerini belirtmek için kullanılırken, sıralanabililik, veri yapıları için daha global ve zorlu ölçütler tanımlamaktadır. İspatlar, programın daha geniş atomik bloklarla adım adım yeniden yazılması ile yapılmaktadır. Buradaki yenilik, indirme ve soyutlama tekniklerini uygulayan ispat adımlarının, birbirinin bir sonraki çıktısını geliştirecek şekilde değişimli olarak kullanılmasıdır. İstenilen atomiklik seviyesine ulaşılınca, iddialar, ortaya çıkan programdaki atomik blokların içerisinde ardışık olarak denetlenmekte, iddiaların hepsi ispatlanınca orijinal programın doğruluğu ilan edilmektedir. Bu strateji, kullanıcının tasarım amacını açıkça ifade etmesini sağlayarak, ve program içerisindeki ardışık özellikler ve koşut-zaman kontrol mekanizmalarina olan ilginin net bir şekilde ayrımını kolaylaştırarak, ispatları önemli ölçüde basitleştirmektedir. İspat sistemimiz, var olan yöntemleri tamamlayıcı olup, bunların daha uysal bir şekilde uygulanmasına imkan vermektedir. Açık erişimli yazılım aracımız QED-Verifier, ispat kurallarının gerek duyduğu alt-seviye mantıksal çıkarım işlemlerini Z3 SMT çözücünün otomatik olarak denetleyebileceği doğrulama şartları olarak ifade ederek, ispatları mekanize etmektedir. QED'deki stratejimizin basit ve pratikliği, literatürde iyi bilinen programlar doğrulanarak ispatlanmış, atomikliğin, küçük parçalı kilitleme ve bloklanmayan algoritmalar gibi karışık koşut-zaman teknikleri kullanan programlar hakkında çıkarım yapmak için güçlü bir araç olduğu gösterilmiştir.