Characterization and verification of correctness criteria for event-driven asynchronous programs

Asenkron programlama, kullanıcı girdilerine hızlı yanıt vermenin önemli bir gereksinim olduğu olaya dayalı modern web ve mobil uygulamalarda yaygın olarak kullanılmaktadır. Bu programlar, asenkron program çalışmasının getirdiği farklı kontrol akışı ve çok iş parçacıklı programların doğasında olan zorluklardan ötürü eşzamanlılık hatalarına yatkındırlar. Yakın zamanda, olaya dayalı ve asenkron programlardaki program hatalarını yakalamayı amaçlayan çalışmalar yapılmış olsa da, bu programlar için çalışma platformundan ve uygulamadan bağımsız, üst seviyeli bir doğruluk kriteri henüz tanımlanmamıştır. Bu tezin amacı, olaya-dayalı asenkron programlar için bir doğruluk kriterinin tanımlanması ve bu programlardaki eşzamanlılık hatalarının belirlenmesinde kullanılacak yöntem ve araçlar geliştirilmesidir. Bu doğrultuda, asenkron programların eş zamanlılık davranışlarını inceleyen statik ve dinamik araçlar geliştirdik. Eşzamanlı bir asenkron programın çalışma davranışlarının bazı kısıtlama parametrelerine göre belirlenmiş bir alt kümesini, nondeterministik, tek iş parçacıklı bir programda kodlamayı sağlayan yöntemler üzerinde çalıştık. Geliştirdiğimiz yöntem, programda var olan senkronizasyonu göz önüne alarak verilen bir kısıtlama parametresi için daha çok eşzamanlı program davranışını inceleyebilmeye olanak sağlamaktadır. Bir başka çalışma olarak, Android uygulamalarındaki asenkroni hatalarını yakalayan dinamik bir araç geliştirdik. Bu araç, çok iş parçacıklı programların incelenmesinde bilinen bir teknik olan sistematik eşzamanlılık taramasını olaya-dayalı asenkron programlara uyarlamaktadır. Araç, verilen bir dizi kullanıcı girdisi için, uygulamadaki olay işleme prosedürlerinin oluşturduğu asenkron görevlerin farklı çalışma sıralarını sistematik olarak test etmektedir. Asenkron programlardaki eşzamanlılık hatalarını incelemede elde ettiğimiz deneyime dayanarak, asenkroniye karşı dayanıklılık olarak isimlendirdiğimiz bir doğruluk kriteri tanımladık. Bu kriter, programcının olaya-dayalı asenkron programın çalışma davranışları konusundaki beklentilerini karşılamakta ve programın bazı kısımları araşındaki etkileşimi göz ardı edebilmesine izin vermektedir. Kabaca asenkroniye karşı dayanıklılık, program içindeki asenkroniye ve programın farklı parçalarının paylaşılan bellek üzerinde girişikleme yaparak işlem yapmasına bakılmaksızın programın tüm olay işleme prosedürlerinin ve tüm asenkron görevlerinin izole bir şekilde çalıştığı soyut bir görünümü ile aynı davranışları sergilemesini gerektirmektedir. Asenkroniye karşı dayanıklılık, iki sezgisel özelliğin; olay serileştirilebilirliği ve olay determinizminin birleşimi olarak ifade edilebilir. Kriterin bu şekilde ifade edilebilmesi, algoritmik olarak verimli bir şekilde kontrol edilebilmesine olanak sağladığı için önemlidir. Olay serileştirilebilirliği, farklı ortamlarda da kullanılan serileştirilebilirlik kavramının olay işleme prosedürlerine uyarlamasıdır. Bu özellik, bir dizi olay işleme prosedürünün eşzamanlı çalışmasının, olay işleme prosedürlerinin seri olarak, bir olayın işlenmesi tamamen bittikten sonra bir başka olay işlenerek art arda çalışmasına denk olmasını gerektirmektedir. Olay determinizmi tek bir olay işleme prosedürüne odaklanır. Bir olay işleme prosedürünün, oluşturduğu asenkron görevlerin paylaşılmış bellek üzerinde girişikleme yaparak çalışmasına bakılmaksızın tek deterministik sonucu olmasını gerektirmektedir. Olay serileştirilebilirliği ve olay determinizmi özelliklerinin doğrulanması için yeni yöntemler geliştirdik. Sunduğumuz yöntemin dikkat çekici yanı, eşzamanlı çalışabilen sınırsız sayıda asenkron görev içeren çok iş parçacıklı programların analizini tek iş parçacıklı programlarda ulaşılabilirlik problemine indirgemesidir. Açık kaynaklı Android uygulamaları üzerinde yaptığımız deneysel çalışmalar, asenkroniye karşı dayanıklılık analizinin pratikte uygulanabilir olduğunu göstermektedir. Ayrıca, uygulamalardaki gerçek eşzamanlılık hatalarının asenkroniye karşı dayanıklılık ihlali olarak yakalanabilmesi ve önceden bilinmeyen bazı eşzamanlılık hatalarının da bulunması önerdiğimiz doğruluk kriterinin geçerliliğini göstermektedir.