AXIOMATIC FRAMEWORKS FOR DEVELOPING BSP-STYLE PROGRAMS*
作者:
A. STEWART,
M. CLINT,
J. GABARRÓ,
期刊:
Parallel Algorithms and Applications
(Taylor Available online 2000)
卷期:
Volume 14,
issue 4
页码: 271-292
ISSN:1063-7192
年代: 2000
DOI:10.1080/10637199808947391
出版商: Taylor & Francis Group
关键词: BSP;Axiomatic semantics;Program correctness
数据来源: Taylor
摘要:
In bulk-synchronous parallel (BSP) computation a superstep comprises a collection of concurrently executed processes with initial and terminal synchronisations. Data transfer between processes is realised through asynchronous communications. BSP programs can be organised either as explicit compositions of supersteps or as parallel compositions of threads (processes) which include synchronisation alignment operations. In this paper axiomatic semantics for the two approaches are proposed: in both cases the semantics are based on a new form of multiple substitution -predicate substitutionwhich generalises previous definitions of substitution.Predicate substitutiontogether with global synchronisation provide a means of linking state based and process semantics of BSP. Features of both models are illustrated through correctness proofs of matrix multiplication programs
点击下载:
PDF (537KB)
返 回