Researcher:
Mutluergil, Süha Orhun

Loading...
Profile Picture
ORCID

Job Title

PhD Student

First Name

Süha Orhun

Last Name

Mutluergil

Name

Name Variants

Mutluergil, Süha Orhun

Email Address

Birth Date

Search Results

Now showing 1 - 4 of 4
  • Placeholder
    Publication
    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/A
    While 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.
  • Placeholder
    Publication
    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/A
    We 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.
  • Placeholder
    Publication
    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/A
    We 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.
  • Placeholder
    Publication
    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/A
    Linearizability 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.