Gevşetilmiş bellek modelleri üstünde çalışan proğramlarin doğruluğunun kontrolu için durağan yöntemler

Koşut-zamanlılık heryerde bulunmaktadır. Birçok internet, gerçek zamanlı ve gömülü yazılımlar doğası gereği koşut zamanlılık kullanıllarak tasarlanır. Fakat, koşut zamanlı yazılımları programlamak karmaşık ve hataya meyilli eylemlerdir. Doğasında bulunan tutarsızlık gereği, programcının yazdığı programın nasıl bir davranış göstereceğini anlaması zordur. Bir Swing dokümantasyonu der ki : "Eğer kullanmaktan sakınabiliyorsanız, akışları kullanmaktan sakının. Akşları kullanması zor olabiliyor ve programınızın hata ayıklanma işlemini zorlaştırabiliyor. Genellikle, grafiksel bileşen özellikleri gibi kullanıcı arayüz ¸calışmalarında kesinlikle gerekli olmayabilirler.", [97]. Diğer bir dökümanda [98] ise : "Aynı kümedeki kilitler için yarışan akışların neden olduğu kilitlenme akışlı programlarda çözülmesi en zor problemdir. O kadar zordur ki çözmeye bile teşebbüs etmeyiz. ... Buna rağmen, kilitlenmenin var olup olmadığını belirleyebilmek için tek seçenek kaynak kodun sıkı bir incelenmesidir...". Sonuç olarak koşut-zamanlılıktan kaynaklananan hataları tespit etmek ve tekrar üretebilmek kaynak kodu gözden geçirme, tek akışlı bir program için geliştirilen sınama teknikleri gibi klasik yazılım mühendisliği teknikleri ile zordur. Çoğunlukla programlama dili gercekleştiricileri ve koşut-zamanlı kütüphane gerçekleştiricileri koşut-zamanlılık ile zorluk çekenlerdir. Bu temel olarak yazılım ve donanımın ilişkisini çözümlemenin zorluğundan kaynaklanır. S.Adve ve H-J.Boehm der ki: "Donanım mimarları için zorluğun bir parçası programlama dilleri seviyesinde açık bir bellek modelinin olmamasıdır. Programcının donanımdan ne bekleyeceğini muallakta bırakmaktadır", [31]. Bütün bu problemler, yazılım ve donanım ilişkisini formal bir şekilde belirtmeyi önemli kılmaktadır çünkü formal modeller açıkça belli olmayan tutarsızlıkları ifade edebilir. Bu formal tanımlama çabasının ana ürünü bellek modellerinin üzerinde gerçekleştirildi, örneklerden biri geleneksel paylaşımlı belleklerde ardışık tutarlılık, diğeri işlembilgisel belleklerde serileşebilmedir. Bu modelleme çalışmaları bir programın beklenen davranışlarını formal olarak tanımladığı için önemlidir. Bu modelleme çalışmaları geleneksel paylaşımlı belleklerde yarış-içermeyen (DRF) ve işlembilgisel belleklerde ¸celi¸ski-i¸cermeyen gibi s¨ozle¸smeler sa˘galyarak g¨uvenilirlik garantileri tanımlarlar. Çoğunlukla daha çok başarıma ihtiyaç duyulduğundan ardışık tutarlılık veya sıkı serileşebilme gibi sözleşmeleri zorunlu kılarak yazılım uygulamalar için işlemcileri yavaşlatmaya gerek yoktur. Bellek erişimini optimize etmek için, bazı bellek modelleri yazmaların atomikliğini gevşetebilir, makina komutlarının yerlerini değiştirebilir veya okumalardan sonra gerçekleşen yazmaların yarattığı çelişkileri göz ardı edebilir. Bu durumda, algoritma veya koşut-zamanlı veri yapısı tasarlarken bu tip güçlü modeller, örneğin, ardışık tutarlılık (SC) veya sıkı serileşebilme, açısından düşünmek doğru program üretmek için güvenilir olmayabilir. Sonuç olarak daha gevşek memory modelleri sunulmuştur. Bu tezde sırası ile geleneksel paylaşımlı bellek alanında ve işlembilgisel bellek alanında iki gevşetilmis bellek modeli olan yazmaların-tam-sıralaması (TSO) ve bellekkopyası-soyutlanma (SI) üzerinde çalışan programlar için durağan doğrulama yöntemi sunuyoruz. Kısım 2 içersinde, bellek-kopyası-soyutlama ve benzeri gevşek bellek modelleri üzerinde çalıştırılan programların doğrulanması için durağan doğrulama yöntemi sunuyoruz. Bellek-kopyası-soyutlama ve benzeri gevşek bellek modeller oldukça fazla kullanılan modellerdir. SI altında çalışan işlemler için ardışık olarak çalışıyormuş gibi yorum yapabilme imkanı kaybolur, bu işlemler artık serileşebilir işlemler değildir. Bu tezde önceki yapılan işten [23] farklı olarak, serileşemez programları da kotarıyoruz. Bir kaynak kodu diğer kaynak koda SI semantiğini içerecek şekilde dönüştürmeyi sunuyoruz. Dönüştürülmüş programın kullanıcı tarafından kaynak koda eklenen ek sözleşme dipnotları ile birlikte doğrulanması orjinal programın SI altında doğrulanmasına denktir. Bizim SI semantiği için önerdiğimiz dönüştürme tekniği VCC'nin modülerliğini ve ölçeklenirliğini korumaktadır. Yöntemimizi işlembilgisel bellek literatüründeki deneme programlarına uyguladık [95]. Kısım 3 içersinde, x86-TSO bellek modelleri üzerinde çalışan programlar ile ilgili kolay yorumlamayı sağlamak için program iyileştirmeyi sağlayan kanıt yöntemi sunuyoruz. 3.4 bölümünde kaynak kodun içine TSO semantiğini ek kod olarak yerleştiriyoruz ve programın yorumlanmasını kolaylaştırana kadar TSO'ya özgü iyileştirme adımlarını uyguluyoruz, [94]. TSO'ya özgü işlemci yerel yazma tamponlarını ve belleğe yazma işlemini soyutlanmış halını kaynak kodun içine yerleştiriyoruz. Bu yöntemde belirli proglamlama kalıplarının belirli iyileştirme kalıpları ile örtüşüp örtüşmediğini gözlemliyoruz. Bu yöntemin kullanılabilir olduğunu mekanik iyileştirmelerini engelsiz kilitleme yöntemi Spin-Lock ve acquire/release programlama kalıbı gösteren Send-Receive örneği için 3.4.7 kısımında 3.4 ile gösterdik.