Types for Safe Locking

13 years 8 months ago

Download slang.soe.ucsc.edu

Abstract. 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 signiﬁcant 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-veriﬁcation calculus, the type system is eﬀective and easy to apply. We emphasize a core, ﬁrst-order type system focused on race conditions; we also consider extensions with...

Cormac Flanagan, Martín Abadi

Real-time Traffic