Static methods for checking correctness of programs on relaxed memory systems

Concurrency is everywhere. Many internet, real-time and embedded applications are most naturally designed using concurrency. However, programming conccurent software is complex, error-prone task. Because of inherent non-determinism, it is difficult for the programmer to understand the effect of his or her program. The Swing documentation states : "If you can get away with it, avoid using threads. Threads can be difficult to use, and they make programs harder to debug. In general, they aren't necessary for strictly GUI work, such as component properties", [97]. Another note in [98] states "Deadlock between threads competing for the same set of locks is the hardest problem to solve in any threaded program. It is a hard enough problem, in fact, that we will not solve it or even attempt to solve it. .... Nontheless, a close examination of the source code is the only option available to determine if deadlock is a possibility ...". As a result we can state that concurrency bugs are difficult to detect, reproduce and diagnose using conventional software engineering techniques such as code review and test-based techniques developed developed for sequential programs. Generally, language and concurrency library implementers are the ones who have iv difficulty with concurrency. This is mainly due to hardness of resolving the internals of interaction of hardware and software to build reliable software. S.Adve and H.-J.Boehm state: "Part of challenge for hardware architects was the lack of clear memory models at the programming language level. It was unclear what programmers expect hardware to do", [31]. All these problems make formalising HW/SW interaction crucially important because formal models can express aspects of non-determinism that are not apperent. The main product of this formalisation effort has been made on memory models; e.g sequential consistency (SC) in traditional shared memory, serializability in transactional memory. They are important because they define and formalize the expected behaviours of a program. They define safety guarantees for programs with providing contracts such as data-race-freeness (DRF) in traditional shared memory, conflict free in transactional memory between hardware and software; e.g. data-race-free program under SC model. Mostly due to performance need, we do not need to enforce sequential consistency or strict serializability in transactional memory and slow down the processors for some applications. To optimize memory access, some memory models may introduce relaxing atomicity of writes, allow instruction reordering or ignore write-after-read conflicts. In this case, thinking in terms of these strong models, e.g. SC or strict serializability, when designing concurrent data structures or algorithms cannot be reliable to produce correct programs. As a result, weaker memory models are proposed. In this thesis, we propose static verification methods for programs running on two weak memory models such as total-store-order (TSO) and snap-shot-isolation (SI) models respectively from traditional shared memory and transactional memory domains. In chapter 2, we present a static verification approach for programs running under snapshot isolation (SI) and similar relaxed transactional semantics. Relaxed conflict detection schemes such as snapshot isolation (SI) are used widely. Under SI, transactions are no longer guaranteed to be serializable, and the simplicity of reasoning sequentially within a transaction is lost. In this thesis, we present an approach for statically verifying properties of transactional programs operating under SI. Differently from earlier work [23], we handle transactional programs even when they are designed not to be serializable. We present a source-to-source transformation which augments the program with an encoding of the SI semantics. Verifying the resulting program with transformed user annotations and specifications is equivalent to verifying the original transactional program running under SI – a fact we prove formally. Our encoding preserves the modularity and scalability of VCC's verification approach. We applied our method successfully to benchmark programs from the transactional memory literature [95]. In chapter 3, we propose a proof method approach for refining programs to make them easy to reason under x86-TSO model. In this approach we introduce store buffers explicitly into source and try to refine program via applying TSO specific sound refinement steps [94]. We put the store buffers into source and abstract the TSO memory flush operation explicitly in the source. In this approach, we try to observe whether specific type of programming patterns result in specific type of refinement pattern. We show applicability of the approach with mechanized refinement of mechanized refinement of non-blocking Spin-Lock and acquire/release pattern SendReceive in Section 3.4.7 by approach 3.4.