Output details
11 - Computer Science and Informatics
University of Edinburgh
A Model of Cooperative Threads
<08> Originality: First denotational model of shared-memory cooperative threads. Model is given in context of automatic mutual exclusion (AME), includes spawning, and is fully abstract. Using Plotkin's algebraic theory of effects (ATE), the model is characterised equationally, including a novel dendriform equational account of thread-spawning.
Significance: Provides basic theory for AME, a current paradigm for programming multicores, via a Shared Transactional Memory execution model. Applies ATE (mentioned in Plotkin's SIGPLAN 2010 award citation) to state-of-the-art programming constructs.
Rigour: In TCS special issue for POPL 2009 (major programming languages conference, acceptance rate 22.5%). Standard mathematical definition and proof approach, 39 pages.