An Algebraic Theory for Shared-State Concurrency

Yotam Dvir; Ohad Kammar; Ori Lahav

doi:10.1007/978-3-031-21037-2_1

An Algebraic Theory for Shared-State Concurrency

Yotam Dvir^*, Ohad Kammar^*, Ori Lahav^*

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

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 Hyland et al.'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.

Original language	English
Title of host publication	Programming Languages and Systems: 20th Asian Symposium, APLAS 2022, Auckland, New Zealand, December 5, 2022, Proceedings
Editors	Ilya Sergey
Publisher	Springer, Cham
Pages	2-24
Number of pages	22
ISBN (Electronic)	978-3-031-21037-2
ISBN (Print)	978-3-031-21036-5
DOIs	https://doi.org/10.1007/978-3-031-21037-2_1
Publication status	Published - 25 Nov 2022
Event	Asian Symposium on Programming Languages - University of Auckland, Auckland, New Zealand Duration: 5 Dec 2022 → 10 Dec 2022 Conference number: 20 https://conf.researchr.org/home/aplas-2022

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Cham
Volume	13658
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	Asian Symposium on Programming Languages
Abbreviated title	APLAS
Country/Territory	New Zealand
City	Auckland
Period	5/12/22 → 10/12/22
Internet address	https://conf.researchr.org/home/aplas-2022

Keywords

shared state
concurrency
denotational semantics
monads
equational theory
program refinement
program equivalence
compiler transformations
compiler optimisations

Access to Document

10.1007/978-3-031-21037-2_1Licence: All Rights Reserved

dvir-kammar-lahav-an-algebraic-theory-for-shared-state-concurrencyAccepted author manuscript, 789 KBLicence: Creative Commons: Attribution (CC-BY)

https://link.springer.com/chapter/10.1007/978-3-031-21037-2_1Licence: All Rights Reserved

1 Active

Effectful theories of programming languages: mathematically structured programming
Kammar, O.
Other (Learned Society)
1/12/21 → 31/12/23
Project: Research

Cite this

@inproceedings{6e8b74ca71bd44e5a382193b8593700e,

title = "An Algebraic Theory for Shared-State Concurrency",

abstract = "We present a monadic denotational semantics for a higher-orderprogramming 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 Hyland et al.'s equational theory of resumptions thatextends 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 isdirectionally 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.",

keywords = "shared state, concurrency, denotational semantics, monads, equational theory, program refinement, program equivalence, compiler transformations, compiler optimisations",

author = "Yotam Dvir and Ohad Kammar and Ori Lahav",

note = "Supported by the Israel Science Foundation (grant numbers 1566/18 and 814/22) and the European Research Council (ERC) under the European Union{\textquoteright}s Horizon 2020 research and innovation programme (grant agreement no. 851811); and by a Royal Society University Research Fellowship and Enhancement Award. ; Asian Symposium on Programming Languages, APLAS ; Conference date: 05-12-2022 Through 10-12-2022",

year = "2022",

month = nov,

day = "25",

doi = "10.1007/978-3-031-21037-2_1",

language = "English",

isbn = "978-3-031-21036-5",

series = "Lecture Notes in Computer Science",

publisher = "Springer, Cham",

pages = "2--24",

editor = "Ilya Sergey",

booktitle = "Programming Languages and Systems: 20th Asian Symposium, APLAS 2022, Auckland, New Zealand, December 5, 2022, Proceedings",

url = "https://conf.researchr.org/home/aplas-2022",

}

Dvir, Y, Kammar, O & Lahav, O 2022, An Algebraic Theory for Shared-State Concurrency. in I Sergey (ed.), Programming Languages and Systems: 20th Asian Symposium, APLAS 2022, Auckland, New Zealand, December 5, 2022, Proceedings. Lecture Notes in Computer Science, vol. 13658, Springer, Cham, pp. 2-24, Asian Symposium on Programming Languages, Auckland, New Zealand, 5/12/22. https://doi.org/10.1007/978-3-031-21037-2_1

An Algebraic Theory for Shared-State Concurrency. / Dvir, Yotam; Kammar, Ohad; Lahav, Ori.

Programming Languages and Systems: 20th Asian Symposium, APLAS 2022, Auckland, New Zealand, December 5, 2022, Proceedings. ed. / Ilya Sergey. Springer, Cham, 2022. p. 2-24 (Lecture Notes in Computer Science; Vol. 13658).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - An Algebraic Theory for Shared-State Concurrency

AU - Dvir, Yotam

AU - Kammar, Ohad

AU - Lahav, Ori

N1 - Conference code: 20

PY - 2022/11/25

Y1 - 2022/11/25

N2 - We present a monadic denotational semantics for a higher-orderprogramming 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 Hyland et al.'s equational theory of resumptions thatextends 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 isdirectionally 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.

AB - We present a monadic denotational semantics for a higher-orderprogramming 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 Hyland et al.'s equational theory of resumptions thatextends 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 isdirectionally 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.

KW - shared state

KW - concurrency

KW - denotational semantics

KW - monads

KW - equational theory

KW - program refinement

KW - program equivalence

KW - compiler transformations

KW - compiler optimisations

U2 - 10.1007/978-3-031-21037-2_1

DO - 10.1007/978-3-031-21037-2_1

M3 - Conference contribution

SN - 978-3-031-21036-5

T3 - Lecture Notes in Computer Science

SP - 2

EP - 24

BT - Programming Languages and Systems: 20th Asian Symposium, APLAS 2022, Auckland, New Zealand, December 5, 2022, Proceedings

A2 - Sergey, Ilya

PB - Springer, Cham

T2 - Asian Symposium on Programming Languages

Y2 - 5 December 2022 through 10 December 2022

ER -

An Algebraic Theory for Shared-State Concurrency

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Projects

Effectful theories of programming languages: mathematically structured programming

Cite this