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

Awerbuch, Baruch; Kirousis, Lefteris M.; Kranakis, Evangelos; Vitányi, Paul M. B.

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

MSC:

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

Keywords:

asynchronous process; concurrent data object; shared-concurrent register; atomic register

Citations:

Zbl 0656.00031