From BSP routines to high-performance ones: Formal verification of a transformation case

Paderborn’s and Oxford’s BSPLib are C libraries supporting the development of Bulk-Synchronous Parallel (BSP) algorithms. The BSP model allows an estimation of the execution time, avoids deadlocks and non-determinism. A natural semantics of the classical BSP communication routines have been given and used to certify a classical numerical computation using the Coq proof assistant. In this paper, we present a semantics that emphasises the highperformance primitives and is here used to formally verify (using Coq) a simple function of optimisation of the source code that transforms classical BSP routines to their high-performance versions.