Modeling distributed computing in a way enabling the use of formal methods is a challenge that has been approached from different angles, among which two techniques emerged at the turn of the century: protocol complexes, and directed algebraic topology. In both cases, the considered computational model generally assumes communication via shared objects, typically a shared memory consisting of a collection of read-write registers. Our paper is concerned with network computing, where the processes are located at the nodes of a network, and communicate by exchanging messages along the edges of that network. Applying the topological approach for verification in network computing is a considerable challenge, mainly because the presence of identifiers assigned to the nodes yields protocol complexes whose size grows exponentially with the size of the underlying network. However, many of the problems studied in this context are of local nature, and their definitions do not depend on the identifiers or on the size of the network. We leverage this independence in order to meet the above challenge, and present $\textit{local}$ protocol complexes, whose sizes do not depend on the size of the network. As an application of the design of "compact" protocol complexes, we reformulate the celebrated lower bound of $\Omega(\log^*n)$ rounds for 3-coloring the $n$-node ring, in the algebraic topology framework.
翻译:为了能够使用形式化方法对分布式计算进行建模,这一挑战已从不同角度得到探讨,其中本世纪初出现的两种技术尤为突出:协议复形与有向代数拓扑。在这两种情况下,所考虑的计算模型通常假设通过共享对象进行通信,典型的是由一组读写寄存器构成的共享内存。本文关注网络计算场景,其中进程位于网络节点上,并通过沿网络边交换消息进行通信。将拓扑方法应用于网络计算的验证面临巨大挑战,主要原因在于节点分配标识符会导致协议复形的规模随底层网络规模呈指数增长。然而,此类研究背景下的许多问题本质上是局部的,其定义既不依赖于标识符也不依赖于网络规模。我们利用这一独立性来应对上述挑战,提出了规模不依赖于网络规模的$\textit{局部}$协议复形。作为"紧致"协议复形设计的一个应用,我们在代数拓扑框架下重新表述了对$n$节点环进行3种颜色着色时$\Omega(\log^*n)$轮次这一著名下界。