Types for Safe Locking
Types for Safe Locking
复制标题
安全锁定类型
DOI：
--
复制
发表时间：
1999
期刊：
影响因子：
--
通讯作者：
M. Abadi
中科院分区：
文献类型：
--
作者：
C. Flanagan;M. Abadi
争用条件是两个线程同时操作一个数据结构而不同步的情况。争用条件是多线程编程中常见的错误。它们经常导致意想不到的不确定性和错误的结果。此外，它们非常难以诊断，试图消除它们可能会引入死锁。在实践中，通常通过谨慎的编程原则来避免竞争条件和死锁：用锁保护每个共享数据结构，并对锁获取施加部分顺序。在本文中，我们展示了通过一组静态规则可以捕获这个规程（如果不是完全捕获，在很大程度上）。我们将这些规则作为并发命令式语言的类型系统。虽然比成熟的程序验证演算弱，但类型系统是有效的，易于应用。我们强调一个核心的一阶系统，专注于竞争条件；我们还考虑带有多态性、存在类型和锁类型的偏序的扩展。
A race condition is a situation where two threads manipulate a data structure simultaneously, without synchronization. Race conditions are common errors in multithreaded programming. They often lead to unintended nondeterminism and wrong results. Moreover, they are notoriously hard to diagnose, and attempts to eliminate them can introduce deadlocks. In practice, race conditions and deadlocks are often avoided through prudent programming discipline: protecting each shared data structure with a lock and imposing a partial order on lock acquisitions. In this paper we show that this discipline can be captured (if not completely, to a significant extent) through a set of static rules. We present these rules as a type system for a concurrent, imperative language. Although weaker than a full-blown program-verification calculus, the type system is effective and easy to apply. We emphasize a core, first-order type system focused on race conditions; we also consider extensions with polymorphism, existential types, and a partial order on lock types.