无限多进程的部分互斥
分布式、并行与集群计算
2011-12-07 v2
摘要
部分互斥是完全图上的饮酒哲学家问题。该问题是指，一个进程只有当某个有限邻居进程集 nbh 中的其他进程都不在其临界区时，才能进入其代码的临界区 CS。对于 CS 的每次执行，集合 nbh 可由环境给定。我们提出了该问题的一个无饥饿解决方案，设定中包含无限多个进程，每个进程具有有限内存，并通过异步消息进行通信。该方案具有先到先服务的特性，这是在异步消息所能保证的范围内实现的。对于 CS 的每次执行以及 nbh 中的每个进程，需要三到六条消息。该方案的正确性通过不变量和时序逻辑进行论证，并已使用证明助手 PVS 进行了验证。
引用
@article{arxiv.1111.5775,
title = {Partial mutual exclusion for infinitely many processes},
author = {Wim H. Hesselink},
journal= {arXiv preprint arXiv:1111.5775},
year = {2011}
}