Concurrent separation logic for pipelined parallelization

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

11 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 languageEnglish (US)
Title of host publicationStatic Analysis - 17th International Symposium, SAS 2010, Proceedings
Pages151-166
Number of pages16
DOIs
StatePublished - Nov 12 2010
Event17th International Static Analysis Symposium, SAS 2010 - Perpignan, France
Duration: Sep 14 2010Sep 16 2010

Publication series

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

Other

Other17th International Static Analysis Symposium, SAS 2010
CountryFrance
CityPerpignan
Period9/14/109/16/10

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Concurrent separation logic for pipelined parallelization'. Together they form a unique fingerprint.

  • 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