zbMATH — the first resource for mathematics

Commutativity-based concurrency control for abstract data types. (English) Zbl 0674.68016
Two new concurrency control algorithms for abstract data types are presented. The algorithms permit a high level of concurrency. Both algorithms are described formally. The algorithms are quite general to work for arbitrary data types, with partial and nondeterministic operations. The author proves that both algorithms ensure dynamic atomicity. He also presents a correctness condition that concurrency and recovery must ensure in order to satisfy online dynamic atomicity. To specify behaviour of objects, the author uses an automaton, that is an effective and convenient tool describing a set of sequences (the serial specification). He describes algorithms using a state machine. Proving theorems the author applies an inductive technique.
Reviewer: J.Woźniak

68N25 Theory of operating systems
68Q45 Formal languages and automata
Full Text: DOI