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).

Appendix

• Machine & Logic Formalization
• Proof of Progress
• Proof of Preservation
• Coq formalization of Separation Algebra
• Extended from the Mechanized Semantic Library
• Proof for example program (where the list order and shape is preserved)