Verifying Parallel Loops with Separation Logic

TL;DR

This paper introduces a method using separation logic to specify and verify loop dependences, aiding compilers in safely parallelizing loops by checking user annotations and determining necessary synchronization.

Contribution

It presents a novel approach that combines separation logic with loop dependence analysis to verify parallelization safety and synchronization points.

Findings

Effective verification of loop dependences using separation logic

Automatic identification of synchronization needs in parallel loops

Enhancement of parallelizing compiler correctness

Abstract

This paper proposes a technique to specify and verify whether a loop can be parallelised. Our approach can be used as an additional step in a parallelising compiler to verify user annotations about loop dependences. Essentially, our technique requires each loop iteration to be specified with the locations it will read and write. From the loop iteration specifications, the loop (in)dependences can be derived. Moreover, the loop iteration specifications also reveal where synchronisation is needed in the parallelised program. The loop iteration specifications can be verified using permission-based separation logic.