Abstract
BSP is a model of parallel computation which employs global synchronisation as a means of ensuring that a set of communications has reached completion. The efficiency properties of the model have been widely investigated. In this paper the model's associated semantic framework is studied. An axiomatic treatment of global synchronisation is presented. The proof rule proposed for synchronisation is evaluated in the context of semantic frameworks for a general parallel process model and for data-parallel computation.
Chapter PDF
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Apt K. R., Francez N., de Roever W. P.: A proof system for communicating sequential processes. ACM Trans. Programming Languages Systems,. 2 (3) (1980) 359–385.
Bouge L., Le Guyadec Y., Virot B., Utard G.: On the expressivity of a weakest precondition calculus for a simple data-parallel programming language. Parallel Processing: CONPAR 94-VAPP VI, eds: B. Buchberger & J. Volkert, LNCS 854, Springer-Verlag, pp 100–111, 1994.
Clint M.: Program proving: coroutines, Acta Informatica, 2 (1) (1973) 50–63.
Clint M., Narayana K. T.: Programming structures for synchronous parallelism, Parallel Computing 83, eds: F. Feilmeier, J. Joubert, U. Schendel, North-Holland, pp 405–412, 1984.
Dahl O.-J.: Verifiable Programming, Prentice-Hall International, 1992.
Dijkstra E. W.: A Discipline of Programming, Prentice-Hall, 1976.
FORTRAN 90 International Standard, ISO: IEC 1539: 1991.
Francez N.: Program Verification, Addison-Wesley, 1992.
Gabarro J., Gavalda R.: An approach to correctness of data parallel algorithms, Journal of Parallel and Distributed Computing, 22 (1994) 185–201.
Gerbessiotis A. V., Valiant L. G.: Direct bulk-synchronous parallel algorithms, Journal of Parallel and Distributed Computing, 22 (1994) 251–267.
Gries D.: The Science of Programming, Springer-Verlag, 1981.
Hoare C. A. R.: An axiomatic basis for computer programming, Comm. ACM, 12 (10) (1969) 576–580.
Hoare C. A. R.: Communicating Sequential Processes, Prentice Hall, 1985.
Jifeng H., Miller Q., Chen L.: Algebraic laws for BSP programming, Euro-Par 96 Parallel Processing, Vol. 2, eds: L. Bouge, P. Fraigniaud, A. Mignotte, Y. Robert, LNCS 1124, Springer-Verlag, pp 359–368, 1996.
Jones C. B.: Tentative steps towards a development method for interfering programs, ACM Trans. Programming Languages Systems,. 5 (4) (1983) 596–619.
Jones C. B.: Systematic Software Development using VDM (2nd edn.), Prentice Hall, 1990.
Levin G., Gries D.: Proof techniques for communicating sequential processes, Acta Informatica, 15 (1981) 281–302.
Owicki S., Gries D.: An axiomatic proof technique for parallel pograms, Acta Informatica, 6 (1976) 319–340.
Stewart A.: An axiomatic treatment of SIMD assignment, BIT, 30 (1990) 70–82.
Stewart A.: Reasoning about data-parallel array assignment, Journal of Parallel and Distributed Computing, 27 (1) (1995) 79–85.
Valiant L. G.: A bridging model for parallel computation, Comm. ACM, 33 (8) (1990) 103–111.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Stewart, A., Clint, M. (1997). Synchronising asynchronous communications. In: Lengauer, C., Griebl, M., Gorlatch, S. (eds) Euro-Par'97 Parallel Processing. Euro-Par 1997. Lecture Notes in Computer Science, vol 1300. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0002777
Download citation
DOI: https://doi.org/10.1007/BFb0002777
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63440-9
Online ISBN: 978-3-540-69549-3
eBook Packages: Springer Book Archive