Abstract
Transactional memory is a programming abstraction intended to simplify the synchronization of conflicting memory accesses (by concurrent threads) without the difficulties associated with locks. In a previous work we presented a formal framework for proving that a transactional memory implementation satisfies its specifications and provided with model checking verification of some using small instantiations. This paper extends the previous work to capture non-transactional accesses to memory, which occurs, for example, when using legacy code. We provide a mechanical proof of the soundness of the verification method, as well as a mechanical verification of a version of the popular tcc implementation that includes non-transactional memory accesses. The verification is performed by the deductive temporal checker tlpvs.
This research was supported in part by ONR grant N00014-99-1-0131 and NSF grants CCF-0742686 and CNS-0720525.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abadi, M., Lamport, L.: The existence of refinement mappings. Theoretical Computer Science 82(2), 253–284 (1991)
Cohen, A., Pnueli, A., Zuck, L.D.: Verification of transactional memories that support non-transactional memory accesses. In: TRANSACT 2008 (February 2008)
Cohen, A., O’Leary, J.W., Pnueli, A., Tuttle, M.R., Zuck, L.D.: Verifying correctness of transactional memories. In: Proceedings of the 7th International Conference on Formal Methods in Computer-Aided Design (FMCAD), November 2007, pp. 37–44 (2007)
Hammond, L., Wong, W., Chen, M., Carlstrom, B.D., Davis, J.D., Herzberg, B., Prabhu, M.K., Wijaya, H., Kozyrakis, C., Olukotun, K.: Transactional memory coherence and consistency. In: Proc. 31st annu. Int. Symp. on COmputer Architecture, p. 102. IEEE Computer Society, Los Alamitos (2004)
Herlihy, M., Moss, J.E.B.: Transactional memory: architectural support for lock-free data structures. In: ISCA 1993: Proceedings of the 20th annual international symposium on Computer architecture, San Diego, California, United States, pp. 289–300. ACM Press, New York (1993)
Kesten, Y., Pnueli, A.: Verification by augmented finitary abstraction. Inf. Comput. 163(1), 203–243 (2000)
Kesten, Y., Pnueli, A., Shahar, E., Zuck, L.D.: Network invariants in action. In: Brim, L., Jančar, P., Křetínský, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 101–115. Springer, Heidelberg (2002)
Lamport, L.: Specifying Systems: The TLA + Language and Tools for Hardware and Software Engineers. Addison-Wesley, Reading (2002)
Larus, J.R., Rajwar, R.: Transactional Memory. Morgan & Claypool Publishers (2007)
Owre, S., Shankar, N., Rushby, J.M., Stringer-Calvert, D.W.J.: PVS System Guide. Computer Science Laboratory, SRI International, Menlo Park, CA (September 1999)
Pnueli, A., Arons, T.: Tlpvs: A pvs-based ltl verification system. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol. 2772, pp. 596–625. Springer, Heidelberg (2004)
Scott, M.L.: Sequential specification of transactional memory semantics. In: Proc. TRANSACT the First ACM SIGPLAN Workshop on Languages, Compiler, and Hardware Suppport for Transactional Computing, Ottawa (2006)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cohen, A., Pnueli, A., Zuck, L.D. (2008). Mechanical Verification of Transactional Memories with Non-transactional Memory Accesses. In: Gupta, A., Malik, S. (eds) Computer Aided Verification. CAV 2008. Lecture Notes in Computer Science, vol 5123. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-70545-1_13
Download citation
DOI: https://doi.org/10.1007/978-3-540-70545-1_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-70543-7
Online ISBN: 978-3-540-70545-1
eBook Packages: Computer ScienceComputer Science (R0)