Treffer: Two-Stage Programming Of Parallel And Distributed Applications

This paper presents the application of Two-Stage Programming (2sp) for developing error-free parallel /distributed applications through automatic verification of computed results with respect to a given specification. The presentation focuses the case study of the parallel block-striped partitioning variant of Prim's algorithm for finding a minimum spanning tree of a dense graph. We show that the 2sp implementation of the algorithm succeeds to provide: a full functional (formal) specification, a specification-consistent (reliable) imperative coordination, automatic error detection at run-time, enhanced support for debugging, and good efficiency. 1 INTRODUCTION The Specification-Consistent Coordination Model (SCCM) [1] proposes a mixed-paradigm (functional /imperative) approach to build error-free programs based on automatic verification of computed results. It combines elements of program verification, run-time checking, and result-checking [2] (see [3] for a comparison with related a.