A separation logic for concurrent randomized programs

Joseph Tassarotti; Robert Harper

doi:10.1145/3290377

A separation logic for concurrent randomized programs

Joseph Tassarotti, Robert Harper

Computer Science

Research output: Contribution to journal › Article › peer-review

Abstract

We present Polaris, a concurrent separation logic with support for probabilistic reasoning. As part of our logic, we extend the idea of coupling, which underlies recent work on probabilistic relational logics, to the setting of programs with both probabilistic and non-deterministic choice. To demonstrate Polaris, we verify a variant of a randomized concurrent counter algorithm and a two-level concurrent skip list. All of our results have been mechanized in Coq.

Original language	English (US)
Article number	64
Journal	Proceedings of the ACM on Programming Languages
Volume	3
Issue number	POPL
DOIs	https://doi.org/10.1145/3290377
State	Published - Jan 2019

Keywords

Concurrency
Probability
Separation logic

ASJC Scopus subject areas

Software
Safety, Risk, Reliability and Quality

Access to Document

10.1145/3290377

Cite this

@article{0d0aa9711eca4f3090f816f5bd441da4,

title = "A separation logic for concurrent randomized programs",

abstract = "We present Polaris, a concurrent separation logic with support for probabilistic reasoning. As part of our logic, we extend the idea of coupling, which underlies recent work on probabilistic relational logics, to the setting of programs with both probabilistic and non-deterministic choice. To demonstrate Polaris, we verify a variant of a randomized concurrent counter algorithm and a two-level concurrent skip list. All of our results have been mechanized in Coq.",

keywords = "Concurrency, Probability, Separation logic",

author = "Joseph Tassarotti and Robert Harper",

note = "Publisher Copyright: {\textcopyright} 2019 Copyright held by the owner/author(s).",

year = "2019",

month = jan,

doi = "10.1145/3290377",

language = "English (US)",

volume = "3",

journal = "Proceedings of the ACM on Programming Languages",

issn = "2475-1421",

publisher = "Association for Computing Machinery (ACM)",

number = "POPL",

}

TY - JOUR

T1 - A separation logic for concurrent randomized programs

AU - Tassarotti, Joseph

AU - Harper, Robert

PY - 2019/1

Y1 - 2019/1

N2 - We present Polaris, a concurrent separation logic with support for probabilistic reasoning. As part of our logic, we extend the idea of coupling, which underlies recent work on probabilistic relational logics, to the setting of programs with both probabilistic and non-deterministic choice. To demonstrate Polaris, we verify a variant of a randomized concurrent counter algorithm and a two-level concurrent skip list. All of our results have been mechanized in Coq.

AB - We present Polaris, a concurrent separation logic with support for probabilistic reasoning. As part of our logic, we extend the idea of coupling, which underlies recent work on probabilistic relational logics, to the setting of programs with both probabilistic and non-deterministic choice. To demonstrate Polaris, we verify a variant of a randomized concurrent counter algorithm and a two-level concurrent skip list. All of our results have been mechanized in Coq.

KW - Concurrency

KW - Probability

KW - Separation logic

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

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

U2 - 10.1145/3290377

DO - 10.1145/3290377

M3 - Article

AN - SCOPUS:85120123796

SN - 2475-1421

VL - 3

JO - Proceedings of the ACM on Programming Languages

JF - Proceedings of the ACM on Programming Languages

IS - POPL

M1 - 64

ER -

A separation logic for concurrent randomized programs

Abstract

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this