Techniques for verifying transactional programs and linearizability

Abstract

Bu tezde, çoklu-iş parçacıklı ve koşut-zamanlı programların doğrulanması ile ilgili iki önemli probleme değinmekteyiz. Önce koşut-zamanlı bir uygulamanın doğrusallaştırılabilirliğini ispatlamak problemini ele alıyoruz. Geçerli bir ispat sistemine dayanarak doğrusallaştırılabilirlik ispatlarının mümkün kılındığı bir metod sunuyoruz. Metodumuz koşut-zamanlı uygulamanın amaçlanan tanımlamalarına dönüştürülmesine dayanmaktadır. Bu dönüştürülmeler ispat sistemin kuralları tarafından yönetilmektedir. Her dönüşüm adımı programın doğruluk ile ilgili davranışlarını korumaktadır. Limitte programın doğruluğunu gösteren tanımına ulaşılır. Yaklaşımımızda, doğrusallaştırılabilirlik kavramını, koşut-zamanlı programları ve ispat sisteminin kurallarını tanımlamaktayız. Ardından teorik bulgularımıza yer vermekteyiz.İkinci olarak, programcı tarafından tanımlanan çakışmaları bulan işlemsel programların doğrulanması problemini ele alıyoruz. Performans açısından bu t¨ur sistemler istenilse de bu sistemler kendilerini kullanan işlemsel programların doğrulanmasını zorlaştırmaktadır. Özellikle de bu sistemler dizisel kanıtların yapılmasını engellemektedir. Yaklaşımımızda, önce bu tip programları modelliyoruz.Sonra, dizisel kanıtların yapılmasını sağlayan bir reçete sunuyoruz. Bu reçetede program üzerinde soyutlamalar yapılmaktadır. Soyutlamalar yapıldıktan sonra, doğrulama işi otomatik dizisel doğrulamaya dönüşmektedir. Bu da VCC ve HAVOC gibi dizisel doğrulama araçlarıyla yapılabilir. Ana teoremimiz ise, soyutlanmış program doğrulamasının ilk orijinal işlemsel programın doğrulaması anlamına geldiğini ispatlamaktadır.

In this thesis, we consider two significant software verification problem regarding concurrent, multi-threaded programs. First, we consider the problem of proving the linearizability of a concurrent implementation. We suggest a sound method for verifying a concurrent implementation is linearizable based on a sound proof system. Our method is based on transforming the concurrent implementation into the specification aimed for the implementation. The transformation is governed by proof rules of the proof system. Each transformation step preserves certain behaviors of the program that are relevant to the specification of the program. At the limit, we obtain a program that is being the sequential specification considered for the correctness of the original concurrent program. In our approach, we provide the formalization of the linearizability notion, concurrent programs as well as the proof system and its rules. We then state our theoretical findings.Second, we study the verification of transactional programs with programmer-defined conflict detection. While programmer-defined conflict detection is desirable in terms of performance issues of the transactional memory systems, such relaxed conflict detection complicates the verification of the programs that use these transactional systems. In particular, the ability to use sequential reasoning provided by conventional transactional memories is lost when the relaxed conflict detection is introduced. In our approach, we first model and formalize such transactional programs. Then, we provide a recipe for the verification process in which we regain the ability to use sequential reasoning. This recipe includes abstractions provided by the programmer on the original program. After the abstractions are introduced, the verification problem becomes the sequential verification problem automated by sequential verification tools such as VCC and HAVOC. Our soundness theorem guarantees that once the abstracted program is verified, so is the original transactional program.