Atomicity failure and the retrenchment atomicity pattern

Richard Banach, Czesław Jeske, Anthony Hall, Susan Stepney

    Research output: Contribution to journalArticlepeer-review


    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. © 2011 British Computer Society.
    Original languageEnglish
    Pages (from-to)439-464
    Number of pages25
    JournalFormal Aspects of Computing
    Issue number3
    Publication statusPublished - May 2013


    • Air traffic control
    • Atomic actions
    • Compensated transactions
    • Mondex
    • Refinement
    • Retrenchment
    • Software transactional memory


    Dive into the research topics of 'Atomicity failure and the retrenchment atomicity pattern'. Together they form a unique fingerprint.

    Cite this