Abstract E ects and Concurrency
Nick Benton, Martin O. Hofmann, Vivek Prakash Nigam · 2014
We describe a denotational semantics for an abstract e ect system for a higher-order, shared-variable concurrent programming language. We prove the soundness of a number of general e ectbased program equivalences, including a parallelization equation that specifies su cient conditions for replacing sequential composition with parallel composition. We also exploit the structure given by e ect annotations and abstract locations to show the soundness of some operations on fine-grained concurrent data structures, such as Michael-Scott queues, that allow concurrent access to di erent parts of mutable data structures. Our semantics is based on refining a trace-based semantics for first-order programs due to Brookes. By moving from concrete to