Skip to main content
SpringerLink
Log in
Book cover

International Conference on Runtime Verification

RV 2010: Runtime Verification pp 421–435Cite as

Runtime Verification for Software Transactional Memories

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 6418))

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.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Bloom, B.H.: Space/time trade-offs in hash coding with allowable errors. Communications of the ACM 13(7), 422–426 (1970)

    Article  MATH  Google Scholar 

  2. Minh, C.C., Chung, J., Kozyrakis, C., Olukotun, K.: STAMP: Stanford transactional applications for multi-processing. In: Proceedings of The IEEE International Symposium on Workload Characterization (September 2008)

    Google Scholar 

  3. Chen, K., Malik, S., Patra, P.: Runtime validation of transactional memory systems. In: International Symposium on Quality Electronic Design, pp. 750–756 (2008)

    Google Scholar 

  4. Cohen, A., O’Leary, J., Pnueli, A., Tuttle, M.R., Zuck, L.: Verifying correctness of transactional memories. In: International Conference on Fomal Methods in Computer Aided Design, pp. 37–44. IEEE Computer Society, Los Alamitos (2007)

    Google Scholar 

  5. Cohen, A., Pnueli, A., Zuck, L.D.: Mechanical verification of transactional memories with non-transactional memory accesses. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 121–134. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  6. Dice, D., Shalev, O., Shavit, N.N.: Transactional locking II. In: Dolev, S. (ed.) DISC 2006. LNCS, vol. 4167, pp. 194–208. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  7. Elmas, T., Qadeer, S., Tasiran, S.: Goldilocks: A race and transaction-aware Java runtime. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 245–255 (2007)

    Google Scholar 

  8. Farzan, A., Madhusudan, P.: Monitoring atomicity in concurrent programs. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 52–65. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  9. Flanagan, C., Freund, S.N.: Atomizer: A dynamic atomicity checker for multithreaded programs. In: ACM SIGPLAN Symposium on Principles of Programming Languages, pp. 256–267 (2004)

    Google Scholar 

  10. Flanagan, C., Freund, S.N.: FastTrack: Efficient and precise dynamic race detection. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 121–133 (2009)

    Google Scholar 

  11. Flanagan, C., Freund, S.N., Yi, J.: Velodrome: A sound and complete dynamic atomicity checker for multithreaded programs. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 293–303 (2008)

    Google Scholar 

  12. Guerraoui, R., Henzinger, T.A., Jobstmann, B., Singh, V.: Model checking transactional memories. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 372–382. ACM, New York (2008)

    Google Scholar 

  13. Guerraoui, R., Henzinger, T.A., Singh, V.: Nondeterminism and completeness in model checking transactional memories. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 21–35. Springer, Heidelberg (2000)

    Google Scholar 

  14. Guerraoui, R., Henzinger, T.A., Singh, V.: Software transactional memory on relaxed memory models. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 321–336. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  15. Guerraoui, R., Kapałka, M.: On the correctness of transactional memory. In: ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, pp. 175–184. ACM, New York (2008)

    Google Scholar 

  16. Hadzilacos, T., Yannakakis, M.: Deleting completed transactions. In: ACM SIGACT-SIGMOD Symposium on Principles of Database Systems, pp. 43–46 (1986)

    Google Scholar 

  17. Herlihy, M., Luchangco, V., Moir, M., Scherer, W.N.: Software transactional memory for dynamic-sized data structures. In: ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing, pp. 92–101. ACM, New York (2003)

    Google Scholar 

  18. Herlihy, M., Moss, J.E.B.: Transactional memory: Architectural support for lock-free data structures. In: International Symposium on Computer Architecture, pp. 289–300. ACM, New York (1993)

    Google Scholar 

  19. Manovit, C., Hangal, S., Chafi, H., McDonald, A., Kozyrakis, C., Olukotun, K.: Testing implementations of transactional memory. In: International Conference on Parallel Architectures and Compilation Techniques, pp. 134–143 (2006)

    Google Scholar 

  20. Papadimitriou, C.H.: The serializability of concurrent database updates. Journal of the ACM 26(4) (1979)

    Google Scholar 

  21. Savage, S., Burrows, M., Nelson, G., Sobalvarro, P., Anderson, T.E.: Eraser: A dynamic data race detector for multithreaded programs. ACM Trans. Comput. Syst. 15(4), 391–411 (1997)

    Article  Google Scholar 

  22. Scott, M.L.: Sequential specification of transactional memory semantics. In: ACM SIGPLAN Workshop on Transactional Computing (2006)

    Google Scholar 

  23. Shavit, N., Touitou, D.: Software transactional memory. In: ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing, pp. 204–213. ACM, New York (1995)

    Google Scholar 

  24. Tasiran, S.: A compositional method for verifying software transactional memory implementations. Technical Report MSR-TR-2008-56, Microsoft Research (2008)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Science and Technology, Austria

    Vasu Singh

Authors
  1. Vasu Singh
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Computer Science, University of Manchester, Kilburn Building, Oxford Road, M13 9PL, Manchester, UK

    Howard Barringer

  2. INRIA, Rennes - Bretagne Atlantique, France

    Ylies Falcone

  3. Department of Computer Science, Saarland University, 66123, Saarbrücken, Germany

    Bernd Finkbeiner

  4. Jet Propulsion Laboratory, M/S 3041-285, 4800 Oak Grove Drive, 91109, Pasadena, CA, USA

    Klaus Havelund

  5. PRECISE Center, Department of Computer and Information Science, University of Pennsylvania, 19104, Philadelphia, PA, USA

    Insup Lee  & Oleg Sokolsky  & 

  6. Department of Computer Science, University of Malta, MSD 06, Msida, Malta

    Gordon Pace

  7. Department of Computer Science, University of Illinois at Urbana-Champaign, 201 N. Goodwin, 61801, Urbana, IL, USA

    Grigore Roşu

  8. Microsoft Research,, One Microsoft Way, 98052, Redmond, WA, USA

    Nikolai Tillmann

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Singh, V. (2010). Runtime Verification for Software Transactional Memories. In: Barringer, H., et al. Runtime Verification. RV 2010. Lecture Notes in Computer Science, vol 6418. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16612-9_32

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-16612-9_32

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-16611-2

  • Online ISBN: 978-3-642-16612-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation