Effect-dependent transformations for concurrent programs
Nick Benton, Martin O. Hofmann, Vivek Prakash Nigam · 2016
We describe a denotational semantics for an abstract effect system for a higher-order, shared-variable concurrent language. The semantics validates general effect-based program equivalences, including sufficient conditions for replacing sequential composition with parallel composition. Effect annotations refer to abstract locations, specified by contracts, rather than physical footprints, allowing us to also show soundness of some transformations involving fine-grained concurrent data structures, such as Michael-Scott queues.