abs.tex 3.23 KB
Newer Older
ehilin02's avatar
ehilin02 committed
1
%!TEX root = aplas2021.tex
2
3

\begin{abstract}
ehilin02's avatar
ehilin02 committed
4
%Pointer arithmetic is widely used in low-level programs, e.g. memory allocators. 
ehilin02's avatar
ehilin02 committed
5
Heap list is a data structure used in many memory allocators, to describe the physical layout of the memory. 
6
7
%
%The verification of such programs usually requires simultaneous reasoning about pointer arithmetic and unbounded heap regions.
ehilin02's avatar
ehilin02 committed
8
The specification of the programs in memory allocators usually requires using pointer arithmetic inside inductive definitions to define heap lists. % in memory allocators. 
9
10
11
%
In this work, we investigate decision problems for SLAH, a separation logic fragment 
that allows some form of pointer arithmetic inside inductive definitions, 
ehilin02's avatar
ehilin02 committed
12
thus enabling specification of properties for programs manipulating heap lists. 
13
14
15
%
Pointer arithmetic inside inductive definitions is challenging for automated reasoning.  
%
ehilin02's avatar
ehilin02 committed
16
17
We tackle this challenge and achieve decision procedures for both satisfiability and entailment of SLAH formulas.
% specifying heap lists data structures. 
18
19
20
21
22
23
24
%
The crux of our decision procedure for satisfiability is to compute summaries of inductive definitions capturing heap lists. We show that although the summary is naturally expressed as an existentially quantified non-linear arithmetic formula, it can actually be transformed into an equivalent linear arithmetic formula. 
%
The decision procedure for entailment, on the other hand, has to match and split the spatial atoms according to the arithmetic relation between address variables. 
%
We report on the implementation of these decision procedures and their 
good performance in solving problems issued from the verification of 
Mihaela SIGHIREANU's avatar
Mihaela SIGHIREANU committed
25
building block programs manipulating heap-lists used in memory allocators.
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
%
\hide{
We study the decidability of the verification problem for 
an extension of the array separation logic (ASL) 
allowing the specification of data structures like 
pointers, memory blocks or heap-lists, 
which are lists built inside memory blocks. 
The logic, called \slah, adds to ASL %an
inductively defined predicates specifying singly linked heap-lists. 
%
We show that the logic is suitable for the compositional verification 
of programs manipulating heap-lists, e.g., memory allocators. 
%
We propose decision procedures for satisfiability and entailment of \slah, 
which are substantial extensions of those proposed for ASL 
because they have to deal with pointer arithmetic inside inductive definitions.
% 
Our decision procedures propose some new ideas to tackle this challenge. 
The crux of our decision procedure for satisfiability is 
to compute a summary of the inductive definition of the heap-list predicate.
We show that although the summary is expressed as 
an existentially quantified non-linear arithmetic constraint, 
it can actually be transformed into an equivalent linear arithmetic formula. 
%
The decision procedure for entailment 
uses the decision procedure for satisfiability as an oracle 
and deals with the pointer arithmetic in the inductive definitions. 
%
We implemented the decision procedures and 
did experiments to evaluate their performance. 
The experimental results demonstrate the effectiveness of the solver
for deciding problems issued from the verification 
of heap-list manipulating programs.
}
\end{abstract}