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. © 2011 British Computer Society.
Original language | English |
---|---|
Pages (from-to) | 439-464 |
Number of pages | 25 |
Journal | Formal Aspects of Computing |
Volume | 25 |
Issue number | 3 |
DOIs | |
Publication status | Published - May 2013 |
Keywords
- Air traffic control
- Atomic actions
- Compensated transactions
- Mondex
- Refinement
- Retrenchment
- Software transactional memory