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.
Concurrency is everywhere. Many internet, real-time and embedded applicationsare most naturally designed using concurrency. However, programming conccurentsoftware is complex, error-prone task. Because of inherent non-determinism, it isdifficult for the programmer to understand the effect of his or her program. TheSwing documentation states :`If you can get away with it, avoid using threads. Threads can be difficult to use,and they make programs harder to debug. In general, they aren't necessary for strictlyGUI work, such as component properties`, [97]. Another note in [98] states`Deadlock between threads competing for the same set of locks is the hardest problem to solve in any threaded program. It is a hard enough problem, in fact, that wewill not solve it or even attempt to solve it. .... Nontheless, a close examination ofthe source code is the only option available to determine if deadlock is a possibility...`.As a result we can state that concurrency bugs are difficult to detect, reproduceand diagnose using conventional software engineering techniques such as code reviewand test-based techniques developed developed for sequential programs.Generally, language and concurrency library implementers are the ones who haveivdifficulty with concurrency. This is mainly due to hardness of resolving the internalsof interaction of hardware and software to build reliable software. S.Adve and H.-J.Boehm state:`Part of challenge for hardware architects was the lack of clear memory models atthe programming language level. It was unclear what programmers expect hardware todo`, [31].All these problems make formalising HW/SW interaction crucially important because formal models can express aspects of non-determinism that are not apperent.The main product of this formalisation effort has been made on memory models; e.gsequential consistency (SC) in traditional shared memory, serializability in transactional memory. They are important because they define and formalize the expectedbehaviours of a program. They define safety guarantees for programs with providingcontracts such as data-race-freeness (DRF) in traditional shared memory, conflict freein transactional memory between hardware and software; e.g. data-race-free programunder SC model.Mostly due to performance need, we do not need to enforce sequential consistencyor strict serializability in transactional memory and slow down the processors for someapplications. To optimize memory access, some memory models may introduce relaxing atomicity of writes, allow instruction reordering or ignore write-after-read conflicts.In this case, thinking in terms of these strong models, e.g. SC or strict serializability, when designing concurrent data structures or algorithms cannot be reliable toproduce correct programs. As a result, weaker memory models are proposed.In this thesis, we propose static verification methods for programs running ontwo weak memory models such as total-store-order (TSO) and snap-shot-isolation(SI) models respectively from traditional shared memory and transactional memorydomains.In chapter 2, we present a static verification approach for programs running undersnapshot isolation (SI) and similar relaxed transactional semantics. Relaxed conflictdetection schemes such as snapshot isolation (SI) are used widely. Under SI, transactions are no longer guaranteed to be serializable, and the simplicity of reasoningsequentially within a transaction is lost. In this thesis, we present an approach forstatically verifying properties of transactional programs operating under SI. Differently from earlier work [23], we handle transactional programs even when they aredesigned not to be serializable.We present a source-to-source transformation which augments the program withan encoding of the SI semantics. Verifying the resulting program with transformeduser annotations and specifications is equivalent to verifying the original transactionalprogram running under SI – a fact we prove formally. Our encoding preserves themodularity and scalability of VCC's verification approach. We applied our methodsuccessfully to benchmark programs from the transactional memory literature [95].In chapter 3, we propose a proof method approach for refining programs to makethem easy to reason under x86-TSO model. In this approach we introduce storebuffers explicitly into source and try to refine program via applying TSO specificsound refinement steps [94]. We put the store buffers into source and abstract theTSO memory flush operation explicitly in the source. In this approach, we try toobserve whether specific type of programming patterns result in specific type of refinement pattern. We show applicability of the approach with mechanized refinementof mechanized refinement of non-blocking Spin-Lock and acquire/release pattern SendReceive in Section 3.4.7 by approach 3.4.
153