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.

翻译：本文旨在描述并解释并发算法和集合并发算法的理论基础，考虑一个异步共享内存系统，其中任意数量的进程可能崩溃。并发算法的验证通常通过其进展条件来描述，该条件保证最终会有好的结果发生，也称为算法的安全性；以及正确性，该条件保证不会发生坏的结果，也称为算法的活性。本文详细解释了并发算法正确性的含义，重点聚焦于线性化，并探讨了一种更为近期且鲜为人知的推广——集合并发。展示了 SetStackLogic 算法，它既是一个集合并发算法，也是具有多重性栈的一种实现。以形式化和详细的方式证明了 SetStackLogic 算法的性质，旨在为此类算法的形式化提供严谨的范式；该范式也可用于其他算法。此外，通过场景示例解释了算法的运行机制，说明了其在一些可能执行中的动态过程。