A Type System for Preventing Data Races and Deadlocks in Java Programs
Chandrasekhar Boyapati, Robert Lee, Martin Rinard · DSpace@MIT (Massachusetts Institute of Technology) · 2002
... guaranteed to be free of data races and deadlocks. Our type system allows programmers to partition the locks into a xed number of equivalence classes and specify a partial order among the equivalence classes. The type checker then statically data structures to describe the partial order. For example, programmers can specify that nodes in a tree must be locked in the tree-order. Our system allows mutations to the data structure that change the partial order at runtime. The type checker statically veri es that the mutations do not introduce cycles in the partial order, and that the changing of the partial order does not lead to deadlocks. We do not know of any other sound static system for preventing deadlocks that allows changes to the partial order at runtime.