Verification Of A Multicore Programming Library
Summary:
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.
Ö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.