Geri Dön

Techniques for verifying transactional programs and linearizability

İşlemsel programların ve doğrusallaştırılabilirliğin doğrulaması için teknikler

  1. Tez No: 309877
  2. Yazar: ÖMER SUBAŞİ
  3. Danışmanlar: YRD. DOÇ. DR. SERDAR TAŞIRAN
  4. Tez Türü: Yüksek Lisans
  5. Konular: Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrol, Computer Engineering and Computer Science and Control
  6. Anahtar Kelimeler: Belirtilmemiş.
  7. Yıl: 2012
  8. Dil: İngilizce
  9. Üniversite: Koç Üniversitesi
  10. Enstitü: Fen Bilimleri Enstitüsü
  11. Ana Bilim Dalı: Bilgisayar Bilimleri ve Mühendisliği Ana Bilim Dalı
  12. Bilim Dalı: Belirtilmemiş.
  13. 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

  1. 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

    İngilizce

    2010

    Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolKoç Üniversitesi

    Bilgisayar Mühendisliği Ana Bilim Dalı

    DR. SHAZ QADEER

    YRD. DOÇ. DR. SERDAR TAŞIRAN

  2. 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

    İngilizce

    2015

    Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolKoç Üniversitesi

    Bilgisayar Bilimleri ve Mühendisliği Ana Bilim Dalı

    DOÇ. DR. SERDAR TAŞIRAN

  3. Automated testing for solidity smart contracts

    Solidity akıllı sözleşmeleri için otomatik testle

    SEFA AKCA

    Doktora

    İngilizce

    İngilizce

    2022

    Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolThe University of Edinburgh

    Bilgisayar ve Enformatik Mühendisliği Ana Bilim Dalı

    YRD. DOÇ. DR. AJITHA RAJAN

  4. 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

    İngilizce

    2003

    Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolBoğaziçi Üniversitesi

    Sistem ve Kontrol Mühendisliği Ana Bilim Dalı

    PROF. DR. EMİN ANARIM

  5. 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

    Türkçe

    2024

    Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolHitit Üniversitesi

    Adli Bilimler Ana Bilim Dalı

    DR. ÖĞR. ÜYESİ MUSTAFA COŞAR