Tez No	İndirme	Tez Künye	Durumu
434273		Characterization and verification of correctness criteria for event-driven asynchronous programs / Olaya-dayalı asenkron programlar için doğruluk kriteri tanımlanması ve doğrulanması Yazar:BURCU ÖZKAN Danışman: DOÇ. DR. SERDAR TAŞIRAN Yer Bilgisi: Koç Üniversitesi / Fen Bilimleri Enstitüsü / Bilgisayar Bilimleri ve Mühendisliği Ana Bilim Dalı Konu:Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrol = Computer Engineering and Computer Science and Control Dizin:Bilgisayar yazılımları = Computer softwares	Onaylandı Doktora İngilizce 2016 158 s.
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.
Asynchronous programming is ubiquitous in modern event driven web and mobile applications for which responsiveness to user inputs is a key concern. These programs are prone to concurrency errors due to the different control flow of asynchronous execution and the inherent scheduling nondeterminism of multithreading. Though recent work focuses on detecting bugs in event driven and asynchronous programs, there is no high-level correctness criteria that is independent of the computing platform or the application logic. The goal of this dissertation is the characterization of the correctness of event-driven asynchronous programs and building techniques and tools for detecting the concurrency bugs in these programs. Towards formulating a correctness criteria, we build static and dynamic concurrency exploration tools for asynchronous programs. We devise a sequentialization-based technique which encodes a particular subset of possible concurrent program behaviors into a nondeterministic sequential program, where this subset of behaviors is specified by some bounding parameters. By taking the program synchronization into account, our method provides an ecient exploration that can capture a larger set of concurrent program behaviors for a given bounding parameter. We also develop a dynamic exploration tool to detect and reproduce asynchrony bugs in Android applications. It adopts systematic concurrency exploration that is well-known for multithreaded programs to event-driven asynchronous programs. Given a sequence of user inputs to an application, the tool systematically executes alternate schedules of tasks in the execution of this sequence of event handlers. Based on our experience on the analysis of concurrency bugs in asynchronous programs, we define a correctness criteria, robustness against asynchrony. It captures the programmer expectations about the behavior of an event-driven asynchronous program and enables the programmer to ignore certain interference among some parts of his program. Roughly, regardless of the asynchrony and the concurrent accesses to the memory, robustness requires a program to exhibit the same set of behaviors with an abstract view of its execution in which the event handlers and asynchronous invocations run in isolation. Robustness against asynchrony can be formulated as a conjunction of two intuitive properties: event serializability and event determinism. This formulation of robustness is important as it yields an efficient algorithmic checking method. Event serializability is an adaptation of the serializability property used in some other contexts to the event handlers in a program. It requires the executions of a sequence of event handlers to be equivalent to a serial execution of them in which an event handler is dispatched only after the completion of all asynchronous tasks of the previous event. Event determinism focuses on a single event handler and requires it to produce a deterministic outcome regardless of the interleaving execution of its asynchronous invocations. We present novel algorithms for the verification of event determinism and event serializability. Remarkably, our method reduces the analysis of the event-driven asynchronous programs with unbounded number of concurrent tasks to the reachability problems in sequential programs. Our experimental work on the open source Android applications shows that our robustness checking algorithm is viable and can be used in practice. Moreover, the real concurrency bugs in the applications can be captured as robustness violations and unknown bugs can be uncovered by checking the robustness of an application.