Techniques for runtime monitoring and static verification of concurrent software

Abstract

Veri yapılarının ve servislerin koşut-zamanlı gerçekleştirmeleri, veritabanları, Internet sunucuları ve dosya sistemleri gibi geniş kullanım alanına sahip pek çok sistemin omurgasını oluşturmaktadır. Bu yazılımlar, koşut-zamanlı olarak çalışan çok sayıda istemciye verimli şekilde cevap verebilmek için küçük parçalı kilitleme ve bloklanmayan operasyonlar gibi eşleme teknikleri kullanırlar. Bu tekniklerin yanlış kullanımı, veri bozulması ve işletim sisteminin çökmesi, ve hatta bir uçuş kontrol sisteminin arızası gibi ciddi sonuçları olan koşut-zaman hatalarına yol açar. Koşut-zaman hatalarının tespiti, yeniden oluşturulması ve düzeltilmesi aslen ardışık yazılımlar için geliştirilen tekniklerle zor olmaktadır. Bu zorluk, koşut-zamanlı yazılımları kesin olarak, ve koşularının büyük kısmını kapsayacak şekilde sınayabilecek yeni program analizlerine ihtiyaç oluşturmaktadır. Bu tezde, bu ihtiyaca cevap veren ve farklı yollar izleyen iki teknik sunulmaktadır.Yarış durumları çoğu kez yüksek seviyede hataların belirtisidir ve istenmeyen koşulara yol açmaktadır. Bu tezin ilk kısmı, programın koşularını izleyerek, bir yarış durumunun hemen öncesinde bir DataRaceException fırlatan çalıştırma ortamı olan Goldilocks'ı sunmaktadır. Böylece, yarış durumu oluşturacak veri erişimlerinin oluşması engellenmekte, ve bu yarış durumlarının, teşhisinin zor olacağı hatalara yol açmadan işlenmesine izin verilmektedir. Sunulan çalışma ortamında çok-örgülü koşuların yarışsız, ve Java Bellek Modeli'ne göre ardışık tutarlı olması garantilenmektedir. Bu teminat, programcılara kolay kullanılabilir ve net bir semantik sağlamakta, ve hata ayıklama sırasında koşut-zamanla ilişkili pek çok olasılığın ortadan kaldırılmasına yardımcı olmaktadır. Böylece DataRaceException, değerli bir hata ayıklama aracı olmakta, aynı zamanda eğer makul bir hesaplama masrafıyla desteklenirse, yazılım için dağıtımı sonrası önemli bir güvenlik mekanizması olabilecektir. Ayrıca bu tezde, DataRaceException'ı desteklemek için Goldilocks adlı dinamik ve kesin bir yarış durumu tespit algoritması gerçekleştirilmiştir. Goldilocks algoritması genel ve sezgisel olmakla birlikte, farklı eşleme desenlerini ve yazılım işlem belleğini kullanan programları aynı biçimde işleyebilmektedir. Algoritmamız ve DataRaceException, Kaffe adlı bir Java sanal makinesinde gerçeklenmiş, ve sistemimiz çeşitli açık erişimli Java programları kullanılarak değerlendirilmiştir. Deneylerimiz, bu gerçekleştirmenin makul masrafları olduğunu ve başarımının literatürdeki diğer algoritmalarla rekabetçi olduğunu göstermektedir.Goldilocks gibi çalışma-zamanı izleme teknikleri hataların yokluğunu tamamen garanti edemez. Koşut-zamanlı yazılım, örneğin bir dosya sistemi ya da standart kütüphanenin bir parçası ise, hiç bir koşusunun hataya yol açmayacağının doğrulanması gerekmektedir. Bu, programın kaynak kodu üzerinde yapılacak durağan bir biçimsel ispat ile başarılabilir. Örgülerin paylaşımlı bellek üzerindeki olan küçük parçalı etkileşimleri, biçimsel ispatların kullanıcının ek girdileri açısından pahalı olmasına yol açmaktadır. Tezin ikinci kısmında, koşut-zamanlı programların durağan doğrulanması için geliştirdiğimiz bir ispat sistemi olan QED sunulmaktadır. Yaklaşımımızın kilit noktası, atomikliğin, güvenlik özelliklerinin ispatındaki zorlukların üstesinden gelmek amacıyla merkezi ispat aracı olarak kullanılmasıdır. İddialar ve sıralanabilirlik gibi geniş çapta kabul gören iki güvenlik özelliği desteklenmektedir. İddialar, programın yerel özelliklerini belirtmek için kullanılırken, sıralanabililik, veri yapıları için daha global ve zorlu ölçütler tanımlamaktadır. İspatlar, programın daha geniş atomik bloklarla adım adım yeniden yazılması ile yapılmaktadır. Buradaki yenilik, indirme ve soyutlama tekniklerini uygulayan ispat adımlarının, birbirinin bir sonraki çıktısını geliştirecek şekilde değişimli olarak kullanılmasıdır. İstenilen atomiklik seviyesine ulaşılınca, iddialar, ortaya çıkan programdaki atomik blokların içerisinde ardışık olarak denetlenmekte, iddiaların hepsi ispatlanınca orijinal programın doğruluğu ilan edilmektedir. Bu strateji, kullanıcının tasarım amacını açıkça ifade etmesini sağlayarak, ve program içerisindeki ardışık özellikler ve koşut-zaman kontrol mekanizmalarina olan ilginin net bir şekilde ayrımını kolaylaştırarak, ispatları önemli ölçüde basitleştirmektedir. İspat sistemimiz, var olan yöntemleri tamamlayıcı olup, bunların daha uysal bir şekilde uygulanmasına imkan vermektedir. Açık erişimli yazılım aracımız QED-Verifier, ispat kurallarının gerek duyduğu alt-seviye mantıksal çıkarım işlemlerini Z3 SMT çözücünün otomatik olarak denetleyebileceği doğrulama şartları olarak ifade ederek, ispatları mekanize etmektedir. QED'deki stratejimizin basit ve pratikliği, literatürde iyi bilinen programlar doğrulanarak ispatlanmış, atomikliğin, küçük parçalı kilitleme ve bloklanmayan algoritmalar gibi karışık koşut-zaman teknikleri kullanan programlar hakkında çıkarım yapmak için güçlü bir araç olduğu gösterilmiştir.

Concurrent implementations of data structures and services form the backbone of many widely-used systems such as databases, Internet servers, and file systems. In order to respond efficiently to a large number of clients accessing concurrently, such software makes use of sophisticated synchronization techniques including fine-grained locking and non-blocking operations. Incorrect use of these techniques makes software prone to concurrency bugs, which can have serious consequences, such as data corruption, operating system crash, or even more catastrophic results, e.g., failure of an aircraft flight control system. Concurrency-related bugs are notoriously difficult to detect, reproduce, and diagnose using code review and testing-based techniques originally developed for sequential programs. This difficulty creates demand for new program analyses that are capable of examining concurrent software precisely with high coverage of its executions. In this thesis, we present two techniques, each following a different direction to respond to this demand.Data races are often symptomatic of higher-level logical errors and may have unintended consequences. The first part of this thesis presents Goldilocks, a Java runtime that monitors program executions and throws a DataRaceException when a data race is about to occur. This prevents racy accesses from taking place, and allows race conditions to be handled before they cause errors that may be difficult to diagnose later. Multithreaded executions in our runtime are guaranteed to be race free and thus sequentially consistent as per the Java Memory Model. This strong guarantee provides an easy-to-use, clean semantics to programmers, and helps to rule out many concurrency-related possibilities as the cause of errors. Therefore, the DataRaceException is a valuable debugging tool, and, if supported with reasonable computational overhead, can be an important safety mechanism for deployed programs. To support the DataRaceException, we developed a novel, precise data-race detection algorithm called Goldilocks. The Goldilocks algorithm is general, intuitive, and can handle different synchronization patterns and software transactional memory uniformly. We have implemented our algorithm and the DataRaceException in the Kaffe Java Virtual Machine and evaluated our system on a variety of publicly available Java benchmarks. Our experiments indicate that our implementation has reasonable overhead and its performance is competitive with those of other algorithms in the literature.Runtime monitoring as in Goldilocks cannot fully guarantee absence of bugs. When the concurrent software is a part of, for example, a file system or a standard library, one has to verify that no execution of the software leads to an error. This can be accomplished by doing a static, formal proof on the program text. The interaction between threads over shared memory and at fine levels of concurrency make formal proofs expensive in terms of manual effort, requiring complex annotations and invariants, along with many auxiliary variables. In the second part of the thesis, we present QED, a proof system for static verification of concurrent programs. The key feature of our approach in QED is the use of atomicity as the central proof tool to overcome the challenges in proofs of safety properties. We support two widely-accepted safety specification, assertions and linearizability. While assertions specify local properties of the program, linearizability provides more global and stringent criteria for data structure implementations. A proof is done by rewriting the program with larger atomic blocks in a number of steps. A novel feature of our approach is alternating proof steps that apply reduction and abstraction, each of which improves the outcome of the other in a following step. After reaching a desired level of atomicity, we check assertions sequentially within the atomic blocks of the resulting program and declare the original program correct when we discharge all the assertions. This strategy leads to significantly simplified proofs by allowing the user the express the design intent in a clear way and facilitating a clean separation of concerns about the sequential properties and the concurrency control mechanisms in the program. Our proof system is orthogonal and complementary to existing methods and enables more tractable application of them. Our publicly available software tool, QED-Verifier, mechanizes proofs by encoding the low-level logical reasoning required by the proof rules as verification conditions automatically checked by the Z3 SMT solver. We demonstrated the simplicity and practicality of our proof strategy by verifying well-known programs from the literature and showed that atomicity is a powerful tool for reasoning about programs using a wide range of intricate concurrency techniques including fine-grained locking and non-blocking algorithms.