
An Event-B Approach to the Development of Fork/Join Parallel Programs
Published: 18 February 2022
Eai Endorsed Transactions on AI and Robotics
,
Volume 1,
pp 1-6; https://doi.org/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.
Keywords: Fork/Join parallel programs / illustrate / decomposition / refinement / modeling / obligations
Scifeed alert for new publications
Never miss any articles matching your research from any publisher- Get alerts for new papers matching your research
- Find out the new papers from selected authors
- Updated daily for 49'000+ journals and 6000+ publishers
- Define your Scifeed now
Click here to see the statistics on "Eai Endorsed Transactions on AI and Robotics" .