Concurrent separation logic for pipelined parallelization

Christian J. Bell; Andrew W. Appel; David Walker

doi:10.1007/978-3-642-15769-1_10

Concurrent separation logic for pipelined parallelization

Christian J. Bell, Andrew W. Appel, David Walker

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

15 Scopus citations

Abstract

Recent innovations in automatic parallelizing compilers are showing impressive speedups on multicore processors using shared memory with asynchronous channels. We have formulated an operational semantics and proved sound a concurrent separation logic to reason about multithreaded programs that communicate asynchronously through channels and share memory. Our logic supports shared channel endpoints (multiple producers and consumers) and introduces histories to overcome limitations with local reasoning. We demonstrate how to transform a sequential proof into a parallelized proof that targets the output of the parallelizing optimization DSWP (Decoupled Software Pipelining).

Original language	English (US)
Title of host publication	Static Analysis - 17th International Symposium, SAS 2010, Proceedings
Pages	151-166
Number of pages	16
DOIs	https://doi.org/10.1007/978-3-642-15769-1_10
State	Published - 2010
Event	17th International Static Analysis Symposium, SAS 2010 - Perpignan, France Duration: Sep 14 2010 → Sep 16 2010

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	6337 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Other

Other	17th International Static Analysis Symposium, SAS 2010
Country/Territory	France
City	Perpignan
Period	9/14/10 → 9/16/10

All Science Journal Classification (ASJC) codes

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-642-15769-1_10

Cite this

Bell, C. J., Appel, A. W., & Walker, D. (2010). Concurrent separation logic for pipelined parallelization. In Static Analysis - 17th International Symposium, SAS 2010, Proceedings (pp. 151-166). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6337 LNCS). https://doi.org/10.1007/978-3-642-15769-1_10

@inproceedings{30a53de0e7a1455b95aa4d0eb6582a76,

title = "Concurrent separation logic for pipelined parallelization",

abstract = "Recent innovations in automatic parallelizing compilers are showing impressive speedups on multicore processors using shared memory with asynchronous channels. We have formulated an operational semantics and proved sound a concurrent separation logic to reason about multithreaded programs that communicate asynchronously through channels and share memory. Our logic supports shared channel endpoints (multiple producers and consumers) and introduces histories to overcome limitations with local reasoning. We demonstrate how to transform a sequential proof into a parallelized proof that targets the output of the parallelizing optimization DSWP (Decoupled Software Pipelining).",

author = "Bell, {Christian J.} and Appel, {Andrew W.} and David Walker",

year = "2010",

doi = "10.1007/978-3-642-15769-1_10",

language = "English (US)",

isbn = "3642157688",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "151--166",

booktitle = "Static Analysis - 17th International Symposium, SAS 2010, Proceedings",

}

Bell, CJ, Appel, AW & Walker, D 2010, Concurrent separation logic for pipelined parallelization. in Static Analysis - 17th International Symposium, SAS 2010, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 6337 LNCS, pp. 151-166, 17th International Static Analysis Symposium, SAS 2010, Perpignan, France, 9/14/10. https://doi.org/10.1007/978-3-642-15769-1_10

Concurrent separation logic for pipelined parallelization. / Bell, Christian J.; Appel, Andrew W.; Walker, David.
Static Analysis - 17th International Symposium, SAS 2010, Proceedings. 2010. p. 151-166 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6337 LNCS).

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

TY - GEN

T1 - Concurrent separation logic for pipelined parallelization

AU - Bell, Christian J.

AU - Appel, Andrew W.

AU - Walker, David

PY - 2010

Y1 - 2010

N2 - Recent innovations in automatic parallelizing compilers are showing impressive speedups on multicore processors using shared memory with asynchronous channels. We have formulated an operational semantics and proved sound a concurrent separation logic to reason about multithreaded programs that communicate asynchronously through channels and share memory. Our logic supports shared channel endpoints (multiple producers and consumers) and introduces histories to overcome limitations with local reasoning. We demonstrate how to transform a sequential proof into a parallelized proof that targets the output of the parallelizing optimization DSWP (Decoupled Software Pipelining).

AB - Recent innovations in automatic parallelizing compilers are showing impressive speedups on multicore processors using shared memory with asynchronous channels. We have formulated an operational semantics and proved sound a concurrent separation logic to reason about multithreaded programs that communicate asynchronously through channels and share memory. Our logic supports shared channel endpoints (multiple producers and consumers) and introduces histories to overcome limitations with local reasoning. We demonstrate how to transform a sequential proof into a parallelized proof that targets the output of the parallelizing optimization DSWP (Decoupled Software Pipelining).

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

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

U2 - 10.1007/978-3-642-15769-1_10

DO - 10.1007/978-3-642-15769-1_10

M3 - Conference contribution

AN - SCOPUS:78149253189

SN - 3642157688

SN - 9783642157684

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 151

EP - 166

BT - Static Analysis - 17th International Symposium, SAS 2010, Proceedings

T2 - 17th International Static Analysis Symposium, SAS 2010

Y2 - 14 September 2010 through 16 September 2010

ER -

Concurrent separation logic for pipelined parallelization

Abstract

Publication series

Other

All Science Journal Classification (ASJC) codes

Access to Document

Other files and links

Fingerprint

Cite this