Loading...
Please wait, while we are loading the content...
Similar Documents
VYRD: Verifying concurrent programs by runtime refinement-violation detection (2005)
| Content Provider | CiteSeerX |
|---|---|
| Author | Elmas, Tayfun Tasiran, Serdar |
| Description | We present a runtime technique for checking that a concurrentlyaccessed 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. |
| File Format | |
| Language | English |
| Publisher | ACM Press |
| Publisher Date | 2005-01-01 |
| Publisher Institution | In PLDI ’05: Proc. of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation |
| Access Restriction | Open |
| Subject Keyword | Performance Impact Runtime Checking First Phase Scan File System Executable Specification Verifying Concurrent Program Verification Tool Unnoticed Subtle Concurrency Bug B-link Tree Data Structure Logged Execution Conforms General Applicability Lightweight Verification Method Industrial-scale Concurrent Data Structure Implementation Storage Management Module Refinement Checking Data Structure Operation Boxwood Project Logged Information Runtime Refinement-violation Detection Atomized Interpretation Novel Feature Runtime Technique Significant Improvement Java Class Library Refinement Appropriate Modest Computational Cost File System Concurrentlyaccessed Data Structure Implementation Experimental Result Constructed Example Separate Verification Thread Novel Storage Infrastructure Concurrent Program Atomic Method Special Attention Scan Filesystem |
| Content Type | Text |
| Resource Type | Article |
