SMTLOC:基于多源频谱的SMT求解器缺陷定位

SMT求解器作为重要的基础软件,其存在的缺陷可能会导致依赖于它的软件功能失效,甚至带来安全事故.然而,修复SMT求解器缺陷是一个十分耗时的任务,因为开发者需要花费大量的时间和精力来理解并找到缺陷的根本原因.虽然已有许多软件缺陷定位方面的研究,但尚未有系统的工作研究如何自动定位SMT求解器缺陷.因此,提出一种基于多源频谱的SMT求解器缺陷定位方法SMTLOC.首先,对于给定的SMT求解器缺陷,SMTLOC提出一种枚举算法,用以对触发该缺陷的公式进行变异,从而生成一组不触发缺陷,但与触发缺陷的公式具有相似执行路径的证人公式.然后,SMTLOC根据证人公式的执行路径以及SMT求解器的源码信息,提出一种融合覆盖频谱和历史频谱的文件可疑度计算方法,从而定位可能存在缺陷的文件.为了验证SMTLOC的有效性,收集60个SMT求解器缺陷.实验结果表明,SMTLOC的缺陷定位效果明显优于传统的频谱缺陷定位方法,SMTLOC可以将46.67%的缺陷定位在TOP-5的文件内,定位效果提升了133.33%.

适用于非静力大气模式的近似黎曼求解器应用研究

基于多矩非静力大气模式,开展了3类垂向近似黎曼求解器应用研究。多矩非静力大气模式具有高精度与数值守恒特性,其垂向采用守恒的有限差分格式进行数值离散,而网格单元边界通量计算是通过求解黎曼问题来实现的,因此采用合适的近似黎曼求解器对准确模拟非静力大气垂直运动显得十分关键。LLF(Local Lax-Friedrich)、LMARS(Low Mach Approximate Riemann Solver)和HLLC(Harten-Lax-van Leer Contact)为计算流体力学(CFD)中常用的3种近似黎曼求解器,它们的计算代价和复杂程度逐渐增加。一维标准数值试验表明:LLF计算最为经济,但具有较强的耗散;LMARS具有适用于大气流动的假设,对于数值粘性的控制较好且计算量不大;HLLC建立的三波模型可以避免对中间特征场的过度数值耗散。基于LLF近似黎曼求解器计算经济的特点,通过优化LLF近似黎曼求解器各特征波动的粘性系数,能够实现与LMARS、HLLC近似黎曼求解器相同的性能,且计算代价最小。二维非静力数值试验表明,优化的LLF近似黎曼求解器能够规避常规LLF近似黎曼求解器的数值耗散过大问题,正确模拟小尺度非静力垂直运动,达到更复杂的LMARS、HLLC近似黎曼求解器模拟效果且并未增加计算量,这为非静力大气数值模式提供了良好的参考价值。

基于多样性SAT求解器和新颖性搜索的软件产品线测试

软件产品线测试是一项非常具有挑战性的工作.基于相似性的测试方法通过提升测试集的多样性以达到提高测试覆盖率和缺陷检测率的目的.因其具有良好的可拓展性和较好的测试效果,目前已成为软件产品线测试的重要手段之一.在该测试方法中,如何产生多样化的测试用例和如何维护测试集的多样性是两个关键问题.针对以上问题,提出一种基于多样性可满足性(SAT)求解器和新颖性搜索(novelty search,NS)的软件产品线测试算法.具体地,所提算法同时采用两类多样性SAT求解器产生多样化的测试用例.特别地,为了改善随机局部搜索SAT求解器的多样性,提出一种基于概率向量的通用策略产生候选解.此外,为同时维护测试集的全局和局部多样性,设计并运用两种基于NS算法思想的归档策略.在50个真实软件产品线上的消融和对比实验验证多样性SAT求解器和两种归档策略的有效性,以及所提算法较其他主流算法的优越性.

基于PARDISO直接求解器的三维自然电位正反演

近年来自然电位法在海底硫化物资源的勘探和评价中发挥了重要作用。本文开展的是基于PARDISO直接求解器的3D自然电位正反演算法研究。首先,利用有限体积法离散自然电位控制方程,采用PARDISO直接求解器提高正演计算的效率,通过数值解与解析解对比,验证了正演算法的可靠性。其次,在3D反演算法中考虑了地形因素,同时将最小支撑约束与深度加权加入目标泛函中,理论模型数据的反演结果很好地恢复了矿体的结构。最后,利用该算法对室内沙箱实验获得的自然电位数据进行反演,结果显示得出的电流密度异常与金属棒的位置基本一致。因此,本文提出的反演算法在未来大规模自然电位数据反演中具有重要作用。

高焓流动中的可压缩颗粒两相流并行求解器:数值方法及其验证

在极端力学环境下可压缩点力颗粒两相流理论方程的基础上,提出一种基于动态链表数组的并行颗粒求解器,使其与可压缩流体求解器耦合。与基于欧拉坐标系的携带流体相不同,基于拉格朗日坐标系的求解器采用动态链表数组对弥散颗粒相进行内存分配,可以解决因使用全局数组解决拉格朗日/欧拉坐标系转换带来的弥散颗粒群内存利用率低和计算效率低下问题。最后对多物理效应的可压缩颗粒两相流求解器进行验证,并在马赫数渐进趋于零的情况下,对两个不可压缩槽道颗粒湍流标模进行验证。

面向众核CPU的稠密线性求解器性能评测与优化

稠密线性求解器在高性能计算和机器学习等领域扮演着重要的角色。其典型的并行算法实现通常构建在著名的fork-join或task-based编程模型之上。尽管采用fork-join模型的主流稠密线性代数库能将大部分的计算转移到高度优化、高性能的BLAS 3例程上,由于fork-join不灵活的执行流,它们仍然未能高效地利用众核CPU的计算资源。采用task-based编程模型的开源库能实现更加灵活、负载更均衡的算法,因此能获得明显的性能提升。然而,在众核CPU平台上,尤其是对于中等矩阵规模的问题而言,它们仍然有较大的优化空间。对稠密线性求解器的性能进行了全面的测评,以定位性能瓶颈,并提出了2种优化策略,以提高程序性能。具体地,通过重叠LU分解和下三角求解的计算过程,减少同步开销线程的空等,从而提高算法的并行性;进一步通过减少冗余的矩阵打包操作,降低算法的访存开销。分别在2个主流的众核CPU平台(Intel®Xeon Gold®6252N(48核)和HiSilicon Kunpeng 920(64核))上进行了性能评估。实验结果表明,该优化的稠密线性求解器在上述两个CPU平台上,相比最佳开源实现分别取得了10.05%(Xeon)和13.63%(Kunpeng 920)的性能提升。

基于FluxNet的热传导方程反问题的求解器

热传导偏微分方程的求解是工业应用中一种重要的计算,为了解决传统的热传导方程正演运算耗时过长的问题,提出一个基于新型的网络结构FluxNet的求解器。通过热传导方程的正演运算获得关于温度场分布图以及对应的热流密度图的数据集,基于深度学习训练该数据集,建立一个具有卷积层和反卷积层的热流密度网络结构FluxNet模型。使用该求解器预测数据以及实际数据的热流密度图进行测试和验证,实验结果得出该求解器预测的热流密度结构相似度均达到90%以上,达到了工业应用需求。

变分量子线性求解算法在高速飞行器定常绕流数值模拟中的应用

CFD方法在用于三维大规模复杂流动的空气动力学数值模拟时,面临着计算成本高、模拟时间长等瓶颈问题。近年来,量子计算为航空航天CFD领域带来了新的解决思路,通过利用量子比特的叠加态和纠缠特性,理论上相比于经典计算机能够实现对数级的存储缩减和指数级的效率加速,在处理大规模空气动力学模拟等任务上具有巨大的潜力。聚焦于量子计算技术在航空航天CFD领域的应用探索,针对高速定常流动问题,采用变分量子线性求解器(variational quantum linear solver,VQLS)辅助求解CFD时间离散环节得到的高维线性方程组,进而发展了可以在含噪声中等规模量子(noisy intermediate-scale quantum,NISQ)器件上实现的VQLS-CFD耦合方法。通过三维双椭球模型和探测器火星科学实验室模型的超声速数值模拟测试,验证了VQLS-CFD耦合方法可以实现大规模复杂流动的鲁棒及准确模拟,并产生与试验数据吻合度较高的计算结果,最终获得高可信度的气动预测结果。然而,介绍的量子计算流体力学(quantum computational fluid dynamics,QCFD)方法在计算效率方面尚未达到真正意义上的加速效果,这一现象的突破将依赖量子计算机硬件的持续发展与QCFD算法的不断优化与成熟。

基于多区多求解器的金属-介质复合目标电磁散射特性分析

在导弹类金属-介质复合目标电磁散射特性求解过程中,采用常规迭代求解方法存在难以收敛以及内迭代边界积分区域重复求解的问题。针对该问题,在传统有限元边界积分区域分解法(finite element boundary integral domain decomposition method,FE-BI-DDM)的基础上,采用了更为灵活的多区多求解器的方法(multi domain multi solver method,MDMSM)。该方法对导弹类金属-介质复合目标中难以收敛的金属区域,使用快速直接求逆的方法求解,由于可以使用独立的网格模型进行电磁建模,避免了内迭代部分的模型重复建立过程,从而大幅减少了整体模型求解时间。实验结果表明:所提方法可以在相同计算精度的条件下,以不过多增加内存空间为前提,大幅缩短了导弹类目标的金属-介质复合模型的电磁求解时间。该方法为开展导弹类目标特性分析提供了一条可行的技术途径。

结构力学求解器在“结构力学”课程中的应用研究

为了有效提升“结构力学”课程的教学效果,本文简要介绍了结构力学求解器并对其在课程教学中的应用进行了探究。通过对静定和超静定结构的示例分析,可知结构力学求解器能够完成力学实验,并直观地反映不同结构体系的受力特点。通过对结构几何组成分析和静定桁架内力计算的示例可知,结构力学求解器能够加深学生对力学问题的理解,培养并提升解决工程实践问题的能力和素养。结构力学求解器具有良好的教学效果,但也存在一定的局限性,需要进一步的探究和开发,以提高求解器在教学过程中的应用效率。

基于OpenFOAM的磁流体求解器的开发和应用

基于计算流体力学平台OpenFOAM,本文开发了一套可压缩磁流体求解器,并将其应用于二维和三维的跨音速束流模拟.该求解器对OpenFOAM自带的密度基中心差分黎曼求解器rhoCentralFoam进行了修改,植入一个隐式压力分离算法用以控制磁场散度误差并保证模拟结果的数值精度.本文对此求解器进行了检测,证明了它的收敛阶在1—2之间,并将其应用到强激光等离子体的磁流体模拟.利用该求解器,本文讨论了外加均匀轴向磁场对激光等离子体喷流的影响,发现了喷嘴和结节位置与热压比开方之间的线性关系.本文还分析了电容线圈中产生的非均匀磁场对激光等离子体喷流的影响.初步模拟结果表明,当线圈中心磁场相同时,小尺寸线圈产生的磁场会加快喷嘴和结节的形成,等效的均匀轴向磁场更大.此模拟结果可以作为我们将来的磁化喷流实验的参考.同时,这样物理结果表明该磁流体求解器适合做面向激光等离子体实验的工程计算,可以应对构型比较复杂的场合.

基于Kokkos模板元编程的性能可移植求解器开发

【目的】解决面向多样化异构计算架构的求解器应用编程问题。【应用背景】超级计算机的硬件架构日益多样化,新的异构架构因生态不够完善,往往导致软件移植研发门槛过高、研发周期过长,以及存在针对不同硬件反复适配、移植等问题。【方法】在Kokkos代数算子库基础上,开发一套面向国产E级计算环境的“性能可移植”模板元接口开源框架,用于线性代数求解器编程。【结果】本文给出其用于Krylov子空间算法的简单编程示范,实现了面向国产异构处理器的线性代数求解器移植,部分求解器相较于10核超线程Xeon CPU有数十倍以上加速。【结论】性能可移植编程可成为应对多样化异构计算的解决方案。

基于黎曼求解器的SPH算法及其应用

基于传统光滑粒子流体动力学方法(SPH)进行数值模拟时,在边界处存在压力和速度震荡,甚至导致求解失败。为准确求解SPH方程式中的粒子的物理粘性,减小数值耗散,将黎曼求解器纳入SPH格式中,通过重整化过程对连续性方程中的梯度算子进行了校正。通过一系列经典算例的数值模拟结果表明,基于黎曼求解器的SPH算法能够准确的模拟液体的流动,且具有良好的准确性和鲁棒性。

基于OpenFOAM的真实流体模型库及均相求解器开发

为了正确认识高压环境下的流体非理想性特征,及其对于低温射流喷雾过程的影响作用,将多种不同真实流体模型写入到开源CFD程序OpenFOAM仿真平台中,编译形成具有广泛通用性的真实流体热物理模型库;并将高压下真实流体特征的影响引入到压力修正算法中;开发出适用于描述超临界环境下低温流体流动过程的均相求解器。对高压下流体热物理性质的非理想性,以及超临界环境下的低温液氮射流喷注过程进行研究。结果表明:高压下的真实流体效应主要体现在低温区域,本文所建立的模型库可以在任意热力学状态范围内正确预测流体热物性;基于此模型库所开发的均相求解器可正确预测超临界环境下低温射流的详细流动特征和结构,而理想气体模型则会大幅低估射流核心区密度分布,中心线上误差高达68.9%;综合考虑计算精度和效率,PR EoS及相关模型更适合于这类超临界流动问题的求解;低温射流跨临界喷注中局部区域所发生的虚假沸腾现象会导致射流温升速率降低、体积膨胀速率加快;射流核心区压缩因子明显<1,在数值仿真时必须考虑高压环境下的真实流体效应。

基于SMT求解器的路径敏感程序验证

随着软件规模的不断扩大以及复杂度的不断增长,人们越来越关注软件的可信性问题.验证程序是否满足断言所描述的性质,是保证软件可信性的一种常见方法.路径敏感的程序验证由于不可能遍历所有的路径,需要合并路径信息,因此造成精度上的损失.提出一种基于SMT求解器的路径敏感程序验证方法,在保证精确度的前提下,有效减少路径搜索空间.其基本思想是,利用最大强连通分量压缩循环路径,然后根据目标断言对控制流图进行切片.使用一种布尔表达式方法对路径空间进行抽象,结合抽象解释和符号执行技术对路径进行验证.结合F-Soft平台和Z3工具对该方法进行了实验验证,结果表明,该方法在验证的精确度和效率上都有较好的效果.

基于精确Riemann求解器的明满流过渡过程模拟

Preissmann窄缝法模拟明满流过渡过程方法简单,但存在明显的非物理振荡,抑制非物理振荡是该方法应用的关键。基于Godunov格式和精确Riemann求解器对明满流过渡过程进行模拟,针对Riemann问题代数恒等式在明满流交界处不光滑问题,提出了三阶收敛方法与二分法结合的迭代求解方法,保证迭代收敛至真实解;针对由于变量空间重构方法不能准确表达变量在空间中真实物理状态而导致的非物理振荡,提出了基于精确Riemann解的变量空间重构方法,准确表达激波间断在单元内的空间分布状态,从机理上抑制了非物理振荡。实例研究表明,数值计算结果与解析解或实测值吻合良好,研究成果为明满流过渡过程的高精度数值模拟提供了新的方法。

《结构力学求解器》的算法与性能—第十届全国结构工程学术会议特邀报告

本文介绍了新近开发的《结构力学求解器》工程版的功能和特色，并对其中的若干算法及性能进行了综述性的介绍。文中揭示了求解器工程版对于工程中大型结构分析计算的适用性、实用性和有效性，通过同大型权威商业软件ANSYS的算例比较，展示了求解器工程版采用一些先进算法所带来的求解速度和精度方面的出色表现。

使用SAT求解器产生所有极小冲突部件集

产生所有的极小冲突部件集为基于模型诊断中的一个重要步骤.本文将待诊断系统的行为模型及观测分别使用合取范式(CNF)形式的文件描述,从而提出将判定系统组件子集是否为冲突集的问题转化为:首先提取相关组件的CNF模型及观测,然后调用成熟的SAT求解器判定可满足性.随后,通过有效地结合CSISE-tree等方法来产生所有的极小冲突集.为进一步提高效率,给出了充分利用系统输入/输出结构信息的启发式策略.实验结果表明,使用结合SAT求解器及CSISE-tree等方法能够较快产生所有极小冲突集,并且启发式策略使得求解效率进一步提高(平均提高约21%,最高者甚至达到约48%).

基于GPU的高性能稀疏矩阵向量乘及CG求解器优化

以有限元/有限差分等为代表的一类数值方法,其总体矩阵常常具有"带状"、稀疏的特点。针对"带状"稀疏矩阵,提出和实现了一种高效的矩阵向量乘存储格式和算法"bDIA"。基于nVidia的GTX280系列GPU对其进行了测试,结果显示:与CUSP支持的5种常见稀疏矩阵存储格式和算法相比较,所提出的bDIA格式以及相应的spMV算法的单双精度浮点效率均可以提高1倍以上,并突破了该系列GPU在spMV计算时4%的单精度浮点效率上限和22.2%的双精度浮点效率上限;应用于共轭梯度(CG)与稳定双共轭梯度(BiCGStab)求解器,相对于DIA格式均有1.5倍左右的加速。

基于瞬态多物理场求解器的电磁轨道炮发射过程建模与仿真

为研究电磁轨道炮发射过程中瞬态多物理场的作用机制与内在规律,建立包含电路、电磁场、热场和结构场的数学模型。模型中计入材料非线性、结构变形、接触碰撞等实际因素。采用隐式有限元格式求解电磁场和热场以及显式有限元格式求解结构场,利用载荷传递和时间同步实现各物理场之间的耦合,发展出一种瞬态多物理场求解器。通过固体电枢型电磁轨道炮、同步感应式电磁线圈炮等算例,讨论了发射过程计算结果的合理性。结果表明,电磁炮的发射是多场耦合、多部件相互作用下的一个复杂动力学过程,存在电流和磁场扩散、温升、应力传播、接触碰撞等瞬态现象,发射性能与结构、材料和激励密切相关。该求解器可为电磁发射系统及其关键部件提供一种辅助设计手段。