Mike Dodds (University of Cambridge): Generic Reasoning for Bespoke Concurrency Constructs

Abstract: Synchronisation constructs such as locks and barriers are often treated as primitive in program logics such as separation logic. The result has been a large number of custom logics, each addressing a single construct. This has two problems: first, each logic is incompatible with all the others, and second, logics have no way of justifying the specifications of constructs against their implementations. We have proposed a higher-order separation logic that is expressive enough to prove abstract specifications for synchronisation constructs In this talk I will discuss using our logic to give a specification to compiler-inserted barriers, and show how our logic can define new abstractions for dealing simply with complex patterns of concurrency.