Richard Banach, Czeslaw Jeske, Anthony Hall, Susan Stepney.
Atomicity Failure and the Retrenchment Atomicity Pattern.

Formal Aspects of Computing 25(3):439-464, 2013.
doi:10.1007/s00165-011-0216-1

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.

@article(SS-FACS-11,
  author = "Richard Banach and Czeslaw Jeske and Anthony Hall and Susan Stepney",
  title = "Atomicity Failure and the Retrenchment Atomicity Pattern",
  journal  = "Formal Aspects of Computing",
  volume = 25,
  issue = 3,
  pages = "439-464",
  year = 2013
)