An Algebraic Theory for Shared-State Concurrency
We present a monadic denotational semantics for a higher-order programming language with shared-state concurrency, i.e. global-state in the presence of interleaving concurrency. Central to our approach is the use of Plotkin and Power’s algebraic effect methodology: designing an equational theory that captures the intended semantics, and proving a monadic representation theorem for it. We use Abadi and Plotkin’s equational theory of resumptions that extends non-deterministic global-state with an operator for yielding to the environment. The representation is based on Brookes-style traces. Based on this representation we define a denotational semantics that is directionally adequate with respect to a standard operational semantics. We use this semantics to justify compiler transformations of interest: redundant access eliminations, each following from a mundane algebraic calculation; while structural transformations follow from reasoning over the monad’s interface.
Presentation (Handout) (presentation.pdf) | 1.53MiB |
Mon 5 DecDisplayed time zone: Auckland, Wellington change
10:30 - 12:00 | Semantics and AnalysisAPLAS at Seminar Room G007 Chair(s): Julian Mackay Victoria University of Wellington | ||
10:30 30mTalk | An Algebraic Theory for Shared-State Concurrency APLAS File Attached | ||
11:00 30mTalk | Decoupling the Ascending and Descending Phases in Abstract Interpretation APLAS Vincenzo Arceri University of Parma, Italy, Isabella Mastroeni University of Verona, Italy, Enea Zaffanella University of Parma, Italy | ||
11:30 30mTalk | Inferring Region Types via an Abstract Notion of Environment Transformation APLAS |