With multicore architectures becoming increasingly prevalent, the problem of constructing scalable and efficient concurrent software has attracted increasing attention. There has been growing interest programming models that allow programmers to demarcate regions of thread code---so-called transactions---that should appear to occur atomically, when viewed from the perspective of other threads.
The premise of this project is that current, monolithic software transactional memory (STM) designs are inherently too inefficient and permit too little parallelism. Instead we propose a very different approach: a library of customized concurrent data structures that can be composed, through a very light-weight run-time, to form transactions. Each data structure is optimized to exploit the semantics of its type. The intellectual merits are the development of new type-specific synchronization and recovery algorithms, along with formal tools to reason about their correctness. These ideas will be embodied in a novel concurrency library and verification toolkit, which will be used to construct benchmarks and applications. The boarder impacts involve incorporating concurrency into education and the potential to benefit society through higher performing, more reliable, and less expensive software.
