Gevşetilmiş bellek modelleri üstünde çalışan proğramlarin doğruluğunun kontrolu için durağan yöntemler
Static methods for checking correctness of programs on relaxed memory systems
- Tez No: 379849
- Danışmanlar: DOÇ. DR. SERDAR TAŞIRAN
- Tez Türü: Yüksek Lisans
- Konular: Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrol, Computer Engineering and Computer Science and Control
- Anahtar Kelimeler: Belirtilmemiş.
- Yıl: 2015
- Dil: İngilizce
- Üniversite: Koç Üniversitesi
- Enstitü: Fen Bilimleri Enstitüsü
- Ana Bilim Dalı: Bilgisayar Bilimleri ve Mühendisliği Ana Bilim Dalı
- Bilim Dalı: Belirtilmemiş.
- Sayfa Sayısı: 153
Özet
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.
Özet (Çeviri)
Concurrency is everywhere. Many internet, real-time and embedded applications are most naturally designed using concurrency. However, programming conccurent software is complex, error-prone task. Because of inherent non-determinism, it is difficult for the programmer to understand the effect of his or her program. The Swing 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 strictly GUI 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 we will not solve it or even attempt to solve it. .... Nontheless, a close examination of the 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, reproduce and diagnose using conventional software engineering techniques such as code review and test-based techniques developed developed for sequential programs. Generally, language and concurrency library implementers are the ones who have iv difficulty with concurrency. This is mainly due to hardness of resolving the internals of 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 at the programming language level. It was unclear what programmers expect hardware to do”, [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.g sequential consistency (SC) in traditional shared memory, serializability in transactional memory. They are important because they define and formalize the expected behaviours of a program. They define safety guarantees for programs with providing contracts such as data-race-freeness (DRF) in traditional shared memory, conflict free in transactional memory between hardware and software; e.g. data-race-free program under SC model. Mostly due to performance need, we do not need to enforce sequential consistency or strict serializability in transactional memory and slow down the processors for some applications. 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 to produce correct programs. As a result, weaker memory models are proposed. In this thesis, we propose static verification methods for programs running on two weak memory models such as total-store-order (TSO) and snap-shot-isolation (SI) models respectively from traditional shared memory and transactional memory domains. In chapter 2, we present a static verification approach for programs running under snapshot isolation (SI) and similar relaxed transactional semantics. Relaxed conflict detection schemes such as snapshot isolation (SI) are used widely. Under SI, transactions are no longer guaranteed to be serializable, and the simplicity of reasoning sequentially within a transaction is lost. In this thesis, we present an approach for statically verifying properties of transactional programs operating under SI. Differently from earlier work [23], we handle transactional programs even when they are designed not to be serializable. We present a source-to-source transformation which augments the program with an encoding of the SI semantics. Verifying the resulting program with transformed user annotations and specifications is equivalent to verifying the original transactional program running under SI – a fact we prove formally. Our encoding preserves the modularity and scalability of VCC's verification approach. We applied our method successfully to benchmark programs from the transactional memory literature [95]. In chapter 3, we propose a proof method approach for refining programs to make them easy to reason under x86-TSO model. In this approach we introduce store buffers explicitly into source and try to refine program via applying TSO specific sound refinement steps [94]. We put the store buffers into source and abstract the TSO memory flush operation explicitly in the source. In this approach, we try to observe whether specific type of programming patterns result in specific type of refinement pattern. We show applicability of the approach with mechanized refinement of mechanized refinement of non-blocking Spin-Lock and acquire/release pattern SendReceive in Section 3.4.7 by approach 3.4.
Benzer Tezler
- Column generation approach for dynamic berth allocation problem
Dinamik rıhtım tahsis etme problemi için kolon üretme yöntemi
ÖZGE NARİN
Yüksek Lisans
İngilizce
2010
Endüstri ve Endüstri MühendisliğiKoç ÜniversitesiEndüstri Mühendisliği Ana Bilim Dalı
DOÇ. DR. CEYDA OĞUZ
- Gerçekliği izleme, bilişsel yanlılık ve temsilsel değişimin içgörüsel problem çözmeye etkisi
The effect of reality monitoring, cognitive biases and representational change on insight problem solving
GAYE ÖZEN AKIN
- Koklear implant ve işitme cihazı kullanan okul çağı çocuklarınınbilgisayar tabanlı cnsvs (the central nervous system vital signs) ile nörobilişsel değerlendirilme sonuçlarının yorumlanması:randomize kontrollü bir çalışma
Interpretation of neurocognitive assessment results with computer-based cnsvs (the centralnervous system vital signs) of school-age children using cochlear implants and hearing aids: a randomized controlled study
RUKİYE AYYILDIZ
Yüksek Lisans
Türkçe
2023
Kulak Burun ve Boğazİstanbul Aydın ÜniversitesiOdyoloji Ana Bilim Dalı
DOÇ. DR. DENİZHAN DİZDAR
- Bir Riemann manifoldunda gevşetilmiş elastik çizgi
Relaxed elastic line in a Riemannian manifold
GÖZDE ÖZKAN
Yüksek Lisans
Türkçe
2010
MatematikSüleyman Demirel ÜniversitesiMatematik Ana Bilim Dalı
DOÇ. DR. AHMET YÜCESAN
- Birim yüklenme probleminin matematiksel ve akıllı sezgisel yaklaşımlar kullanılarak çözülmesi
Solving unit commitment problem using mathematical and intelligent heuristic approaches
ÜMMÜHAN BAŞARAN FİLİK
Doktora
Türkçe
2010
Elektrik ve Elektronik MühendisliğiAnadolu ÜniversitesiElektrik-Elektronik Mühendisliği Ana Bilim Dalı
YRD. DOÇ. DR. MEHMET KURBAN