Algoritmo Concurrente por Conjuntos de Pilas con Multiplicidad: SetStackLogic

TL;DR

This paper presents the theoretical foundations of concurrent set algorithms, focusing on the SetStackLogic algorithm, a set-concurrent stack implementation with formal properties and illustrative scenarios.

Contribution

It introduces and formalizes the SetStackLogic algorithm, a novel set-concurrent stack with multiplicity, and provides a detailed correctness proof and operational scenarios.

Findings

SetStackLogic is a correct set-concurrent stack algorithm.

The paper formalizes the properties and correctness of set-concurrent algorithms.

Operational scenarios illustrate the algorithm's behavior in various executions.

Abstract

This article aims to describe and explain the theoretical foundations of concurrent and set concurrent algorithms, considering an asynchronous shared memory system where any number of processes can crash. Verification of concurrent algorithms is often described in terms of their progress condition, which guarantees that eventually something good will happen, also called the security of the algorithms, and correctness, which guarantees that nothing bad will happen, also called liveliness. of the algorithms. The meaning of correctness of a concurrent algorithm is explained in detail, focusing on linearizability, and a generalization is addressed, concurrency by sets; which is much more recent and less well known. The {\it SetStackLogic} algorithm is shown, which is a set-concurrent algorithm and is also an implementation of a stack with multiplicity. The properties of the algorithm {\it SetStackLogic} are demonstrated in a formal and detailed way, in order to present a rigorous scheme in the formalization of this type of algorithm; same that could be used for other algorithms. In addition, the operation of the algorithm is explained through scenario examples that illustrate its dynamics in some possible executions.