Koşut-zamanlı yazılımlar için çalışma-zamanı izleme ve durağan doğrulama teknikleri

Concurrent implementations of data structures and services form the backbone of many widely-used systems such as databases, Internet servers, and file systems. In order to respond efficiently to a large number of clients accessing concurrently, such software makes use of sophisticated synchronization techniques including fine-grained locking and non-blocking operations. Incorrect use of these techniques makes software prone to concurrency bugs, which can have serious consequences, such as data corruption, operating system crash, or even more catastrophic results, e.g., failure of an aircraft flight control system. Concurrency-related bugs are notoriously difficult to detect, reproduce, and diagnose using code review and testing-based techniques originally developed for sequential programs. This difficulty creates demand for new program analyses that are capable of examining concurrent software precisely with high coverage of its executions. In this thesis, we present two techniques, each following a different direction to respond to this demand.Data races are often symptomatic of higher-level logical errors and may have unintended consequences. The first part of this thesis presents Goldilocks, a Java runtime that monitors program executions and throws a DataRaceException when a data race is about to occur. This prevents racy accesses from taking place, and allows race conditions to be handled before they cause errors that may be difficult to diagnose later. Multithreaded executions in our runtime are guaranteed to be race free and thus sequentially consistent as per the Java Memory Model. This strong guarantee provides an easy-to-use, clean semantics to programmers, and helps to rule out many concurrency-related possibilities as the cause of errors. Therefore, the DataRaceException is a valuable debugging tool, and, if supported with reasonable computational overhead, can be an important safety mechanism for deployed programs. To support the DataRaceException, we developed a novel, precise data-race detection algorithm called Goldilocks. The Goldilocks algorithm is general, intuitive, and can handle different synchronization patterns and software transactional memory uniformly. We have implemented our algorithm and the DataRaceException in the Kaffe Java Virtual Machine and evaluated our system on a variety of publicly available Java benchmarks. Our experiments indicate that our implementation has reasonable overhead and its performance is competitive with those of other algorithms in the literature.Runtime monitoring as in Goldilocks cannot fully guarantee absence of bugs. When the concurrent software is a part of, for example, a file system or a standard library, one has to verify that no execution of the software leads to an error. This can be accomplished by doing a static, formal proof on the program text. The interaction between threads over shared memory and at fine levels of concurrency make formal proofs expensive in terms of manual effort, requiring complex annotations and invariants, along with many auxiliary variables. In the second part of the thesis, we present QED, a proof system for static verification of concurrent programs. The key feature of our approach in QED is the use of atomicity as the central proof tool to overcome the challenges in proofs of safety properties. We support two widely-accepted safety specification, assertions and linearizability. While assertions specify local properties of the program, linearizability provides more global and stringent criteria for data structure implementations. A proof is done by rewriting the program with larger atomic blocks in a number of steps. A novel feature of our approach is alternating proof steps that apply reduction and abstraction, each of which improves the outcome of the other in a following step. After reaching a desired level of atomicity, we check assertions sequentially within the atomic blocks of the resulting program and declare the original program correct when we discharge all the assertions. This strategy leads to significantly simplified proofs by allowing the user the express the design intent in a clear way and facilitating a clean separation of concerns about the sequential properties and the concurrency control mechanisms in the program. Our proof system is orthogonal and complementary to existing methods and enables more tractable application of them. Our publicly available software tool, QED-Verifier, mechanizes proofs by encoding the low-level logical reasoning required by the proof rules as verification conditions automatically checked by the Z3 SMT solver. We demonstrated the simplicity and practicality of our proof strategy by verifying well-known programs from the literature and showed that atomicity is a powerful tool for reasoning about programs using a wide range of intricate concurrency techniques including fine-grained locking and non-blocking algorithms.