An Event-B Approach to the Development of Fork/Join Parallel Programs

Authors

  • Jie Peng Gannan University of Science and Technology, Ganan 341000, China
  • Tangliu Wen Gannan University of Science and Technology, Ganan 341000, China
  • Yiguo Yang School of Computer Engineering and Science, Shanghai University, Shanghai 2000444,China
  • Guoming Huang Gannan University of Science and Technology, Ganan 341000, China

DOI:

https://doi.org/10.4108/airo.v1i.16

Keywords:

Event-B, Fork/Join, refinement, decomposition

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.

Downloads

Download data is not yet available.

Downloads

Published

18-02-2022

How to Cite

[1]
J. Peng, . T. Wen, Y. Yang, and G. Huang, “An Event-B Approach to the Development of Fork/Join Parallel Programs”, EAI Endorsed Trans AI Robotics, vol. 1, p. e6, Feb. 2022.

Most read articles by the same author(s)