Logical classification of distributed algorithms (Bakery algorithms as an example)
type: Item
instance of: scholarly article
title: Logical classification of distributed algorithms (Bakery algorithms as an example)
zbMATH Open document ID: 1221.68162
author: Uri Abraham
published in: Theoretical Computer Science
publication date: 2011-06-06T00:00:00Z
review text: The paper is focused on the appropriateness of predicate language structures to study concurrency in intuitive terms. It demonstrates this appropriateness by proposing a logical classification of Bakery type algorithms. Two well-known algorithms, the Ricart-Agrawala algorithm and a take-a-number Bakery algorithm with different pre-conditions (message passing versus shared memory), have a high degree of similarity at intuitive level that can be expressed in a formal way, and, moreover, properties like mutual-exclusion can be also deduced from the formal description. Another important result of the study is the fact that the Tarskian event structures are more appropriate to be used in reasoning process than the temporal logic structures, especially due to the particular global state approach using history structures.
reviewed by: Dana Petcu
Mathematics Subject Classification ID: 68Q85
Mathematics Subject Classification ID: 03B70
Mathematics Subject Classification ID: 68W15
zbMATH DE Number: 5904443
zbMATH Keywords: distributed algorithms
zbMATH Keywords: models of concurrency
zbMATH Keywords: logical classification
zbMATH Keywords: Tarski structures
zbMATH Keywords: mutual exclusion
MaRDI profile type: Publication
full work available at URL: j.tcs.2011.01.030
OpenAlex ID: W2043514550
cites work: Q4256353
cites work: Q4873992
cites work: The Birth of Model Checking
cites work: Q2753706
cites work: A little knowledge goes a long way
cites work: Q4473994
cites work: A new solution of Dijkstra's concurrent programming problem
cites work: The synchronization of independent processes
cites work: Time, clocks, and the ordering of events in a distributed system
cites work: A New Approach to Proving the Correctness of Multiprocess Programs
cites work: On interprocess communication. I: Basic formalism
cites work: Modeling concurrency with partial orders
cites work: Q4808646
cites work: The Black-White Bakery Algorithm and Related Bounded-Space, Adaptive, Local-Spinning and FIFO Algorithms
DOI: 10.1016/J.TCS.2011.01.030
description: scientific article; zbMATH DE number 5904443