Researcher:
Elmas, Tayfun

Profile Picture
ORCID

Job Title

PhD Student

First Name

Tayfun

Last Name

Elmas

Name

Name Variants

Elmas, Tayfun

Email Address

Birth Date

Filters

2004 - 201013

Advanced Search

Filter by

Settings

Researcher Of Publications: search.filters.isAuthorOfPublication.dcb2b788-d90c-4447-a46a-b87af897c023

Search Results

Now showing 1 - 10 of 13
  • Placeholder
    PublicationMetadata only
    A novel test coverage metric for concurrently-accessed software components (A work-in-progress paper)
    (Springer-Verlag Berlin, 2006) N/A; Department of Computer Engineering; N/A; Department of Computer Engineering; Department of Computer Engineering; Taşıran, Serdar; Elmas, Tayfun; Bölükbaşı, Güven; Keremoğlu, M. Erkan; Faculty Member; PhD Student; Undergraduate Student; Reseacher; Department of Computer Engineering; College of Engineering; Graduate School of Sciences and Engineering; College of Engineering, College of Engineering; N/A; N/A; N/A; N/A
    We propose a novel, practical coverage metric called "location pairs" (LP) for concurrently-accessed software components. The LP metric captures well common concurrency errors that lead to atomicity or refinement violations. We describe a software tool for measuring LP coverage and outline an inexpensive application of predicate abstraction and model checking for ruling out infeasible coverage targets.
  • Placeholder
    PublicationMetadata only
    Distributed document sharing with text classification over content-addressable network
    (Springer-Verlag Berlin, 2004) N/A; Department of Computer Engineering; Elmas, Tayfun; Özkasap, Öznur; PhD Student; Faculty Member; Department of Computer Engineering; Graduate School of Sciences and Engineering; College of Engineering; N/A; 113507
    Content-addressable network is a scalable and robust distributed hash table providing distributed applications to store and retrieve information in an efficient manner. We consider design and implementation issues of a document sharing system over a content-addressable overlay network. Improvements and their applicability on a document sharing system are discussed. We describe our system prototype in which a hierarchical text classification approach is proposed as an alternative hash function to decompose dimensionality into lower dimensional realities. Properties of hierarchical document categories are used to obtain probabilistic class labels which also improves searching accuracy.
  • Placeholder
    PublicationMetadata only
    A calculus of atomic actions
    (N/A, 2009) Qadeer, Shaz; N/A; Department of Computer Engineering; Elmas, Tayfun; Taşıran, Serdar; PhD Student; Faculty Member; Department of Computer Engineering; Graduate School of Sciences and Engineering; College of Engineering; N/A; N/A
    We present a proof calculus and method for the static verification of assertions and procedure specifications in shared-memory concurrent programs. The key idea in our approach is to use atomicity as a proof tool and to simplify the verification of assertions by rewriting programs to consist of larger atomic actions. We propose a novel, iterative proof style in which alternating use of abstraction and reduction is exploited to compute larger atomic code blocks in a sound manner. This makes possible the verification of assertions in the transformed program by simple sequential reasoning within atomic blocks, or significantly simplified application of existing concurrent program verification techniques such as the Owicki-Gries or rely-guarantee methods. Our method facilitates a clean separation of concerns where at each phase of the proof, the user worries only about only either the sequential properties or the concurrency control mechanisms in the program. We implemented our method in a tool called QED.We demonstrate the simplicity and effectiveness of our approach on a number of benchmarks including ones with intricate concurrency protocols.
  • Placeholder
    PublicationMetadata only
    A classification of concurrency bugs in java benchmarks by developer intent
    (Association for Computing Machinery (ACM), 2006) Department of Computer Engineering; Department of Computer Engineering; N/A; Keremoğlu, M. Erkan; Taşıran, Serdar; Elmas, Tayfun; Researcher; Faculty Member; PhD Student; Department of Computer Engineering; College of Engineering; College of Engineering; Graduate School of Sciences and Engineering; N/A; N/A; N/A
    This work addresses the issue of selecting the formal correctness criterion for a concurrent Java program that best corresponds to the developer's intent. We study a set of concurrency-related bugs detected in Java benchmarks reported in the literature. On these programs, we determine whether race-freedom, atomicity or refinement is the simplest and most appropriate criterion for program correctness. Our purpose is to demonstrate empirically the fact that the appropriate fix for a concurrency error and the selection of a program analysis tool for detecting such an error must be based on the proper expression of the designer's intent using a formal correctness criterion.
  • Placeholder
    PublicationMetadata only
    VYRD: verifying concurrent programs by runtime refinement-violation detection
    (Association for Computing Machinery (ACM), 2005) Qadeer, Shaz; N/A; Department of Computer Engineering; Elmas, Tayfun; Taşıran, Serdar; PhD Student; Faculty Member; Department of Computer Engineering; Graduate School of Sciences and Engineering; College of Engineering; N/A; N/A
    We present a runtime technique for checking that a concurrently-accessed data structure implementation, such as a file system or the storage management module of a database, conforms to an executable specification that contains an atomic method per data structure operation. The specification can be provided separately or a non-concurrent, "atomized" interpretation of the implementation can serve as the specification. The technique consists of two phases. In the first phase, the implementation is instrumented in order to record information into a log during execution. In the second, a separate verification thread uses the logged information to drive an instance of the specification and to check whether the logged execution conforms to it. We paid special attention to the general applicability and scalability of the techniques and to minimizing their concurrency and performance impact. The result is a lightweight verification method that provides a significant improvement over testing for concurrent programs. We formalize conformance to a specification using the notion of refinement: Each trace of the implementation must be equivalent to some trace of the specification. Among the novel features of our work are two variations on the definition of refinement appropriate for runtime checking: I/O and "view" refinement. These definitions were motivated by our experience with two industrial-scale concurrent data structure implementations: the Boxwood project, a B-link tree data structure built on a novel storage infrastructure [10] and the Scan file system [9]. I/O and view refinement checking were implemented as a verification tool named VYRD (VerifYing concurrent programs by Runtime Refinement-violation Detection). VYRD was applied to the verification of Boxwood, Java class libraries, and, previously, to the Scan filesystem. It was able to detect previously unnoticed subtle concurrency bugs in Boxwood and the Scan file system, and the known bugs in the Java class libraries and manually constructed examples. Experimental results indicate that our techniques have modest computational cost.
  • Placeholder
    PublicationMetadata only
    VyrdMC: driving runtime refinement checking with model checkers
    (Elsevier, 2006) N/A; Department of Computer Engineering; Elmas, Tayfun; Taşıran, Serdar; PhD Student; Faculty Member; Department of Computer Engineering; Graduate School of Sciences and Engineering; College of Engineering; N/A; N/A
    This paper presents VyrdMC, a runtime verification tool we are building for concurrent software components. The correctness criterion checked by VyrdMC is refinement: Each execution of the implementation must be consistent with an atomic execution of the specification. VyrdMC combines testing, model checking, and Vyrd, the runtime refinement checker we developed earlier. A test harness first drives the component to a non-trivial state which serves as the starting state for a number of simple, very small multi-threaded test cases. An execution-based model checker explores for each test case all distinct thread interleavings while Vyrd monitors executions for refinement violations. This combined approach has the advantage of improving the coverage of runtime refinement checking at modest additional computational cost, since model checkers are only used to explore thread interleavings of a small, fixed test program. The visibility and detailed checking offered by using refinement as the correctness criterion differentiate our approach from simply being a restricted application of model checking. An important side benefit is the reduction in program instrumentation made possible if VyrdMC is built using a model checker with its own virtual machine, such as Java PathFinder [8]. We are investigating the use of two different model checkers for building VyrdMC: Java PathFinder, an explicit-state model checker and Verisoft, a "stateless" model checker [7].
  • 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
    Goldilocks: efficiently computing the happens-before relation using locksets
    (Springer, 2006) Qadeer, S.; N/A; Department of Computer Engineering; Elmas, Tayfun; Taşıran, Serdar; PhD Student; Faculty Member; Department of Computer Engineering; Graduate School of Sciences and Engineering; College of Engineering; N/A; N/A
    We present a new lockset-based algorithm, Goldilocks, for precisely computing the happens-before relation and thereby detecting data-races at runtime. Dynamic race detection algorithms in the literature are based on vector clocks or locksets. Vector-clock-based algorithms precisely compute the happens-before relation but have significantly more overhead. Previous lockset-based race detection algorithms, on the other hand, are imprecise. They check adherence to a particular synchronization discipline, i.e., a sufficient condition for race freedom and may generate false race warnings. Our algorithm, like vector clocks, is precise, yet it is efficient since it is purely lockset based. We have implemented our algorithm inside the Kaffe Java Virtual Machine. Our implementation incorporates lazy evaluation of locksets and certain "short-circuit checks" which contribute significantly to its efficiency. Experimental results indicate that our algorithm's overhead is much less than that of the vector-clock algorithm and is very close to our implementation of the Eraser lockset algorithm.
  • Placeholder
    PublicationMetadata only
    Goldilocks: a race and transaction-aware java runtime
    (Assoc Computing Machinery, 2007) Qadeer, Shaz; N/A; Department of Computer Engineering; Elmas, Tayfun; Taşıran, Serdar; PhD Student; Faculty Member; Department of Computer Engineering; Graduate School of Sciences and Engineering; College of Engineering; N/A; N/A
    Data races of, tell result in unexpected and erroneous behavior. In addition 10 causing data corruption and leading programs to crash, the presence of data races complicates the semantics of an execution which might no longer be sequentially consistent. Motivated by these observations, we have designed and implemented a Java runtime system that monitors program executions and throws a DataRaceException when a data race is about to occur. Analogous to other runtime exceptions, the DataRaceException. provides two key benefits. First, accesses causing race conditions are interrupted and handled before they cause errors that may be difficult to diagnose later. Second, if no DataRaceException is thrown in an execution, it is guaranteed to be sequentially consistent. This strong guarantee helps to rule Out many concurrency-related possibilities its the cause of erroneous behavior. When a DataRaceException is caught, the operation, thread, or program causing it call be terminated gracefully. Alternatively, the DataRaceException can serve its a conflict-detection mechanism in Optimistic uses of concurrency. We start with the definition of data-race-free executions in the Java memory model. We generalize this definition to executions that use transactions in addition to locks and volatile variables for synchronization. We present a precise and efficient algorithm for dynamically verifying that an execution is free of data races. This algorithm generalizes the Goldilocks algorithm for data-race detection by handling transactions and providing the ability to distinguish between read and write accesses. We have implemented our algorithm and the DataRaceException in the Kaffe Java Virtual Machine. We have evaluated our system on a variety of publicly available Java benchmarks and it few microbenchmarks that combine lock-based and transaction-based synchronization. Our experiments indicate that our implementation has reasonable overhead. Therefore, we believe that in addition to being a debugging tool, the DataRaceException may be a viable mechanism to enforce the safety of executions of multithreaded Java programs.
  • Placeholder
    PublicationMetadata only
    Goldilocks: a race-aware Java runtime
    (Association for Computing Machinery (ACM), 2010) Qadeer, Shaz; N/A; Department of Computer Engineering; Elmas, Tayfun; Taşıran, Serdar; PhD Student; Faculty Member; Department of Computer Engineering; Graduate School of Sciences and Engineering; College of Engineering; N/A; N/A
    We present GOLDILOCKS, a Java runtime that monitors program executions and throws a DataRaceException when a data race is about to occur This prevents racy accesses from taking place, and allows race conditions to be handled before they cause errors that may be difficult to diagnose later The DataRaceException is a valuable debugging tool, and, if supported with reasonable computational overhead, can be an important safety feature for deployed programs Experiments by us and others on race aware Java runtimes indicate that the DataRaceException may be a viable mechanism to enforce the safety of executions of multithreaded Java programs An important benefit of DataRaceException is that executions in our runtime are guaranteed to be race free and thus sequentially consistent as per the Java Memory Model This strong guarantee provides an easy to-use, clean semantics to programmers, and helps to rule out many concurrency-related possibilities as the cause of errors To support the DataRaceException, our runtime incorporates the novel Goldilocks algorithm for precise dynamic race detection The Goldilocks algorithm is general, intuitive, and can handle different synchronization patterns uniformly.