Techniques for verifying transactional programs and linearizability
İşlemsel programların ve doğrusallaştırılabilirliğin doğrulaması için teknikler
- Tez No: 309877
- Danışmanlar: YRD. 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: 2012
- 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ı: 73
Özet
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.
Özet (Çeviri)
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.
Benzer Tezler
- Techniques for runtime monitoring and static verification of concurrent software
Koşut-zamanlı yazılımlar için çalışma-zamanı izleme ve durağan doğrulama teknikleri
TAYFUN ELMAS
Doktora
İngilizce
2010
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolKoç ÜniversitesiBilgisayar Mühendisliği Ana Bilim Dalı
DR. SHAZ QADEER
YRD. DOÇ. DR. SERDAR TAŞIRAN
- 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
İSMAİL KURU
Yüksek Lisans
İngilizce
2015
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolKoç ÜniversitesiBilgisayar Bilimleri ve Mühendisliği Ana Bilim Dalı
DOÇ. DR. SERDAR TAŞIRAN
- Automated testing for solidity smart contracts
Solidity akıllı sözleşmeleri için otomatik testle
SEFA AKCA
Doktora
İngilizce
2022
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolThe University of EdinburghBilgisayar ve Enformatik Mühendisliği Ana Bilim Dalı
YRD. DOÇ. DR. AJITHA RAJAN
- How cryptographic implementations affect mobile agent systems
Şifreleme gerçekleştirmelerinin gezgin aracı internet sistemlerini nasıl etkilediği
İSMAİL ULUKUŞ
Yüksek Lisans
İngilizce
2003
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolBoğaziçi ÜniversitesiSistem ve Kontrol Mühendisliği Ana Bilim Dalı
PROF. DR. EMİN ANARIM
- Kullanıcıların mobil uygulama güvenlik farkındalıklarının makine öğrenmesi teknikleriyle incelenmesi
Investigation of users' mobile application security awareness using machine learning techniques
ESMA ERDOĞAN
Yüksek Lisans
Türkçe
2024
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolHitit ÜniversitesiAdli Bilimler Ana Bilim Dalı
DR. ÖĞR. ÜYESİ MUSTAFA COŞAR