XPS: EXPL: CCA: Collaborative Research: Nixing Scale Bugs in HPC Applications

大规模仿真是现代科学与工程的一个基本组成部分。不幸的是，为了在大型并行计算机上执行模拟而编写的程序经常遭受软件缺陷的困扰，这些缺陷是由于所采用的并行化方法的规模和多样性造成的。尤其严重的是在进行大量资源分配（例如，内存请求）时发生的软件错误。基于正式的主动测试技术对于定位此类缺陷至关重要。然而，这些测试工具本身很少在并行机器上运行，更不用说在大规模上运行了，这使得在高保证的情况下发现大规模错误变得非常困难和耗时。并行化验证工具的努力应该重用现有的技术，以方便并行化、结果收集和故障处理。该项目的关键创新包括可以通过工作流描述大规模验证运行的洞察力，这使得利用已经可用的分布式计算平台成为可能，特别是来自Argonne的Swift/T。pi的互补背景很好地匹配了在三种广泛使用的并发模型（即MPI， OpenMP和CUDA）的背景下推动形式化方面和分布式验证的需求。这项工作将有助于创建一个公共的、分布式的、正式的主动测试框架。推动这项研究的工具和案例研究软件将由pi维护，并在开源许可下通过网站和存储库免费发布。它们将促进学术界、政府实验室和工业的研究人员和软件开发人员对科学模拟代码的大规模调试。该项目还将产生教学材料和最佳实践，帮助教育学生使用现有的基于工作流程的问题解决方法。它将有助于培养现在和未来的科学家、工程师和程序员，从而帮助保持我们国家在计算、国土和能源安全以及STEM教育方面的领导地位。

Large-scale simulation is a fundamental component of modern science and engineering. Unfortunately, programs written to perform simulations on large-scale parallel computers frequently suffer from software defects that result from the sheer scale and the variety of parallelization approaches employed. Especially egregious are software bugs that occur when large resource allocations (e.g., memory requests) are made. Formally based active-testing techniques are essential to locate such defects. However, these testing tools are themselves seldom run on parallel machines, let alone at large scale, making it difficult and very time consuming to find scale bugs with high assurance. Efforts to parallelize verification tools should reuse existing technology for easy parallelization, result collection, and fault handling. Key innovations of this project include the insight that large-scale verification runs can be described through work-flows, which makes it possible to take advantage of already available distributed computing platforms, in particular Swift/T from Argonne. The complementary backgrounds of the PIs are well matched with the need to push both formal aspects and distributed verification in the context of three widely-used concurrency models, namely MPI, OpenMP, and CUDA. This work will help create a public distributed formal active testing framework. The tools and case-study software driving this research will be maintained by the PIs and released freely under open-source licenses through websites and repositories. They will facilitate large-scale debugging of scientific simulation codes by researchers and software developers in academia, government labs, and industry. The project will also generate pedagogical material and best practices, helping educate students in the use of existing work-flow based problem solving approaches. It will help train present and future scientists, engineers, and programmers, thus assisting in maintaining our nation's leadership in computing, homeland and energy security, and STEM education.