Cited By
View all- Börger ESchewe K(2016)Concurrent abstract state machinesActa Informatica10.1007/s00236-015-0249-753:5(469-492)Online publication date: 1-Aug-2016
Atomicity failure and the retrenchment atomicity pattern
Pages 439 - 464
Abstract
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 Atomicity Pattern. 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 Atomicity Pattern is seen to perform well.
References
References
[1]
Abadi M, Birrell A, Harris T, Isard M (2008) Semantics of transactional memory and automatic mutual exclusion. In: Proceedings of POPL 2008
[2]
Abrial J-R (2003) Event based sequential program development: application to constructing a pointer program. In: Araki et al. [AGM03], pp 51–74
[3]
Abrial J-R, Cansell D, Méry D (2005) Refinement and reachability in event-B. In: Proceedings of ZB 2005. LNCS, vol 3455, pp 222–241
[4]
Araki K, Gnesi S, Mandrioli D (2003) International symposium of formal methods Europe. LNCS, vol. 2805, Pisa, Italy. Springer, Berlin
[5]
Abadi M, Harris T, Mehrara M (2009) Transactional memory with strong atomicity using off-the-shelf memory protection hardware. In: Proceedings of PPoPP 2009
[6]
Ben-Ari M Principles of concurrent programming 1982 Englewood Cliffs Prentice Hall
[7]
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
[8]
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
[9]
Butler M, Ferreira C, Henderson P, Chessell M, Griffin C, and Vines D Extending the concept of transaction compensation IBM Syst J 2002 47 743-758
[10]
Butler M, Ferreira C, and Ng M Precise modelling of compensating business transactions and its application to BPEL J UCS 2005 11 712-743
[11]
Butler M, Hoare T, Ferreira C (2004) A trace semantics for long-running transactions. In: 25 years of CSP, July 2004
[12]
Bernstein P, Hadzilacos V, Goodman N (1987) Concurrency control and recovery in database systems. Addison-Wesley, Reading
[13]
Banach R, Jeske C (2009) Retrenchment and refinement interworking: the tower theorems. Available at [RET]
[14]
Banach R, Jeske C, and Poppleton M Composition mechanisms for retrenchment J Log Algor Prog 2008 75 209-229
[15]
Banach R, Jeske C, Poppleton M, and Stepney S Retrenching the purse: the balance enquiry quandary, and generalised and (1,1) forward refinements Fund Inf 2007 77 29-69
[16]
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–142
[17]
Bernstein PA and Newcomer E Transaction processing 1997 Menlo Park Morgan Kaufmann
[18]
Börger E The ASM refinement method Formal Aspects Comput 2003 15 237-275
[19]
Banach R, Poppleton M (2000) Fragmented retrenchment, concurrency and fairness. In: Proceedings of IEEE ICFEM2000, York. IEEE Computer Society Press, Los Angeles, pp 143–151
[20]
Banach R and Poppleton M Retrenching partial requirements into system definitions: a simple feature interaction case study Requir Eng J 2003 8 266-288
[21]
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–398
[22]
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–245
[23]
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–90
[24]
Banach R, Poppleton M, Jeske C, and Stepney S Engineering and theoretical underpinnings of retrenchment Sci Comput Program 2007 67 301-329
[25]
Börger E and Stärk RF Abstract state machines. In: A method for high level system design and analysis 2003 Berlin Springer
[26]
Banach R and Schellhorn G Atomic actions and their refinement to isolated protocols Form Asp Comp 2010 22 33-61
[27]
Banach R and Schellhorn G On the refinement of atomic actions ENTCS 2008 201 3-30
[28]
Connolly T and Begg C Database systems: a practical approach to design, implementation and management 2004 Reading Addison Wesley
[29]
Coulouris G, Dollimore J, and Kindberg T Distributed systems: concepts and design 2005 Reading Addison Wesley
[30]
Cooper D, Stepney S, Woodcock J (2002) Derivation of Z refinement proof rules. Technical report YCS-2002-347, University of York
[31]
Derrick J and Boiten E Refinement in Z and Object-Z. FACIT 2001 Berlin Springer
[32]
Department of Trade and Industry (1991) Information technology security evaluation criteria. http://www.cesg.gov.uk/site/iacs/itsec/media/formal-docs/Itsec.pdf
[33]
Dalessandro L, Scott M (2009) Strong isolation is a weak idea. In: Proceedings of Transaction 2009
[34]
Eder J, Liebhart W (1997) Workflow transactions. In: Workflow Handbook. Wiley, New York, pp 157–163
[35]
Elmasri R and Navathe S Fundamentals of database systems 2003 Reading Addison Wesley
[36]
Francez N, Forman I (1990) Superimposition for interactive processes. In: Proceedings of CONCUR 1990. LNCS, vol 458. Springer, Berlin, pp 230–245
[37]
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–320
[38]
George C and Haxthausen A Specification, proof, and model checking of the mondex electronic purse using RAISE Form Asp Comp 2008 20 101-116
[39]
Garcia-Molina H, Ullman J, and Widom J Database systems: the complete book 2003 Englewood Cliffs Prentice Hall
[40]
Gray J and Reuter A Transaction processing 1993 Menlo Park Morgan Kaufmann
[41]
Hall A Using formal methods to develop an ATC information system IEEE Softw 1996 13 66-76
[42]
Harris T and Bacon J Operating systems: concurrent and distributed software design 2003 Reading Addison Wesley
[43]
Harris T, Fraser K (2003) Language support for lightweight transactions. In: Proceedings of OOPSLA 2003
[44]
Haxthausen AE, George C, Schütz M (2006) Specification and proof of the Mondex electronic purse. In: Proceedings of 1st asian working conference on verified software, AWCVS’06, UNU-IIST reports 348, Macau
[45]
Herlihy M, Moss E (1993) Transactional memory: architectural support for lock-free data structures. In: Proceedings of 20th ISCA, pp 289–300
[46]
Harris T, Marlow S, Peyton-Jones S, Herlihy M (2005) Composable memory transactions. In: Proceedings of PPoPP 2005
[47]
Harris T, Plesko M, Shinnar A, Tarditi D (2006) Optimizing memory transactions. In: Proceedings of PLDI 2006, pp 14–25
[48]
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
[49]
Isard M, Birrell A (2007) Automatic mutual exclusion. In: Proceedings of workshop on hot topics in operating systems 2007
[50]
ISO/IEC 13568 (2002) Information Technology—Z Formal specification notation—Syntax, type system and semantics: international standard. http://www.iso.org/iso/en/ittf/PubliclyAvailableStandards/c021573_ISO_IEC_13568_2002(E).zip
[51]
Jeske C (2005) Algebraic integration of retrenchment and refinement. PhD thesis, University of Manchester
[52]
Jajodia S and Kerschberg L Advanced transaction models and architectures 1997 Dordrecht Kluwer
[53]
Jones CB, O’Hearne P, and Woodcock J Verified software: a grand challenge IEEE Comput 2006 39 4 93-95
[54]
Jones C, Woodcock J (eds)(2008) Special issue on the Mondex verification. Form Asp Comp 20(1): 1–139
[55]
Katz S A superimposition control construct for distributed systems ACM TPLAN 1993 15 2 337-356
[56]
Khan B, Horsnell M, Rogers I, Luján M, Dinn A, Watson I (2008) An object-aware hardware transactional memory. In: Proceedings of ICHPCC, pp 51–58
[57]
Lynch N, Merritt M, Weihl W, and Fekete A Atomic transactions 1994 Menlo Park Morgan Kaufmann
[58]
Loney K Oracle database 10g: the complete reference 2004 New York McGraw-Hill
[59]
Larus J, Rajwar R (2006) Transactional memory. Morgan and Claypool
[60]
Lynch N Distributed algorithms 1996 Menlo Park Morgan Kaufmann
[61]
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
[62]
Papazoglou M Web services: principles and technology 2007 Englewood Cliffs Prentice Hall
[63]
Poppleton M, Banach R (2003) Structuring retrenchments in B by Decomposition. In: Araki et al. [AGM03], pp 814–833
[64]
Raynal M Distributed algorithms and protocols 1988 New York Wiley
[65]
Retrenchment Homepage. http://www.cs.man.ac.uk/retrenchment
[66]
Rajwar R, Goodman J (2002) Transactional lock-free execution of lock-based programs. In: Proceedings of 10th SASPLO, pp 5–17
[67]
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–103
[68]
Silberschatz A, Baer P, and Gagne G Operating system concepts 2005 New York Wiley
[69]
Schellhorn G Verification of ASM refinements using generalized forward simulation JUCS 2001 7 952-979
[70]
Schellhorn G ASM refinement and generalisations of forward simulation in data refinement: a comparison Theor Comput Sci 2005 336 403-435
[71]
Stepney S, Cooper D, Woodcock J (2000) An electronic purse: specification, refinement and proof. Technical report PRG-126, Oxford University Computing Laboratory
[72]
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
[73]
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–31
[74]
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–199
[75]
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
[76]
Spivey JM The Z notation: a reference manual 1992 2 Englewood Cliffs Prentice-Hall
[77]
Woodcock J and Banach R The verification grand challenge JUCS 2007 13 5 661-668
[78]
Woodcock J and Davies J Using Z: specification, refinement and proof 1996 Englewood Cliffs Prentice-Hall
[79]
Woodcock JCP First steps in the verified software grand challenge IEEE Comput 2006 39 10 57-64
[80]
Web Services Org. http://www.webservices.org/
[81]
Woodcock J, Stepney S, Cooper D, Clark J, and Jacob J The certification of the Mondex electronic purse to ITSEC level E6 Form Asp Comp 2008 20 5-19
[82]
Weikum G and Vossen G Transaction processing 2002 Menlo Park Morgan Kaufmann
[83]
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
[84]
Zikopoulos P, Baklarz G, and Melnyk R Official guide to DB2 Version 8 2003 Englewood Cliffs Prentice Hall
Recommendations
Weak atomicity for the x86 memory consistency model
We consider the interaction of weakly atomic Software Transactional Memory (STM) providing single global lock atomicity with the x86 memory consistency model. We show that a practical design for such an STM requires that some program behaviour be ...
A criterion for atomicity
AbstractMost proof methods for reasoning about concurrent programs are based upon theinterleaving semantics of concurrent computation: a concurrent program is executed in a stepwise fashion, with only one enabled action being executed at each step. ...
Retrenchment and the Atomicity Pattern
SEFM '07: Proceedings of the Fifth IEEE International Conference on Software Engineering and Formal MethodsThe 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 ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
© British Computer Society 2011.
Publisher
Springer-Verlag
Berlin, Heidelberg
Publication History
Published: 01 May 2013
Accepted: 24 October 2011
Revision received: 20 February 2011
Received: 02 April 2010
Published in FAC Volume 25, Issue 3
Author Tags
Qualifiers
- Research-article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 47Total Downloads
- Downloads (Last 12 months)31
- Downloads (Last 6 weeks)8
Reflects downloads up to 01 Jan 2025
Other Metrics
Citations
Cited By
View all- Börger ESchewe K(2016)Concurrent abstract state machinesActa Informatica10.1007/s00236-015-0249-753:5(469-492)Online publication date: 1-Aug-2016
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in