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 fixed buffer capacities on both sender and receiver. This protocol is modelled using CSP, and verified using the refinement checker FDR2. This verification 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.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
S. D. Brookes and A. W. Roscoe. An improved failures model for communicating processes. In S. D. Brookes, A. W. Roscoe, and G. Winskel, editors, Proceedings of the NSF-SERC Seminar on Concurrency, pages 281–305. Springer-Verlag Lecture Notes in Computer Science, volume 197, 1985.
S. R. Donaldson, J. M. D. Hill, and D. B. Skillicorn. BSP cluster: high performance, reliable and very low cost. Parallel Computing: Special Issue on Cluster Computing, 1998. Submitted for publication.
S. R. Donaldson, J. M. D. Hill, and D. B. Skillicorn. Performance results for a reliable low-latency cluster communication protocol. In PC-NOW ’99: International Workshop on Personal Computer based Networks Of Workstations, held in conjunction with IPPS’99 (under submission), 1999.
Message Passing Interface Forum. MPI A Message-Passing Interface Standard, May 1994.
J. M. D. Hill, B. McColl, D. C. Stefanescu, M. W. Goudreau, K. Lang, S. B. Rao, T. Suel, T. Tsantilas, and R. Bisseling. BSPlib: The BSP Programming Library. Technical Report PRG-TR-29-97, Oxford University Computing Laboratory, May 1997.
C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall International, 1985.
A. W. Roscoe. Model checking CSP. In A. W. Roscoe, editor, A Classical Mind: Essays in honour of C.A.R. Hoare, pages 353–378. Prentice-Hall International, 1994.
A. W. Roscoe. The Theory and Practice of Concurrency. Prentice-Hall International 1997.
A. C. Simpson, J. C. P. Woodcock, and J. W. Davies. Safety through security. In Proceedings of the Ninth International Workshop on Software Specification and Design, pages 18–24. IEEE Computer Society Press, 1998.
D. B. Skillicorn, J. M. D. Hill, and W. F. McColl. Questions and answers about BSP. Scientific Programming, 6 (3):249–274, Fall 1997.
L. G. Valiant. A bridging model for parallel computation. Journal of the ACM, 33(8):103–111, August 1990.
L. G. Valiant. Bulk-synchronous parallel computer. U.S. Patent No. 5083265, 1992.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1999 Springer-Verlag
About this paper
Cite this paper
Simpson, A.C., Hill, J.M.D., Donaldson, S.R. (1999). BSP in CSP: Easy as ABC. In: Rolim, J., et al. Parallel and Distributed Processing. IPPS 1999. Lecture Notes in Computer Science, vol 1586. Springer, Berlin, Heidelberg . https://doi.org/10.1007/BFb0098009
Download citation
DOI: https://doi.org/10.1007/BFb0098009
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65831-3
Online ISBN: 978-3-540-48932-0
eBook Packages: Springer Book Archive