An Event-B Approach to the Development of Fork/Join Parallel Programs
Keywords:Event-B, Fork/Join, refinement, decomposition
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.
How to Cite
Copyright (c) 2022 Jie Peng, Tangliu Wen, Yiguo Yang, Guoming Huang
This work is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International License.
This is an open access article distributed under the terms of the CC BY-NC-SA 4.0, which permits copying, redistributing, remixing, transformation, and building upon the material in any medium so long as the original work is properly cited.