Despite the growth of multi-core technology, a large subset of programmers still have neither the tools nor the language features to write concurrent programs eectively. When many programmers are simultaneously working on large, complex code bases with unknown bugs and insucient documentation, they are unlikely to be very productive unless the programming language aords them the power to create abstractions and modularise their code. Applications are formed by composing independent modules. However, concurrent algorithms do not compose well. Using classical language features such as locks and compare-and-swap operations, one either has to rewrite the algorithm from scratch or expose its internal implementation to the client.
Atomic sections have simple semantics and allow programmers to compose concurrent algorithms. However, atomic sections are typically implemented using transactions. Thus, they lack performance and are restrictive to programmers. Here, we explore the implementation of atomic sections using locks instead of transactions.
Firstly, we give a type system that uses universe type annotations (a form of ownership types) to verify that programmer-supplied locks are sucient to give race safety and implement programmer-denoted atomic sections. We prove that the system prevents races during execution, and give some extensions including a type system for checking that atomic sections have been implemented correctly.
Secondly, we develop a program analysis that facilitates implementing atomic sections (denoted by the programmer) with automatically-inserted locks. There is no annotation overhead since everything is inferred. Since the implementation takes complete responsibility for the locking protocol used, the programmer does not need to know that locks are being used internally. This means we must ensure the program does not deadlock, for which we use runtime deadlock detection and rollback. Our program analysis builds on related work by having improved accuracy, a nice characterisation of recursive object structures, and a machine-checked proof of correctness.
pubs.doc.ic.ac.uk: built & maintained by Ashok Argent-Katwala.