Tez No	İndirme	Tez Künye	Durumu
518086		Verification of concurrent programs via refinement proofs / İyileştirme ispatları ile koşut-zamanlı programların doğrulanması Yazar:SÜHA ORHUN MUTLUERGİL Danışman: PROF. DR. ATTİLA GÜRSOY Yer Bilgisi: Koç Üniversitesi / Fen Bilimleri Enstitüsü / Bilgisayar Bilimleri ve Mühendisliği Ana Bilim Dalı Konu:Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrol = Computer Engineering and Computer Science and Control Dizin:Formel doğrulama = Formal verification	Onaylandı Doktora İngilizce 2018 152 s.
Ç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.
Multi-core processors are preferred in many technological devices due to their increasing performance and reduced costs. They perform a range of tasks from helping people in their daily routines (i.e., via apps in cell-phones) to assist vital missions (i.e., flight control systems, surgery assistant devices, military databases and operating system kernels). To harness full potential of these devices, programmers need to develop efficient concurrent libraries. However, writing a concurrent library is a difficult and error-prone task. To ensure correctness of the library, the programmer needs to consider all possible interleavings of the concurrent execution units and provide synchronization mechanisms whenever necessary to prevent undesired behaviors. Most of the time, testing is inconclusive and standard debugging tools are incapable of exposing bugs. Formal treatment is necessary, especially for mission critical software components. In this thesis, we focus on ensuring safety properties of concurrent libraries i.e., something bad never happens or the program never reaches to a bad state. However, assertion checking for arbitrary programs is undecidable for the concurrent settings we consider. To overcome this undecidability barrier, researchers propose stronger correctness criteria that depend on the executions of the program instead of reachable states. Basically, refinement proofs are used to demonstrate that executions of both the specification program and the implementation show similar properties. Based on the choice of the property on executions, correctness proofs can be efficiently performed. For instance, linearizability is the standard correctness criterion for concurrent data structures like stacks and queues. It allows us to establish observational refinement relation between the concurrent implementation and the atomic specification. Linearizability can be shown by establishing forward or backward simulations between systems. In particular, finding a backward simulation relation is more difficult for concurrent data structures. In addition, existence of a backward or forward simulation is never guaranteed. As a part of this thesis, we show that contrary to common belief, many complex implementations including the Herlihy & Wing Queue and the Time-Stamped Stack can be proven correct by finding forward simulations. Our result on existence of forward simulations leads to simple and natural correctness proofs that are amenable to automation. There are other ways of proving linearizability. Lipton's reduction theory combined with program abstraction techniques is a strong tool for performing refinement proofs. Another part of the thesis describes a linearizability proof for the concurrent Chase-Lev Work-Stealing Queue (WSQ) implementation on Sequentially Consistent (SC) memory. The proof is mechanized and performed by using CIVL proof system. The proof consists of naturally structured refinement layers. The lowest level description is the WSQ implementation with the finest grained actions of which atomicity is guaranteed by the hardware. Through the upper layers, atomic blocks get coarser by using reduction, abstraction techniques and Owicki-Gries (OG) annotations. The highest layer consists of a simple atomic action for each queue operation that is tight enough to show linearizability. The last part of the thesis presents a method for showing robustness of a program running under the Total Store Ordering (TSO) memory model, i.e., all of its TSO executions are equivalent to SC executions. This method utilizes SC reduction and abstraction techniques to address TSO robustness problem. In addition, we introduce an abstraction technique that allows us to obtain robust programs from non-robust programs by over-approximating both TSO and SC executions. This abstraction yields programs tight enough so that using existing reasoning methods for the SC semantics is sufficient for proving TSO invariants. We have evaluated these methods on a large set of benchmarks using CIVL proof system.