{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,2]],"date-time":"2022-04-02T21:07:37Z","timestamp":1648933657570},"reference-count":84,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2013,5,1]],"date-time":"2013-05-01T00:00:00Z","timestamp":1367366400000},"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,5]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            The issues surrounding the question of atomicity, both in the past and nowadays, are briefly reviewed, and a picture of an ACID (atomic, consistent, isolated, durable) transaction as a refinement problem is presented. An example of a simple air traffic control system is introduced, and the discrepancies that can arise when read-only operations examine the state at atomic and finegrained levels are handled by retrenchment. Non-ACID timing aspects of the ATC example are also handled by retrenchment, and the treatment is generalised to yield the Retrenchment\n            <jats:italic>Atomicity Pattern<\/jats:italic>\n            . The utility of the pattern is confirmed against a number of different case studies. One is the Mondex Electronic Purse, its protocol treated as a conventional atomic transaction. Another is the recovery protocol of Mondex, viewed as a compensated transaction (leading to the view that compensated transactions in general fit the pattern). A final one comprises various unruly phenomena occurring in the implementations of software transactional memory systems, which can frequently display non-ACID behaviour. In all cases the\n            <jats:italic>Atomicity Pattern<\/jats:italic>\n            is seen to perform well.\n          <\/jats:p>","DOI":"10.1007\/s00165-011-0216-1","type":"journal-article","created":{"date-parts":[[2011,11,25]],"date-time":"2011-11-25T09:59:26Z","timestamp":1322215166000},"page":"439-464","source":"Crossref","is-referenced-by-count":1,"title":["Atomicity failure and the retrenchment atomicity pattern"],"prefix":"10.1145","volume":"25","author":[{"given":"Richard","family":"Banach","sequence":"first","affiliation":[{"name":"School of Computer Science, University of Manchester, Oxford Road, M13 9PL, Manchester, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Czes\u0142aw","family":"Jeske","sequence":"additional","affiliation":[{"name":"School of Computer Science, University of Manchester, Oxford Road, M13 9PL, Manchester, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anthony","family":"Hall","sequence":"additional","affiliation":[{"name":"Independent Consultant, Oxford, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Susan","family":"Stepney","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of York, YO10 5DD, Heslington, York, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Abadi M Birrell A Harris T Isard M (2008) Semantics of transactional memory and automatic mutual exclusion. In: Proceedings of POPL 2008","DOI":"10.1145\/1328438.1328449"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Abrial J-R (2003) Event based sequential program development: application to constructing a pointer program. In: Araki et\u00a0al. [AGM03] pp 51\u201374","DOI":"10.1007\/978-3-540-45236-2_5"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Abrial J-R Cansell D M\u00e9ry D (2005) Refinement and reachability in event-B. In: Proceedings of ZB 2005. LNCS vol 3455 pp 222\u2013241","DOI":"10.1007\/11415787_14"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Araki K Gnesi S Mandrioli D (2003) International symposium of formal methods Europe. LNCS vol. 2805 Pisa Italy. Springer Berlin","DOI":"10.1007\/b13229"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Abadi M Harris T Mehrara M (2009) Transactional memory with strong atomicity using off-the-shelf memory protection hardware. In: Proceedings of PPoPP 2009","DOI":"10.1145\/1504176.1504203"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.5555\/578092"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Banach R (2009) Coarse grained retrenchment and the mondex denial of service attacks. In: Proceedings of IEEE TASE-09 York. IEEE Computer Society Press Los Angeles","DOI":"10.1109\/TASE.2009.19"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Bruni R Butler M Ferreira C Hoare T Melgratti H Montanari U (2005) Comparing two approaches to compensable flow composition. In: Proceedings of CONCUR 2005","DOI":"10.1007\/11539452_30"},{"key":"e_1_2_1_2_9_2","first-page":"743","article-title":"Extending the concept of transaction compensation","volume":"47","author":"Butler M","year":"2002","journal-title":"IBM Syst J"},{"key":"e_1_2_1_2_10_2","first-page":"712","article-title":"Precise modelling of compensating business transactions and its application to BPEL","volume":"11","author":"Butler M","year":"2005","journal-title":"J UCS"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Butler M Hoare T Ferreira C (2004) A trace semantics for long-running transactions. In: 25\u00a0years of CSP July 2004","DOI":"10.1007\/11423348_8"},{"key":"e_1_2_1_2_12_2","unstructured":"Bernstein P Hadzilacos V Goodman N (1987) Concurrency control and recovery in database systems. Addison-Wesley Reading"},{"key":"e_1_2_1_2_13_2","unstructured":"Banach R Jeske C (2009) Retrenchment and refinement interworking: the tower theorems. Available at [RET]"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2007.11.001"},{"key":"e_1_2_1_2_15_2","first-page":"29","article-title":"Retrenching the purse: the balance enquiry quandary, and generalised and (1,1) forward refinements","volume":"77","author":"Banach R","year":"2007","journal-title":"Fund Inf"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Back RJR Kurki-Suonio R (1983) Decentralisation of process nets with centralised control. In: 2nd ACM SIGACT-SIGOPS symposium on principles of distributed computing pp 131\u2013142","DOI":"10.1145\/800221.806716"},{"key":"e_1_2_1_2_17_2","volume-title":"Transaction processing","author":"Bernstein PA","year":"1997"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-003-0012-7"},{"key":"e_1_2_1_2_19_2","unstructured":"Banach R Poppleton M (2000) Fragmented retrenchment concurrency and fairness. In: Proceedings of IEEE ICFEM2000 York. IEEE Computer Society Press Los Angeles pp 143\u2013151"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00766-002-0157-6"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Banach R Poppleton M Jeske C Stepney S. Retrenching the purse: finite sequence numbers and the tower pattern. In: FM 2005. LNCS vol 3582. Springer Berlin pp 382\u2013398","DOI":"10.1007\/11526841_26"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Banach R Poppleton M Jeske C Stepney S (2006) Retrenching the purse: finite exception logs and validating the small. In: IEEE\/NASA Software Engineering Workshop 30 2006. IEEE Computer Society Press Los Angeles pp 234\u2013245","DOI":"10.1109\/SEW.2006.28"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Banach R Poppleton M Jeske C Stepney S (2006) Retrenching the purse: hashing injective CLEAR codes and security properties. In: 2nd IEEE international symposium on leveraging applications of formal methods verification and validation 2006. IEEE Computer Society Press Los Angeles pp 82\u201390","DOI":"10.1109\/ISoLA.2006.17"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.04.002"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-18216-7","volume-title":"Abstract state machines. In: A method for high level system design and analysis","author":"B\u00f6rger E","year":"2003"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-009-0103-1"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"publisher","DOI":"10.5555\/1349891.1350068"},{"key":"e_1_2_1_2_28_2","volume-title":"Database systems: a practical approach to design, implementation and management","author":"Connolly T","year":"2004"},{"key":"e_1_2_1_2_29_2","volume-title":"Distributed systems: concepts and design","author":"Coulouris G","year":"2005"},{"key":"e_1_2_1_2_30_2","unstructured":"Cooper D Stepney S Woodcock J (2002) Derivation of Z refinement proof rules. Technical report YCS-2002-347 University of York"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"publisher","DOI":"10.5555\/379171"},{"key":"e_1_2_1_2_32_2","unstructured":"Department of Trade and Industry (1991) Information technology security evaluation criteria. http:\/\/www.cesg.gov.uk\/site\/iacs\/itsec\/media\/formal-docs\/Itsec.pdf"},{"key":"e_1_2_1_2_33_2","unstructured":"Dalessandro L Scott M (2009) Strong isolation is a weak idea. In: Proceedings of Transaction 2009"},{"key":"e_1_2_1_2_34_2","unstructured":"Eder J Liebhart W (1997) Workflow transactions. In: Workflow Handbook. Wiley New York pp 157\u2013163"},{"key":"e_1_2_1_2_35_2","volume-title":"Fundamentals of database systems","author":"Elmasri R","year":"2003"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"crossref","unstructured":"Francez N Forman I (1990) Superimposition for interactive processes. In: Proceedings of CONCUR 1990. LNCS vol 458. Springer Berlin pp 230\u2013245","DOI":"10.1007\/BFb0039063"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"crossref","unstructured":"Gore M Ghosh R (1999) Recovery in distributed extended long-lived transaction models. In: Proceedings of sixth international conference on database systems for advanced applications. IEEE Computer Society Los Angeles pp 313\u2013320","DOI":"10.1109\/DASFAA.1999.765765"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-007-0054-3"},{"key":"e_1_2_1_2_39_2","volume-title":"Database systems: the complete book","author":"Garcia-Molina H","year":"2003"},{"key":"e_1_2_1_2_40_2","volume-title":"Transaction processing","author":"Gray J","year":"1993"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"publisher","DOI":"10.1109\/52.506463"},{"key":"e_1_2_1_2_42_2","volume-title":"Operating systems: concurrent and distributed software design","author":"Harris T","year":"2003"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"crossref","unstructured":"Harris T Fraser K (2003) Language support for lightweight transactions. In: Proceedings of OOPSLA 2003","DOI":"10.1145\/949305.949340"},{"key":"e_1_2_1_2_44_2","unstructured":"Haxthausen AE George C Sch\u00fctz M (2006) Specification and proof of the Mondex electronic purse. In: Proceedings of 1st asian working conference on verified software AWCVS\u201906 UNU-IIST reports 348 Macau"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"crossref","unstructured":"Herlihy M Moss E (1993) Transactional memory: architectural support for lock-free data structures. In: Proceedings of 20th ISCA pp 289\u2013300","DOI":"10.1145\/173682.165164"},{"key":"e_1_2_1_2_46_2","doi-asserted-by":"crossref","unstructured":"Harris T Marlow S Peyton-Jones S Herlihy M (2005) Composable memory transactions. In: Proceedings of PPoPP 2005","DOI":"10.1145\/1065944.1065952"},{"key":"e_1_2_1_2_47_2","doi-asserted-by":"crossref","unstructured":"Harris T Plesko M Shinnar A Tarditi D (2006) Optimizing memory transactions. In: Proceedings of PLDI 2006 pp 14\u201325","DOI":"10.1145\/1133255.1133984"},{"key":"e_1_2_1_2_48_2","doi-asserted-by":"crossref","unstructured":"Hammond L Wong V Chen M Carlstrom B Davis J Hertzberg B Prabhu Ma Wijaya H Kozyrakis C Olukotun K (2004) Transactional memory coherence and consistency. In: Proceedings of 31st ISCA","DOI":"10.1145\/1028176.1006711"},{"key":"e_1_2_1_2_49_2","unstructured":"Isard M Birrell A (2007) Automatic mutual exclusion. In: Proceedings of workshop on hot topics in operating systems 2007"},{"key":"e_1_2_1_2_50_2","unstructured":"ISO\/IEC 13568 (2002) Information Technology\u2014Z Formal specification notation\u2014Syntax type system and semantics: international standard. http:\/\/www.iso.org\/iso\/en\/ittf\/PubliclyAvailableStandards\/c021573_ISO_IEC_13568_2002(E).zip"},{"key":"e_1_2_1_2_51_2","unstructured":"Jeske C (2005) Algebraic integration of retrenchment and refinement. PhD thesis University of Manchester"},{"key":"e_1_2_1_2_52_2","doi-asserted-by":"publisher","DOI":"10.5555\/549927"},{"key":"e_1_2_1_2_53_2","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2006.145"},{"key":"e_1_2_1_2_54_2","doi-asserted-by":"crossref","unstructured":"Jones C Woodcock J (eds)(2008) Special issue on the Mondex verification. Form Asp Comp 20(1): 1\u2013139","DOI":"10.1007\/s00165-007-0064-1"},{"key":"e_1_2_1_2_55_2","doi-asserted-by":"publisher","DOI":"10.1145\/169701.169682"},{"key":"e_1_2_1_2_56_2","doi-asserted-by":"crossref","unstructured":"Khan B Horsnell M Rogers I Luj\u00e1n M Dinn A Watson I (2008) An object-aware hardware transactional memory. In: Proceedings of ICHPCC pp 51\u201358","DOI":"10.1145\/1378533.1378552"},{"key":"e_1_2_1_2_57_2","volume-title":"Atomic transactions","author":"Lynch N","year":"1994"},{"key":"e_1_2_1_2_58_2","doi-asserted-by":"publisher","DOI":"10.5555\/983350"},{"key":"e_1_2_1_2_59_2","doi-asserted-by":"crossref","unstructured":"Larus J Rajwar R (2006) Transactional memory. Morgan and Claypool","DOI":"10.2200\/S00070ED1V01Y200611CAC002"},{"key":"e_1_2_1_2_60_2","volume-title":"Distributed algorithms","author":"Lynch N","year":"1996"},{"key":"e_1_2_1_2_61_2","doi-asserted-by":"crossref","unstructured":"Menon V Balensiefer S Shpeisman T Adl-Tabatabai A-R Hudson R Saha B Welc A (2008) Practical weak-atomicity semantics for Java STM. In: Proceedings of SPAA 2008","DOI":"10.1145\/1378533.1378588"},{"key":"e_1_2_1_2_62_2","volume-title":"Web services: principles and technology","author":"Papazoglou M","year":"2007"},{"key":"e_1_2_1_2_63_2","doi-asserted-by":"crossref","unstructured":"Poppleton M Banach R (2003) Structuring retrenchments in B by Decomposition. In: Araki et\u00a0al. [AGM03] pp 814\u2013833","DOI":"10.1007\/978-3-540-45236-2_44"},{"key":"e_1_2_1_2_64_2","doi-asserted-by":"publisher","DOI":"10.5555\/49077"},{"key":"e_1_2_1_2_65_2","unstructured":"Retrenchment Homepage. http:\/\/www.cs.man.ac.uk\/retrenchment"},{"key":"e_1_2_1_2_66_2","doi-asserted-by":"crossref","unstructured":"Rajwar R Goodman J (2002) Transactional lock-free execution of lock-based programs. In: Proceedings of 10th SASPLO pp 5\u201317","DOI":"10.1145\/605432.605399"},{"key":"e_1_2_1_2_67_2","doi-asserted-by":"crossref","unstructured":"Ramadan H Rossbach C Porter D Hofmann Ow Bhandari A Witchel E (2007) MetaTM\/TxLinux: transactional memory for an operating system. In: Proceedings of 34th ISCA pp 92\u2013103","DOI":"10.1145\/1273440.1250675"},{"key":"e_1_2_1_2_68_2","volume-title":"Operating system concepts","author":"Silberschatz A","year":"2005"},{"key":"e_1_2_1_2_69_2","first-page":"952","article-title":"Verification of ASM refinements using generalized forward simulation","volume":"7","author":"Schellhorn G","year":"2001","journal-title":"JUCS"},{"key":"e_1_2_1_2_70_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.11.013"},{"key":"e_1_2_1_2_71_2","unstructured":"Stepney S Cooper D Woodcock J (2000) An electronic purse: specification refinement and proof. Technical report PRG-126 Oxford University Computing Laboratory"},{"key":"e_1_2_1_2_72_2","unstructured":"Schellhorn G Grandy H Haneberg D Moebius N Reif W (2007) A systematic verification approach for Mondex electronic purses using ASMs. In: Proceedings of Dagstuhl workshop on rigorous methods for software construction and analysis 2007. LNCS. Springer Berlin"},{"key":"e_1_2_1_2_73_2","doi-asserted-by":"crossref","unstructured":"Schellhorn G Grandy H Haneberg D Reif W (2006) The Mondex challenge: machine checked proofs for an electronic purse. In: Proceedings of FM 2006 LNCS vol 4085. Springer Berlin pp 16\u201331","DOI":"10.1007\/11813040_2"},{"key":"e_1_2_1_2_74_2","doi-asserted-by":"crossref","unstructured":"Salem K Garcia-Molina H Alonso R (1989) Altruistic locking: a strategy for coping with long lived transactions. In: Proceedings of second international workshop on high performance transaction systems. LNCS vol 359. Springer Berlin pp 175\u2013199","DOI":"10.1007\/3-540-51085-0_47"},{"key":"e_1_2_1_2_75_2","doi-asserted-by":"crossref","unstructured":"Shpeisman T Menon V Adl-Tabatabai A-R Balensiefer S Grossman D Hudson R Moore K Saha B (2007) Enforcing isolation and ordering in STM. In: Proceedings of PLDI 2007","DOI":"10.1145\/1250734.1250744"},{"key":"e_1_2_1_2_76_2","volume-title":"The Z notation: a reference manual","author":"Spivey JM","year":"1992","edition":"2"},{"issue":"5","key":"e_1_2_1_2_77_2","first-page":"661","article-title":"The verification grand challenge","volume":"13","author":"Woodcock J","year":"2007","journal-title":"JUCS"},{"key":"e_1_2_1_2_78_2","volume-title":"Using Z: specification, refinement and proof","author":"Woodcock J","year":"1996"},{"key":"e_1_2_1_2_79_2","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2006.340"},{"key":"e_1_2_1_2_80_2","unstructured":"Web Services Org. http:\/\/www.webservices.org\/"},{"key":"e_1_2_1_2_81_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-007-0060-5"},{"key":"e_1_2_1_2_82_2","volume-title":"Transaction processing","author":"Weikum G","year":"2002"},{"key":"e_1_2_1_2_83_2","doi-asserted-by":"crossref","unstructured":"Yen L Bobba J Marty M Moore K Volos H Hill M Swift M Wood D (2007) LogTM-SE: decoupling hardware transactional memory from caches. In: Proceedings of 13th ISHPCA","DOI":"10.1109\/HPCA.2007.346204"},{"key":"e_1_2_1_2_84_2","doi-asserted-by":"publisher","DOI":"10.5555\/861530"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-011-0216-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-011-0216-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-011-0216-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:53:01Z","timestamp":1641484381000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-011-0216-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,5]]},"references-count":84,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2013,5]]}},"alternative-id":["10.1007\/s00165-011-0216-1"],"URL":"https:\/\/doi.org\/10.1007\/s00165-011-0216-1","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,5]]}}}