arXivDaily arXiv每日学术速递 周一至周五更新
arXiv 1111.5775cs.DC
收藏

无穷多过程的部分互斥

Partial mutual exclusion for infinitely many processes

Wim H. Hesselink

摘要:

部分互斥是完全图的哲学家饮酒问题。问题是,只有当其他进程的某个有限集nbh不在其临界区时,进程才可能进入其代码的临界区CS。对于CS的每次执行,可以由环境给出集合nbh。我们提出了一个饥饿免费的解决方案,这个问题的无限多个进程,每个进程的内存有限,异步消息通信的设置。该解决方案具有先到先服务的属性,因为这可以通过异步消息来保证。对于CS的每次执行和nbh中的每个流程,需要三到六条消息。用不变量和时态逻辑论证了解的正确性。已通过证明助手PVS进行验证。

英文摘要:

Partial mutual exclusion is the drinking philosophers problem for complete graphs. It is the problem that a process may enter a critical section CS of its code only when some finite set nbh of other processes are not in their critical sections. For each execution of CS, the set nbh can be given by the environment. We present a starvation free solution of this problem in a setting with infinitely many processes, each with finite memory, that communicate by asynchronous messages. The solution has the property of first-come first-served, in so far as this can be guaranteed by asynchronous messages. For every execution of CS and every process in nbh, between three and six messages are needed. The correctness of the solution is argued with invariants and temporal logic. It has been verified with the proof assistant PVS.

机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。

↑