Researcher:
Sezgin, Ali

Profile Picture
ORCID

Job Title

Other

First Name

Ali

Last Name

Sezgin

Name

Name Variants

Sezgin, Ali

Email Address

Birth Date

Filters

2009 - 20104

Advanced Search

Filter by

Settings

Researcher Of Publications: search.filters.isAuthorOfPublication.4f40330f-6d28-43fc-ab9c-211b7320cb48

Search Results

Now showing 1 - 4 of 4
  • Placeholder
    PublicationMetadata only
    Run-time verification of optimistic concurrency
    (Springer, 2010) Qadeer, Shaz; N/A; Department of Computer Engineering; Department of Computer Engineering; Sezgin, Ali; Taşıran, Serdar; Muşlu, Kıvanç; Researcher; Faculty Member; Undergraduate Student; Department of Computer Engineering; N/A; College of Engineering; College of Engineering; N/A; N/A; N/A
    Assertion based specifications are not suitable for optimistic concurrency where concurrent operations are performed assuming no conflict among threads and correctness is cast in terms of the absence or presence of conflicts that happen in the future. What is needed is a formalism that allows expressing constraints about the future. In previous work, we introduced tressa claims and incorporated prophecy variables as one such formalism. We investigated static verification of tressa claims and how tressa claims improve reduction proofs. In this paper, we consider tressa claims in the run-time verification of optimistic concurrency implementations. We formalize, via a simple grammar, the annotation of a program with tressa claims. Our method relieves the user from dealing with explicit manipulation of prophecy variables. We demonstrate the use of tressa claims in expressing complex properties with simple syntax. We develop a run-time verification framework which enables the user to evaluate the correctness of tressa claims. To this end, we first describe the algorithms for monitor synthesis which can be used to evaluate the satisfaction of a tressa claim over a given execution. We then describe our tool implementing these algorithms. We report our initial test results.
  • Placeholder
    PublicationMetadata only
    Simplifying linearizability proofs with reduction and abstraction
    (Springer, 2010) Qadeer, Shaz; N/A; N/A; N/A; Department of Computer Engineering; Elmas, Tayfun; Sezgin, Ali; Subaşı, Ömer; Taşıran, Serdar; PhD Student; N/A; PhD Student; Faculty Member; Department of Computer Engineering; Graduate School of Sciences and Engineering; N/A; Graduate School of Sciences and Engineering; College of Engineering; N/A; N/A; N/A; N/A
    The typical proof of linearizability establishes an abstraction map from the concurrent program to a sequential specification, and identifies the commit points of operations. If the concurrent program uses fine-grained concurrency and complex synchronization, constructing such a proof is difficult. We propose a sound proof system that significantly simplifies the reasoning about linearizability. Linearizability is proved by transforming an implementation into its specification within this proof system. The proof system combines reduction and abstraction, which increase the granularity of atomic actions, with variable introduction and hiding, which syntactically relate the representation of the implementation to that of the specification. We construct the abstraction map incrementally, and eliminate the need to reason about the location of commit points in the implementation. We have implemented our method in the QED verifier and demonstrated its effectiveness and practicality on several highly-concurrent examples from the literature.
  • Placeholder
    PublicationMetadata only
    Tressa: claiming the future
    (Springer, 2010) Qadeer, Shaz; N/A; N/A; Sezgin, Ali; Taşıran, Serdar; Researcher; Faculty Member; N/A; N/A; N/A; N/A
    Unlike sequential programs, concurrent programs have to account for interference on shared variables. Static verification of a desired property for such programs crucially depends on precisely asserting the conditions for interference. In a static proof system, in addition to program variables, auxiliary (history) variables summarizing the past of the program execution are used in these assertions. Capable of expressing reachability only, assertions (and history variables) are not as useful in the proofs of programs using optimistic concurrency. Pessimistic implementations which allow access to shared data only after synchronization (e.g. locks) guarantee exclusivity; optimistic concurrency implementations which check for interference after shared data is accessed abandon exclusivity in favor of performance. In this paper, we propose a new construct, tressa, to express properties, including interference, about the future of an execution. A tressa claim states a condition for reverse reachability from an end state of the program, much like an assert claim states a condition for forward reachability from the initial state of the program. As assertions employ history variables, tressa claims employ prophecy variables, originally introduced for refinement proofs. Being the temporal dual of history variables, prophecy variables summarize the future of the program execution. We present the proof rules and the notion of correctness of a program for two-way reasoning in a static setting: forward in time for assert claims, backward in time for tressa claims. We have incorporated our proof rules into the QED verifier and have used our implementation to verify a small but sophisticated algorithm. Our experience shows that the proof steps and annotations follow closely the intuition of the programmer, making the proof itself a natural extension of implementation.
  • Placeholder
    PublicationMetadata only
    An annotation assistant for interactive debugging of programs with common synchronization idioms
    (2009) Qadeer, Shaz; N/A; Department of Computer Engineering; Department of Computer Engineering; Sezgin, Ali; Taşıran, Serdar; Elmas, Tayfun; Researcher; Faculty Member; PhD Student; Department of Computer Engineering; N/A; College of Engineering; Graduate School of Sciences and Engineering; N/A; N/A; N/A
    This paper explores an approach to improving the practical usability of static verification tools for debugging synchronization idioms. Synchronization idioms such as mutual exclusion and readers/writer locks are widely-used to ensure atomicity of critical regions. We present an annotation assistant that automatically generates program annotations. These annotations express noninterference between program statements, ensured by the synchronization idioms, and are used to identify atomic code regions. This allows the programmer to debug the use of the idioms in the program. We start by formalizing several well-known idioms by providing an abstract semantics for each idiom. For programs that use these idioms, we require the programmer to provide a few predicates linking the idiom with its realization in terms of program variables. From these, we automatically generate a proof script that is mechanically checked. These scripts include steps such as automatically generating assertions and annotating program actions with them, introducing auxiliary variables and invariants. We have successfully shown the applicability of this approach to several concurrent programs from the literature.