BSP-Why: A Tool for Deductive Verification of BSP Algorithms with Subgroup Synchronisation

摘要

We present BSP-WHY, a tool for deductive verification of BSP algorithms with subgroup synchronisation. From BSP programs, BSP-WHY generates sequential codes for the back-end condition generator why and thus benefits from its large range of existing provers. By enabling subgroups, the user can prove the correctness of programs that run on hierarchical machines-e.g. clusters of multi-cores. In general, bsp-why is able to generate proof obligations of MPI programs that only use collective operations. Our case studies are distributed state-space construction algorithms, the basis of model-checking.