Publication: Runtime refinement checking of concurrent data structures
Program
KU-Authors
KU Authors
Co-Authors
Qadeer, Shaz
Publication Date
Language
Type
Embargo Status
Journal Title
Journal ISSN
Volume Title
Alternative Title
Abstract
We present a runtime technique for checking that a concurrent implementation of a data structure conforms to a high-level executable specification with atomic operations. The technique consists of two phases. In the first phase, the implementation code is instrumented in order to record information about its execution into a log. In the second phase, a verification thread runs concurrently with the implementation and uses the logged information to check that the execution conforms to the high-level specification. We pay special attention to reducing the impact of the runtime analysis on the concurrency characteristics and performance of the implementation. We are currently applying our technique to Boxwood [1], a distributed implementation of a B-link tree data structure.
Source
Publisher
Elsevier Science Bv
Subject
Computer science
Citation
Has Part
Source
Electronic Notes In Theoretical Computer Science
Book Series Title
Edition
DOI
10.1016/j.entcs.2004.01.028