Runtime Refinement Checking for Concurrent Data Structures

Опубликовано 6 сентября 2016, 5:06

Runtime Refinement Checking for Concurrent Data Structures (the VYRD* project: VerifYing Refinement by Runtime Detection) 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.