×

A bulk-synchronous parallel process algebra. (English) Zbl 1112.68105

Summary: The Calculus of Communicating Systems (CCS) process algebra is a well-known formal model of synchronization and communication. It is used for the analysis of safety and liveness in protocols or distributed programs. In more recent work, it is used for the analysis of security properties. Bulk-Synchronous Parallelism (BSP) is an algorithm and programming model of data-parallel computation. It is useful for the design, analysis and programming of scalable parallel algorithms. Many current evolutions require the integration of distributed and parallel programming: grid systems for sharing resources across the Internet, secure and reliable global access to parallel computer systems, geographic distribution of confidential data on randomly accessible systems, etc. Such software services must provide guarantees of safety, liveness, security together with scalable and reliable performance. Formal models are therefore needed to combine parallel performance and concurrent behavior. With this goal in mind, we propose here an integration of BSP with CCS semantics, generalize its cost (performance) model and sketch its application to scheduling problems in meta-computing.

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)

Software:

BSPedupack; BSPlib; MPI
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Loulergue, F.; Hains, G.; Foisy, C., A calculus of functional BSP programs, Science of Computer Programming, 37, 1-3, 253-277 (2000) · Zbl 0954.68036
[2] Valiant, L., A bridging model for parallel computation, Communications of the ACM, 33, 8, 103 (1990)
[3] Skillicorn, D.; Hill, J. M.D.; McColl, W. F., Questions and answers about bsp, Scientific Programming, 6, 3, 249-274 (1997)
[4] Bisseling, R., Parallel scientific computation, a structured approach using BSP and MPI (2004), Oxford University Press: Oxford University Press Oxford · Zbl 1059.65133
[5] Nemeth, Z.; Sunderam, V., Characterizing grids: attributes, definitions, and formalisms, Journal of Grid Computing, 1, 9-23 (2003)
[6] (Foster, I.; Kesselman, C., The grid: blueprint for a new computing infrastructure (1999), Morgan Kaufmann: Morgan Kaufmann Los Altos, CA)
[7] Milner R. Operational and algebraic semantics of concurrent processes. In: Van Leeuwen J, editors. Handbook of theoretical computer science. Amsterdam, Cambridge, MA: North-Holland, MIT-Press; 1990.; Milner R. Operational and algebraic semantics of concurrent processes. In: Van Leeuwen J, editors. Handbook of theoretical computer science. Amsterdam, Cambridge, MA: North-Holland, MIT-Press; 1990.
[8] Milner, R., Communication and concurrency (1989), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ · Zbl 0683.68008
[9] (Van Leeuwen, J., Handbook of theoretical computer science (1990), North-Holland, MIT-Press: North-Holland, MIT-Press Amsterdam, Cambridge, MA) · Zbl 0712.68054
[10] Gondran, M.; Minoux, M.; Vajda, S., Graphs and algorithms (1984), Wiley: Wiley New York
[11] Krishnan P. Distributed CCS. In: Theories of concurrency: unification and extension: CONCUR-91. Lecture notes in computer science, vol. 527. Berlin: Springer; August 1991. p. 393-407.; Krishnan P. Distributed CCS. In: Theories of concurrency: unification and extension: CONCUR-91. Lecture notes in computer science, vol. 527. Berlin: Springer; August 1991. p. 393-407.
[12] Rebeuf X. Un modèle de coût symbolique pour les programmes parallèles asynchrones à dépendances structurées. Thèse de Doctorat d’Université, Université d’Orléans, Décembre 2000.; Rebeuf X. Un modèle de coût symbolique pour les programmes parallèles asynchrones à dépendances structurées. Thèse de Doctorat d’Université, Université d’Orléans, Décembre 2000.
[13] Benoit, A.; Cole, M.; Gilmore, S.; Hillston, J., Evaluating the performances of skeleton-based high level parallel programs, (Bubak, M.; van Albada, D.; Sloot, P.; Dongarra, J., The international conference on computational science (ICCS 2004), Part III. Lecture notes in computer science (2004), Springer: Springer Berlin), 299-306
[14] Prasad KVS. Combinators and bisimulation proofs for restartable systems. PhD thesis, University of Edinburgh; December 1987.; Prasad KVS. Combinators and bisimulation proofs for restartable systems. PhD thesis, University of Edinburgh; December 1987.
[15] Aceto, L.; Jeffrey, A., A complete axiomatization of timed bisimulation for a class of timed regular behaviours, Theoretical Computer Science, 152, 2, 251-268 (1995) · Zbl 0872.68039
[16] Katoen J-P, D’Argenio PR. General distributions in process algebra. Lecture notes in computer science, vol. 2090; 2001.; Katoen J-P, D’Argenio PR. General distributions in process algebra. Lecture notes in computer science, vol. 2090; 2001.
[17] Chen J. A timed mobile calculus. In: The 16th Nordic workshop on programming theory (NWPT’04); 2004.; Chen J. A timed mobile calculus. In: The 16th Nordic workshop on programming theory (NWPT’04); 2004.
[18] Milner, R.; Parrow, J.; Walker, D., A calculus of mobile processes, I and II, Information and Computation, 100, 1, 1-40 (1992), and 41-77 · Zbl 0752.68036
[19] Fournet G, Gonthier G. The reflexive CHAM and the join-calculus. In: 23rd annual ACM symposium on principles of programming languages (POPL’96), St. Petersburg, FL, USA; January 1996. p. 371-385.; Fournet G, Gonthier G. The reflexive CHAM and the join-calculus. In: 23rd annual ACM symposium on principles of programming languages (POPL’96), St. Petersburg, FL, USA; January 1996. p. 371-385.
[20] Snir, M.; Gropp, W., MPI the complete reference (1998), MIT Press: MIT Press Cambridge, MA
[21] Hill, J. M.D.; McColl, B.; Stefanescu, D. C.; Goudreau, M. W.; Lang, K.; Rao, S. B., Bsplib: the bsp programming library, Parallel Computing, 24, 14, 1947-1980 (1998)
[22] Anantharaman S, Hains G. A synchronous bisimulation-based approach for information flow analysis. In: Third workshop on automated verification of critical systems: (AVOCS’03); April 2003.; Anantharaman S, Hains G. A synchronous bisimulation-based approach for information flow analysis. In: Third workshop on automated verification of critical systems: (AVOCS’03); April 2003.
[23] Loulergue F. Parallel juxtaposition for bulk synchronous parallel ML. In Kosch H, Boszorményi L, Hellwagner H. editors. Euro-Par 2003. Lecture notes in computer science, vol. 2790. Berlin: Springer; 2003. p. 781-8.; Loulergue F. Parallel juxtaposition for bulk synchronous parallel ML. In Kosch H, Boszorményi L, Hellwagner H. editors. Euro-Par 2003. Lecture notes in computer science, vol. 2790. Berlin: Springer; 2003. p. 781-8. · Zbl 1033.68532
[24] Loulergue F. Parallel superposition for bulk synchronous parallel ML, In: Sloot PMA, et al. editors. International conference on computational science (ICCS 2003), Part III, Lecture notes in computer science, vol. 2659. Berlin: Springer; June 2003. p. 223-32.; Loulergue F. Parallel superposition for bulk synchronous parallel ML, In: Sloot PMA, et al. editors. International conference on computational science (ICCS 2003), Part III, Lecture notes in computer science, vol. 2659. Berlin: Springer; June 2003. p. 223-32.
[25] Merlin A. Modéles opérationnels communicants, performances et algébres de chemins. Thèse de Doctorat d’Université, Université d’Orléans, Décembre 2004.; Merlin A. Modéles opérationnels communicants, performances et algébres de chemins. Thèse de Doctorat d’Université, Université d’Orléans, Décembre 2004.
[26] Lafrance S, Mullins J. Using admissible interference to detect denial of service vulnerabilities. In: Morris JM, Aziz B, Oehl F. editors. Sixth international workshop in formal methods. Electronic workshops in computing (eWiC), British Computer Society (BCS); 2003.; Lafrance S, Mullins J. Using admissible interference to detect denial of service vulnerabilities. In: Morris JM, Aziz B, Oehl F. editors. Sixth international workshop in formal methods. Electronic workshops in computing (eWiC), British Computer Society (BCS); 2003.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.