Runtime verification for software transactional memories
Singh V. 2010. Runtime verification for software transactional memories. RV: International Conference on Runtime Verification, LNCS, vol. 6418, 421–435.
Download
No fulltext has been uploaded. References only!
Conference Paper
| Published
| English
Scopus indexed
Author
Editor
Sokolsky, Oleg;
Rosu, Grigore;
Tilmann, Nikolai;
Barringer, Howard;
Falcone, Ylies;
Finkbeiner, Bernd;
Havelund, Klaus;
Lee, Insup;
Pace, Gordon
Corresponding author has ISTA affiliation
Department
Series Title
LNCS
Abstract
Software transactional memories (STMs) promise simple and efficient concurrent programming. Several correctness properties have been proposed for STMs. Based on a bounded conflict graph algorithm for verifying correctness of STMs, we develop TRACER, a tool for runtime verification of STM implementations. The novelty of TRACER lies in the way it combines coarse and precise runtime analyses to guarantee sound and complete verification in an efficient manner. We implement TRACER in the TL2 STM implementation. We evaluate the performance of TRACER on STAMP benchmarks. While a precise runtime verification technique based on conflict graphs results in an average slowdown of 60x, the two-level approach of TRACER performs complete verification with an average slowdown of around 25x across different benchmarks.
Publishing Year
Date Published
2010-01-01
Publisher
Springer
Volume
6418
Page
421 - 435
Conference
RV: International Conference on Runtime Verification
Conference Location
St. Julians, Malta
Conference Date
2010-11-01 – 2010-11-04
IST-REx-ID
Cite this
Singh V. Runtime verification for software transactional memories. In: Sokolsky O, Rosu G, Tilmann N, et al., eds. Vol 6418. Springer; 2010:421-435. doi:10.1007/978-3-642-16612-9_32
Singh, V. (2010). Runtime verification for software transactional memories. In O. Sokolsky, G. Rosu, N. Tilmann, H. Barringer, Y. Falcone, B. Finkbeiner, … G. Pace (Eds.) (Vol. 6418, pp. 421–435). Presented at the RV: International Conference on Runtime Verification, St. Julians, Malta: Springer. https://doi.org/10.1007/978-3-642-16612-9_32
Singh, Vasu. “Runtime Verification for Software Transactional Memories.” edited by Oleg Sokolsky, Grigore Rosu, Nikolai Tilmann, Howard Barringer, Ylies Falcone, Bernd Finkbeiner, Klaus Havelund, Insup Lee, and Gordon Pace, 6418:421–35. Springer, 2010. https://doi.org/10.1007/978-3-642-16612-9_32.
V. Singh, “Runtime verification for software transactional memories,” presented at the RV: International Conference on Runtime Verification, St. Julians, Malta, 2010, vol. 6418, pp. 421–435.
Singh V. 2010. Runtime verification for software transactional memories. RV: International Conference on Runtime Verification, LNCS, vol. 6418, 421–435.
Singh, Vasu. Runtime Verification for Software Transactional Memories. Edited by Oleg Sokolsky et al., vol. 6418, Springer, 2010, pp. 421–35, doi:10.1007/978-3-642-16612-9_32.
Google Scholar