Publication:
Runtime refinement checking of concurrent data structures

Placeholder

Departments

School / College / Institute

Program

KU Authors

Co-Authors

Qadeer, Shaz

Publication Date

Language

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

item.page.datauri

Link

Rights

Copyrights Note

Endorsement

Review

Supplemented By

Referenced By

0

Views

0

Downloads

View PlumX Details