Olaya-dayalı asenkron programlar için doğruluk kriteri tanımlanması ve doğrulanması

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 e cient 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.