Researcher: Mutluergil, Süha Orhun
Name Variants
Mutluergil, Süha Orhun
Email Address
Birth Date
4 results
Search Results
Now showing 1 - 4 of 4
Publication Metadata only Verification tools for transactional programs(Springer, 2015) Cristal, Adrian; Cohen, Ernie; Unsal, Osman; Elmas, Tayfun; N/A; Department of Computer Engineering; N/A; N/A; Özkan, Burcu Külahcıoğlu; Taşıran, Serdar; Mutluergil, Süha Orhun; Kuru, İsmail; PhD Student; Faculty Member; PhD Student; PhD Student; Department of Computer Engineering; Graduate School of Sciences and Engineering; College of Engineering; Graduate School of Sciences and Engineering; Graduate School of Sciences and Engineering; N/A; N/A; N/A; N/AWhile transactional memory has been investigated intensively, its use as a programming primitive by application and system builders is only recently becoming widespread, especially with the availability of hardware support in mainstream commercial CPUs. One key benefit of using transactional memory while writing applications is the simplicity of not having to reason at a low level about synchronization. For this to be possible, verification tools that are aware of atomic blocks and their semantics are needed. While such tools are clearly needed for the adoption of transactional memory in real systems, research in this area is quite preliminary. In this chapter, we provide highlights of our previous work on verification tools for transactional programs.Publication Metadata only Reasoning about TSO programs using reduction and abstraction(Springer, 2018) Bouajjani, Ahmed; Enea, Constantin; Tasiran, Serdar; N/A; Mutluergil, Süha Orhun; PhD Student; Graduate School of Sciences and Engineering; N/AWe present a method for proving that a program running under the Total Store Ordering (TSO) memory model is robust, i.e., all its TSO computations are equivalent to computations under the Sequential Consistency (SC) semantics. This method is inspired by Lipton's reduction theory for proving atomicity of concurrent programs. For programs which are not robust, we introduce an abstraction mechanism that allows to construct robust programs over-approximating their TSO semantics. This enables the use of proof methods designed for the SC semantics in proving invariants that hold on the TSO semantics of a non-robust program. These techniques have been evaluated on a large set of benchmarks using the infrastructure provided by CIVL, a generic tool for reasoning about concurrent programs under the SC semantics.Publication Metadata only A mechanized refinement proof of the Chase-Lev deque using a proof system(Springer, 2019) Taşıran, Serdar; N/A; Mutluergil, Süha Orhun; PhD Student; Graduate School of Sciences and Engineering; N/AWe present a linearizability proof for the concurrent Chase-Lev work-stealing queue (WSQ) implementation on sequentially consistent memory. We used the CIVL proof system to carry out the proof. The lowest-level description of the WSQ is the data structure code described in terms of fine-grained actions whose atomicity is guaranteed by hardware. Higher level descriptions consist of increasingly coarser action blocks obtained using a combination of Owicki-Gries (OG) annotations and reduction and abstraction. We believe that the OG annotations (location invariants) we provided to carry out the refinement proofs at each level provide insight into the correctness of the algorithm. The top-level description for the WSQ consists of a single atomic action for each data structure operation, where the specification of the action is tight enough to show that the WSQ data structure is linearizable.Publication Metadata only Proving linearizability using forward simulations(2017) Bouajjani, Ahmed; Emmi, Michael; Enea, Constantin; N/A; Mutluergil, Süha Orhun; PhD Student; Graduate School of Sciences and Engineering; N/ALinearizability is the standard correctness criterion for concurrent data structures such as stacks and queues. It allows to establish observational refinement between a concurrent implementation and an atomic reference implementation. Proving linearizability requires identifying linearization points for each method invocation along all possible computations, leading to valid sequential executions, or alternatively, establishing forward and backward simulations. In both cases, carrying out proofs is hard and complex in general. In particular, backward reasoning is difficult in the context of programs with data structures, and strategies for identifying statically linearization points cannot be defined for all existing implementations. In this paper, we show that, contrary to common belief, many such complex implementations, including, e.g., the Herlihy and Wing Queue and the Time-Stamped Stack, can be proved correct using only forward simulation arguments. This leads to simple and natural correctness proofs for these implementations that are amenable to automation.