Geri Dön

Verification of a multicore programming library

Bir çok çekirdekli programlama kütüphanesinin doğrulanması

  1. Tez No: 286363
  2. Yazar: ETEM DENİZ
  3. Danışmanlar: YRD. DOÇ. DR. ALPER ŞEN
  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: 2011
  8. Dil: İngilizce
  9. Üniversite: Boğaziçi Üniversitesi
  10. Enstitü: Fen Bilimleri Enstitüsü
  11. Ana Bilim Dalı: Bilgisayar Mühendisliği Ana Bilim Dalı
  12. Bilim Dalı: Belirtilmemiş.
  13. Sayfa Sayısı: 76

Özet

Yüksek performanslı yazılım ihtiyaçlarının sürekli artmasıyla beraber çok çekirdekli yazılım geliştirme ihtiyacı da artmaktadır. Bu durum, çok çekirdekli yazılımların potansiyel olarak birden fazla yürütme çizelgesine sahip olması nedeniyle, yazılımların güvenilirliğini azaltır ve doğrulanmaya harcanan çabayı artırır. Ardışıl yazılımlardaki hataları ortadan kaldırmak için kullanılan doğrulama yaklaşımları çok çekirdekli yazılımlarındaki hataları bulunması için yeterli değildir. Çok çekirdekli yazılım doğrulama yöntemlerinin koşutzamanlılığın yanısıra verimli ve ölçeklenebilir olmasına ihtiyacımız vardır. İleti geçirme kütüphanelerini kullanarak iletişim kuran çok çekirdekli yazılımlar için doğrulama ve kapsama teknikleri sunuyoruz. Özellikle yeni endüstri standartı olan ve Multicore Association tarafından geliştirilen Çok Çekirdekli İletişim Uygulama Programlama Arayüzü'nü (MCAPI) kullanan yazılımların güvenilirliğini arttırmak için teknikler sağlıyoruz. Çok çekirdekli yazılımlardaki mevcut ve potansiyel hataları bulmamızı sağlayan dinamik, öngörücü teknikler geliştirdik. Bu hata türlerinden bazıları kilitlenmeler, yarış durumları ve zamansal doğruluk savlarının ihlalleridir. Doğrulama tekniklerini, mutasyon sınaması temelli kapsama ölçümü ile tamamlanır. Kapsama ölçümleri doğrulama testlerinin kalitesinin ölçülmesine imkan sağlar. Tekniklerimiz için araçlar geliştirdik ve MCAPI standartını kullanan bir takım çok çekirdekli program üzerinde araçlarımızın geçerliliklerini denetledik. Tekniklerimizin deneysel olarak etkinliklerini gösterdik. Doğrulama aracımızın otomatik olarak çok çekirdekli programları doğruladığını ve zamansal doğruluk savlarının ihlalini, olası kilitlenme ve yarış durumlarının listesini bulduğunu gördük. Geleneksel dinamik doğrulama teknikleri kullanılarak bulunamayan hataları bulduk. Kapsama aracımız çok çekirdekli programların doğrulanması için kullanılan test kümelerinin kalitesinin iyileştirilmesinde yardımcı olur. Ayrıca kapsama aracımızla orijinal yürütme çizelgesinden farklı potansiyel yürütme çizelgelerini de keşfedebiliriz.

Özet (Çeviri)

As the demand for high performance software is constantly increasing, the need to develop multicore software is increasing, too. This results in degraded reliability of software and increased verification effort since multicore software has potentially more than one execution schedule. Verification approaches for eliminating errors in sequential software are not adequate for full coverage of errors in multicore software. We need not only concurrency aware but also efficient and scalable verification methods for multicore software. We present verification and coverage methods for multicore software that uses message passing libraries for communication. Specifically, we provide techniques to improve reliability of software using the new industry standard Multicore Communication API (MCAPI) by the Multicore Association. We develop dynamic predictive verification techniques that allow us to find actual and potential errors in a multicore software. Some of these error types are deadlocks, race conditions, and violation of temporal assertions. We complement our verification techniques with a mutation testing based coverage metric. Coverage metrics enable measuring the quality of verification test sets. We implemented our techniques in tools and validated them on several multicore programs that use MCAPI standard. We experimentally show the effectiveness of our methods. We show that our verification tool automatically verifies multicore programs and finds violation of temporal assertions, list of potential deadlocks, and race conditions. We find errors that are not found using traditional dynamic verification techniques. Our coverage tool helps to improve the quality of verification test sets for multicore programs. Furthermore, we can potentially explore execution schedules different than the original execution with our coverage tool.

Benzer Tezler

  1. İki parametreli zemine oturan betonarme yapıların doğrusal olmayan hesabı ve görsel tabanlı bir bilgisayar yazılımı

    Nonlinear analysis of reinforced concrete structures on two-parameter soil model and visual computer software

    ONUR AVCIOĞLU

    Doktora

    Türkçe

    Türkçe

    2015

    İnşaat Mühendisliğiİstanbul Teknik Üniversitesi

    İnşaat Mühendisliği Ana Bilim Dalı

    PROF. DR. ENGİN ORAKDÖĞEN

  2. Verification of concurrent programs via refinement proofs

    İyileştirme ispatları ile koşut-zamanlı programların doğrulanması

    SÜHA ORHUN MUTLUERGİL

    Doktora

    İngilizce

    İngilizce

    2018

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

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

    PROF. DR. ATTİLA GÜRSOY

  3. ComCoS: An enhanced cache partitioning technique for integrated modular avionics

    ComCoS: Entegre modüler aviyonikler için gelişmiş bir önbellek bölümleme tekniği

    YAKUP HÜNER

    Yüksek Lisans

    İngilizce

    İngilizce

    2023

    Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrolİstanbul Teknik Üniversitesi

    Savunma Teknolojileri Ana Bilim Dalı

    DR. ÖĞR. ÜYESİ RAMAZAN YENİÇERİ

  4. Yüz tanıma sisteminin paralel programlama ile optimizasyonu

    Optimization of face recognition system with parallel programming

    KADRİYE ÖZ

    Yüksek Lisans

    Türkçe

    Türkçe

    2012

    Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolKarabük Üniversitesi

    Bilgisayar Mühendisliği Ana Bilim Dalı

    YRD. DOÇ. DR. SALİH GÖRGÜNOĞLU

  5. Schedulability analysis of real-time multi-frame co-simulations on multi-core platforms

    Çok-çekirdekli platformlarda gerçek zamanlı çok-çerçeveli eş-benzetim için çizelgelenebilirlik çözümlemesi

    MUHAMMAD UZAİR AHSAN

    Doktora

    İngilizce

    İngilizce

    2020

    Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolOrta Doğu Teknik Üniversitesi

    Bilgisayar Mühendisliği Ana Bilim Dalı

    PROF. DR. MEHMET HALİT SEYFULLAH OĞUZTÜZÜN