Information about the memory locations accessed by a program is, for instance, required for program parallelisation and program verification. Existing inference techniques for this information provide only partial solutions for the important class of array-manipulating programs. In this paper, we present a static analysis that infers the memory footprint of an array program in terms of permission pre- and postconditions as used, for example, in separation logic. This formulation allows our analysis to handle concurrent programs and produces specifications that can be used by verification tools. Our analysis expresses the permissions required by a loop via maximum expressions over the individual loop iterations. These maximum expressions are then solved by a novel maximum elimination algorithm, in the spirit of quantifier elimination. Our approach is sound and is implemented; an evaluation on existing benchmarks for memory safety of array programs demonstrates accurate results, even for programs with complex access patterns and nested loops.
基于堆栈的访问控制机制在Java和Microsoft的公共语言运行时（Common Language Runtime）的安全体系结构中起着基础性的作用。它在运行时通过在程序执行安全关键操作之前检查当前调用堆栈中的方法以获得授予的权限来实施。虽然堆栈检查是很好的研究，有相对较少的工作自动生成的访问控制策略，大多数现有的工作推断安全策略假设的权限检查堆栈检查点是事先知道的。生成访问控制策略的实用方法仍然是由开发人员根据特定领域的知识和试错测试手动完成的。在本文中，我们提出了一个系统的方法来自动生成的Java程序，必须确保程序通过堆栈检查的访问控制策略。这些技术是基于抽象解释的上下文敏感静态程序分析。我们的分析模型的程序相结合的上下文敏感的调用图与依赖图。因此，我们能够准确地识别在堆栈检查点的许可要求，这通常是在以前的研究中被忽略。
Arrays are commonly used in a variety of software to store and process data in loops. Automatically proving safety properties of such programs that manipulate arrays is challenging. We present a novel verification technique, called full-program induction, for proving (a sub-class of) quantified as well as quantifier-free properties of programs manipulating arrays of parametric size $N$. Instead of inducting over individual loops, our technique inducts over the entire program (possibly containing multiple loops) directly via the program parameter $N$. The technique performs non-trivial transfor…
Writing correct programs for weak memory models such as the C11 memory model is challenging because of the weak consistency guarantees these models provide. The first program logics for the verification of such programs have recently been proposed, but their usage has been limited thus far to manual proofs. Automating proofs in these logics via first-order solvers is non-trivial, due to reasoning features such as higher-order assertions, modalities and rich permission resources. In this paper, we provide the first implementation of a weak memory program logic using existing deductive verificat…
The array is a fundamental data structure that provides an efficient way to store and retrieve non-sparse data contiguous in memory. Arrays are important for the performance of many memory-intensive applications due to the design of modern memory hierarchies: contiguous storage facilitates spatial locality and predictive access patterns which enables prefetching. Operations on large arrays often lend themselves well to parallelisation, such as a fork-join style divide-and-conquer algorithm for sorting. For parallel operations on arrays to be deterministic, data-race freedom must be guaranteed.…
We present a full-program induction technique for proving (a sub-class of) quantified as well as quantifier-free properties of programs manipulating arrays of parametric size N. Instead of inducting over individual loops, our technique inducts over the entire program (possibly containing multiple loops) directly via the program parameter N. Significantly, this does not require generation or use of loop-specific invariants. We have developed a prototype tool Vajra to assess the efficacy of our technique. We demonstrate the performance of Vajra vis-a-vis several state-of-the-art tools on a set o…
Automatic verification of array manipulating programs is a challenging problem because it often amounts to the inference of in ductive quantified loop invariants which, in some cases, may not even be firstorder expressible. In this paper, we suggest a novel verification tech nique that is based on induction on userdefined rank of program states as an alternative to loopinvariants. Our technique, dubbed inductive rank reduction, works in two steps. Firstly, we simplify the verification problem and prove that the program is correct when the input state con tains an input array of length B or les…
Large volumes of data generated by scientific experiments and simulations come in the form of arrays, while programs that analyze these data are frequently expressed in terms of array operations in an imperative, loop-based language. But, as datasets grow larger, new frameworks in distributed Big Data analytics have become essential tools to large-scale scientific computing. Scientists, who are typically comfortable with numerical analysis tools but are not familiar with the intricacies of Big Data analytics, must now learn to convert their loop-based programs to distributed data-parallel prog…
Array-intensive programs are often amenable to parallelization across many cores on a single machine as well as scaling across multiple machines and hence are well explored, especially in the domain of high-performance computing. These programs typically undergo loop transformations and arithmetic transformations in addition to parallelizing transformations. Although a lot of effort has been invested in improving parallelizing compilers, experienced programmers still resort to hand-optimized transformations which is typically followed by careful tuning of the transformed program to finally obt…
We present a novel verification technique to prove interesting properties of a class of array programs with a symbolic parameter N denoting the size of arrays. The technique relies on constructing two slightly different versions of the same program. It infers difference relations between the corresponding variables at key control points of the joint control-flow graph of the two program versions. The desired post-condition is then proved by inducting on the program parameter $N$, wherein the difference invariants are crucially used in the inductive step. This contrasts with classical technique…
University of Edinburgh（爱丁堡大学）；University of Oxford（牛津大学）；ETH Zurich（苏黎世联邦理工学院）；Graphcore；Microsoft Research（微软研究院）；Epic Games；DeepMind
Automatic differentiation (AD) is a technique for computing the derivative of a function represented by a program. This technique is considered as the de-facto standard for computing the differentiation in many machine learning and optimisation software tools. Despite the practicality of this technique, the performance of the differentiated programs, especially for functional languages and in the presence of vectors, is suboptimal. We present an AD system for a higher-order functional array-processing language. The core functional language underlying this system simultaneously supports both so…
Multidimensional arrays (NDArrays) are a central abstraction in modern scientific computing environments. Unfortunately, they can make reasoning about programs harder as the number of different array shapes used in an execution of a program is usually very large, and they rarely appear explicitly in program text. To make things worse, many operators make implicit assumptions about the shapes of their inputs: array addition is commonly enriched with broadcasting semantics, while matrix multiplication assumes that the lengths of contracted dimensions are equal. Because precise reasoning about sh…
An increasing number of scientific applications are making use of irregular data access patterns. An important class of such patterns involve subscripted-subscripts, wherein an array value appears in the index expression of another array. Even though the information required to parallelize loops with such patterns is often available in the program, present compiler techniques fall short of analyzing that information. In this paper we present a study of subscripted-subscripts, the properties that define the subscript arrays, and an algorithm based on symbolic range aggregation, that will help p…
Array Program Transformation with Loo.py by Example: High-Order Finite Elements
University of Illinois at Urbana-Champaign（伊利诺伊大学厄巴纳-香槟分校）；Naval Postgraduate School（海军研究生学院）；Virginia Polytechnic Institute and State University（弗吉尼亚理工大学）
