Logical classification of distributed algorithms (Bakery algorithms as an example) (Q541220)

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.