[PRL] Torture chamber: Thu 1:30 in 366

[Aaron Turon]

I've gotten a request for the abstract:

Fine-grained concurrent data structures (or FCDs) reduce the
granularity of critical sections in both time and space, thus making
it possible for clients to access different parts of a mutable data
structure in parallel. However, the tradeoff is that the
implementations of FCDs are very subtle and tricky to reason about
directly. Consequently, they are carefully designed to be contextual
refinements of their coarse-grained counterparts, meaning that their
clients can reason about them as if all access to them were
sequentialized.

We propose a new semantic model, based on Kripke logical relations,
that supports direct proofs of contextual refinement in the setting of
a type-safe higher-order language. The key idea behind our model is to
provide a simple way of expressing the ``local life stories'' of
individual pieces of an FCD's hidden state by means of protocols that
the threads concurrently accessing that state must follow. By endowing
these protocols with a simple yet powerful transition structure, as
well as the ability to assert invariants on both heap states and
specification code, we are able to support clean and intuitive
refinement proofs for the most sophisticated types of FCDs, such as
conditional compare-and-set (CCAS).

On Tue, Sep 4, 2012 at 11:07 AM, Aaron Turon <turon at ccs.neu.edu> wrote:
> I'll be holding a torture chamber for my HOPE talk "Logical relations
> for fine-grained concurrency" on Thursday, 1:30-3, in WVH366.  Please
> come and provide torture!