Deadlock-Free Channels and Locks
Deadlock-Free Channels and Locks
复制标题
无死锁通道和锁
DOI：
10.1007/978-3-642-11957-6_22
复制
发表时间：
2010
影响因子：
2.8
通讯作者：
Jan Smans
中科院分区：
文献类型：
--
作者：
K. R. M. Leino;Peter Müller;Jan Smans
消息传递和锁定相结合来保护共享状态是一种有用的并发模式。但是，使用这种模式的程序容易出现死锁。也就是说，执行可以达到这样的状态，其中集合中的每个线程等待该集合中的另一个线程释放锁或发送消息。
本文提出了一种模块化的验证技术，防止死锁的程序，同时使用消息传递和锁定。该方法通过强制执行两个规则来防止死锁：（0）仅当另一个线程持有发送义务时才允许阻塞接收，以及（1）每个线程必须根据全局顺序执行获取和接收操作。该方法被证明是合理的，并已在Chalice程序验证器中实现。
The combination of message passing and locking to protect shared state is a useful concurrency pattern. However, programs that employ this pattern are susceptible to deadlock. That is, the execution may reach a state where each thread in a set waits for another thread in that set to release a lock or send a message.
This paper proposes a modular verification technique that prevents deadlocks in programs that use both message passing and locking. The approach prevents deadlocks by enforcing two rules: (0) a blocking receive is allowed only if another thread holds an obligation to send and (1) each thread must perform acquire and receive operations in accordance with a global order. The approach is proven sound and has been implemented in the Chalice program verifier.