基于模型驱动的分治并行函数式程序生成及自动验证

王昌晶, 王忠文, 潘 丞 , 黄 箐, 左正康

1江西师范大学计算机信息工程学院 江西 中国 330022

2江西师范大学管理科学与工程研究中心 江西 中国 330022

1 引言

随着大数据和人工智能的发展, 并行计算已经成为实现高性能计算的主要技术手段。分治法[1]作为一种通用的并行计算框架日益受到重视, 它是提高多核资源利用率和执行效率最有潜力的途径。分治法的主要思想是将一个复杂问题分解为规模更小、结构与原问题一致的子问题进行并行计算, 递归地求解子问题, 最终将子问题的解进行合并得到原问题的解, 它能够充分地发挥多核处理器性能, 高效利用计算机空间资源且提高任务的执行效率。

并行算法是并行计算的核心和瓶颈技术[2], 因此并行算法的正确性是提高网络环境下软件可靠性的关键。形式化方法是基于严格数学基础, 对计算机硬件和软件系统进行描述、开发和验证的技术[3], 是并行算法高可信的根本保证。大量的工业实践表明,形式化方法已经成为复杂安全苛求系统可信构建的重要方法, 在处理软件开发复杂性和提高软件可靠性方面具有无可取代的潜力。随着形式化验证技术的发展, 在形式化研究领域出现了许多性能优良的程序证明器, 在数学定理证明、软/硬件验证等方面发挥着重要作用, 如Coq[4]、Dafny[5]和Isabelle[6]等。其中Isabelle是基于高阶逻辑的交互式定理证明器[7],作为最具代表性之一的程序证明器, 它既支持多种对象逻辑又允许自定义新逻辑, 具有丰富的类型系统、强大的规则库和灵活高效的命令集, 同时能够充分利用多核处理器并行证明[8], 达到了“提高验证效率和保证算法程序的高可信”的目标。

高可信并行算法的生成及验证, 已经逐渐成为计算机科学非常热门的一个研究方向。现有的大多数并行算法生成研究, 串行算法是直接通过经验给出的, 算法连接函数和辅助函数的获得需要更多的信息, 如弱右逆[9]; 或通过特定的重写规则[10]或合成算法[11]。并行算法的验证, 需要证明串行算法提升至并行算法满足可并行性的同态定理, 现有的传统手工证明方法对其验证, 不仅易错, 且可信度低; 或采用验证工具如Dafny, Dafny的类与类之间仅支持有限的继承, 代码存在冗余, 通用性和可复用性较弱[12];且Dafny是一种命令式与函数式混合的描述语言,在验证时探索前后置条件以及大量的中间断言是一段相当痛苦的过程[13]。

针对上述挑战, 融合形式化方法, 本文提出了一种基于模型驱动的分治并行函数式程序生成方法及自动验证方法。模型驱动开发是一种面向模型的新型软件设计方法[14]。在该方法中, 模型转换是软件开发的核心, 软件的各个方面由各种模型来表达,最终的软件由模型通过模型转换来生成。该方法使得软件开发人员不必再去关心编程语言的细节和执行平台的特性, 提高了软件工程的抽象和自动化水平。

首先, 将问题抽象为功能规约, 并通过本团队提出的分划递推法[15]和循环不变式开发新策略[16]推导出用Radl描述的串行算法; 通过对循环不变式进行展开并归纳, 推导得到相应的辅助函数和算法连接函数, 将串行算法进行提升得到原问题用Radl+描述的并行算法; 进而, 利用Isabelle定理证明器来自动验证算法连接函数满足同态定理[17], 即提升后的算法满足可并行性。

函数式编程已经成为当前最流行的编程模式之一, 它作为一种采用函数进行程序设计的编程范式,比命令式编程具有更强的数学表达性[18], 更加强调对函数的计算而不是对指令的运行, 能够极大减少代码量、软件开发时间及成本, 有利于降低软件复杂性。同时, 函数式编程不会产生副作用, 不需要考虑死锁, 利于部署多个线程的并行计算, 因此天然支持并行。Haskell[19]作为当前比较流行的一门通用的纯函数式编程语言, 具有简洁、表达力强的语法和丰富的内置数据类型, 提供了抽象的编程能力, 且易于维护。

最后, 通过本文设计的“Radl+→Haskell并行程序生成系统”软件原型将并行算法转换为Haskell并行函数式可执行程序。实验结果表明, 本文能够生成和验证数组最小和、最大基因序列等一系列算法的并行函数式程序。自动验证减少了传统手工验证易错性和繁琐的工作量, 保证了算法正确性, 对大幅度提升高可信并行函数式程序的开发效率具有重要意义。

本文提出一种基于模型驱动的分治并行程序生成及自动验证方法。本文创新点如下:

1) 提出一种基于模型驱动的方法将复杂算法问题生成分治并行函数式程序, 首次实现从抽象规约到具体分治并行函数式程序完整的生成过程。本文首先使用分划递推法推导出串行算法, 然后基于循环不变式的扩展与归纳来得到辅助函数和算法连接函数, 以将串行算法提升为并行算法。该方法的串行算法是通过推导得到的, 而非经验给出。算法连接函数和辅助函数生成的输入只需要串行算法, 生成过程更加系统和一般化。

2) 使用Isabelle定理证明器对提升后的算法满足同态定理自动验证, 证明该算法的可并行化, 保障了并行算法的可靠性并提高了验证效率。使用Isabelle较Dafny通用性和复用性更强, 也无须在验证时探索前后置条件以及大量的中间断言。

3) 将验证成功的Radl+并行算法通过设计的软件原型和转换规则映射为具体的Haskell并行函数式程序, 生成的函数式程序具有良好的扩展性和天然的并行性。基于原型系统, 本文通过模型驱动方法对一系列典型案例生成了Haskell并行函数式程序。

本文的组织结构如下: 第2节阐述本文提出的模型驱动的分治并行程序设计及自动验证方法步骤;第3节简述问题规约到串行算法的推导过程; 第4节阐述串行算法如何提升至并行算法; 第5节通过Isabelle验证并行算法的可并行性; 第6节介绍Haskell并行函数式程序的生成; 第7节通过实验验证了本文方法具有良好的加速比; 第8节介绍相关工作; 第9节总结全文并介绍未来工作展望。

2 基于模型驱动的分治并行函数式程序生成及自动验证方法

针对复杂算法问题分治并行函数式程序生成及验证的挑战, 本文将模型驱动方法与形式化方法结合, 研究关于复杂线性算法问题的并行程序生成及验证的完整过程。首先将问题规约进行变换至用Radl[20](Recurrence-based Algorithm Design Language)描述的串行算法, 然后构造辅助函数和算法连接函数将算法提升至用Radl+描述的并行算法, 进而使用Isabelle对该并行算法满足同态定理进行自动验证,最终将验证成功的可并行化算法映射至Haskell并行函数式程序。

本文主要针对在列表上的单路(Single-pass)函数,且求解该函数的串行程序是单层循环(无嵌套循环)结构, 采用分治并行模式来设计和生成并行程序。假设类型S是一个列表的类型, 类型Sc是该列表元素的任一具体类型, 如int, float, char和bool等。下面给出单路函数的正式定义[21]。

定义1.(左向函数, 右向函数) 函数h:S→Sc是左向函数, 当且仅当存在一个二元连接算子⊕, 使得h([a]•x)=a⊕h(x); 函数h是右向函数, 当且仅当存在一个二元连接算子⊗, 使得h(x•[a])=h(x)⊗a。

定义2.(单路函数) 函数h:S→Sc是单路函数,当且仅当h是左向或右向函数。

假设一个计算f(a)的分治并行模式策略如下:

上述f(a)表示函数f作用于列表a, 分划算子ɣ通过一个分划函数将a分划为n个子列表且并行计算它们的结果, 连接算子⊙利用算法连接函数合并子列表的值, 直至最终合并为一个结果, 其中每一层的合并均可并行执行。基于分治并行模式驱动的函数f计算过程如图1所示:

图1 函数f的分治并行计算Figure 1 D&C parallel computing of function f

模型驱动的分治并行函数式程序生成及自动验证方法步骤如图2所示, 分为如下四个阶段:

图2 模型驱动的分治并行函数式程序生成及自动验证方法步骤Figure 2 Model-driven D&C parallel functional program generation and automatic verification method steps

第一阶段, 从问题描述出发, 用Radl语言精确地描述求解问题的功能规约, 正确使用分划递推法和量词特性对其进行规约变换, 构造问题求解的递推关系,并根据本团队提出循环不变式的开发新策略来构造问题的循环不变式, 基于所得的递推关系和循环不变式进行算法构造, 得到求解问题的Radl串行算法;

第二阶段, 对循环不变式进行展开并归纳, 推导得到需要添加的辅助函数(目标函数不可直接并行时)和算法连接函数。将辅助函数和算法连接函数组合构造得到分治并行算法。为Radl语言添加并行性描述, 扩充为用于描述分治并行算法的Radl+语言,对提升得到的并行算法进行描述;

第三阶段, 从定理的角度去证明满足同态定理性质的函数一定是可并行的, 通过定理证明器Isabelle定义相关函数, 创建算法连接函数满足同态定理的相关引理, 自动验证并行算法的可并行性;

第四阶段, 通过设计的“Radl+→Haskell并行程序生成系统”软件原型和提出的“Radl+→Haskell转换规则”将Radl+算法映射为具体可执行的Haskell并行函数式程序, 并放至GHC平台[22]运行

3 串行算法生成

本文首先从问题规约出发, 使用本研究团队提出的分划递推法[15], 基于规约变换规则构造求解问题的所有递推关系, 并通过循环不变式的开发策略推导求解问题的循环不变式, 最终得到求解问题的具有单重循环结构的串行算法, 并使用Radl语言描述。

3.1 分划递推法

为精确地刻画问题的功能规约, 令q表示满足交换律和结合律的二元运算符, 量词Q表示q对任何集合的应用, 则量词Q(除N外)是q的一般化, 并进行如下约定: ∀代表全称量词、∃代表存在量词、Σ代表求和量词、Π代表求积量词、N代表计数量词、MAX和MIN分别代表极大和极小量词等。即∀是逻辑运算符⋀的一般化, ∃是⋁的一般化, Σ是+的一般化, Π是*的一般化,MAX和MIN分别是max和min的一般化。

在本文中, 我们以AQ表示问题的前置条件,AR表示问题的后置条件,S表示求解问题的程序。根据Hoare逻辑得到以下Hoare三元组[23,24]规约:

式(2)表示S在执行前满足条件AQ, 在终止后满足条件AR。同时AR可以定义为以下形式:

式(3)表示在范围r(i)上q对函数f(i)进行q运算所得的量, 其中i表示约束于Q的变量,q是Q的一般化, 表示满足交换律和结合律的二元运算符。

功能规约和普通程序的一个显著区别是可以对功能规约进行数学推演(公式推演), 使其从一种形式变换为另一种形式。功能规约有两个作用: 第一, 判断程序的多种规范形式是否等价; 第二, 变换功能规约, 寻找求解问题的算法。本文主要涉及第二个作用, 具体规则如下:

规则1.单点范围 (Qi:i=k:f(i))=f(k)

规则2.范围分裂

(Qi:r(i):f(i))=(Qi:r(i)

⋀b(i):f(i))q(Qi:r(i)⋀¬b(i):f(i))

规则3.交叉积

(Qi,J:r(i)⋀s(i,J):f(i,J))

=(Qi:r(i):(QJ:s(i,J):f(i,J)))

其中J表示任何约束变量的非空集合。

规则4.一般分配律 如果⊙对q满足分配律,i不是函数g的自由变量, 则有:

分划递推法的主要思想是应用数学工具、程序设计知识和领域知识推导产生问题求解的设计思想和方法并给出它的形式规约表达, 功能规约通过上述规则1-4可以进行等价变换, 将复杂问题分划为一系列更简单的子问题, 并通过不断地推导可以得到问题求解的递推关系, 有利于解决复杂问题, 减小问题功能规约向算法程序转变的难度, 对软件自动化具有重要意义。分划递推法的定义如下:

定义3.(分划递推法) 假设问题P的解可分划为由n个计算步产生的结果序列AR1,AR2,…,ARn,且∀i,j:ARi∩ARj=∅, 其中1≤i＜j≤n, 则每一ARi都是问题P的子解, 等式ARj=F()表示ARj是其子解的函数, 其中表示多个子解ARi的序列, 则ARn是问题P的解, 称ARj=F()为求解问题P的递推关系。通过上述分划和递归过程得到问题P的递推关系的方法, 称为分划递推法。

下面以数组最小和问题作为全文的运行实例来详细说明本文提出的方法。本节先给出通过分划递归法推导得到该问题的两个递归关系:

数组最小和实例给定一串已知长度的实数序列并将元素存放于数组a[0:n], 计算a中相邻元素的最小和mss。则该问题的前置条件AQ为n≥0, 后置条件AR为mss(n)≡(MINi,j:0≤i≤j≤n:sum(i,j)), 其中sum(i,j)=Σk:i≤k≤j:a[k], 表示a的子段元素a[i]~a[j]之和, 函数mss称为求解实例的目标函数。

下面通过规则1-4对AR进行规约变换:

式(4)已经得到了mss的递推关系式, 其包含了函数mts, 继续通过规则1~4对mts(n)进行转换:

通过上述转换, 最终得到原问题的全部递推关系, 如式(6)所示:

3.2 开发循环不变式

循环不变式是推导、开发和证明算法程序的基础和关键, 体现了循环程序的本质特征, 在形式化方法中占有重要的地位。传统的循环不变式定义和开发策略只能推导一些简单问题的循环不变式, 而对于相对复杂的算法问题很难得到满意的结果。

本研究团队在文献[16]中已经提出循环不变式的新定义和开发策略:

定义4(循环不变式) 给定循环DO和它的所有循环变量的集合A, 一个反映A中每一元素的变化规律并在每次循环执行前后均为真的谓词称作循环DO的循环不变式。

令I表示DO的循环不变式, 由定义4定义的I表示A的函数I(A)。集合A由若干个子集组成: 循环变量集合X、AR中出现的循环变量Y和集合Z, 其中Z=A-X-Y。这样DO的前置断言用AQ(A)表示, 后置断言用AR(Y)表示。

策略1(适用于现存的算法程序) 以循环程序正确性验证为基准, 考察循环初始条件及循环结束所得的信息, 分析程序所解问题的实际背景、数学性质和程序特征, 通过归纳推理找出所有循环变量的变化规律, 即为所求循环不变式。

策略2(适用于待开发的算法程序) 考察被求解问题的前后置断言和数学特性, 利用行之有效的算法设计方法确定解问题的总策略(在很多情况下是确定问题求解序列的递推关系)和所需的全部循环变量,用谓词描述每一变量的变化规律, 即为所求循环不变式; 若递推关系中子解数超过1, 则还需引进一集合变量或一起堆栈作用的序列变量, 递归定义序列中的内容。

数组最小和实例根据定义4和策略2(本实例属于待开发问题), 首先通过归纳推理找出所有循环变量的变化规律, 分别用状态变量t和s存放递推关系中mts(i)和mss(i)的值, 并约束循环控制变量i的变化范围, 然后用谓词精确表达上述循环变量的变化规律, 从而得到原问题的循环不变式inv为:

3.3 串行算法生成

Radl是一种基于递推关系的算法设计语言[20],它是为实现算法程序形式化和半自动开发的分划递推方法而定义的, 其主要功能是描述问题规约、规约变换规则和算法。用Radl描述串行算法的一般形式如下:

Radl ALGORITHM:

|[Initialized definitions of operational variables]|

{AQ^AR}

BEGIN:

TERMINATION:

RECUR:

END

一个给定问题的串行算法设计可以分为以下三个步骤:

1) 用Radl语言精确地形式化描述问题的功能规约, 即算法要完成的工作;

2) 通过分划递推法将问题按照3.1节的各规则分划为若干与原问题结构相同但规模更小的子问题, 然后对子问题继续分划, 直至每一个子问题都能直接求解(最小子问题), 构造出求解问题的递推关系;

3) 通过3.2节提出的策略推导出原问题的循环不变式, 确定递推关系中变量的初值和递推的终止条件, 最终组合构造得到原问题的串行算法。

数组最小和实例根据式(6)和式(7), 可以得到如下数组最小和的串行算法(由Radl语言描述), 其中t表示第i次循环时a以a[i]为终点的最小子段和,s表示第i次循环时子段a[0..i]中相邻元素的最小和,i=1++1表示变量i的初始值为1, 每次循环增长1。

ALGORITHM 1.mss串行算法.

|[Inn:integer,a:array[0..n,integer];Aux i:integer;Outs,c:integer]|

{AQ}⋀{AR}

BEGIN:t,s=a[0],a[0];i= 1++1

TERMINATION:i=n+1

RECUR:

t=min(t+a[i],a[i])

s=min(s,t)

END

4 串行算法提升

当串行算法可直接并行时, 可用目标函数对子问题并行求解, 然后采用算法连接函数对其直接合并。而当串行算法不可直接并行时, 可通过本文提出的策略3推导出辅助函数, 将其与目标函数一并添加至算法连接函数的参数中, 提升至能有效进行分治连接的并行算法, 并使用Radl+语言描述。其中本文针对两种情形下的算法连接函数构造提出了开发方法(策略4)。

4.1 辅助函数

本文的辅助函数是由不可直接并行的串行算法提升为并行算法所需要额外构造的函数, 它对算法提升起辅助作用。假设类型S是一个列表的类型, 类型Sc是该列表元素的任一具体类型, 如int, float,char和bool等。下面给出可直接并行函数和辅助函数的定义。

定义5.(可直接并行函数) 函数h:S→Sc是可直接并行函数, 当且仅当h(x•y)=h(x)⊙h(y), 其中•:S×S→S是S上的列表拼接运算, ⊙:Sc×Sc→Sc是Sc上的连接运算。

定义6.(辅助函数) 若函数h:S→Sc作用在列表x•y上的解可通过h(x•y)=(f(x),φ(x))⊙(f(y),φ(y))得到, 且φ≠0, 其中h=(f,φ),f是问题求解的目标函数,φ是计算f的辅助函数。

根据定义5可知, 若函数h可以通过一个连接算子⊙直接合并其左子序列x和右子序列y的分治计算结果, 则称h是可直接并行的, 此时串行算法在不需要辅助函数的情况下可直接提升为并行算法, 如图3所示。

图3 并行算法生成步骤Figure 3 Parallel algorithm generation steps

在算法设计中许多基于列表的函数是不可直接并行的, 即大部分复杂算法问题在分划成子问题后分治计算得到的结果不能轻易地直接合并, 此时需构造合适的辅助函数φ并将其添加到h的算法连接函数中, 才能提升为并行算法。

根据定义6, 我们提出了辅助函数的开发策略,如策略3所示。

策略3.(辅助函数开发策略) 当函数不可直接并行时, 通过归纳法将问题的循环不变式进行展开, 然后将原问题上的解分为两个部分(即目标函数f分别作用在左子序列和右子序列上的解), 在连接算子⊙的参数列表中(或称h的元组中)将目标函数剔除, 剩余函数部分φ即为所需额外构造的辅助函数。

数组最小和实例以ti,si分别记录状态变量t,s在第i次循环的状态。为便于观察分治过程, 以ti..j,si..j分别记录mts(i..j) ,mss(i..j)的值, 表示mts,mss作用在子列表a[i:j]上的结果。对3.2节得到的循环不变式即式(7)进行展开, 可得。

式(8)中以mi..j记录sum(i,j)的值, 表示sum作用在子列表a[i:j]上的结果。与式(4)函数mts(j)表示以a[j]为终点的最小子段和类似, 式(9)中mps(n)=(MINi:0≤i≤n:sum(0,i))表示以a[0]为起点的最小子段和, 且以pi..j表示mps作用在子列表a[i:j]上的结果。对式(8)和式(9)继续展开:

根据策略3, 从式(8)和式(10)可推导出sum是计算mts的辅助函数, 从式(9)和式(11)可推导出mts和mps是计算mss的辅助函数。

4.2 算法连接函数

算法连接函数是在原问题分划成子问题后进行合并的函数, 即连接算子⊙对应的函数。当问题采用分治并行模式求解时, 该问题将被分解成若干子问题并行求解, 最终需推导合适的算法连接函数将这些子问题的解合并为原问题的解。基于策略3, 本文针对两种情形下的算法连接函数构造, 提出了以下算法连接函数的开发策略:

策略4.(算法连接函数开发策略) 当目标函数f作用在列表x•y上可直接并行时, 算法连接函数的参数由目标函数分别作用在左、右子序列的值fx和fy组成; 否则, 需通过策略2对循环不变式展开并归纳, 根据归纳结果构造辅助函数作用在子序列上的值φx或φy, 再将该值与fx,fy添加到算法连接函数的参数中。

数组最小和实例假设数组a分划为a[0..i]和a[i+1..n]两个子段, 若采用两个线程分别计算它们的函数值, 如图4所示:

图4 两个线程的计算过程Figure 4 The calculation process of two threads

显然,这两个线程是并行执行的, 但它们各自内部是串行计算的。执行结束后需找到合适的算法连接函数将它们的结果进行合并, 此时对式(8)和(10)、式(9)和(11)分别进行归纳, 可得:

mps的算法连接函数与函数mts归纳过程同理,再根据定义4可得函数sum是可直接并行的, 它们的算法连接函数很容易得到, 限于篇幅此处省略。最终,采用如下算法连接函数来合并两个线程的计算结果,其中suml表示函数sum作用在a[0..i]上,sumr表示函数sum作用在a[i+1..n]上, 其余函数同理。

4.3 算法提升

算法提升是指串行算法转换为并行算法的过程。当串行算法可直接并行时, 可推导出合适的算法连接函数将其提升为并行算法, 否则在提升过程中需要向该算法添加辅助函数, 并使其算法连接函数满足同态定理(见5.1节的详细定义)。

Radl语言具有引用透明性, 易于数学推导, 但不具有并行规约描述, 只适用于描述串行算法, 因此本文受并行算法导论PRAM模型[25]启发, 定义了Radl+作为本文的并行算法设计语言, 它在Radl的基础上增加了并行算法的定义和调用。首先在ALGORITHM中初始化全局变量, 然后在BEGIN中调用分划程序和合并程序, 程序均用PROCEDURE定义, 循环体用RECUR和RECUR_parallel两种形式表示, 两者可嵌套使用, 其中RECUR表示以串行方式依次计算每个循环过程, 而RECUR_parallel …END_parallel表示以并行方式将多个循环过程同时计算。Radl+的一个典型嵌套结构如下所示:

Radl+ ALGORITHM:

|[Initialized definitions of operational variables]|

{AQ^AR}

BEGIN:

END

PROCEDURE:

BEGIN:

RECUR>

RECUR>

TERMINATION:

RECUR:

BEGIN:

RECUR_parallel>

RECUR_parallel>

TERMINATION:

parallel>

RECUR_parallel:

END_parallel

END

数组最小和实例根据4.1节和4.2节推导出的辅助函数和算法连接函数(式(13)), 可以得到如下数组最小和的并行算法ALGORITHM 2(由Radl+语言描述)。

在ALGORITHM 2中, 函数Mss_divide(n)将序列a的元素划分为logn个元素为一组, 然后并行求得每组元素的sum,mps,mts和mss值, 此过程可用(n/logn)个处理器在O(logn)时间内完成。Mss_join(p)函数在每次循环中都并行地将第2i-1组和第2i组(i=0 top/2)的sum,mps,mts和mss值合并为一个组,直至最终只有一组, 该组的mss值即为原问题的解,此过程可用(p/2)个处理器在O(logp)时间内完成。为了简便, 假定(n/logn)、logn和logp是整数。

5 可并行性

本文使用同态定理来验证提升后的并行算法正确性, 即可并行性。同态定理约定了两个线程可并行求解, 且互不干扰, 最终通过连接操作符将其进行合并, 因此满足同态定理的并行算法具有良好的并行性。同时, 使用Isabelle定义了同态定理统一验证框架并进行自动证明, 其证明步骤可分为算法函数定义和同态定理验证。

5.1 同态定理

同态函数是一个代数结构到同类代数结构的映射, 它保持所有相关的结构不变。在本文中我们研究一类特殊的同态, 即一组列表上的同态。假设类型S是一个列表的类型, 类型Sc是该列表元素的任一具体类型, 如int, float, char和bool等。下面给出同态函数的正式定义。

定义7(⊙-同态函数) 若函数h:S→Sc对于任意列表x,y∈S, 存在一个二元运算符⊙能够使得h(x•y)=h(x)⊙h(y), 则称h满足同态定理, 其中h为⊙-同态函数。

ALGORITHM 2.mss并行算法

|[In n:integer,a:array[0..n,integer];Auxi,p:integer;Outsum,mps,mts,mss:integer]|

{AQ}⋀{AR}

BEGIN :

Mss_divide(n)

Mss_join(n/logn)

END

PROCEDUREMss_divide(n)

BEGIN :sum(0) ,mps(0) ,mts(0) ,mss(0) =a[0],i= 1++1

TERMINATION :i=n/logn

RECUR_parallel :

sum((i-1)logn+1) =sum((i-1)logn) +a[(i-1)logn+1]

mps((i-1)logn+1) =min(mps((i-1)logn) ,sum((i-1)logn) +a[(i-1)logn+1])

mts((i-1)logn+1) =min(mts((i-1)logn) +a[(i-1)logn+1],a[(i-1)logn+1])

mss((i-1)logn+1) =min(mss((i-1)logn) ,a[(i-1)logn+1],mts((i-1)logn+1))

END_parallel

PROCEDUREMss_join(p)

BEGIN :sum(i) =sum((i-1)logn+1) ,mps(i) =mps((i-1)logn+1) ,

mts(i) =mts((i-1)logn+1) ,mss(i) =mss((i-1)logn+1) , (i:integer= 1 top)

TERMINATION :p= 0

RECUR :

BEGIN :i= 1

TERMINATION :i=p/2

RECUR_parallel :

sum(i) =sum(2i-1) +sum(2i)

mps(i) =min(mps(2i-1) ,sum(2i-1) +mps(2i))

mts(i) =min(mts(2i-1) +sum(2i) ,mts(2i))

mss(i) =min(mss(2i-1) ,mss(2i) ,mts(2i-1) +mps(2i))

END_parallel

p=p/2

END

显然, 定义7中的函数h作用在列表上是可直接并行的, 此时称h是列表同态函数, 它是一类在算法设计中普遍存在的函数, 如求和函数sum, 长度函数length, 最大值函数max等。

文献[26]给出第一同态定理及其证明。

定理1(第一同态定理) 函数h:S→Sc是同态的,当且仅当h是一个map函数和一个reduce函数的复合运算, 即h=reduce(⊙)◦map f, 其中函数map和reduce分别为:

定理1表明, 当一个函数是map和reduce函数的复合形式时, 其并行性是显而易见的, 因此它一定是同态的。上述同态都是函数可直接并行时存在的同态。然而, 大部分复杂算法问题的目标函数都是不可直接并行的, 此时应该修改代码使其满足同态,具体分析过程如下。

文献[27]给出了定理2及其证明。

定理2(列表同态定理) 若函数h:S→Sc是⊙-同态的, 则它的左向和右向函数具有同样的连接算子⊙。若函数h仅是左向或右向函数, 且存在对应的二元连接算子⊕或⊗, 则h是⊕-或⊗-同态函数。定理2表明当一个函数无论是左向或右向函数(即它是单路函数), 它都是列表同态的。

根据定义6和定理1,2, 我们得到如下推论:

推论1若函数h:S→Sc可写成元组形式h=(f,φ), 且h(x•y)=(f(x),φ(x))⊙(f(y),φ(y)), 其中φ是计算f的辅助函数, 则h是同态的, 且原问题的解可由f=fst◦reduce(⊙)◦maph投影得到, 其中fst函数返回元组的第一个元素。

证明:

式(15)显然满足同态定理, 即函数h是同态的。

推论1指出, 当目标函数f直接作用在列表x•y上不可并行时, 可添加辅助函数φ改写为元组形式h, 使得算法连接函数满足同态定理, 然后通过算法连接函数来合并元组, 最终投影得到目标函数在该列表上的解。

数组最小和实例根据式(13)中原问题的辅助函数和算法连接函数, 并结合推论2,mss与辅助函数mts、mps、sum一起构成元组h=(mss,mts,mps,sum), 则h(x•y)可扩展为以下形式:

此时根据推论1, 函数h显然是同态的, 最终可根据mss=fst◦reduce(⊙)◦maph执行并行计算、连接和投影得到原问题的解。

5.2 Isabelle自动验证

对于4.3节的ALGORITHM 2, 采用Isabelle定理证明器来证明其满足同态定理, 即证明该算法中的算法连接函数可直接并行时满足定义7, 不可直接并行时满足推论1。

Isabelle的证明过程是一个不断创建新理论文件(T.thy)的过程, 理论T既可以继承父理论S1,S2, …,Sn,又可以定义新的类型、函数等, 并创建新的定理或引理进行证明。thy文件由ML语言编写, 其基本结构如图5所示。

图5 thy文件的基本结构Figure 5 The basic structure of thy file

本文中, Declaration用于声明同态定理的统一验证框架, Definition用于定义求解问题需用到的相关算法函数, Proofs用于验证目标函数的算法连接函数满足同态定理。

5.2.1 同态定理统一验证框架

Isabelle标准库的区域(Locale)提供了一种程序的模块化和参数化机制, 它可以灵活地定义一个参数化的程序块, 且这些参数满足一定的逻辑条件[28]。因此, 本文使用区域技术在Isabelle的声明部分中定义了同态定理的统一验证框架, 描述同态定理验证的一般统一形式, 如图6所示。

图6 同态定理统一验证框架的区域定义Figure 6 The locale definition of unified verification framework for homomorphism theorem

图6定义了一个BaseLoc区域, 关键字fixes声明局部参数Obj(目标函数)、Aux(辅助函数)和ObjJoin(目标函数的算法连接函数), 5.2.2节对其进行了具体实现。关键字assumes定义局部参数需满足的逻辑规约HomObj, 即ObjJoin满足同态定理, 5.2.3节给出了其具体验证过程。

实际上, 对于不同算法的Obj、Aux和ObjJoin,其参数类型、个数可能不一致, 而区域扩展和区域继承不支持对父区域fix定义函数的参数进行修改。但是, 对于具体问题的求解, 可使用区域继承技术对BaseLoc区域增加求解问题所需的局部参数和逻辑规约。

数组最小和实例通过区域继承, 在BaseLoc基础上增加具体的目标函数Mss, 辅助函数Mps、Mts和算法连接函数MssJoin, 并增加新的逻辑规约HomMss, 即MssJoin满足同态定理。最终得到新的区域MssLoc, 如图7所示。

图7 mss同态定理验证的区域定义Figure 7 The locale definition of mss homomorphism theorem verification

5.2.2 算法函数定义

根据具体算法问题进行相应的区域继承, 需对该区域新增的局部参数和逻辑规约进行实例化, 之后本节将对局部参数进行具体实现。

Isabelle标准库提供了递归函数定义命令primrec和非递归函数定义命令definition。因此, 在Isabelle的定义部分用这些命令实现新增局部参数(即具体问题的目标函数f、辅助函数φ和算法连接函数⊙)的功能。

数组最小和实例根据图7的MssLoc区域, 对新增的局部参数Mss、Mps、Mts和MssJoin进行实例化, 具体实现步骤如下:

1) 用definition和primrec命令定义函数Mps,Mts和Mss, 并定义其它相关函数Min和Sum, 如图8所示;

图8 相关函数定义Figure 8 The definitions of related function

2) 根据MssLoc区域新增的局部参数MssJoin,用definition命令定义与其等价的算法连接函数MssJoin。根据4.2节式(13)及4.3节ALGORITHM 2中Mss_join的RECUR_parallel部分, 再定义Sum、Mps和Mts的算法连接函数SumJoin,MpsJoin和MtsJoin, 如图9所示。

图9 算法连接函数定义Figure 9 The definitions of algorithmic join function

5.2.3 同态定理验证

定义算法函数之后, 需在Isabelle的证明部分对目标函数的算法连接函数满足同态定理(其数学形式为h(x•y)=(f(x),φ(x))⊙(f(y),φ(y)))进行正确性证明, 即证明BaseLoc区域的逻辑规约HomObj的正确性。Isabelle中采用theorem命令创建与HomObj等价的同态定理, 并通过如下策略完成证明[29]:

策略5.使用apply命令来引入Isabelle内置规则库的规则来进行化简。

策略6.创建相应的中间引理并进行证明,然后使该引理作为化简规则来进行化简。

策略7.使用Sledgehammer工具来调用其他定理证明器来辅助证明, 如CVC4[30], SPASS[31]和Z3[32]等。

数组最小和实例根据MssLoc区域定义的逻辑规约HomMss, 在Isabelle创建与其等价的同态定理HomMss, 并证明其正确性。为此, 先根据策略6定义相应的辅助引理HomSum, HomMps和 HomMts,再根据策略5和策略7, 使用apply命令和Sledgehammer工具对这些引理和定理进行结构化方式证明。具体的验证结构如图10所示。

图10 mss的同态验证结构Figure 10 The homomorphic verification structure of mss

图10定理和每个引理的结构化证明分为基础情况证明(Nil)和归纳情况(Cons)证明。对于基础情况,另外创建引理BasecaseSum, BasecaseMps, BasecaseMts和BasecaseMss并对它们进行证明; 归纳情况可借由基础情况和其它辅助引理完成证明。图11给出了定理与最重要的辅助引理之间的依赖关系。

图11 定理与辅助引理的依赖关系Figure 11 Dependencies of theorems and auxiliary lemmas

最终成功验证完定理和所有引理, 下面仅列出最为重要的算法连接函数MssJoin满足同态定理的结构化证明脚本, 限于篇幅其它从略。HomMss作为需要验证的定理, 基础情况证明依赖于中间引理BasecaseMss, 归纳情况证明需引入前面的函数定义(MssJoin,MpsJoin,Min)和引理(HomMps, HomMts),如图12所示。

图12 mss的同态验证过程Figure 12 The homomorphic verification process of mss

6 并行程序生成

为生成Haskell并行函数式程序, 本文提出了由Radl+并行算法转换为Haskell并行程序的转换规则,并基于此规则设计了“Radl+→Haskell并行程序生成系统”的软件原型, 最终将映射生成的Haskell程序放至GHC平台运行成功。

6.1 Radl+→Haskell并行程序生成系统

至此, 我们已经实现了从问题的规约推导至Radl+并行算法。为了实现从抽象规约到具体程序的完整生成过程, 本文设计了一个“Radl+→Haskell并行程序生成系统”的软件原型, 将Radl+算法映射为Haskell并行函数式程序。软件原型系统的结构图如图13所示:

图13 “Radl+→Haskell并行程序生成系统”结构图Figure 13 The structure diagram of “Radl+→Haskell Parallel Program Generation System”

该软件原型的输入为Radl+描述的分治并行算法,输出为Haskell并行函数式程序, 两者在数学上和逻辑上是等价的, 中间的转换过程基于如下转换规则:

转换规则(Radl+→Haskell转换规则)

· 使用Radl+描述的ALGORITHM转换为Haskell的主程序Main::IO(), 它是程序执行的起点;

· 使用Radl+描述的分划函数转换为Haskell的par函数, 表示两个线程的并行计算。如l‘par’r表示程序的主任务分成线程l和r并行计算,且l和r分别递归产生更多的子线程;

· 使用Radl+描述的合并函数转换为Haskell的pseq函数, 表示一个线程的连续计算。当par运行完成后, 用pseq合并函数结果来进行同步。

数组最小和实例使用Radl+描述的ALGORITHM 2作为“Radl+→Haskell并行程序生成系统”的输入, 在生成系统中进行语法分析, 其中四个函数sum、mps、mts和mss根据转换规则映射得到的Haskell函数定义, 如图14所示。Haskell分治并行计算包Control.Parallel增加了par和pseq函数来声明函数的并行性。

图14 Haskell函数定义Figure 14 Haskell function definitions

最终经软件原型生成的Haskell并行函数式程序如图15所示。

图15 Haskell并行程序生成Figure 15 Haskell parallel program generation

6.2 Haskell并行程序实现

GHC作为Haskell的编译器, 支持在对称的共享内存多处理器(Symmetric Multi-Processing, SPM)上并行运行Haskell程序, 特别适合于分治并行。Haskell程序默认在一个处理器上(即单线程)线性运行, 因此编写并行程序需向GHC声明并行性。一种方法是使用并行Haskell来分叉线程, 即使用多线程来执行程序任务。更简单的机制是从纯代码中提取并行性, 它使用一对组合函数par和pseq[33], 组合语法是par l(pseq r(l⊙r))或l′par′r′pseq′ (l⊙r)。GHC在编译Haskell文件时需要-threaded参数才能支持并行, 生成可执行文件, 并通过参数-N来设置运行该文件的线程数量, 参数-s使系统输出文件运行的统计结果。

数组最小和实例将上一节生成的Haskell并行函数式程序放至GHC平台编译并运行, 对该算法输入一个包含100万个元素的列表, 使用两个线程2536.486秒就得到了该列表最小和的计算结果, 如图16所示。

图16 mss的Haskell并行实现Figure 16 Haskell parallel implementation of mss

7 实验

本节将通过软件原型生成的Haskell并行函数式程序放至GHC平台运行, 与串行Haskell程序的执行时间进行对比, 证明本文提出的方法具有良好的加速比。

7.1 实验数据与环境

根据第2节提出的模型驱动的分治并行程序生成及自动验证方法步骤, 我们对一系列复杂算法问题(包括可直接并行函数和不可直接并行函数)进行了程序生成和Isabelle验证, 其程序生成和自动验证方法与数组最小和案例一致, 限于篇幅不再赘述。这些复杂算法中包含的函数如下:

1)min,max,sum,length: 这些函数均为常见结构简单的可直接并行函数。其中min用于求解列表所有元素的最小值;max用于求解列表所有元素的最大值;sum用于求解列表所有元素的和;length用于求解列表的长度, 即元素的个数。

2)fac,poly: 这些函数用于多项式求值问题。其中fac求解给定元素的length次幂, 它是并行计算poly的辅助函数, 它是可直接并行的;poly用于列表的多项式求值, 它是不可直接并行的。

3)mps,mts,mss: 这些函数用于求解数组最小和问题, 它们都是不可直接并行的。其中mps计算列表的最小前缀和;mts计算列表的最小后缀和;mss计算列表所有子段的最大和。

4)bal,mp,mt,mg: 这些函数用于求解最大基因序列问题, 除bal外均为不可直接并行函数。其中bal判断序列是否为连续基因, 它是mp和mt的辅助函数;mp标志以序列第一个元素开始的基因最长连续长度, 它是mt和mg的辅助函数;mt标志以序列最后一个元素结束的基因最长连续长度, 它是mg的辅助函数;mg标志整个序列中的基因最长连续长度。

在上述算法的函数中, 输入均采用文件导入方式, 该文件为包含2亿个随机数的int型列表。本文实验采用的是Intel(R) Core(TM) CPU i9-9900K服务器, 显卡内存为32GB, 最大线程数量为16, 操作系统为Win10, 在GHC平台(版本为9.2.2)上编译并运行经软件原型生成的Haskell并行程序。

7.2 实验结果与分析

本文在GHC平台上通过设置不同线程数量运行Haskell并行程序, 与Haskell串行程序(即一个线程)比较得到不同线程情况下运行时间的加速比, 如图17所示:

图17 相对于串行程序的加速比Figure 17 Speedups relative to the sequential program

理论上并行程序中利用的线程越多, 加速比越高。但实际并非完全如此, 根据图17, 我们可以分两类进行讨论:

1) 常见函数(如min、max等)和一些辅助函数(如bal、mp等)使用2线程时加速比略高于理想状态下的加速比2, 这种超线性加速比成因是数据量较大,需要较大的内存, 而程序运行时选择多核处理器上的高速缓存, 其读写性能高于内存, 可以产生额外的加速效果。在4线程时并行性能较为稳定几乎不变, 之后在8~16线程时缓慢下降。这是因为这些函数的结构和计算过程较为简单, 高性能电脑能够以较少的线程数进行快速计算, 若线程数过多, 反而会造成多线程合并计算结果的时间过久, 加长线程之间的通信时间, 同时会增加大量计算内存空间,从而使得加速比降低。

2) 对于三个复杂算法问题的目标函数mss、poly和mg, 加速比一直在随着线程数量而增长, 在16线程时甚至达到了3倍。这是因为这些函数本身结构较为复杂, 调用的辅助函数过多(mss和mg都有3个)或本身运算量大(poly一直在做幂运算, 使得数值增长速度不断加快), 采用的线程越多, 才能加快多线程对函数的计算时间和合并时间, 使得加速比不断增加。

8 相关工作

并行程序的设计与验证已经有较多工作进行了深入研究, 本文通过以下两个方面与较为经典的相关工作进行比较:

分治并行程序设计: Gorlatch S[34]提出了一种系统的cons&snoc并行化方法, 将问题抽象为函数并给定其列表同态[35]表示, 该方法可成功应用于已知的所有同态, 但辅助函数直接给出, 没有推导过程, 且生成的并行算法不完整。Kazutaka Morita等人[9]基于第三同态定理[36], 通过函数的弱右逆实现来自动推导出代价最优的列表同态函数, 简化了列表同态的推导, 最终生成可执行的C++并行程序, 但弱右逆函数的推导过程过于复杂, 没有统一的推导规则。Azadeh Farzan等人[37-39]利用语法引导合成(Syntaxguided synthesis, 简称SyGuS)的方法, 研究了对单重和双重循环结构的串行程序进行分治并行化, 最终生成C++并行程序, 并提出了使用Dafny程序证明器验证并行程序满足同态定理的方法, 但该工作的串行程序都是通过经验直接给出, 辅助函数的推导过程也过于简略。熊英飞等人[40-41]基于演绎法与归纳法实现了算法合成工具AutoLifter, 不仅能够自动合成分治并行算法, 还可以推广到其它算法策略(如动态规划), 在AutoLifter合成算法正确性方面, 采用Occam求解器进行概率保证。

并行程序验证: 主要分为两类, 一类是基于模型检验的方法, 如基于Petri网的验证方法[42]、模型检测方法(如SPIN[43]、SMV[44]等)等。Petri网能够直接反映死锁和互斥性质, 但关于内容的形式化表示有限,如缺乏描述变量变化的方式[45]; 模型检测方法在面对复杂问题时往往会产生状态爆炸问题。另一类是基于定理证明的方法, 如Rely-Guarantee推理方法[46]和基于并发分离逻辑的验证方法[47]等。Rely-Guarantee推理方法是一种容错(Fault-tolerance)的验证方法, 但证明过程复杂, 验证时所需的依赖-卫式条件难以获得; 并发分离逻辑方法是一种验证并行程序性质较为经典的方法, 它是一种避错(Fault-avoidance)的验证方法, 限制条件高, 由于可能涉及到指针操作, 验证抽象粒度小, 验证效率低。行为时序逻辑TLA+方法[48]既支持模型检验, 也支持定理证明, 但定理证明方面目前仅支持安全性的验证, 不支持活性的验证。

本文首次实现了从问题规约推导至串行算法,再提升至并行算法并通过Isabelle验证其满足同态定理的可并行性, 最终生成分治并行Haskell函数式程序的完整过程。与现有的主要研究工作进行对比, 在生成方面, 该方法的串行算法是通过推导得到的,而非经验给出, 算法连接函数和辅助函数生成的输入只需要串行算法, 生成过程更加系统和一般化;在验证方面, 使用Isabelle定理证明器对提升后的算法满足同态定理自动验证, 证明该算法的可并行性,保障了并行算法的可靠性和正确性。使用定理证明器Isabelle较Dafny通用性和复用性更强, 也无须在验证时探索前后置条件以及大量的中间断言。最终生成的是Haskell并行函数式程序, 更加简洁、清晰,不会产生副作用, 天然支持并行。

9 总结与展望

随着大数据和人工智能的发展, 高可信并行算法的生成及验证已经逐渐成为计算机科学非常热门的一个研究方向。本文采用分治并行模式, 并结合形式化推导方法提出了一种基于模型驱动的分治并行函数式程序生成及自动验证方法。(1)首先, 从问题描述出发, 使用分划递推法来寻找函数之间的递推关系及循环不变式, 将递推关系和循环不变式组合构造串行算法; (2)其次, 扩展循环不变式且采用归纳法推导出辅助函数和算法连接函数来将其提升为并行算法, 并使用一种新的并行算法设计语言Radl+来描述; (3)然后, 使用Isabelle定理证明器对算法连接函数满足同态定理进行证明, 保障了并行算法的可靠性和正确性; (4)最后, 基于提出的“Radl+→Haskell转换规则”, 将验证成功的Radl+并行算法通过设计的“Radl+→Haskell并行程序生成系统”软件原型映射为具体的Haskell并行函数式程序。实验表明, 本文提出的方法能够对多项式求值、最大基因序列等一系列算法问题生成并行函数式程序, 并具有良好的加速比。

在并行程序生成方面, 本文是通过形式化方法来进行推导的, 生成过程更加系统和一般化, 同时生成的函数式程序具有良好的扩展性和天然的并行性; 在并行程序验证方面, 通过定理证明器自动验证, 保障了生成的并行程序的可靠性并提高了验证效率。使用Isabelle定理证明器验证算法连接函数满足同态定理, 即提升后的串行算法满足可并行性来实现并行程序的验证, 是一种新的验证思路, 验证相对更加简单。

在未来工作中, 一是深入挖掘整体函数同态性与单步递推计算函数的结合律、单位元性质之间的联系, 探索某特定子类问题验证的统一求解策略;二是考虑将本文方法扩展到双重循环程序, 使其能够生成更多复杂算法问题的并行程序; 三是将本文方法运用到真实工业应用场景, 使其能够生成和验证更有意义的并行算法, 如大数据的分布式计算框架MapReduce[49]和Spark[50]。