开发一种在CIVL模型检查循环中的数值算法

中文摘要 AI 辅助

在大型科学模拟框架中验证数值算法具有挑战性：该框架过于庞大，无法进行模型检查，而单元测试仅能覆盖采样输入。我们报告了一个案例研究，在该研究中，我们为Flash-X（一个大规模多物理场模拟框架）开发了一种新的云内单元（CIC）沉积算法，并将CIVL模型检查器保持在开发循环中。我们并未在Flash-X庞大的基础设施内验证该算法，而是仅提取算法所需的接口，形成一个小的、自包含的C模型，该模型抽象掉了与算法无关的Flash-X基础设施实现细节。随后，新算法在此C模型中构建和检查。CIVL模型检查器利用粒子位置的符号值，能够验证CIC沉积算法所需的物理性质。它证明了两个物理性质——质量守恒和沉积位置——适用于模拟域内所有允许位置的连续体。CIVL还验证了算法的内存安全性，以及在指定边界内所有秩分布下无MPI死锁和数据竞争条件。首先编写验证性质，并在自底向上原型设计工作流的每个阶段持续检查，将CIVL转变为设计护栏，大大增强了对扩展算法的信心。在我们的案例研究中，CIVL发现了算法中的一个并发缺陷，而基于随机种子的测试未能触发该缺陷。本文展示了我们的工作流程，旨在帮助读者理解其相比测试的优势、成本和权衡。

英文摘要

Verifying a numerical algorithm in a large scientific simulation framework is challenging: the framework is too big to model-check, and the unit tests exercise only sampled inputs. We report a case study in which we developed a new cloud-in-cell (CIC) deposition algorithm for Flash-X, a large-scale multiphysics simulation framework, keeping the CIVL model checker in the development loop. Rather than verify the algorithm within Flash-X's hefty infrastructure, we extract only the interfaces that the algorithm needs into a small, self-contained C model, which abstracts away implementation details of the Flash-X infrastructure that are unrelated to the new algorithm. The new algorithm is then built and checked within this C model. The CIVL model checker enables verification of the required physical properties of the CIC deposition algorithm using symbolic values for the particle positions. It proves two physical properties---mass conservation and the deposition location---for the continuum of admissible positions in the simulation domain. CIVL also verifies the algorithm's memory safety and freedom from MPI deadlocks and data race conditions over all rank distributions within specified bounds. Writing the verifying properties first and continuously checking them at each stage of the bottom-up prototyping workflow turned CIVL into a design guardrail that greatly increased confidence in the extended algorithm. During our case study, CIVL surfaced a concurrency defect in the algorithm that our random-seed-based tests failed to exercise. This paper shows our workflow, with the goal of helping readers understand its benefits, cost, and tradeoffs compared with testing.

发表机构

• Argonne National Laboratory（阿贡国家实验室）
• RIKEN Center for Computational Science（理化学研究所计算科学中心）

机构由 AI 辅助整理，请以论文原文为准。