Investigating Atomicity and Observability

Jon Burton (University of Newcastle upon Tyne, UK)

Cliff B. Jones (University of Newcastle upon Tyne, UK)

Abstract: Using the fiction of atomicity as a design abstraction and then refining atomicity as we develop an implementation is widely used in areas of concurrent computing such as database systems and transaction processing. In each of these and similar areas, associated notions of correctness are used in order to show that a particular implementation artefact which exhibits concurrency is correct in some sense with respect to a (possibly notional) description which executes with a greater degree of sequentiality. Of crucial importance in the proof and deployment of such notions of correctness is the issue of observability: i.e. in what broad sense do (human or computer) users of a particular implementation artefact observe the effects of its executions. For example, if a human user is allowed to observe directly the execution of a particular concurrent component then he or she will be able to detect the fact of concurrent - and so non-atomic - execution. In general, however, the notion of observability is treated implicitly or not at all. In this paper, we make it explicit and look at the issue of exploring more fully the connections between atomicity and observability. The ultimate aim of this consideration is to work towards constructing a more general framework for (software or hardware) development by refining atomicity.

Keywords: formal development method, observability, refinement of atomicity

Categories: F.3.1