Computer Science and Engineering PhD Thesis Defense by Süha Orhun Mutluergil

KOÇ UNIVERSITY

GRADUATE SCHOOL OF SCIENCES & ENGINEERING

COMPUTER SCIENCE & ENGINEERING

PhD THESIS DEFENSE BY SUHA ORHUN MUTLUERGIL

Title:  Verification of Concurrent Programs via Refinement Proofs

Speaker: Süha Orhun Mutluergil

Time: June 22, 2018, 13:00

Place: ENG 208

Koç University

Rumeli Feneri Yolu

Sariyer, Istanbul

Thesis Committee Members:

Prof. Dr. Attila Gürsoy (Advisor, Koç University)

Assoc. Prof. Dr. Öznur Özkasap (Koç University)

Asst. Prof. Dr. Didem Unat (Koç University)

Prof. Dr. Ahmed Bouajjani (IRIF, University of Diderot, Paris)

Asst. Prof. Dr. Tankut Barış Aktemur (Özyeğin University)

Assoc. Prof. Dr. Constantin Enea (Co-advisor, IRIF, University of Diderot, Paris)

Abstract:

Multi-core processors are preferred in many technological devices due to their increasing performance and reduced costs. They perform a range of tasks from helping people in their daily routines (i.e., via apps in cell-phones) to assist vital missions (i.e., flight control systems, surgery assistant devices, military databases and operating system kernels). To harness full potential of these devices, programmers need to develop efficient concurrent libraries.

However, writing a concurrent library is a difficult and error-prone task. To ensure correctness of the library, the programmer needs to consider all possible interleavings of the concurrent execution units and provide synchronization mechanisms whenever necessary to prevent undesired behaviors. Most of the time, testing is inconclusive and standard debugging tools are incapable of exposing bugs. Formal treatment is necessary, especially for mission critical software components.

In this thesis, we focus on ensuring safety properties of concurrent libraries i.e., something bad never happens or the program never reaches to a bad state. However, assertion checking for arbitrary programs is undecidable for the concurrent settings we consider. To overcome this undecidability barrier, researchers propose stronger correctness criteria that depend on the executions of the program instead of reachable states. Basically, refinement proofs are used to demonstrate that executions of both the specification program and the implementation show similar properties. Based on the choice of the property on executions, correctness proofs can be efficiently performed.

For instance, linearizability is the standard correctness criterion for concurrent data structures like stacks and queues. It allows us to establish observational refinement relation between the concurrent implementation and the atomic specification. Linearizability can be shown by establishing forward or backward simulations between systems. In particular, finding a backward simulation relation is more difficult for concurrent data structures. In addition, existence of a backward or forward simulation is never guaranteed. As a part of this thesis, we show that contrary to common belief, many complex implementations including the Herlihy&Wing Queue and the Time-Stamped Stack can be proven correct by finding forward simulations. Our result on existence of forward simulations leads to simple and natural correctness proofs that are amenable to automation.

There are other ways of proving linearizability. Lipton’s reduction theory combined with program abstraction techniques is a strong tool for performing refinement proofs. Another part of the thesis describes a linearizability proof for the concurrent Chase-Lev Work-Stealing Queue (WSQ) implementation on Sequentially Consistent (SC) memory. The proof is mechanized and performed by using CIVL proof system. The proof consists of naturally structured refinement layers. The lowest level description is the WSQ implementation with the finest grained actions of which atomicity is guaranteed by the hardware.  Through the upper layers, atomic blocks get coarser by using reduction, abstraction techniques and Owicki–Gries (OG) annotations. The highest layer consists of a simple atomic action for each queue operation that is tight enough to show linearizability.

The last part of the thesis presents a method for showing robustness of a program running under the Total Store Ordering (TSO) memory model, i.e., all of its TSO executions are equivalent to SC executions. This method utilizes SC reduction and abstraction techniques to address TSO robustness problem. In addition, we introduce an abstraction technique that allows us to obtain robust programs from non-robust programs by over-approximating both TSO and SC executions. This abstraction yields programs tight enough so that using existing reasoning methods for the SC semantics is sufficient for proving TSO invariants. We have evaluated these methods on a large set of benchmarks using CIVL proof system.