Research Article
An Event-B Approach to the Development of Fork/Join Parallel Programs
@ARTICLE{10.4108/airo.v1i.16, author={Jie Peng and Tangliu Wen and Yiguo Yang and Guoming Huang}, title={An Event-B Approach to the Development of Fork/Join Parallel Programs}, journal={EAI Endorsed Transactions on AI and Robotics}, volume={1}, number={1}, publisher={EAI}, journal_a={AIRO}, year={2022}, month={2}, keywords={Event-B, Fork/Join, refinement, decomposition}, doi={10.4108/airo.v1i.16} }- Jie Peng
Tangliu Wen
Yiguo Yang
Guoming Huang
Year: 2022
An Event-B Approach to the Development of Fork/Join Parallel Programs
AIRO
EAI
DOI: 10.4108/airo.v1i.16
Abstract
Fork/Join is a simple but effective technique for exploiting the parallelism. When developing a parallel program using Fork/Join, one of the main things is how a large task is decomposed into subtasks whose results can be combined as a final result. In this paper we show how to develop Fork/Join parallel programs through refinement and decomposition. We take Fork/Join style task decomposition as a refinement which we call Fork/Join refinement. Proof obligations of refinement can ensure the correctness of decomposition. For practical application, we provide a refinement pattern for the Fork/Join refinement and extend an atomicity decomposition diagram to illustrate it. Our approach provides a good framework for modeling Fork/Join parallel programs and showing proof obligations of correctness for such programs. We illustrate the approach by applying it on a small case.
Copyright © 2022 Jie Peng et al., licensed to EAI. This is an open access article distributed under the terms of the Creative Commons Attribution license, which permits unlimited use, distribution and reproduction in any medium so long as the original work is properly cited.