| 摘要: |
| 并行计算作为人工智能发展的动力,使得并行算法的可解释性和安全性成为人工智能领域重要研究方向。形式化方法以数理逻辑为基础,已经成为复杂安全苛求系统可信构建的重要方法,而函数式编程则在算法领域中具有更强的数学表达性。本文旨在提出一种基于模型驱动的分治并行函数式程序生成及自动验证方法,融合形式化方法,以解决目前分治并行程序生成和验证中缺乏可解释性、易错、低可信度等问题。首先,采用分划递推法和循环不变式等新策略推导出串行算法;然后,利用辅助函数和算法连接函数将其提升为并行算法,并使用我们提出的并行算法设计语言Radl+进行描述;进而,采用同态定理验证框架在Isabelle中验证算法连接函数满足同态定理,即提升后的算法可并行化;最后,提出了Radl+→Haskell转换规则,设计了“Radl+→Haskell并行程序生成系统”软件原型。实验结果表明,本文能够生成和验证一系列算法的并行函数式程序,并且能够产生良好的加速比。本文方法不仅具有一定的可解释性,而且自动验证减少了传统手工验证易错性和繁琐的工作量,保证算法正确性和提高安全性,对大幅度提升高可信并行函数式程序的开发效率具有重要意义。 |
| 关键词: 模型驱动|分治并行|函数式程序|程序生成|自动验证 |
| DOI：10.19363/J.cnki.cn10-1380/tn.2023.05.07 |
| 投稿时间：2022-09-11修订日期：2022-12-12 |
| 基金项目:本课题得到国家自然科学基金项目(No. 62262031), 江西省教育厅科技重点项目(No. GJJ2200302, No. GJJ210307), 江西省研究生创新基金项目(No. YC2022-s349)资助。 |
|
| Model-driven Divide-and-conquer Parallel Functional Program Generation and Automatic Verification |
| WANG Changjing,WANG Zhongwen,PAN Cheng,HUANG qing,ZUO Zhengkang |
| School of Computer and Information Engineering, Jiangxi Normal University, Jiangxi 330022, China;Management science and Engineering Research Center, Jiangxi Normal University, Jiangxi 330022, China |
| Abstract: |
| Parallel computing as a driving force for the development of artificial intelligence has made the interpretability and security of parallel algorithms an important research direction in the field of artificial intelligence. Formal methods, based on mathematical logic, have become an important approach for the credible construction of complex secure caustic systems, while functional programming has a stronger mathematical expressiveness in the field of algorithms. The purpose of this paper is to propose a model-driven divide-and-conquer parallel functional program generation and automatic verification method by fusing formal methods to solve the current problems of lack of interpretability, error-prone, and low trustworthiness in divide-and-conquer parallel program generation and verification. First, a sequential algorithm is derived using the partition-and-recur method and the new strategy of loop invariant development; then, it is lifted to a parallel algorithm using auxiliary functions and algorithmic join functions and described using our proposed parallel algorithm design language Radl+; further, the homomorphism theorem verification framework is used to verify in Isabelle that the algorithmic connectivity functions satisfy the homomorphism theorem, i.e., the elevated algorithm is parallelizable; and Finally, we propose the Radl+→Haskell transformation rule and design a software prototype of “Radl+→Haskell Parallel Program Generation System”. The experimental results show that this paper can generate and verify parallel functional programs for a series of algorithms, and can produce good speedup. The method not only has certain interpretability, but also reduces the error-prone and tedious workload of traditional manual verification, ensures the correctness of algorithms and improves security, which is of great significance to significantly improve the development efficiency of highly trusted parallel functional programs. |
| Key words: model-driven|divide-and-conquer parallel|functional programing|program generation|automatic verification |
