Concurrency on modern processors is commonly thought to be difficult to understand because of "weak" semantics, where instructions are reordered and stores are not atomic. Tony Hoare has recently advanced a form of semantics called the "tracelet" semantics. In tracelet models program components denote tracelets, small portions of global partially-ordered traces. This semantics is named by analogy with separation logic, whose semantics is based on "heaplets", or small portions of heap. The tracelet semantics has elegant mathematical properties, and forms a model of concurrent separation logic, a recent program logic for concurrency. And yet, because of its reliance on partial orders, the semantics appears to be well suited to weak memory. There is the alluring, but as yet unrealized, possibility of an elegant semantics and logic associated to weak memory.
The purpose of this internship opportunity is to investigate the tracelet semantics for a programming language over weak memory, in detail. It may be that the fit of tracelets to weak memory is good, and it may be that it is not a good fit. Finding the answer in either case would expand knowledge. This internship will be supervised by Jade Alglave and Peter O'Hearn. Jade has extensive experience on modelling weak memory using partial orders, and Peter has extensive experience on logic and semantics, particularly on separation logic.
There is a possibility that this work may lead onto a PhD position, and partial funding for the internship itself might be available.