Verification of a multicore programming library
Bir çok çekirdekli programlama kütüphanesinin doğrulanması
- Tez No: 286363
- Danışmanlar: YRD. DOÇ. DR. ALPER ŞEN
- 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: 2011
- Dil: İngilizce
- Üniversite: Boğaziçi Üniversitesi
- Enstitü: Fen Bilimleri Enstitüsü
- Ana Bilim Dalı: Bilgisayar Mühendisliği Ana Bilim Dalı
- Bilim Dalı: Belirtilmemiş.
- 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
- İ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
2015
İnşaat Mühendisliğiİstanbul Teknik Üniversitesiİnşaat Mühendisliği Ana Bilim Dalı
PROF. DR. ENGİN ORAKDÖĞEN
- 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
2018
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolKoç ÜniversitesiBilgisayar Bilimleri ve Mühendisliği Ana Bilim Dalı
PROF. DR. ATTİLA GÜRSOY
- 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
2023
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrolİstanbul Teknik ÜniversitesiSavunma Teknolojileri Ana Bilim Dalı
DR. ÖĞR. ÜYESİ RAMAZAN YENİÇERİ
- 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
2012
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolKarabük ÜniversitesiBilgisayar Mühendisliği Ana Bilim Dalı
YRD. DOÇ. DR. SALİH GÖRGÜNOĞLU
- 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
2020
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolOrta Doğu Teknik ÜniversitesiBilgisayar Mühendisliği Ana Bilim Dalı
PROF. DR. MEHMET HALİT SEYFULLAH OĞUZTÜZÜN