Verifying spatial properties of array computations
Verifying spatial properties of array computations
复制标题
验证数组计算的空间属性
DOI：
10.1145/3133899
复制
发表时间：
2017
影响因子：
--
通讯作者：
Orchard D
中科院分区：
文献类型：
--
作者：
Orchard D
数组计算是数值建模和计算科学应用的核心。然而，数组索引的低级操作是程序错误的一个来源。许多从业者都意识到需要确保程序的正确性，但很少有来自编程研究社区的技术被科学家应用。我们的目标是通过为科学代码提供有针对性的轻量级验证技术来改变这种情况。我们专注于所有太常见的错误阵列偏移误差作为一个概括的off-by-one错误。首先，我们报告了对11个真实世界的计算科学代码库的代码分析研究，确定了数组使用的常见习惯用法及其空间属性。这为科学代码中常见的数组编程习惯提供了急需的数据。根据这些数据，我们设计了一种轻量级的声明式规范语言，通过一小组组合子捕获大多数数组访问模式。我们详细介绍了一个语义模型，我们的规范语言，既检查和推断规范的验证工具的设计和实现。我们评估我们的工具对我们的语料库的科学代码。使用推理模式，我们在大约110万行代码中发现了大约87，000个目标，表明绝大多数数组计算都是以简单，规则，静态形状的模式从数组中读取的。我们还研究了我们的语料库包之一的提交日志，找到了过去的bug修复，我们的规范系统区分了更改，因此可以应用于检测此类bug。
Arrays computations are at the core of numerical modelling and computational science applications. However, low-level manipulation of array indices is a source of program error. Many practitioners are aware of the need to ensure program correctness, yet very few of the techniques from the programming research community are applied by scientists. We aim to change that by providing targetted lightweight verification techniques for scientific code. We focus on the all too common mistake of array offset errors as a generalisation of off-by-one errors. Firstly, we report on a code analysis study on eleven real-world computational science code base, identifying common idioms of array usage and their spatial properties. This provides much needed data on array programming idioms common in scientific code. From this data, we designed a lightweight declarative specification language capturing the majority of array access patterns via a small set of combinators. We detail a semantic model, and the design and implementation of a verification tool for our specification language, which both checks and infers specifications. We evaluate our tool on our corpus of scientific code. Using the inference mode, we found roughly 87,000 targets for specification across roughly 1.1 million lines of code, showing that the vast majority of array computations read from arrays in a pattern with a simple, regular, static shape. We also studied the commit logs of one of our corpus packages, finding past bug fixes for which our specification system distinguishes the change and thus could have been applied to detect such bugs.
登录
查看更多内容
DOI：
--
发表时间：
1997-12
期刊：
--
影响因子：
--
作者：
M. Griebel;T. Dornseifer;T. Neunhoeffer
通讯作者：
M. Griebel;T. Dornseifer;T. Neunhoeffer
DOI：
--
发表时间：
1997-09
期刊：
--
影响因子：
--
作者：
Tao Pang
通讯作者：
Tao Pang
GPGPU程序的规范和验证
DOI：
10.1016/j.scico.2014.03.013
发表时间：
2013
期刊：
Sci. Comput. Program.
影响因子：
--
作者：
S. Blom;M. Huisman;M. Mihelčić
通讯作者：
M. Mihelčić
闪电演讲：以轻量级规范支持软件可持续性
DOI：
10.17863/cam.4599
发表时间：
2016
期刊：
--
影响因子：
--
作者：
Contrastin MOJP
通讯作者：
Contrastin MOJP
“验证数组计算的空间属性”的证明
DOI：
--
发表时间：
2017
期刊：
影响因子：
--
作者：
Dominic A. Orchard;Mistral Contrastin;Matthew Danish;A. Rice
通讯作者：
A. Rice