Runtime Refinement Checking for Concurrent Data Structures (the VYRD* project: VerifYing Refinement by Runtime Detection)

August 30, 2004
Serdar Tasiran | Koc University, Instanbul, Turkey

The goal of the VYRD Project is to develop a runtime verification framework for concurrently accessed data structures. Databases and file systems have such data structures at their core. Stringent performance requirements force the use of tricky synchronization mechanisms for coordinating access to shared data, which makes these systems prone to concurrency errors.

In this talk, we present a method for verifying that a concurrent data structure implementation refines a specification with atomic operations. Complete verification of refinement for complex implementations is often impractical. Our method instead detects refinement violations that occur at runtime. We instrument the implementation to record its actions into a log in the order they happen. The verifier then uses the log to reconstruct interesting aspects of data structure state at certain points in the execution, runs the specification in parallel, and checks that refinement conditions are met. Refinement is formulated in terms of a correspondence between the specification and implementation states and/or method return values. To check a particularly simple notion of refinement, very little annotation by the programmer is required. We report results on the application of our method to a filesystem and the Boxwood project (on storage infrastructure) being developed at MSR Silicon Valley. We are investigating ways to generalize and automate our technique and to obtain more coverage from runtime checking.

*: In Norse mythology, the three sisters of Vyrd weave together the threads of fate.

Speaker Details

Serdar Tasiran received the B.S. degree in electrical engineering from Bilkent University, Ankara, Turkey in 1991 and the M.S. and Ph.D. degrees in electrical engineering and computer sciences from the University of California, Berkeley in 1995 and 1998. He was a research scientist with the Gigascale Systems Research Center (1998-2000), and the Systems Research Center (Compaq/HP Labs). Since 2003, he has been an assistant professor at Koc University, Istanbul, Turkey. He has had visiting appointments at Microsoft Research, EPFL, and MIT Research Laboratory for Electronics. Dr. Tasiran’s research focus is the application of formal and algorithmic methods to system verification and validation, particularly to concurrent software and hardware. His broader research interests include the synthesis, verification, performance analysis and optimization of hardware and software systems.