{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,20]],"date-time":"2026-08-20T14:48:16Z","timestamp":1787237296560,"version":"build-2736575974"},"reference-count":38,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[2013,9,1]],"date-time":"2013-09-01T00:00:00Z","timestamp":1377993600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2013,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>Over the last decade, great progress has been made in developing practical transactional memory (TM) implementations, but relatively little attention has been paid to precisely specifying what it means for them to be correct, or formally proving that they are. In this paper, we present TMS1 (Transactional Memory Specification 1), a precise specification of correct behaviour of a TM runtime library. TMS1 targets TM runtimes used to implement transactional features in an unmanaged programming language such as C or C++. In such contexts, even transactions that ultimately abort must observe consistent states of memory; otherwise, unrecoverable errors such as divide-by-zero may occur before a transaction aborts, even in a correct program in which the error would not be possible if transactions were executed atomically. We specify TMS1 precisely using an I\/O automaton (IOA). This approach enables us to also model TM implementations using IOAs and to construct fully formal and machine-checked correctness proofs for them using well established proof techniques and tools. We outline key requirements for a TM system. To avoid precluding any implementation that satisfies these requirements, we specify TMS1 to be as general as we can, consistent with these requirements. The cost of such generality is that the condition does not map closely to intuition about common TM implementation techniques, and thus it is difficult to prove that such implementations satisfy the condition. To address this concern, we present TMS2, a more restrictive condition that more closely reflects intuition about common TM implementation techniques. We present a simulation proof that TMS2 implements TMS1, thus showing that to prove that an implementation satisfies TMS1, it suffices to prove that it satisfies TMS2. We have formalised and verified this proof using the PVS specification and verification system.<\/jats:p>","DOI":"10.1007\/s00165-012-0225-8","type":"journal-article","created":{"date-parts":[[2012,3,17]],"date-time":"2012-03-17T13:50:48Z","timestamp":1331992248000},"page":"769-799","source":"Crossref","is-referenced-by-count":53,"title":["Towards formally specifying and verifying transactional memory"],"prefix":"10.1145","volume":"25","author":[{"given":"Simon","family":"Doherty","sequence":"first","affiliation":[{"name":"School of Engineering and Computer Science, Victoria University of Wellington, Wellington, New Zealand"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lindsay","family":"Groves","sequence":"additional","affiliation":[{"name":"School of Engineering and Computer Science, Victoria University of Wellington, Wellington, New Zealand"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Victor","family":"Luchangco","sequence":"additional","affiliation":[{"name":"Oracle Labs, Burlington, MA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mark","family":"Moir","sequence":"additional","affiliation":[{"name":"Oracle Labs, Burlington, MA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","unstructured":"Aydonat U Abdelrahmen T (2008) Serializability of transactions in software transactional memory. In: 3rd ACM workshop on transactional computing (TRANSACT)"},{"issue":"1","key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","first-page":"2:1","DOI":"10.1145\/1889997.1889999","article-title":"Semantics of transactional memory and automatic mutual exclusion","volume":"33","author":"Abadi M","year":"2011","journal-title":"ACM Trans Program Lang Syst"},{"key":"e_1_2_1_2_3_2","unstructured":"Adl-Tabatabai A-R Shpeisman T (eds) (2009) Draft specification of transactional language constructs for C++ version 1.0. http:\/\/labs.oracle.com\/scalable\/pubs\/C++-transactional-constructs-1.0.pdf"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Colvin R Doherty S Groves L (2005) Verifying concurrent data structures by simulation. In: Boiten E Derrick J (eds) Proceedings of the refineNet workshop (REFINE). Electronic notes in theoretical computer science. Guildford UK","DOI":"10.1016\/j.entcs.2005.04.026"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Colvin R Groves L Luchangco V Moir M (2006) Formal verification of a lazy concurrent list-based set\u00a0algorithm. In: Proceedings of the 18th international conference on computer aided verification (CAV) pp 475\u2013488","DOI":"10.1007\/11817963_44"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Cohen A O\u2019Leary JW Pnueli A Tuttle MR Zuck LD (2007) Verifying correctness of transactional memories. In: Proceedings of the formal methods in computer aided design (FMCAD) pp 37\u201344","DOI":"10.1109\/FAMCAD.2007.40"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Cohen A Pnueli A Zuck LD (2008) Mechanical verification of transactional memories with non-transactional memory accesses. In: Proceedings of the 20th international conference on computer aided verification (CAV) pp 121\u2013134","DOI":"10.1007\/978-3-540-70545-1_13"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Doherty S Groves L Luchangco V Moir M (2004) Formal verification of a practical lock-free queue algorithm. In: Proceedings of the international conference on formal techniques for networked and distributed systems (FORTE) pp 97\u2013114","DOI":"10.1007\/978-3-540-30232-2_7"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Doherty S Groves L Luchangco V Moir M (2009) Towards formally specifying and verifying transactional memory. In: Proceedings of the refineNet workshop (REFINE). Electronic notes in theoretical computer science. http:\/\/labs.oracle.com\/scalable\/pubs\/Refine09-TM-correctness.pdf","DOI":"10.1016\/j.entcs.2010.01.001"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Doherty S Moir M (2009) Nonblocking algorithms and backward simulation. In: Proceedings of 23rd international conference on distributed computing (DISC)","DOI":"10.1007\/978-3-642-04355-0_28"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Dice D Shalev O Shavit N (2006) Transactional locking II. In: Proceedings of the international conference on distributed computing (DISC) pp 194\u2013208","DOI":"10.1007\/11864219_14"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Dalessandro L Spear MF Scott ML (2010) NOrec: streamlining STM by abolishing ownership records. In: Proceedings of the 15th ACM SIGPLAN symposium on principles and practice of parallel programming (PPoPP) pp 67\u201378","DOI":"10.1145\/1837853.1693464"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Guerraoui R Henzinger TA Jobstmann B Singh V (2008) Model checking transactional memories. In: Proceedings of the 2008 ACM SIGPLAN conference on programming language design and implementation (PLDI) pp 372\u2013382","DOI":"10.1145\/1379022.1375626"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Guerraoui R Henzinger TA Singh V (2008) Completeness and nondeterminism in model checking transactional memories. In: Proceedings of the 19th international conference on concurrency theory (CONCUR) pp 21\u201335","DOI":"10.1007\/978-3-540-85361-9_6"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Guerraoui R Henzinger TA Singh V (2009) Software transactional memory on relaxed memory models. In: Proceedings of the 21st international conference on computer aided verification (CAV) pp 321\u2013336","DOI":"10.1007\/978-3-642-02658-4_26"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Guerraoui R Kapalka M (2008) On the correctness of transactional memory. In: Proceedings of the 13th ACM SIGPLAN symposium on principles and practice of parallel programming (PPoPP) pp 175\u2013184","DOI":"10.1145\/1345206.1345233"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Guerraoui R Kapa\u0142ka M (2010) Principles of Transactional Memory. Synthesis Lectures on Distributed Computing Theory. Morgan Claypool USA","DOI":"10.2200\/S00253ED1V01Y201009DCT004"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Herlihy M Koskinen E (2008) Transactional boosting: a methodology for highly-concurrent transactional objects. In: Proceedings of the 13th ACM SIGPLAN symposium on principles and practice of parallel programming (PPoPP) pp 207\u2013216","DOI":"10.1145\/1345206.1345237"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Herlihy M Moss JEB (1993) Transactional memory: architectural support for lock-free data structures. In: Proceedings of the 20th annual international symposium on computer architecture (ISCA)","DOI":"10.1145\/165123.165164"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Hoare CAR (1972) Towards a theory of parallel programming. In: Operating systems techniques. Academic Press New York pp 61\u201371","DOI":"10.1007\/978-1-4757-3472-0_6"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Hudson RL Saha B Adl-Tabatabai A-R Hertzberg BC (2006) McRT-Malloc: a scalable transactional memory allocator. In: Proceedings of the 5th international symposium on memory management (ISMM) pp 74\u201383","DOI":"10.1145\/1133956.1133967"},{"key":"e_1_2_1_2_22_2","unstructured":"Imbs D de Mend\u00edvil J Raynal M (2008) On the consistency conditions of transactional memories. Technical Report 1917 Institut de Recherche en Informatique et Syst\u00e8mes Aal\u00e1toires"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Imbs D de Mend\u00edvil J Raynal M (2009) Brief announcement: virtual world consistency a new condition for STM systems. In: Proceedings of the 2009 ACM symposium on principles of distributed computing (PODC) pp 280\u2013281","DOI":"10.1145\/1582716.1582764"},{"key":"e_1_2_1_2_24_2","unstructured":"Lev Y Luchangco V Marathe VJ Moir M Nussbaum D Olszewski M (2009) Anatomy of a scalable software transactional memory. In: 4th ACM SIGPLAN workshop on transactional computing (TRANSACT)"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Lynch N Tuttle M (1987) Hierarchical correctness proofs for distributed algorithms. In: Proceedings of the 6th annual ACM symposium on principles of distributed computing (PODC) pp 137\u2013151","DOI":"10.1145\/41840.41852"},{"key":"e_1_2_1_2_26_2","first-page":"219","article-title":"An introduction to input\/output automata","volume":"2","author":"Lynch NA","year":"1989","journal-title":"CWI Q"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1134"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Moore KF Grossman D (2008) High-level small step operational semantics for transactions. In: Proceedings of the 35th annual ACM symposium on principles of prgoramming languages (POPL)","DOI":"10.1145\/1328438.1328448"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2006.05.010"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268134"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"O\u2019Leary J Saha B Tuttle MR (2009) Model checking transactional memory with Spin. In: Proceedings of the 29th IEEE international conference on distributed computing systems (ICDCS) pp 335\u2013342","DOI":"10.1109\/ICDCS.2009.72"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/322154.322158"},{"key":"e_1_2_1_2_33_2","unstructured":"The PVS specification and verification system. http:\/\/pvs.csl.sri.com\/"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"crossref","unstructured":"Ramadan HE Roy I Witchel E (2008) Dependence-aware transactional memory for increased concurrency. In: Proceedings of the 41st annual IEEE\/ACM international symposium on microarchitecture pp 246\u2013257","DOI":"10.1109\/MICRO.2008.4771795"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"crossref","unstructured":"Saha B Adl-Tabatabai A-R Hudson RL Minh CC Hertzberg B (2006) McRT-STM: a high performance software transactional memory system for a multi-core runtime. In: Proceedings of the 11th ACM SIGPLAN symposium on principles and practice of parallel programming (PPoPP) pp 187\u2013197","DOI":"10.1145\/1122971.1123001"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"crossref","unstructured":"Schneider F (1992) Introduction special issue: specification of concurrent systems. Distrib Comput 6(1)","DOI":"10.1007\/BF02276637"},{"key":"e_1_2_1_2_37_2","unstructured":"Scott ML (2006) Sequential specification of transactional memory semantics. In: 1st ACM SIGPLAN workshop on languages compilers and hardware support for transactional computing (TRANSACT)"},{"key":"e_1_2_1_2_38_2","unstructured":"SkySTM Interest Google Group (2009). http:\/\/groups.google.com\/group\/skystm-interest"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-012-0225-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-012-0225-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-012-0225-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T10:58:34Z","timestamp":1641466714000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-012-0225-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,9]]},"references-count":38,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2013,9]]}},"alternative-id":["10.1007\/s00165-012-0225-8"],"URL":"https:\/\/doi.org\/10.1007\/s00165-012-0225-8","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,9]]}}}