BSP in CSP: Easy as ABC

Abstract. In this paper we describe how the language of Communicating Sequential Processes CSP has been applied to the analysis of a transport layer protocol used in the implementation of the Bulk Synchronous Parallel model BSP. The protocol is suited to the bulk transfer of data between a group of processes that communicate over an unreliable medium with xed bu er capacities on both sender and receiver. This protocol is modelled using CSP, and veri ed using the re nement checker FDR2. This veri cation has been used to establish that the protocol is free from the potential for both deadlock and livelock, and also that it is fault-tolerant.

• Type: Conference
• Year: 1999
• Where: IPPS
• Authors: Andrew C. Simpson, Jonathan M. D. Hill, Stephen R. Donaldson
• Keywords: Bulk Synchronous Parallel, Communicating Sequential Processes, Distributed And Parallel Computing, IPPS 1999, Transport Layer Protocol