Sokolsky, Oleg ; Rosu, Grigore ; Tilmann, Nikolai ; Barringer, Howard ; Falcone, Ylies ; Finkbeiner, Bernd ; Havelund, Klaus ; Lee, Insup ; Pace, Gordon
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.
421 - 435
RV: International Conference on Runtime Verification
St. Julians, Malta
2010-11-01 – 2010-11-04
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.