Model-driven Divide-and-conquer Parallel Functional Program Generation And Automatic Verification Method

With the development of big data and artificial intelligence,divide-and-conquer parallel is gaining increasing attention as a general parallel computing framework.It is the most potential way to improve multi-core resource utilization and execution efficiency.As one of the most popular programming paradigms,functional programming has incomparable advantages over imperative programming in the field of algorithms.It has a strong mathematical expressiveness,which makes it easier to be verified,and its transparency makes it easier to support parallel computing.However,the generation of divide-and-conquer parallel functional programs for complex algorithmic problems is currently a challenge,and their verification using traditional manual proof methods is not only error-prone but also low in confidence.In response to the above challenges,we propose a model-driven divide-and-conquer parallel functional program generation and automatic verification method by fusing formal method.First,the functional specification is obtained from the problem description,and the sequential algorithm described in Radl language is derived using the partition-and-recur method and the new strategy of loop invariant development;the corresponding auxiliary functions and algorithmic join functions are derived by extending and inducting the loop invariant,and the sequential algorithm is lifted to a parallel algorithm,which is described using our proposed parallel algorithmic design lan-guage Radl~+;furthermore,according to the unified verification framework of the homomorphic theorem defined by Locale,we verify that the algorithmic join function satisfies the homomorphic theorem,that is,the lifted algorithm can be parallelized;Finally,we propose the“Radl~+→Haskell transformation rule”and design the software prototype of“Radl~+→Haskell Parallel Program Generation System”based on this rule to convert parallel algorithm into Haskell parallel functional executable program,and the speedup experiment is conducted by GHC platform.The experimental results show that this paper is able to generate and verify parallel functional programs for a series of algorithms such as array minimization,polynomial valuation and maximal gene sequence,with certain interpretability and good speedup.The automatic verification reduces the traditional manual verification error-prone and tedious workload,ensures the correctness of the algorithms,and is of great significance to substantially improve the development efficiency of highly trusted parallel functional programs.