Open AccessAn Event-B Approach to the Development of Fork/Join Parallel Programs
Author(s) -
Jie Peng,
Tangliu Wen,
Yiguo Yang,
Guoming Huang
Publication year - 2022
Publication title -
eai endorsed transactions on artificial intelligence and robotics
Language(s) - English
Resource type - Journals
ISSN - 2790-7511
DOI - 10.4108/airo.v1i.16
Subject(s) - fork (system call) , computer science , correctness , join (topology) , fork–join queue , atomicity , task (project management) , decomposition , theoretical computer science , programming language , parallel computing , algorithm , mathematics , operating system , ecology , database transaction , management , combinatorics , economics , queue , queue management system , biology
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.