Permission Inference for Array Programs

TL;DR

This paper introduces a static analysis technique that infers memory permissions for array programs, enabling better verification and parallelization, especially for complex and nested loop structures.

Contribution

It presents a novel permission inference method using maximum elimination, handling concurrent programs and complex access patterns in array manipulation.

Findings

Accurately infers memory permissions for array programs.

Handles concurrent programs and nested loops effectively.

Demonstrates precise results on existing benchmarks.

Abstract

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.