Proofs for ‘Verifying Spatial Properties of Array Computations’
Proofs for ‘Verifying Spatial Properties of Array Computations’
复制标题
“验证数组计算的空间属性”的证明
DOI：
--
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
A. Rice
中科院分区：
文献类型：
--
作者：
Dominic A. Orchard;Mistral Contrastin;Matthew Danish;A. Rice
该技术报告提供了论文的参与证明：验证数组计算的空间属性关于区域近似理论的声音是，我们的推理算法是合理的。正常形式 - 在这里注册了用于实现核心定义的数据结构，以使整体报告更加自我包含。易于交叉引用1（感应变量）在循环主体的范围内被解释为句法变量。指示N-二维阵列的元素，在n尺寸的索引上，由整数表达式e1指定。 EI作为索引）。 “原点”由于索引相对于感应变量4（邻域和仿射索引）的索引。如果e为e g i，e = i + c或e c c，其中c是一个整数常数，而i是指令变量，则邻居索引是指令变量的常数偏移/翻译（关系这里识别 +和 - （例如（-b） + i◦Ib）的 +和 - 的反向关系的术语。常数。
This technical report provides accompanying proofs for the paper: Verifying Spatial Properties of Array Computations. We show three properties of the lattice model of the stencil specification language. 1) that it is sound with respect to the equational theory of region specifications; 2) that is it sound with respect to the theory of region approximation; 3) that the inference algorithm is sound. We further derive useful identities on the specification language and properties of Union Normal Form—the data structure used to implement the model. Core definitions from the paper are restated here to make the overall report more self contained. Numbering for definitions, lemmas, propositions, theorems, and sections is aligned to the paper [1] for easy cross-reference. Definition 1 (Induction variables). An integer variable is an induction variable if it is the control variable of a “for” loop (do in Fortran), incremented by 1 per iteration. A variable is interpreted as an induction variable only within the scope of the loop body. Throughout, syntactic variables i, j, k range over induction variables. Definition 2 (Array subscripts and indices). An array subscript, denoted a(ē), is an expression which indicates the element of an N -dimensional array a at the N -dimensional index ē, specified by a comma-separated sequence of integer expressions e1, . . . , eN . We also refer to each one of these ei as an index. An index ei is called relative if the expression involves an induction variable. An absolute index is an integer expression which is constant with respect to the enclosing loop, i.e., it does not involve an induction variable. Definition 3 (Origin). For an array subscript a(ē), the index ē is called an origin index, if all e ∈ ē are naked induction variable expressions, e.g., a(i, j). We refer to this as the “origin” since the indices are offset by 0 in each dimension relative to the induction variables. Definition 4 (Neighbourhood and affine index). For an array subscript a(ē), an index e ∈ ē is a neighbourhood index (or neighbour) if e is of the form e ≡ i, e ≡ i + c, or e ≡ i c, where c is an integer constant and i is an induction variable. That is, a neighbourhood index is a constant offset/translation of an induction variable. (The relation ≡ here identifies terms up-to commutativity of + and the inverse relationship of + and − e.g., (-b) + i ≡ i b). An affine index is an index expression of the form a*i + b, where a and b are constants.
影响因子：
--
作者：
Orchard D
通讯作者：
Orchard D