A proof technique for register atomicity. (English) Zbl 0669.68019

Foundations of software technology and theoretical computer science, Proc, 8th Conf., Pune/India 1988, Lect. Notes Comput. Sci. 338, 286-303 (1988).
[For the entire collection see Zbl 0656.00031.]
A problem of “serializability” of processes with concurrent operation is considered. The notion of an atomic register is taken as a formal model of such a process. The aim of this paper is to propose a new proof technique for providing register atomicity. The formal criteria consisting of a method of proving atomicity of registers are illustrated by a nontrivial example.
Reviewer: J.Zurawiecki


68N25 Theory of operating systems
68Q60 Specification and verification (program logics, model checking, etc.)
68Q65 Abstract data types; algebraic specification


Zbl 0656.00031