Verification of concurrent programs via refinement proofs

Çok çekirdekli işlemciler, artan başarımları ve düşen fiyatları sebebiyle birçok teknolojik cihazda tercih edilmektedirler. Günlük işlerde insanlara yardım etmekten (cep telefonu uygulamaları ile olduğu gibi), hayati öneme haiz vazifelere (uçuş kontrol sistemleri, ameliyat yardım araçları, askeri veritabanları ve işletim sistemlerinde olduğu gibi) yardım etmeye kadar olan aralıkta birçok görev yerine getirirler. Bu cihazların tam gücünü kullanabilmek için, programcılar yüksek verimli, koşut-zamanlı yazılım kütüphaneleri geliştirmelidir. Fakat, koşut-zamanlı kütüphane yazımı zor ve hataya açık bir iştir. Kütüphanenin doğruluğunu sağlamak için, programcı olası bütün binişimleri dikkate almalı ve gerekli durumlarda istenmeyen davranışları önlemek için eşleme yöntemlerine başvurmalıdır. çoğu zaman test yöntemi doğruluğu sağlamak için sonuçsuz kalır ve standart hata ayıklama araçları hataları ortaya cıkartmakta yetersiz kalır. Özellikle yaşamsal yazılım parçaları için, biçimsel yaklaşım şarttır. Bu tezde, koşut-zamanlı kütüphanelerin emniyet özelliklerini doğrulamaya, yani kötü bir şey asla olmaz veya program kötü bir hale asla erişemezi göstermeye odaklandık. Fakat, herhangi bir program için sav doğrulama problemi, bizim ilgilendiğimiz koşut-zamanlı ortamlar için karar-verilemez bir problem. Bu ``karar-verilemezlik'' engelini aşmak icin, araştırmacılar hal-erişilebilirliği yerine programın yürütümlerine bağlı olan daha güçlü doğruluk kıstasları önermişlerdir. Temel olarak, geliştirme ispatları, hem belirtim programının hem de gerçekleme programının yürütümlerinin benzer özellikler gösterdiğini ispatlamakta kullanılır. Yürütümler üzerindeki ``özellik'' secçimine göre doğruluk ispatları etkin bir şekilde yapılabilir. Mesela, sıralanabilirlik, yığıt ve kuyruk gibi koşut-zamanlı veri yapıları için standart doğruluk kıstasıdır. Bizim koşut-zamanlı gerçekleme ile atomik belirtim arasında gözlemsel geliştirme ilişkisi kurmamıza olanak sağlar. Sıralanabilirlik, sistemler arasında ileri veya geri simülasyon ilişkisi kurularak gösterilebilir. Özellikle koşut-zamanlı veri yapıları için, bir geri simülasyon ilişkisi bulmak daha zordur. Ek olarak, bir geri veya ileri simülasyon ilişkisinin varlığı hiçbir zaman kesin değildir. Bu tezin bir parçası olarak, genel kanının aksine, Herlihy & Wing Kuyruğu ve Zaman-Damgalı Yığıtı da içeren birçok karmaşık gerçeklemenin ileri simülasyon ilişkisi bularak doğruluğunun ispatlanabileceğini gösteriyoruz. İleri simülasyonların varlığına dair sonucumuz otomatikleştirilebilir, doğal ve basit ispatlara yol açıyor. Sıralanabilirliği ispatlamak için başka yöntemler de mevcuttur. Soyutlama teknikleriyle birleştirilmiş Lipton'un indirgeme kuramı geliştirme ispatları için güçlü bir araçtır. Bu tezin başka bir kısmı, Ardışık Sıralı (SC) hafıza üzerinde çalışan Chase-Lev İş-çalan Kuyruğu (WSQ) gerçeklemesinin bir sıralanabilirlik ispatını tasvir ediyor. İspat mekanize edilmiştir ve CIVL ispat sistemi ile yapılmıştır. İspat doğal bir şekilde yapılandırılmış geliştirme katmanlarından oluşmaktadır. En alt seviye betimleme, atomikliği donanım tarafından garanti edilmiş en ince taneli işlemler ile WSQ gerçeklemesidir. Üst katmanlara doğru, indirgeme, soyutlama ve Owicki-Gries (OG) notlarıyla atomik bloklar daha iri taneli hale gelir. En üst katman, her kuyruk yöntemi için, sıralanabilirliği göstermeye yetecek kadar sıkı, basit atomik işlemlerden muteşekkildir. Tezin son bölümü ise Tam Saklama Sırası (TSO) hafıza modeli altında çalışan programların sağlamlığını, yani bütün TSO yürütmelerinin SC yürütmelerine eşdeğer olduğunu, göstermek için bir yöntem sunuyor. Bu yöntem TSO sağlamlık sorununa hitap etmek için SC indirgeme ve soyutlama tekniklerinden faydalanıyor. Ek olarak, sağlam olmayan programların TSO ve SC yürütmelerini fazla yaklaşık tahmin ederek sağlam programlar elde edebilmek için bir soyutlama tekniği takdim ediyoruz. Bu soyutlama TSO değişmezlerini ispatlamak için var olan SC akıl yürütme yöntemlerini kullanmanın yeterli olacaği sıkılıkta programlar hasıl ediyor. Bu yöntemleri geniş bir kıyaslama kümesinde CIVL ispat sistemini kullanarak değerlendirdik.