Composing interfering abstract: Protocols

Filipe Militão; Jonathan Aldrich; Luís Caires

doi:10.4230/LIPIcs.ECOOP.2016.16

Composing interfering abstract: Protocols

Filipe Militão, Jonathan Aldrich, Luís Caires

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

4 Citations (Scopus)

Abstract

The undisciplined use of shared mutable state can be a source of program errors when aliases unsafely interfere with each other. While protocol-based techniques to reason about interference abound, they do not address two practical concerns: the decidability of protocol composition and its integration with protocol abstraction. We show that our composition procedure is decidable and that it ensures safe interference even when composing abstract protocols. To evaluate the expressiveness of our protocol framework for safe shared memory interference, we show how this same protocol framework can be used to model safe, typeful message-passing concurrency idioms.

Original language	English
Title of host publication	30th European Conference on Object-Oriented Programming, ECOOP 2016
Publisher	Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Pages	161-1626
Number of pages	1466
Volume	56
ISBN (Electronic)	978-395977014-9
DOIs	https://doi.org/10.4230/LIPIcs.ECOOP.2016.16
Publication status	Published - 1 Jul 2016
Event	30th European Conference on Object-Oriented Programming, ECOOP 2016 - Rome, Italy Duration: 18 Jul 2016 → 22 Jul 2016

Conference

Conference	30th European Conference on Object-Oriented Programming, ECOOP 2016
Country	Italy
City	Rome
Period	18/07/16 → 22/07/16

Keywords

Aliasing
Linearity
Protocol composition
Shared memory interference

Access to Document

10.4230/LIPIcs.ECOOP.2016.16

Cite this

@inproceedings{d1f15c1668b54ebeba73f33e2ecefd49,

title = "Composing interfering abstract: Protocols",

abstract = "The undisciplined use of shared mutable state can be a source of program errors when aliases unsafely interfere with each other. While protocol-based techniques to reason about interference abound, they do not address two practical concerns: the decidability of protocol composition and its integration with protocol abstraction. We show that our composition procedure is decidable and that it ensures safe interference even when composing abstract protocols. To evaluate the expressiveness of our protocol framework for safe shared memory interference, we show how this same protocol framework can be used to model safe, typeful message-passing concurrency idioms.",

keywords = "Aliasing, Linearity, Protocol composition, Shared memory interference",

author = "Filipe Milit{\~a}o and Jonathan Aldrich and Lu{\'i}s Caires",

note = "sem pdf Defense Advanced Research Projects Agency (DARPA) - FA8750-16-2-0042; 30th European Conference on Object-Oriented Programming, ECOOP 2016 ; Conference date: 18-07-2016 Through 22-07-2016",

year = "2016",

month = jul,

day = "1",

doi = "10.4230/LIPIcs.ECOOP.2016.16",

language = "English",

volume = "56",

pages = "161--1626",

booktitle = "30th European Conference on Object-Oriented Programming, ECOOP 2016",

publisher = "Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing",

}

Militão, F, Aldrich, J & Caires, L 2016, Composing interfering abstract: Protocols. in 30th European Conference on Object-Oriented Programming, ECOOP 2016. vol. 56, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, pp. 161-1626, 30th European Conference on Object-Oriented Programming, ECOOP 2016, Rome, Italy, 18/07/16. https://doi.org/10.4230/LIPIcs.ECOOP.2016.16

Composing interfering abstract : Protocols. / Militão, Filipe; Aldrich, Jonathan; Caires, Luís.

30th European Conference on Object-Oriented Programming, ECOOP 2016. Vol. 56 Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2016. p. 161-1626.

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

TY - GEN

T1 - Composing interfering abstract

T2 - 30th European Conference on Object-Oriented Programming, ECOOP 2016

AU - Militão, Filipe

AU - Aldrich, Jonathan

AU - Caires, Luís

N1 - sem pdf Defense Advanced Research Projects Agency (DARPA) - FA8750-16-2-0042

PY - 2016/7/1

Y1 - 2016/7/1

N2 - The undisciplined use of shared mutable state can be a source of program errors when aliases unsafely interfere with each other. While protocol-based techniques to reason about interference abound, they do not address two practical concerns: the decidability of protocol composition and its integration with protocol abstraction. We show that our composition procedure is decidable and that it ensures safe interference even when composing abstract protocols. To evaluate the expressiveness of our protocol framework for safe shared memory interference, we show how this same protocol framework can be used to model safe, typeful message-passing concurrency idioms.

AB - The undisciplined use of shared mutable state can be a source of program errors when aliases unsafely interfere with each other. While protocol-based techniques to reason about interference abound, they do not address two practical concerns: the decidability of protocol composition and its integration with protocol abstraction. We show that our composition procedure is decidable and that it ensures safe interference even when composing abstract protocols. To evaluate the expressiveness of our protocol framework for safe shared memory interference, we show how this same protocol framework can be used to model safe, typeful message-passing concurrency idioms.

KW - Aliasing

KW - Linearity

KW - Protocol composition

KW - Shared memory interference

UR - http://www.scopus.com/inward/record.url?scp=84982784057&partnerID=8YFLogxK

U2 - 10.4230/LIPIcs.ECOOP.2016.16

DO - 10.4230/LIPIcs.ECOOP.2016.16

M3 - Conference contribution

AN - SCOPUS:84982784057

VL - 56

SP - 161

EP - 1626

BT - 30th European Conference on Object-Oriented Programming, ECOOP 2016

PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing

Y2 - 18 July 2016 through 22 July 2016

ER -

Composing interfering abstract: Protocols

Abstract

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this