About | Contact Us | Register | Login
ProceedingsSeriesJournalsSearchEAI
airo 22(1): 6

Research Article

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

Download469 downloads
Cite
BibTeX Plain Text
  • @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
Jie Peng1, Tangliu Wen1,*, Yiguo Yang2, Guoming Huang1
  • 1: Gannan University of Science and Technology, Ganan 341000, China
  • 2: School of Computer Engineering and Science, Shanghai University, Shanghai 2000444,China
*Contact email: 779137104@qq.com

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
Event-B, Fork/Join, refinement, decomposition
Received
2021-12-23
Accepted
2022-02-01
Published
2022-02-18
Publisher
EAI
http://dx.doi.org/10.4108/airo.v1i.16

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.

EBSCOProQuestDBLPDOAJPortico
EAI Logo

About EAI

  • Who We Are
  • Leadership
  • Research Areas
  • Partners
  • Media Center

Community

  • Membership
  • Conference
  • Recognition
  • Sponsor Us

Publish with EAI

  • Publishing
  • Journals
  • Proceedings
  • Books
  • EUDL