Towards Mechanised Semantics of HPC: The BSP with Subgroup Synchronisation Case
作者： Jean Fortin , Frédéric Gava
DOI: 10.1007/978-3-319-27161-3_20
关键词:
摘要: The underlying objective of this article is to exhibit the problems that might be encountered when working on a mechanised semantics an hpc language. We take for instance language program bsp algorithms with subgroup synchronisation i la mpi. give two using coq system and prove some common properties. By comparing sizes proofs, we discuss about potential scaling would arise if like extend work mainstream or adding more routines.
springer.com
sci-hub.st 参考文章(11)
Julien Tesson, Frédéric Loulergue, Formal semantics of DRMA-style programming in BSPlib parallel processing and applied mathematics. ,vol. 4967, pp. 1122- 1129 ,(2007) , 10.1007/978-3-540-68111-3_119
Jean-Christophe Filliâtre, Claude Marché, The Why/Krakatoa/Caduceus Platform for Deductive Program Verification Computer Aided Verification. pp. 173- 177 ,(2007) , 10.1007/978-3-540-73368-3_21
Andrew W. Appel, Sandrine Blazy, Separation logic for small-step cminor theorem proving in higher order logics. ,vol. 4732, pp. 5- 21 ,(2007) , 10.1007/978-3-540-74591-4_3
Rob H. Bisseling, Parallel Scientific Computation: A Structured Approach using BSP and MPI ,(2004)
Vikram S. Adve, Robert L. Bocchino, Marc Snir, Sarita V. Adve, Parallel programming must be deterministic by default usenix conference on hot topics in parallelism. pp. 4- 4 ,(2009)
Franck Cappello, Amina Guermouche, Marc Snir, On Communication Determinism in Parallel HPC Applications international conference on computer communications and networks. pp. 1- 8 ,(2010) , 10.1109/ICCCN.2010.5560143
Frédéric Gava, Jean Fortin, Two Formal Semantics of a Subset of the Paderborn University BSPlib parallel, distributed and network-based processing. pp. 44- 51 ,(2009) , 10.1109/PDP.2009.49
Jean Fortin, Frédéric Gava, BSP-Why: A Tool for Deductive Verification of BSP Algorithms with Subgroup Synchronisation International Journal of Parallel Programming. ,vol. 44, pp. 574- 597 ,(2016) , 10.1007/S10766-015-0360-Y
Guodong Li, Robert Palmer, Michael DeLisi, Ganesh Gopalakrishnan, Robert M. Kirby, Formal specification of MPI 2.0: Case study in specifying a practical concurrent programming API Science of Computer Programming. ,vol. 76, pp. 65- 81 ,(2011) , 10.1016/J.SCICO.2010.03.007
Xavier Leroy, Mechanized semantics - with applications to program proof and compiler verification. Logics and Languages for Reliability and Security. pp. 195- 224 ,(2010)