Sie können Operatoren mit Ihrer Suchanfrage kombinieren, um diese noch präziser einzugrenzen. Klicken Sie auf den Suchoperator, um eine Erklärung seiner Funktionsweise anzuzeigen.
Findet Dokumente, in denen beide Begriffe in beliebiger Reihenfolge innerhalb von maximal n Worten zueinander stehen. Empfehlung: Wählen Sie zwischen 15 und 30 als maximale Wortanzahl (z.B. NEAR(hybrid, antrieb, 20)).
Findet Dokumente, in denen der Begriff in Wortvarianten vorkommt, wobei diese VOR, HINTER oder VOR und HINTER dem Suchbegriff anschließen können (z.B., leichtbau*, *leichtbau, *leichtbau*).
Dieser Artikel vertieft sich in die kritische Frage der Speichereffizienz in der abstrakten Interpretation, einem Eckpfeiler der statischen Programmanalyse. Es führt eine bahnbrechende Technik zur speichereffizienten Fixpunktberechnung ein, die für die Extraktion von Programminvarianten, die in verschiedenen Client-Anwendungen wie Programmprüfern, Optimierern und Fehlersuchern verwendet werden, unverzichtbar ist. Die vorgeschlagene Methode minimiert den Speicherbedarf, ohne Präzision oder Zeiteffizienz einzubüßen, was sie zu einem bedeutenden Fortschritt auf diesem Gebiet macht. Der Artikel bietet einen umfassenden theoretischen Rahmen, einschließlich des Nachweises von Optimalität und Validität, und präsentiert einen nahezu linearen Zeitalgorithmus für die Erstellung der speichereffizienten Iterationsstrategie. Empirische Auswertungen zeigen erhebliche Speichereinsparungen in praktischen Szenarien, wie etwa die Überprüfung benutzerdefinierter Behauptungen und den Nachweis fehlender Pufferüberläufe. Die Implementierung dieser Technik in einem Werkzeug namens Mikos, das den hochmodernen abstrakten Interpreter IKOS erweitert, zeigt ihre Anwendbarkeit und Effektivität in der realen Welt. Dieser Artikel ist ein Pflichtlektüre für alle, die die Leistungsfähigkeit und Effizienz statischer Analysewerkzeuge verbessern möchten.
KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
Abstract
Practical adoption of static analysis often requires trading precision for performance. This paper focuses on improving the memory efficiency of abstract interpretation without sacrificing precision or time efficiency. Computationally, abstract interpretation reduces the problem of inferring program invariants to computing a fixpoint of a set of equations. This paper presents a method to minimize the memory footprint in Bourdoncle’s iteration strategy, a widely-used technique for fixpoint computation. Our technique is agnostic to the abstract domain used. We prove that our technique is optimal (i.e., it results in minimum memory footprint) for Bourdoncle’s iteration strategy while computing the same result. We evaluate the efficacy of our technique by implementing it in a tool called \(\textsc {Mikos}\), which extends the state-of-the-art abstract interpreter \(\text {IKOS}\). On average \(\textsc {Mikos}\) demonstrated a \(24.57\times \) and \(2.29\times \) reduction in peak-memory usage compared to \(\text {IKOS}\) when verifying user-provided assertions and performing interprocedural buffer-overflow analysis, respectively.
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
1 Introduction
Abstract interpretation [1, 2] is a general framework for expressing static analysis of programs. Program invariants inferred by an abstract interpreter are used in client applications such as program verifiers, program optimizers, and bug finders. To extract the invariants, an abstract interpreter computes a fixpoint of an equation system approximating the program semantics. The efficiency and precision of the abstract interpreter depends on the iteration strategy, which specifies the order in which the equations are applied during fixpoint computation.
The recursive iteration strategy developed by Bourdoncle [3] is widely used for fixpoint computation in academic and industrial abstract interpreters such as NASA IKOS [4], Crab [5], Facebook SPARTA [6], Kestrel Technology CodeHawk [7], and Facebook Infer [8]. Extensions to Bourdoncle’s approach that improve precision [9] and time efficiency [10] have also been proposed.
Anzeige
This paper focuses on improving the memory efficiency of abstract interpretation. This is an important problem in practice because large memory requirements can prevent clients such as compilers and developer tools from using sophisticated analyses. This has motivated approaches for efficient implementations of abstract domains [11‐13], including techniques that trade precision for efficiency [14‐16].
This paper presents a technique for memory-efficient fixpoint computation. Our technique minimizes the memory footprint in Bourdoncle’s recursive iteration strategy. Our approach is agnostic to the abstract domain and does not sacrifice time efficiency. We prove that our technique exhibits optimal peak-memory usage for the recursive iteration strategy while computing the same fixpoint (Sect. 3). Specifically, our approach does not change the iteration order but provides a mechanism for early deallocation of abstract values. Thus, there is no loss of precision when improving memory performance. Furthermore, such “backward compatibility” ensures that existing implementations of Bourdoncle’s approach can be replaced without impacting clients of the abstract interpreter, an important requirement in practice.
Suppose we are tasked with proving assertions at program points 4 and 9 of the control-flow graph in Fig. 1c. Current approaches (Sect. 2.1) allocate abstract values for each program point during fixpoint computation, check the assertions at 4 and 9 after fixpoint computation, and then deallocate all abstract values. In contrast, our approach deallocates abstract values and checks the assertions during fixpoint computation while guaranteeing that the results of the checks remain the same and that the peak-memory usage is optimal.
We prove that our approach deallocates abstract values as soon as they are no longer needed during fixpoint computation. Providing this theoretical guarantee is challenging for arbitrary irreducible graphs such as \(G_3\). For example, assuming that node 8 is analyzed after 3, one might think that the fixpoint iterator can deallocate the abstract value at 2 once it analyzes 8. However, 8 is part of the strongly-connected component \(\{7, 8\}\), and the fixpoint iterator might need to iterate over node 8 multiple times. Thus, deallocating the abstract value at 2 when node 8 is first analyzed will lead to incorrect results. In this case, the earliest that the abstract value at 2 can be deallocated is after the stabilization of component \(\{7, 8\}\).
Anzeige
Furthermore, we prove that our approach performs the assertion checks as early as possible during fixpoint computation. Once the assertions are checked, the associated abstract values are deallocated. For example, consider the assertion check at node 4. Notice that 4 is part of the strongly-connected components \(\{4,5 \}\) and \(\{3,4,5,6 \}\). Checking the assertion the first time node 4 is analyzed could lead to an incorrect result because the abstract value at 4 has not converged. The earliest that the check at node 4 can be executed is after the convergence of the component \(\{3,4,5,6\}\). Apart from being able to deallocate abstract values earlier, early assertion checks provide partial results on timeout.
The key theoretical result (Theorem 12) is that our iteration strategy is memory-optimal (i.e., it results in minimum memory footprint) while computing the same result as Bourdoncle’s approach. Furthermore, we present an almost-linear time algorithm to compute this optimal iteration strategy (Sect. 4).
We have implemented this memory-optimal fixpoint computation in a tool called \(\textsc {Mikos}\) (Sect. 5), which extends the state-of-the-art abstract interpreter for C/C++, \(\text {IKOS}\) [4]. We compared the memory efficiency of \(\textsc {Mikos}\) and \(\text {IKOS}\) on the following tasks:
T1
Verifying user-provided assertions. Task T1 represents the program-verification client of a fixpoint computation. We performed interprocedural analysis of 784 SV-COMP 2019 benchmarks [17] using reduced product of Difference Bound Matrix with variable packing [14] and congruence [18] domains.
T2
Proving absence of buffer overflows. Task T2 represents the bug-finding and compiler-optimization client of fixpoint computation. In the context of bug finding, a potential buffer overflow can be reported to the user as a potential bug. In the context of compiler optimization, code to check buffer-access safety can be elided if the buffer access is verified to be safe. We performed interprocedural buffer overflow analysis of 426 open-source programs using the interval abstract domain.
On Task T1, \(\textsc {Mikos}\)’s peak-memory usage is \(4.07\)% of \(\text {IKOS}\)’s peak-memory usage on average, which is a \(24.57\times \) reduction. For instance, peak-memory required to analyze the SV-COMP 2019 benchmark ldv-3.16-rc1/205_9a-net-rtl8187 decreased from 46 GB to 56 MB. Also, while ldv-3.14/usb-mxl111sf spaced out in \(\text {IKOS}\) with 64 GB memory limit, peak-memory usage was 21 GB for \(\textsc {Mikos}\). On Task T2, \(\textsc {Mikos}\)’s peak-memory usage is, on average, \(43.7\)% of \(\text {IKOS}\)’s peak-memory usage on average, which is a \(2.29\times \) reduction. \(\textsc {Mikos}\) shows a decrease in peak-memory usage to \(43.7\)% (\(2.29\times \)) on average compared to \(\text {IKOS}\). For instance, peak-memory required to analyze a benchmark ssh-keygen decreased from 30 GB to 1 GB.
The contributions of the paper are as follows:
A memory-optimal technique for Bourdoncle’s recursive iteration strategy that does not sacrifice precision or time efficiency (Sect. 3).
An almost-linear time algorithm to construct our memory-efficient iteration strategy (Sect. 4).
\(\textsc {Mikos}\), an interprocedural implementation of our approach (Sect. 5).
An empirical evaluation of the efficacy of \(\textsc {Mikos}\) using a large set of C benchmarks (Sect. 6).
Section 2 presents necessary background on fixpoint computation, including Bourdoncle’s approach; Sect. 7 presents related work; Sect. 8 concludes.
2 Fixpoint computation preliminaries
This section presents background on fixpoint computation that will allow us to clearly state the problem addressed in this paper (Sect. 2.3). This section is not meant to capture all possible approaches to implementing abstract interpretation. However, it does capture the relevant high-level structure of abstract-interpretation implementations such as IKOS [4].
Consider an equation system \(\Phi \) whose dependency graph is . The graph G typically reflects the control-flow graph of the program, though this is not always true. The aim is to find the fixpoint of the equation system \(\Phi \):
(1)
The maps \(\textsc {Pre}:V \rightarrow \mathcal {A}\) and \(\textsc {Post}:V \rightarrow \mathcal {A}\) maintain the abstract values at the beginning and end of each program point, where \(\mathcal {A}\) is an abstract domain. The abstract transformer \(\tau _v :\mathcal {A}\rightarrow \mathcal {A}\) overapproximates the semantics of program point \(v \in V\). After fixpoint computation, \(\textsc {Pre}[v]\) is an invariant for \(v \in V\).
Client applications of the abstract interpreter typically query these fixpoint values to perform assertion checks, program optimizations, or report bugs. Let \(V_C\subseteq V\) be the set of program points where such checks are performed, and let \(\varphi _v :\mathcal {A}\rightarrow bool\) represent the corresponding functions that performs the check for each \(v \in V_C\). To simplify presentation, we assume that the check function merely returns true or false. Thus, after fixpoint computation, the client application computes \(\varphi _v(\textsc {Pre}[v])\) for each \(v \in V_C\).
The exact least solution of the system Eq. 1 can be computed using Kleene iteration provided \(\mathcal {A}\) is Noetherian. However, most interesting abstract domains require the use of widening (\(\triangledown \)) to ensure termination followed by narrowing to improve the post solution. In this paper, we use “fixpoint” to refer to such an approximation of the least fixpoint. Furthermore, for simplicity of presentation, we restrict our description to a simple widening strategy. However, our implementation (Sect. 5) uses more sophisticated widening and narrowing strategies implemented in state-of-the-art abstract interpreters [4, 9].
An iteration strategy specifies the order in which the individual equations are applied, where widening is used, and how convergence of the equation system is checked. For clarity of exposition, we introduce a Fixpoint Machine (FM) consisting of an imperative set of instructions. An \(\texttt {FM}\) program represents a particular iteration strategy used for fixpoint computation. The syntax of Fixpoint Machine programs is defined by the following grammar:
(2)
Informally, the instruction \(\texttt{exec}\ v\) applies \(\tau _v\) for \(v \in V\); the instruction \(\texttt{repeat}\ v\ \texttt {[}P_1 \texttt {]} \) repeatedly executes the \(\texttt {FM}\) program \(P_1\) until convergence and performs widening at v; and the instruction executes \(\texttt {FM}\) programs \(P_1\) and \(P_2\) in sequence.
The syntax (Eq. 2) and semantics (Fig. 2) of the Fixpoint Machine are sufficient to express Bourdoncle’s recursive iteration strategy (Sect. 2.1), a widely-used approach for fixpoint computation [3]. We also extend the notion of iteration strategy to perform memory management of the abstract values as well as perform checks during fixpoint computation (Sect. 2.2).
2.1 Bourdoncle’s recursive iteration strategy
In this section, we review Bourdoncle’s recursive iteration strategy [3] and show how to generate the corresponding \(\texttt {FM}\) program.
Bourdoncle’s iteration strategy relies on the notion of weak topological ordering (WTO) of a directed graph . A WTO is defined using the notion of a hierarchical total ordering (HTO) of a set.
Definition 1
A hierarchical total ordering\(\mathcal {H}\) of a set V is a well parenthesized permutation of V without two consecutive “(”. \(\square \)
An HTO \(\mathcal {H}\) is a string over the alphabet V augmented with left and right parenthesis. Alternatively, we can denote an HTO \(\mathcal {H}\) by the tuple \((V, \preceq , \omega )\), where \(\preceq \) is the total order induced by \(\mathcal {H}\) over the elements of V and \(\omega :V \rightarrow 2^V\). The elements between two matching parentheses are called a component, and the first element of a component is called the head. Given \(l \in V\), \(\omega (l)\) is the set of heads of the components containing l. We use \(\mathcal {C}:V \rightarrow 2^V\) to denote the mapping from a head to its component.
Example 1
Let \(V = \{1, 2, 3, 4, 5, 6, 7, 8, 9\}\). An example HTO \(\mathcal {H}_1(V, \preceq , \omega )\) is \(\mathtt {1\ 2}\)\(\mathtt {3\ 4\ 5\ 6\ 7\ 8\ 9}\). \(\omega (l) = \emptyset \) for all \(l \in V\). \(\mathcal {H}_1\) has no components. \(\square \)
Example 2
Let \(V = \{1, 2, 3, 4, 5, 6, 7, 8, 9\}\). An example HTO \(\mathcal {H}_2(V, \preceq , \omega )\) is \(\mathtt {1\ 2\ 3\ (4\ 5)} \mathtt {6\ (7\ 8)\ 9}\). \(\omega (3) = \emptyset \), \(\omega (5) = \{4\}\), and \(\omega (4) = \{4\}\). It has components \(\mathcal {C}(4) = \{4, 5\}\) and \(\mathcal {C}(7) = \{7, 8\}\). \(\square \)
Example 3
Let \(V = \{1, 2, 3, 4, 5, 6, 7, 8, 9\}\). An example HTO \(\mathcal {H}_3(V, \preceq , \omega )\) is \(\mathtt {1\ 2}\)\(\mathtt {(3\ (4\ 5)\ 6)\ (7\ 8)\ 9}\). \(\omega (3) = \{3\}\), \(\omega (5) = \{3, 4\}\), and \(\omega (1) = \emptyset \). It has components \(\mathcal {C}(4) = \{4, 5\}\), \(\mathcal {C}(7) = \{7, 8\}\) and \(\mathcal {C}(3) = \{3, 6\} \cup \mathcal {C}(4)\). \(\square \)
A weak topological ordering (WTO) \(\mathcal {W}\) of a directed graph can now be defined using the notion of an HTO.
Definition 2
A weak topological ordering\(\mathcal {W}(V, \preceq , \omega )\) of a directed graph is an HTO \(\mathcal {H}(V, \preceq , \omega )\) such that for every edge \(u \rightarrow v\), either (i) \(u \prec v\), or (ii) \(v \preceq u\) and \(v \in \omega (u)\). \(\square \)
Example 4
\(\mathcal {H}_1\) in Example 1 is a WTO \(\mathcal {W}_1\) of the graph \(G_1\) (Fig. 1a). \(\square \)
Example 5
\(\mathcal {H}_2\) in Example 2 is a WTO \(\mathcal {W}_2\) of the graph \(G_2\) (Fig. 1b). \(\square \)
Example 6
\(\mathcal {H}_3\) in Example 3 is a WTO \(\mathcal {W}_3\) of the graph \(G_3\) (Fig. 1c). \(\square \)
Given a directed graph that represents the dependency graph of the equation system, Bourdoncle’s approach uses a WTO \(\mathcal {W}(V, \preceq , \omega )\) of G to derive the following recursive iteration strategy:
The total order \(\preceq \) determines the order in which the equations are applied. The equation after a component is applied only after the component stabilizes.
The stabilization of a component \(\mathcal {C}(h)\) is determined by checking the stabilization of the head h.
Widening is performed at each of the heads.
We now show how the WTO can be represented using the syntax of our Fixpoint Machine (\(\texttt {FM}\)) defined in Eq. 2. The following function \(\texttt{genProg}:\text {WTO} \rightarrow Prog \) maps a given WTO \(\mathcal {W}\) to an \(\texttt {FM}\) program:
(3)
Each node \(v \in V\) is mapped to a single \(\texttt {FM}\) instruction by \(\texttt{genProg}\); we use \(\texttt {Inst}[v]\) to refer to this \(\texttt {FM}\) instruction corresponding to v. Note that if \(v\in V\) is a head, then \(\texttt {Inst}[v]\) is an instruction of the form \(\texttt{repeat}\ v\ \texttt {[}\ldots \texttt {]}\), else \(\texttt {Inst}[v]\) is \(\texttt{exec}\ v\).
Example 7
The WTO \(\mathcal {W}_1\) of graph \(G_1\) (Fig. 1a) is \(\mathtt {1\ 2\ 3\ 4\ 5\ 6\ 7\ 8\ 9}\). The corresponding \(\texttt {FM}\) program is . Note that \(\texttt {Inst}[v] = \texttt{exec}\ v\) for all \(v \in [1, 9]\). \(\square \)
Example 8
The WTO \(\mathcal {W}_2\) of graph \(G_2\) (Fig. 1b) is . The corresponding \(\texttt {FM}\) program is .
Note that . \(\square \)
Example 9
The WTO \(\mathcal {W}_3\) of graph \(G_3\) (Fig. 1c) is . The corresponding \(\texttt {FM}\) program is . \(\square \)
Ignoring the text in gray, the semantics of the \(\texttt {FM}\) instructions shown in Fig. 2 capture Bourdoncle’s recursive iteration strategy. The semantics are parameterized by the graph and a WTO \(\mathcal {W}(V, \preceq , \omega )\).
Fig. 2
The semantics of the fixpoint machine (\(\texttt {FM}\)) instructions of Eq. 2
In this paper, we extend the notion of iteration strategy to indicate when abstract values are deallocated and when checks are executed. The
text in Fig. 2 shows the semantics of the \(\texttt {FM}\) instructions that handle these issues. The right-hand side of \(\Rightarrow \) is executed if the left-hand side evaluates to true. Recall that the set \(V_C \subseteq V\) is the set of program points that have assertion checks. The map \(\textsc {Ck}:V_C \rightarrow \texttt {bool}\) records the result of executing the check \(\varphi _u(\textsc {Pre}[u])\) for each \(u \in V_C\). Thus, the output of the\(\texttt {FM}\)program is the map \(\textsc {Ck}\). In practice, the functions \(\varphi _u\) are expensive to compute. Furthermore, they often write the result to a database or report the output to a user. Consequently, we assume that only the first execution of \(\varphi _u\) is recorded in \(\textsc {Ck}\).
The memory configuration is a tuple where
The map controls the deallocation of values in \(\textsc {Post}\) that have no further use. If , \(\textsc {Post}[u]\) is deallocated after the execution of \(\texttt {Inst}[v]\).
The map controls when the check function \(\varphi _u\) corresponding to \(u \in V_C\) is executed, after which the corresponding \(\textsc {Pre}\) value is deallocated. If , assertions in u are checked and \(\textsc {Pre}[u]\) is subsequently deallocated after the execution of \(\texttt {Inst}[v]\).
The map control deallocation of \(\textsc {Post}\) values that are recomputed and overwritten in the loop of a \(\texttt{repeat}\) instruction before its next use. If , \(\textsc {Post}[u]\) is deallocated in the loop of \(\texttt {Inst}[v]\).
The map control deallocation of \(\textsc {Pre}\) values that are recomputed and overwritten in the loop of a \(\texttt{repeat}\) instruction before its next use. If , \(\textsc {Pre}[u]\) is deallocated in the loop of \(\texttt {Inst}[v]\).
To simplify presentation, the semantics in Fig. 2 does not make explicit the allocations of abstract values: if a \(\textsc {Post}\) or \(\textsc {Pre}\) value that has been deallocated is accessed, then it is allocated and initialized to \(\bot \).
2.3 Problem statement
Two memory configurations are equivalent if they result in the same values for each check in the program:
Definition 3
Given an \(\texttt {FM}\) program P, memory configuration is equivalent to, denoted by , iff for all \(u \in V_C\), we have \(\textsc {Ck}_1[u] = \textsc {Ck}_2[u]\), where \(\textsc {Ck}_1\) and \(\textsc {Ck}_2\) are the check maps corresponding to execution of P using and , respectively. \(\square \)
The default memory configuration performs checks and deallocations at the end of the \(\texttt {FM}\) program after fixpoint has been computed.
Definition 4
Given an \(\texttt {FM}\) program P, the default memory configuration is for all \(v \in V\), for all \(c \in V_C\), and , where z is the last instruction in P. \(\square \)
Example 10
Let \(V_C = \{4, 9\}\).
For all \(\texttt {FM}\) programs, \(P_1\), \(P_2\) and \(P_3\),
for all \(v \in V\). That is, all \(\textsc {Post}\) values are deallocated at the end of the fixpoint computation. Also, , meaning that assertion checks also happen at the end.
, so the \(\texttt {FM}\) programs do not clear abstract values whose values will be recomputed and overwritten in a loop of \(\texttt{repeat}\) instruction. \(\square \)
Given an \(\texttt {FM}\) program P, a memory configuration is valid for P iff it is equivalent to the default configuration; i.e., .
Furthermore, a valid memory configuration is optimal for a given \(\texttt {FM}\) program iff the memory footprint of is smaller than or equal to that of for all valid memory configuration . The problem addressed in this paper can be stated as:
An optimal configuration should deallocate abstract values during fixpoint computation as soon they are no longer needed. The challenge is ensuring that the memory configuration remains valid even without knowing the number of loop iterations for \(\texttt{repeat}\) instructions.
3 Declarative specification of optimal memory configuration
This section provides a declarative specification of an optimal memory configuration (, , , ). Section 4 presents an efficient algorithm for computing .
Definition 5
Given a WTO \(\mathcal {W}(V, \preceq , \omega )\) of a graph , the nesting relation\(\textsf {N}\) is a tuple where iff \(u = v\) or \(v \in \omega (u)\) for \(u, v \in V\). \(\square \)
Let ; that is, equals the set containing v and the heads of components in the WTO that contains v. The nesting relation is a forest; i.e. a partial order such that for all \(v\in V\), is a chain, as proven below.
Theorem 1
is a forest.
Proof
First, we show that is a partial order. Let x, y, z be vertices in V.
Reflexivity: . This is true by the definition of .
Transitivity: and implies . (i) If \(x = y\), . (ii) Otherwise, by definition of , \(y \in \omega (x)\). Furthermore, (ii-1) if \(y = z\), \(z \in \omega (x)\); and hence, . (ii-2) Otherwise, \(z \in \omega (y)\), and by definition of HTO, \(z \in \omega (x)\).
Anti-symmetry: and implies \(x = y\). Suppose \(x \ne y\). By definition of and premises, \(y \in \omega (x)\) and \(x \in \omega (y)\). Then, by definition of HTO, \(x \prec y\) and \(y \prec x\). This contradicts that \(\preceq \) is a total order.
Next, we show that the partial order is a forest. Suppose there exists \(v \in V\) such that is not a chain. That is, there exists such that and . Then, by definition of HTO, \(\mathcal {C}(x) \cap \mathcal {C}(y) = \emptyset \). However, this leads to a contradiction because \(v \in \mathcal {C}(x)\) and \(v \in \mathcal {C}(y)\). Thus, is a chain. \(\square \)
Example 11
For the WTO \(\mathcal {W}_1\) of \(G_1\) in Example 4, is \((V, =)\).
Example 12
For the WTO \(\mathcal {W}_2\) of \(G_2\) in Example 5, is:
implies that v is the earliest instruction at which \(\textsc {Post}[u]\) can be deallocated while ensuring that there are no subsequents reads of \(\textsc {Post}[u]\) during fixpoint computation. We cannot conclude from a dependency as illustrated in the following example.
Example 14
Consider the \(\texttt {FM}\) program \(P_3\) from Example 9, whose graph is in Fig. 1c. Although there is a dependency , memory configuration with is not valid: \(\textsc {Post}[2]\) is read by \(\texttt {Inst}[8]\), which is executed repeatedly as part of \(\texttt {Inst}[7]\); if , then \(\textsc {Post}[2]\) would be deallocated the first time\(\texttt {Inst}[8]\) is executed, and subsequent executions of \(\texttt {Inst}[8]\) will read \(\bot \) as the value of \(\textsc {Post}[2]\), which would be incorrect. \(\square \)
In general, for a dependency , we must find the head of maximal component that contains v but not u as the candidate for . By choosing the head of maximal component, we remove the possibility of having a larger component whose head’s \(\texttt{repeat}\) instruction can execute \(\texttt {Inst}[v]\) after deallocating \(\textsc {Post}[u]\). If there is no component that contains v but not u, we simply use v as the candidate. The following \(\mathop {\mathrm {\texttt {Lift}}}\limits \) operator gives us the candidate of for :
(4)
gives us v and the heads of components that contain v. Subtracting removes the heads of components that also contain u. We put back v to account for the case when there is no component containing v but not u and is empty. Because is a forest, and are chains, and hence, is also a chain. Therefore, maximum is well-defined.
Example 15
Consider the nesting relation from Example 11. For all , \(\mathop {\mathrm {\texttt {Lift}}}\limits (u, v) = v\). Note that there are no components in \(\mathcal {W}_1\). \(\square \)
Example 16
Consider the nesting relation from Example 12. \(\mathop {\mathrm {\texttt {Lift}}}\limits (2, 8)\). We see that 7 is the head of the maximal component containing 8 but not 2. Also, . There is no component that contains 5 but not 4. Similarly, . There is no component that contains 4 but not 5. \(\square \)
Example 17
Consider the nesting relation from Example 13. \(\mathop {\mathrm {\texttt {Lift}}}\limits (6, 3)\). There is no component that contains 3 but not 6. Also, . There is no component that contains 3 but not 5. \(\square \)
For each instruction u, we now need to find the last instruction from among the candidates computed using \(\mathop {\mathrm {\texttt {Lift}}}\limits \). Notice that deallocations of \(\textsc {Post}\) values are at a postamble of \(\texttt{repeat}\) instructions in Fig. 2. Therefore, we cannot use the total order \(\preceq \) of a WTO to find the last instruction: \(\preceq \) is the order in which the instruction begins executing, or the order in which preambles are executed.
Example 18
Let , an incorrect variant of that uses the total order \(\preceq \). Consider the \(\texttt {FM}\) program \(P_3\) from Example 9, whose graph is in Fig. 1c and nesting relation is in Example 13. \(\textsc {Post}[5]\) has dependencies and . \(\mathop {\mathrm {\texttt {Lift}}}\limits (5, 4) = 4\), \(\mathop {\mathrm {\texttt {Lift}}}\limits (5, 3) = 3\). Now, because \(3 \preceq 4\). However, a memory configuration with is not valid: \(\texttt {Inst}[4]\) is nested in \(\texttt {Inst}[3]\). Due to the deletion of \(\textsc {Post}[5]\) in \(\texttt {Inst}[4]\), \(\texttt {Inst}[3]\) will read \(\bot \) as the value of \(\textsc {Post}[5]\). \(\square \)
To find the order in which the instructions finish executing, or the order in which postambles are executed, we define the relation , using the total order \((V, \preceq )\) and the nesting relation :
(5)
In the definition of , the nesting relation takes precedence over \(\preceq \). is a total order.
Theorem 2
is a total order.
Proof
We prove the properties of a total order. Let x, y, z be vertices in V.
Connexity: or . This follows from the connexity of the total order \(\preceq \).
Transitivity: and implies . (i) Suppose . (i-1) If , by transitivity of , . (ii-2) Otherwise, and \(y \preceq z\). It cannot be because transitivity of implies , which is a contradiction. Furthermore, it cannot be \(z \prec x\) because \(y \preceq z \prec x\) and implies \(y \in \omega (z)\) by the definition of HTO. By connexity of \(\preceq \), \(x \preceq z\). (ii) Otherwise and \(x \preceq y\). (ii-1) If , because, otherwise, transitivity of will imply . By connexity of \(\preceq \), it is either \(x \preceq z\) or \(z \prec x\). If \(x \preceq z\), . If \(z \prec x\), by definition of HTO, \(z \in \omega (z)\).
Anti-symmetry: and implies \(x = y\). (i) If , it should be for to be true. By anti-symmetry of , \(x = y\). (ii) Otherwise, and \(x \preceq y\). For to be true, and \(x \preceq y\). By anti-symmetry of \(\preceq \), \(x = y\).\(\square \)
Intuitively, the total order moves the heads in the WTO to their corresponding closing parentheses ‘)’. In terms of the execution order and the order in which \(\textsc {Post}\) values are accessed, the total order has the following meaning.
Theorem 3
For \(u, v \in V\), if \(\texttt {Inst}[v]\) reads \(\textsc {Post}[u]\), then .
Proof
By the definition of the mapping \(\texttt {Inst}\), there must exists \(v' \in V\) such that and for \(\texttt {Inst}[v]\) to read \(\textsc {Post}[u]\). By the definition of WTO, it is either \(u \prec v'\) and \(v' \notin \omega (u)\), or \(v' \preceq u\) and \(v' \in \omega (u)\). In both cases, . Because , and hence , . \(\square \)
Example 19
For \(G_1\) (Fig. 1a) and its WTO \(\mathcal {W}_1\), \(\mathtt {1\ 2\ 3\ 4\ 5\ 6\ 7\ 8\ 9}\), we have . That is, . \(\square \)
Example 20
For \(G_2\) (Fig. 1b) and its WTO \(\mathcal {W}_2\), \(\mathtt {1\ 2\ 3\ (4\ 5)\ 6\ (7\ 8)\ 9}\), we have . Note that \(4 \preceq 5\) while . Postamble of \(\texttt{repeat}\ 4\ \texttt {[}\ldots \texttt {]}\) is executed after \(\texttt {Inst}[5]\), while preamble of \(\texttt{repeat}\ 4\ \texttt {[}\ldots \texttt {]}\) is executed before \(\texttt {Inst}[5]\). Similarly, \(7 \preceq 8\) while . \(\square \)
Example 21
For \(G_3\) (Fig. 1c) and its WTO \(\mathcal {W}_3\), \(\mathtt {1\ 2\ (3\ (4\ 5)\ 6)\ (7\ 8)\ 9}\), we have . Note that \(3 \preceq 5\) while . Postamble of \(\texttt{repeat}\ 3\ \texttt {[}\ldots \texttt {]}\) is executed after \(\texttt {Inst}[5]\), while preamble of \(\texttt{repeat}\ 3\ \texttt {[}\ldots \texttt {]}\) is executed before \(\texttt {Inst}[5]\). \(\square \)
We can now define . Given a nesting relation for the graph , is defined as:
(6)
Example 22
Consider the \(\texttt {FM}\) program \(P_1\) from Example 7, whose graph is in Fig. 1a and nesting relation is in Example 11. An optimal memory configuration defined by Eq. 6 is:
\(\mathop {\mathrm {\texttt {Lift}}}\limits (u, v) = v\) for all and for this case. Therefore, only \((V, \preceq )\) plays a role in determining . \(\square \)
Example 23
Consider the \(\texttt {FM}\) program \(P_2\) from Example 8, whose graph is in Fig. 1b and nesting relation is in Example 12. An optimal memory configuration defined by Eq. 6 is:
Successors of u are first lifted to compute . For example, to compute , 2’s successors, 3 and 8, are lifted to \(\mathop {\mathrm {\texttt {Lift}}}\limits (2, 3) = 3\) and \(\mathop {\mathrm {\texttt {Lift}}}\limits (2, 8) = 7\). Then, the maximum (as per the total order ) of the lifted successors is chosen as . Because , . Thus, \(\textsc {Post}[2]\) is deleted in \(\texttt {Inst}[7]\). \(\square \)
Example 24
Consider the \(\texttt {FM}\) program \(P_3\) from Example 9, whose graph is in Fig. 1c and nesting relation is in Example 13.
An optimal memory configuration defined by Eq. 6 is:
To compute , 5’s successors, 3 and 4, are lifted to \(\mathop {\mathrm {\texttt {Lift}}}\limits (5, 3) = 3\) and \(\mathop {\mathrm {\texttt {Lift}}}\limits (5, 4) = 4\). Then, the maximum (as per the total order ) of the lifted successors is chosen as . Because , , and \(\textsc {Post}[5]\) is deleted in \(\texttt {Inst}[3]\) instead of \(\texttt {Inst}[4]\). \(\square \)
Given and a map , we use to denote the memory configuration (, , , ). Similarly, means (, , , ), and so on. For a given \(\texttt {FM}\) program P, each map X that constitutes a memory configuration is valid for P iff is valid for every valid memory configuration . Also, X is optimal for P iff is optimal for an optimal memory configuration .
Theorem 4
is valid. That is, given an \(\texttt {FM}\) program P and a valid memory configuration , .
Proof
Our approach does not change the iteration order and only changes where the deallocations are performed. Therefore, it is sufficient to show that for all , \(\textsc {Post}[u]\) is available whenever \(\texttt {Inst}[v]\) is executed.
Suppose that this is false: there exists an edge that violates it. Let d be computed by our approach. Then, the execution trace of P has execution of \(\texttt {Inst}[v]\) after the deallocation of \(\textsc {Post}[u]\) in \(\texttt {Inst}[d]\), with no execution of \(\texttt {Inst}[u]\) in between.
Because is a total order, it is either or . It must be , because implies , which contradicts the definition of . Then, by definition of , it is either or . In both cases, the only way \(\texttt {Inst}[v]\) can be executed after \(\texttt {Inst}[d]\) is to have another head h whose \(\texttt{repeat}\) instruction includes both \(\texttt {Inst}[d]\) and \(\texttt {Inst}[v]\). That is, when and .
By definition of WTO and , it is either \(u \prec v\), or . It must be \(u \prec v\), because if , \(\texttt {Inst}[u]\) is part of \(\texttt {Inst}[v]\), making \(\texttt {Inst}[u]\) to be executed before reading \(\textsc {Post}[u]\) in \(\texttt {Inst}[v]\). Furthermore, it must be \(u \prec h\), because if \(h \preceq u\), \(\texttt {Inst}[u]\) is executed before \(\texttt {Inst}[v]\) in each iteration over \(\mathcal {C}(h)\). However, that implies , which combined with , contradicts the definition of . Therefore, no such edge can exist and the theorem is true. \(\square \)
Theorem 5
is optimal. That is, given an \(\texttt {FM}\) program P, memory footprint of is smaller than or equal to that of for all valid memory configuration .
Proof
For to be optimal, deallocation of \(\textsc {Post}\) values must be determined at earliest positions as possible with a valid memory configuration . That is, there should not exists \(u, b \in V\) such that if , \(b \ne d\), is valid, and \(\texttt {Inst}[b]\) deletes \(\textsc {Post}[u]\) earlier than \(\texttt {Inst}[d]\).
Suppose that this is false: such u, b exists. Let d be , computed by our approach. Then it must be for \(\texttt {Inst}[b]\) to be able to delete \(\textsc {Post}[u]\) earlier than \(\texttt {Inst}[d]\). Also, for all , it must be for \(\texttt {Inst}[v]\) to be executed before deleting \(\textsc {Post}[u]\) in \(\texttt {Inst}[b]\).
By definition of , for all . Also, by Theorem 3, . Hence, , making it either , or . If , by definition of \(\mathop {\mathrm {\texttt {Lift}}}\limits \), it must be . Therefore, it must be , which contradicts that . Alternative, if , there must exist \(v \in V\) such that and \(\mathop {\mathrm {\texttt {Lift}}}\limits (u, v) = d\). To satisfy , , and , it must be . However, this makes the analysis incorrect because when stabilization check fails for \(\mathcal {C}(d)\), \(\texttt {Inst}[v]\) gets executed again, attempting to read \(\textsc {Post}[u]\) that is already deleted by \(\texttt {Inst}[b]\). Therefore, no such u, b can exist, and the theorem is true. \(\square \)
3.2 Declarative specification of
implies that v is the earliest instruction at which the assertion check at \(u \in V_C\) can be executed so that the invariant passed to the assertion check function \(\varphi _u\) is the same as when using . Thus, guaranteeing the same check result \(\textsc {Ck}\).
Because an instruction can be executed multiple times in a loop, we cannot simply execute the assertion checks right after the instruction, as illustrated by the following example.
Example 25
Consider the \(\texttt {FM}\) program \(P_3\) from Example 9. Let \(V_C = \{4, 9\}\). A memory configuration with is not valid: \(\texttt {Inst}[4]\) is executed repeatedly as part of \(\texttt {Inst}[3]\), and the first value of \(\textsc {Pre}[4]\) may not be the final invariant. Consequently, executing \(\varphi _4(\textsc {Pre}[4])\) in \(\texttt {Inst}[4]\) may not give the same result as executing it in \(\texttt {Inst}[9]\) (). \(\square \)
In general, because we cannot know the number of iterations of the loop in a \(\texttt{repeat}\) instruction, we must wait for the convergence of the maximal component that contains the assertion check. After the maximal component converges, the \(\texttt {FM}\) program never visits the component again, making \(\textsc {Pre}\) values of the elements inside the component final. Only if the element is not in any component can its assertion check be executed right after its instruction.
Given a nesting relation for the graph , is defined as:
(7)
Because is a forest, is a chain. Hence, is well-defined.
Example 26
Consider the \(\texttt {FM}\) program \(P_1\) from Example 7, whose graph is in Fig. 1a and nesting relation is in Example 11. for all \(v \in V\). \(\square \)
Example 27
Consider the \(\texttt {FM}\) program \(P_2\) from Example 8, whose graph is in Fig. 1b and nesting relation is in Example 12. Suppose that \(V_C= \{5, 9\}\). and . \(\square \)
Example 28
Consider the \(\texttt {FM}\) program \(P_3\) from Example 9, whose graph is in Fig. 1c and nesting relation is in Example 13. If \(V_C= \{5, 9\}\), and . Also, if \(V_C= \{4, 9\}\), and . \(\square \)
Theorem 6
is valid. That is, given an \(\texttt {FM}\) program P and a valid memory configuration ,
Proof
Let . If v is a head, by definition of , \(\mathcal {C}(v)\) is the largest component that contains u. Therefore, once \(\mathcal {C}(v)\) is stabilized, \(\texttt {Inst}[u]\) can no longer be executed, and \(\textsc {Pre}[u]\) remains the same. If v is not a head, then \(v = u\). That is, there is no component that contains u. Therefore, \(\textsc {Pre}[u]\) remains the same after the execution of \(\texttt {Inst}[u]\). In both cases, the value passed to \(\textsc {Ck}[u]\) are the same as when using . \(\square \)
Theorem 7
is optimal. That is, given an \(\texttt {FM}\) program P, memory footprint of is smaller than or equal to that of for all valid memory configuration .
Proof
Because \(\textsc {Pre}\) value is deleted right after its corresponding assertions are checked, it is sufficient to show that assertion checks are placed at the earliest positions with .
Let . By definition of , . For some b to perform assertion checks of u earlier than v, it must satisfy . However, because one cannot know in advance when a component of v would stabilize and when \(\textsc {Pre}[u]\) would converge, the assertion checks of u cannot be performed in \(\texttt {Inst}[b]\). Therefore, our approach puts the assertion checks at the earliest positions, and it leads to the minimum memory footprint. \(\square \)
3.3 Declarative specification of
implies that \(\textsc {Post}[u]\) can be deallocated at v because it is recomputed and overwritten in the loop of a \(\texttt{repeat}\) instruction before a subsequent use of \(\textsc {Post}[u]\).
must be a subset of : only the instructions of the heads of components that contain v recompute \(\textsc {Post}[u]\). We can further rule out the instruction of the heads of components that contain , because deletes \(\textsc {Post}[u]\). We add back to when u is contained in , because deallocation by happens after the deallocation by .
Given a nesting relation for the graph , is defined as:
(8)
where as defined in Eq. 6, and is the ternary conditional choice operator.
Example 29
Consider the \(\texttt {FM}\) program \(P_1\) from Example 7, whose graph is in Fig. 1a, nesting relation is in Example 11, and is in Example 22. There are no \(\texttt{repeat}\) in this FM program, and for all \(u \in V\). \(\square \)
Example 30
Consider the \(\texttt {FM}\) program \(P_2\) from Example 8, whose graph is in Fig. 1b, nesting relation is in Example 12, and is in Example 23.
For 7, . Because , . Therefore, \(\textsc {Post}[7]\) is deleted in each iteration of the loop of \(\texttt {Inst}[7]\).
While \(\texttt {Inst}[9]\) reads \(\textsc {Post}[7]\) in the future, the particular values of \(\textsc {Post}[7]\) that are deleted by are not used in \(\texttt {Inst}[9]\). \(\square \)
Example 31
Consider the \(\texttt {FM}\) program \(P_3\) from Example 9, whose graph is in Fig. 1c, nesting relation is in Example 13, and is in Example 24.
For 5, . Because , = = \(\{5, 4, 3\}\). \(\square \)
Theorem 8
is valid. That is, given an \(\texttt {FM}\) program P and a valid memory configuration , .
Proof
Again, our approach does not change the iteration order and only changes where the deallocations are performed. Therefore, it is sufficient to show that for all , \(\textsc {Post}[u]\) is available whenever \(\texttt {Inst}[v]\) is executed.
Suppose that this is false: there exists an edge that violates it. Let \(d'\) be element in that causes this violation. Then, the execution trace of P has execution of \(\texttt {Inst}[v]\) after the deallocation of \(\textsc {Post}[u]\) in \(\texttt {Inst}[d']\), with no execution of \(\texttt {Inst}[u]\) in between. Because \(\textsc {Post}[u]\) is deleted inside the loop of \(\texttt {Inst}[d']\), \(\texttt {Inst}[v]\) must be nested in \(\texttt {Inst}[d']\) or be executed after \(\texttt {Inst}[d']\) to be affected. That is, it must be either or \(d' \prec v\). Also, because of how is computed, .
First consider the case . By definition of WTO and , it is either \(u \prec v\) or . In either case, \(\texttt {Inst}[u]\) gets executed before \(\texttt {Inst}[v]\) reads \(\textsc {Post}[u]\). Therefore, deallocation of \(\textsc {Post}[u]\) in \(\texttt {Inst}[d']\) cannot cause the violation.
Alternatively, consider \(d' \prec v\) and . Because , \(\textsc {Post}[u]\) is generated in each iteration over \(\mathcal {C}(d')\), and the last iteration does not delete \(\textsc {Post}[u]\). Therefore, \(\textsc {Post}[u]\) will be available when executing \(\texttt {Inst}[v]\). Therefore, such \(u, d'\) does not exists, and the theorem is true. \(\square \)
Theorem 9
is optimal. That is, given an \(\texttt {FM}\) program P, memory footprint of is smaller than or equal to that of for all valid memory configuration .
Proof
Because one cannot know when a component would stabilize in advance, the decision to delete intermediate \(\textsc {Post}[u]\) cannot be made earlier than the stabilization check of a component that contains u. Our approach makes such decisions in all relevant components that contains u.
If , . Because \(\textsc {Post}[u]\) is deleted in \(\texttt {Inst}[d]\), we do not have to consider components in . Alternatively, if , . Because \(\textsc {Post}[u]\) is deleted \(\texttt {Inst}[d]\), we do not have to consider components in . Therefore, is optimal. \(\square \)
3.4 Declarative specification of
implies that \(\textsc {Pre}[u]\) can be deallocated at v because it is recomputed and overwritten in the loop of a \(\texttt{repeat}\) instruction before a subsequent use of \(\textsc {Pre}[u]\).
must be a subset of : only the instructions of the heads of components that contain v recompute \(\textsc {Pre}[u]\). If \(\texttt {Inst}[u]\) is a \(\texttt{repeat}\) instruction, \(\textsc {Pre}[u]\) is required to perform widening. Therefore, u must not be contained in .
Example 32
Consider the \(\texttt {FM}\) program \(P_3\) from Example 9. Let \(V_C = \{4, 9\}\). A memory configuration with is not valid, because \(\texttt {Inst}[4]\) would read \(\bot \) as the value of \(\textsc {Post}[4]\) when performing widening. \(\square \)
Given a nesting relation for the graph , is defined as:
(9)
Example 33
Consider the \(\texttt {FM}\) program \(P_1\) from Example 7, whose graph is in Fig. 1a and nesting relation is in Example 11. for all \(u \in V\). \(\square \)
Example 34
Consider the \(\texttt {FM}\) program \(P_2\) from Example 8, whose graph is in Fig. 1b and nesting relation is in Example 12. Let \(V_C= \{5, 9\}\). and . Therefore, \(\textsc {Pre}[5]\) is deleted in each loop iteration of \(\texttt {Inst}[4]\). \(\square \)
Example 35
Consider the \(\texttt {FM}\) program \(P_3\) from Example 9, whose graph is in Fig. 1c and nesting relation is in Example 13. Let \(V_C= \{5, 9\}\). and . Therefore, \(\textsc {Pre}[5]\) is deleted in each loop iteration of \(\texttt {Inst}[4]\) and \(\texttt {Inst}[3]\). \(\square \)
Theorem 10
is valid. That is, given an \(\texttt {FM}\) program P and a valid memory configuration , .
Proof
\(\textsc {Pre}[u]\) is only used in assertion checks and to perform widening in \(\texttt {Inst}[u]\). Because u is removed from , the deletion does not affect widening.
For all , . Because \(\textsc {Pre}[u]\) is not deleted when \(\mathcal {C}(v)\) is stabilized, \(\textsc {Pre}[u]\) will be available when performing assertion checks in . Therefore, is valid. \(\square \)
Theorem 11
is optimal. That is, given an \(\texttt {FM}\) program P, memory footprint of is smaller than or equal to that of for all valid memory configuration .
Proof
Because one cannot know when a component would stabilize in advance, the decision to delete intermediate \(\textsc {Pre}[u]\) cannot be made earlier than the stabilization check of a component that contains u. Our approach makes such decisions in all components that contains u. Therefore, is optimal.
\(\square \)
Theorem 12
The memory configuration (, , , ) is optimal.
Proof
Theorems 4 and 5 prove that is valid and optimal, respectively. Theorems 6 and 7 prove that is valid and optimal, respectively. Theorems 8 and 9 prove that is valid and optimal, respectively. Finally, Theorems 10 and 11 prove that is valid and optimal, respectively. Therefore, (, , , ) is optimal. \(\square \)
4 Efficient algorithm to compute
Algorithm Generate\(\texttt {FM}\)Program (Algorithm 1) is an almost-linear time algorithm for computing an \(\texttt {FM}\) program P and optimal memory configuration for a given directed graph . Algorithm 1 adapts the bottom-up WTO construction algorithm presented in Kim et al. [10]. In particular, Algorithm 1 applies the \(\texttt{genProg}\) rules (Eq. 3) to generate the \(\texttt {FM}\) program from a WTO. Line 31 generates \(\texttt{exec}\) instructions for non-heads. Line 39 generates \(\texttt{repeat}\) instructions for heads, with their bodies ([ ]) generated on Line 35. Finally, instructions are merged on Line 48 to construct the final output P.
Algorithm Generate\(\texttt {FM}\)Program utilizes a disjoint-set data structure. Operation returns the representative of the set that contains v. In Line 5, the sets are initialized to be for all \(v \in V\). Operation on Line 43 merges the sets containing v and , and assigns to be the representative for the combined set.
is the lowest common ancestor of u, v in the depth-first forest D [19]. Cross and forward edges are initially removed from on Line 7, making the graph reducible. Restoring it on Line 9 when restores some reachability while keeping reducible.
Lines indicated by \(\star \) in Algorithm 1 compute . Lines 37, 41, and 50 compute . Due to the specific order in which the algorithm traverses G, is overwritten with greater values (as per the total order ) on these lines, making the final value to be the maximum among the successors. \(\mathop {\mathrm {\texttt {Lift}}}\limits \) is implicitly applied when restoring the edges in
: edge whose is replaced to on Line 9.
is computed using an auxiliary map and a relation . At the end of the algorithm, will be the maximum element (as per ) in . That is, , where . Once is computed by lines 38, 41, and 51, the transitive reduction of , , is used to find all elements of on Line 56. is computed on Line 43. Note that and . and are computed on Lines 53 and 54, respectively.
Example 36
Consider the graph \(G_3\) (Fig. 1c). Labels of vertices indicate a depth-first numbering (DFN) of \(G_3\). The graph edges are classified into tree, back, cross, and forward edges using the corresponding depth-first forest [20]. Cross and forward edges of \(G_3\), , are removed on Line 7. Because , the removed edge (2, 8) will be restored in Line 9 when . It is restored as (2, 7), because the disjoint set \(\{8\}\) would have already been merged with \(\{7\}\) on Line 43 when , making to be 7 when .
The for-loop on Line 8 visits nodes in V in a descending DFN: from 9 to 1. Calling on Line 10 generates , an \(\texttt {FM}\) instruction for . When , because the SCC whose entry is 9 is trivial, \(\texttt{exec}\ 9\) is generated in Line 32. When , the SCC whose entry is 3 is non-trivial, with the entries of its nested SCCs, . These entries are visited in a topological order (descending postDFN), 4, 6, and their instructions are connected on Line 35 to generate on Line 39. Visiting the nodes in a descending DFN guarantees the instruction of nested SCCs to be present, and removing the cross and forward edges ensures each SCC to have a single entry. Table 1 shows some relevant steps and values within
.
Finally, calling
on Line 11 connects the instructions of entries of outermost SCCs, which is detected by the boolean expression , in a topological order (descending postDFN) to generate the final \(\texttt {FM}\) program. For the given example, it visits the nodes in the order of 1, 2, 3, 7, and 9, correctly generating the \(\texttt {FM}\) program on Line 48.
Due to and , is set to 3 and then to 7 on Line 50. Due to and , is set to 4 and then to 3 in Line 41. is set to 3, as in Line 53. is set to 2 on Line 51, and is set to \(\{2\}\) on Line 56. is set to 4 and then to 3 on Line 41, making to be \(\{3, 4, 5\}\). Because , is set to \(\{3\}\) in Line 54. \(\square \)
Table 1
Relevant steps and values within Generate\(\texttt {FM}\)Program when applied to graph \(G_3\) of Example 36
Generate\(\texttt {FM}\)Program correctly computes , defined in Sect. 3.
Proof
We show that each map is constructed correctly.
: Let \(v'\) be the value of before overwritten in Line 50, 37, or 41. Descending post DFN ordering corresponds to a topological sorting of the nested SCCs. Therefore, in Line 50 and 37, \(v' \prec v\). Also, because for all \(v \in N_h\) in Line 41, . In any case, . Because essentially performs \(\mathop {\mathrm {\texttt {Lift}}}\limits (u,v)\) when restoring the edges, the final is the maximum of the lifted successors, and the map is correctly computed.
: The correctness follows from the correctness of . Because the components are constructed bottom-up, in Line 51 and Line 38 returns . Also, . Thus, is correctly computed.
: At the end of the algorithm is the head of maximal component that contains v, or v itself when v is outside of any components. Therefore, is correctly computed.
: Using the same reasoning as in , and because , is correctly computed.
\(\square \)
Theorem 14
Running time of Generate\(\texttt {FM}\)Program is almost-linear.
Proof
The base WTO-construction algorithm is almost-linear time [10]. The starred lines in Algorithm 1 visit each edge and vertex once. Therefore, time complexity still remains almost-linear time. \(\square \)
5 Implementation
We have implemented our approach in a tool called \(\textsc {Mikos}\), which extends NASA’s \(\text {IKOS}\) [4], a WTO-based abstract-interpreter for C/C++. \(\textsc {Mikos}\) inherits all abstract domains and widening-narrowing strategies from \(\text {IKOS}\). It includes the localized narrowing strategy [9] that intertwines the increasing and decreasing sequences.
Abstract domains in IKOS. \(\text {IKOS}\) uses the state-of-the-art implementations of abstract domains comparable to those used in industrial abstract interpreters such as Astrée [15, 21]. In particular, \(\text {IKOS}\) implements the interval abstract domain [1] using functional data-structures based on Patricia Trees [22] as well as a memory-efficient variable packing Difference Bound Matrix (DBM) relational abstract domain [14].
Interprocedural analysis in IKOS.\(\text {IKOS}\) implements context-sensitive interprocedural analysis by means of dynamic inlining, much like the semantic expansion of function bodies in Astrée [23, Section 5]: at a function call, formal and actual parameters are matched, the callee is analyzed, and the return value at the call site is updated after the callee returns; a function pointer is resolved to a set of callees and the results for each call are joined; \(\text {IKOS}\) returns top for a callee when a cycle is found in this dynamic call chain. To prevent running the entire interprocedural analysis again at the assertion checking phase, invariants at exits of the callees are additionally cached during the fixpoint computation.
Interprocedural extension ofMikos. Although the description of our iteration strategy focused on intraprocedural analysis, it can be extended to interprocedural analysis as follows. Suppose there is a call to function f1 from a basic block contained in component C. Any checks in this call to f1 must be deferred until we know that the component C has stabilized. Furthermore, if function f1 calls the function f2, then the checks in f2 must also be deferred until C converges. In general, checks corresponding to a function call f must be deferred until the maximal component containing the call is stabilized.
When the analysis of callee returns in \(\textsc {Mikos}\), only Pre values for the deferred checks remain. They are deallocated when the checks are performed or when the component containing the call is reiterated.
6 Experimental evaluation
The experiments in this section were designed to answer the following questions:
RQ0 [Accuracy] Does \(\textsc {Mikos}\) (Sect. 5) have the same analysis results as \(\text {IKOS}\)?
RQ1 [Memory footprint] How does the memory footprint of \(\textsc {Mikos}\) compare to that of IKOS?
RQ2 [Runtime] How does the runtime of \(\textsc {Mikos}\) compare to that of IKOS?
Experimental setup All experiments were run on Amazon EC2 r5.2xlarge instances (64 GiB memory, 8 vCPUs, 4 physical cores), which use Intel Xeon Platinum 8175 M processors. Processors have L1, L2, and L3 caches of sizes 1.5 MiB (data: 0.75 MiB, instruction: 0.75 MiB), 24 MiB, and 33 MiB, respectively. Linux kernel version 4.15.0-1051-aws was used, and gcc 7.4.0 was used to compile both \(\textsc {Mikos}\) and \(\text {IKOS}\). Dedicated EC2 instances and BenchExec [24] were used to improve reliability of the results. Time and space limits were set to an hour and 64 GB, respectively.
Benchmarks We evaluated \(\textsc {Mikos}\) on two tasks, Tasks T1 and T2, that represent different client applications of abstract interpretation, each using different benchmarks described in Sects. 6.1 and 6.2, respectively. In both tasks, we excluded benchmarks that did not complete in both\(\text {IKOS}\) and \(\textsc {Mikos}\) given the time and space budget. There were no benchmarks for which \(\text {IKOS}\) succeeded but \(\textsc {Mikos}\) failed to complete. Benchmarks for which \(\text {IKOS}\) took less than 5 seconds were also excluded. Measurements for benchmarks in Tasks T1 and T2 that took less than 5 seconds are summarized in Table 2.
Table 2
Measurements for benchmarks that took less than 5 s are summarized in the table below
\(<\!5\)s
Time (s)
Memory (MB)
Time diff (s)
Memory diff (MB)
Min
Max
Avg
Min
Max
Avg
Min
Max
Avg
Min
Max
Avg
T1
0.11
4.98
0.58
25
564
42
-0.61
+1.44
+0.08
-0.37
+490
+12
T2
0.06
4.98
1.07
9
218
46
-0.05
+1.33
+0.14
-0.43
+172
+18
Time diff shows the runtime of \(\text {IKOS}\) minus that of \(\textsc {Mikos}\) (positive means speedup in \(\textsc {Mikos}\)). Mem diff shows the memory footprint of \(\text {IKOS}\) minus that of \(\textsc {Mikos}\) (positive means memory reduction in \(\textsc {Mikos}\))
Metrics To answer RQ1, we define and use memory reduction ratio (MRR):
(10)
The smaller the MRR, the greater reduction in peak-memory usage in \(\textsc {Mikos}\). If MRR is less than 1, \(\textsc {Mikos}\) has smaller memory footprint than \(\text {IKOS}\).
For RQ2, we report the speedup, which is defined as below:
(11)
The larger the speedup, the greater reduction in runtime in \(\textsc {Mikos}\). If speedup is greater than 1, \(\textsc {Mikos}\) is faster than \(\text {IKOS}\).
RQ0: Accuracy ofMikos As a sanity check for our theoretical results, we experimentally validated Theorem 12 by comparing the analysis results reported by \(\text {IKOS}\) and \(\textsc {Mikos}\). \(\textsc {Mikos}\) used a valid memory configuration, reporting the same analysis results as \(\text {IKOS}\). Recall that Theorem 12 also proves that the fixpoint computation in \(\textsc {Mikos}\) is memory-optimal (i.e., it results in minimum memory footprint).
6.1 Task T1: verifying user-provided assertions
Fig. 3
Task T1. Log-log scatter plots of (a) memory footprint and (b) runtime of \(\text {IKOS}\) and \(\textsc {Mikos}\), with an hour timeout and 64 GB spaceout. Benchmarks that did not complete in \(\text {IKOS}\) are marked \(\times \). All \(\times \)s completed in \(\textsc {Mikos}\). Benchmarks below \(y = x\) required less memory or runtime in \(\textsc {Mikos}\)
Benchmarks For Task T1, we selected all 2928 benchmarks from DeviceDriversLinux64, ControlFlow, and Loops categories of SV-COMP 2019 [17]. These categories are well suited for numerical analysis, and have been used in recent works [10, 25, 26]. From these benchmarks, we removed 435 benchmarks that timed out in both \(\textsc {Mikos}\) and \(\text {IKOS}\), and 1709 benchmarks that took less than 5 s in \(\text {IKOS}\). That left us with 784 SV-COMP 2019 benchmarks.
Abstract domain Task T1 used the reduced product of Difference Bound Matrix (DBM) with variable packing [14] and congruence [18]. This domain is much richer and more expressive than the interval domain used in task T2.
Task Task T1 consists of using the results of interprocedural fixpoint computation to prove user-provided assertions in the SV-COMP benchmarks. Each benchmark typically has one assertion to prove.
Fig. 4
Histograms of MRR (Eq. 10) in task T1 for different ranges. a shows the distribution of benchmarks that used from \(52\) MB to \(642\) MB in \(\text {IKOS}\). They are the bottom 25% in terms of the memory footprint in \(\text {IKOS}\). The distribution significantly tended toward a smaller MRR in the upper range
RQ1: Memory footprint ofMikoscompared toIKOS Fig. 3a shows the measured memory footprints in a log-log scatter plot. For Task T1, the MRR (Eq. 10) ranged from 0.895 to 0.001. That is, the memory footprint decreased to 0.1% in the best case. For all benchmarks, \(\textsc {Mikos}\) had smaller memory footprint than \(\text {IKOS}\): MRR was less than 1 for all benchmarks, with all points below the \(y = x\) line in Fig. 3a. On average, \(\textsc {Mikos}\) required only 4.1% of the memory required by \(\text {IKOS}\), with an MRR 0.041 as the geometric mean.
As Fig. 3a shows, reduction in memory tended to be greater as the memory footprint in the baseline \(\text {IKOS}\) grew. For the top 25% benchmarks with largest memory footprint in \(\text {IKOS}\), the geometric mean of MRRs was 0.009. This trend is further confirmed by the histograms in Fig. 4. While a similar trend was observed in task T2, the trend was significantly stronger in task T1. Table 3 lists RQ1 results for specific benchmarks.
RQ2: Runtime ofMikoscompared toIKOS Fig. 3b shows the measured runtime in a log-log scatter plot. We measured both the speedup (Eq. 11) and the difference in the runtimes. For fair comparison, we excluded 29 benchmarks that did not complete in \(\text {IKOS}\). This left us with 755 SV-COMP 2019 benchmarks. Out of these 755 benchmarks, 740 benchmarks had speedup \(>1\). The speedup ranged from 0.87\(\times \) to 1.80\(\times \), with geometric mean of 1.29\(\times \). The difference in runtimes (runtime of \(\text {IKOS}\) − runtime of \(\textsc {Mikos}\)) ranged from \(-7.47~\text {s}\) to \(1160.04~\text {s}\), with arithmetic mean of \(96.90~\text {s}\). Table 4 lists RQ2 results for specific benchmarks.
Table 3
Task T1. A sample of the results for task T1 in Fig. 3a, excluding the non-completed benchmarks in \(\text {IKOS}\)
Benchmark
\(\text {IKOS}\)
\(\textsc {Mikos}\)
T (s)
MF (MB)
T (s)
MF (MB)
MRR
3.16-rc1/205_9a-net-rtl8187
1500
45,905
1314
56
0.001
4.2-rc1/43_2a-mmc-rtsx
786.5
26,909
594.8
42
0.002
4.2-rc1/43_2a-video-radeonfb
2494
56,752
1930
107
0.002
4.2-rc1/43_2a-net-skge
3523
47,392
3131
98
0.002
4.2-rc1/43_2a-usb-hcd
220.4
17,835
150.8
39
0.002
4.2-rc1/32_7a-target_core_mod
1316
60,417
1110
2967
0.049
challenges/3.14-alloc-libertas
2094
60,398
1620
626
0.010
4.2-rc1/43_2a-net-libertas
1634
59,902
1307
307
0.005
challenges/3.14-kernel-libertas
2059
59,826
1688
2713
0.045
3.16-rc1/43_2a-sound-cs46xx
3101
58,087
2498
193
0.003
The first 5 rows list benchmarks with the smallest memory reduction ratio (MRR)s. The latter 5 rows list benchmarks with the largest memory footprints. The smaller the MRR, the greater the reduction in memory footprint. T: time; MF: memory footprint
Table 4
Task T1. A sample of the results for task T1 in Fig. 3b
Benchmark
\(\text {IKOS}\)
\(\textsc {Mikos}\)
T (s)
MF (MB)
T (s)
MF (MB)
MRR
Speedup
challenges/3.8-usb-main11
42.63
541
48.92
122
0.225
0.87\(\times \)
challenges/3.8-usb-main0
54.31
3025
61.78
190
0.063
0.88\(\times \)
challenges/3.8-usb-main1
42.84
457
47.73
119
0.261
0.90\(\times \)
3.14/complex-kernel-tm6000
745.4
25,903
413.4
234
0.009
1.80\(\times \)
4.2-rc1/43_2a-scsi-st
214.6
20,817
119.6
547
0.026
1.79\(\times \)
3.14/kernel–rtl8723ae
111.9
154
62.48
115
0.746
1.79\(\times \)
The first 3 rows list benchmarks with lowest speedups. The latter 3 rows list benchmarks with highest speedups. T: time; MF: memory footprint
6.2 Task T2: proving absence of buffer overflows
Fig. 5
Task T2. Log-log scatter plots of (a) memory footprint and (b) runtime of \(\text {IKOS}\) and \(\textsc {Mikos}\), with an hour timeout and 64 GB spaceout. Benchmarks that did not complete in \(\text {IKOS}\) are marked \(\times \). All \(\times \)s completed in \(\textsc {Mikos}\). Benchmarks below \(y = x\) required less memory or runtime in \(\textsc {Mikos}\)
Benchmarks For Task T2, we selected all 1503 programs from the official Arch Linux core packages that are primarily written in C and whose LLVM bitcodes are obtainable by gllvm [27]. These include, but are not limited to, coreutils, dhcp, gnupg, inetutils, iproute, nmap, openssh, vim, etc. From these benchmarks, we removed 76 benchmarks that timed out and 8 benchmarks that spaced out in both \(\textsc {Mikos}\) and \(\text {IKOS}\). Also, 994 benchmarks that took less than 5 s in \(\text {IKOS}\) were removed. That left us with 426 open-source benchmarks.
Abstract domain Task T2 used the interval abstract domain [1]. Using a richer domain like DBM caused \(\text {IKOS}\) and \(\textsc {Mikos}\) to timeout on most benchmarks.
Task Task T2 consists of using the results of interprocedural fixpoint computation to prove the safety of buffer accesses. In this task, most program points had checks.
Table 5
Task T2. A sample of the results for task T2 in Fig. 5a, excluding the non-completed benchmarks in \(\text {IKOS}\)
Benchmark
\(\text {IKOS}\)
\(\textsc {Mikos}\)
T (s)
MF (MB)
T (s)
MF (MB)
MRR
lxsession\(-\)0.5.4/lxsession
146.1
5831
81.57
130
0.022
rox\(-\)2.11/ROX-Filer
362.3
9569
400.6
329
0.034
tor\(-\)0.3.5.8/tor-resolve
58.36
1930
53.10
70
0.036
openssh-8.0p1/ssh-keygen
1212
29,670
1170
1128
0.038
xsane\(-\)0.999/xsane
499.8
10,118
467.5
430
0.042
openssh-8.0p1/sftp
3036
45,903
3446
9137
0.199
metacity\(-\)3.30.1/metacity
2111
36,324
2363
6329
0.174
links\(-\)2.19/links
2512
29,761
2740
3930
0.132
openssh-8.0p1/ssh-keygen
1212
29,670
1170
1128
0.038
links\(-\)2.19/xlinks
2523
29,587
2760
3921
0.133
The first 5 rows list benchmarks with the smallest memory reduction ratio (MRR)s. The latter 5 rows list benchmarks with the largest memory footprints. The smaller the MRR, the greater the reduction in memory footprint. T: time; MF: memory footprint
Table 6
Task T2. A sample of the results for task T2 in Fig. 5b
Benchmark
\(\text {IKOS}\)
\(\textsc {Mikos}\)
T (s)
MF (MB)
T (s)
MF (MB)
MRR
Speedup
moserial\(-\)3.0.12/moserial
422.3
109
585.5
107
0.980
0.72\(\times \)
openssh-8.0p1/ssh-pkcs11-helper
82.70
674
94.61
613
0.910
0.87\(\times \)
openssh-8.0p1/sftp
3036
45,903
3446
9137
0.199
0.88\(\times \)
packeth\(-\)1.9/packETH
188.7
153
83.82
120
0.782
2.25\(\times \)
lxsession\(-\)0.5.4/lxsession
146.1
5831
81.57
130
0.022
1.79\(\times \)
xscreensaver\(-\)5.42/braid
6.48
203
4.87
36
0.179
1.33\(\times \)
The first 3 rows list benchmarks with lowest speedups. The latter 3 rows list benchmarks with highest speedups. T: time; MF: memory footprint
RQ1: Memory footprint ofMikoscompared to IKOS Fig. 5a shows the measured memory footprints in a log-log scatter plot. For Task T2, MRR (Eq. 10) ranged from 0.998 to 0.022. That is, the memory footprint decreased to 2.2% in the best case. For all benchmarks, \(\textsc {Mikos}\) had smaller memory footprint than \(\text {IKOS}\): MRR was less than 1 for all benchmarks, with all points below the \(y = x\) line in Fig. 5a. On average, \(\textsc {Mikos}\)’s memory footprint was less than half of that of \(\text {IKOS}\), with an MRR 0.437 as the geometric mean. Table 5 lists RQ1 results for specific benchmarks.
Fig. 6
Histograms of MRR (Eq. 10) in task T2 for different ranges. a shows the distribution of benchmarks that used from \(44\) MB to \(184\) MB in \(\text {IKOS}\). They are the bottom 25% in terms of the memory footprint in \(\text {IKOS}\). The distribution slightly tended toward a smaller MRR in the upper range
RQ2: Runtime ofMikoscompared to IKOS Fig. 5b shows the measured runtime in a log-log scatter plot. We measured both the speedup (Eq. 11) and the difference in the runtimes. For fair comparison, we excluded 1 benchmark that did not complete in \(\text {IKOS}\). This left us with 425 open-source benchmarks. Out of these 425 benchmarks, 331 benchmarks had speedup \(>1\). The speedup ranged from 0.88\(\times \) to 2.83\(\times \), with geometric mean of 1.08\(\times \). The difference in runtimes (runtime of \(\text {IKOS}\) − runtime of \(\textsc {Mikos}\)) ranged from \(-409.74~\text {s}\) to \(198.39~\text {s}\), with arithmetic mean of \(1.29~\text {s}\). Table 6 lists RQ2 results for specific benchmarks (Fig. 6).
7 Related work
Abstract interpretation has a long history of designing time and memory efficient algorithms for specific abstract domains, which exploit variable packing and clustering and sparse constraints [13, 16, 25, 26, 28‐31]. Often these techniques represent a trade-off between precision and performance of the analysis. Nonetheless, such techniques are orthogonal to the abstract-domain agnostic approach discussed in this paper. Approaches for improving precision via sophisticated widening and narrowing strategies [32‐34] are also orthogonal to our memory-efficient iteration strategy. \(\textsc {Mikos}\) inherits the interleaved widening-narrowing strategy implemented in the baseline \(\text {IKOS}\) abstract interpreter.
As noted in Sect. 1, Bourdoncle’s approach [3] is used in many industrial and academic abstract interpreters [4‐8]. Thus, improving memory efficiency of WTO-based exploration is of great applicability to real-world static analysis.
Generic fixpoint-computation approaches for improving running time of abstract interpretation have also been explored [10, 35, 36]. Kim et al. [10] present the notion of weak partial order (WPO), which generalizes the notion of WTO that is used in this paper. Kim et al. describe a parallel fixpoint algorithm that exploits maximal parallelism while computing the same fixpoint as the WTO-based algorithm. Reasoning about correctness of concurrent algorithms is complex; hence, we decided to investigate an optimal memory management scheme in the sequential setting first. However, we believe it would be possible to extend our WTO-based result to one that uses WPO.
The nesting relation described in Sect. 3 is closely related to the notion of Loop Nesting Forest [37, 38], as observed in Kim et al. [10]. The almost-linear time algorithm Generate\(\texttt {FM}\)Program is an adaptation of LNF construction algorithm by Ramalingam [37]. The \(\mathop {\mathrm {\texttt {Lift}}}\limits \) operation in Sect. 3 is similar to the outermost-loop-excluding (OLE) operator introduced by Rastello [39, Section 2.4.4].
Seidl et al. [40] present time and space improvements to a generic fixpoint solver, which is closest in spirit to the problem discussed in this paper. For improving space efficiency, their approach recomputes values during fixpoint computation, and does not prove optimality, unlike our approach. However, the setting discussed in their work is also more generic compared to ours; we assume a static dependency graph for the equation system.
Abstract interpreters such as Astrée [21] and CodeHawk [7] are implemented in OCaml, which provides a garbage collector. However, merely using a reference counting garbage collector will not reduce peak memory usage of fixpoint computation. For instance, the reference count of \(\textsc {Pre}[u]\) can be decreased to zero only after the final check/assert that uses \(\textsc {Pre}[u]\). If the checks are all conducted at the end of the analysis (as is currently done in prior tools), then using a reference counting garbage collector will not reduce peak memory usage. In contrast, our approach lifts the checks as early as possible enabling the analysis to free the abstract values as early as possible.
Symbolic approaches for applying abstract transformers during fixpoint computation [41‐47] allow the entire loop body to be encoded as a single formula. This might appear to obviate the need for \(\textsc {Pre}\) and \(\textsc {Post}\) values for individual basic blocks within the loop; by storing the \(\textsc {Pre}\) value only at the header, such a symbolic approach might appear to reduce the memory footprint. First, this scenario does not account for the fact that \(\textsc {Pre}\) values need to be computed and stored if basic blocks in the loop have checks. Note that if there are no checks within the loop body, then our approach would also only store the \(\textsc {Pre}\) value at the loop header. Second, such symbolic approaches only perform intraprocedural analysis [41]; additional abstract values would need to be stored depending on how function calls are handled in interprocedural analysis. Third, due to the use of SMT solvers in such symbolic approaches, the memory footprint might not necessarily reduce, but might increase if one takes into account the memory used by the SMT solver.
Sparse analysis [48, 49] and database-backed analysis [50] improve the memory cost of static analysis. For specific classes of static analysis such as the IFDS framework [51], there have been approaches for improving the time and memory efficiency [52‐55].
8 Conclusion
This paper presented an approach for memory-efficient abstract interpretation that is agnostic to the abstract domain used. Our approach is memory-optimal and produces the same result as Bourdoncle’s approach without sacrificing time efficiency. We extended the notion of iteration strategy to intelligently deallocate abstract values and perform assertion checks during fixpoint computation. We provided an almost-linear time algorithm that constructs this iteration strategy. We implemented our approach in a tool called \(\textsc {Mikos}\), which extended the abstract interpreter \(\text {IKOS}\). Despite the use of state-of-the-art implementation of abstract domains, \(\text {IKOS}\) had a large memory footprint on two analysis tasks. \(\textsc {Mikos}\) was shown to effectively reduce it. On average \(\textsc {Mikos}\) demonstrated a \(24.57\times \) and \(2.29\times \) reduction in peak-memory usage compared to \(\text {IKOS}\) when verifying user-provided assertions in SV-COMP 2019 benchmarks and performing interprocedural buffer-overflow analysis of open-source programs, respectively.
Open Access This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article’s Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article’s Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/.
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference record of the fourth ACM symposium on principles of programming languages, Los Angeles, California, USA, January 1977, pp 238–252. https://doi.org/10.1145/512950.512973
2.
Cousot P (2021) Principles of abstract interpretation, 1st edn. MIT Press, Cambridge, MA
3.
Bourdoncle F (1993) Efficient chaotic iteration strategies with widenings. In: Formal methods in programming and their applications, international conference, Akademgorodok, Novosibirsk, Russia, June 28–July 2, 1993, Proceedings, pp 128–141. https://doi.org/10.1007/BFb0039704
4.
Brat G, Navas JA, Shi N, Venet A (2014) IKOS: A framework for static analysis based on abstract interpretation. In: Software engineering and formal methods - 12th international conference, SEFM 2014, Grenoble, France, September 1–5, 2014. Proceedings, pp 271–277. https://doi.org/10.1007/978-3-319-10431-7_20
5.
Navas JA (2019) CRAB: CoRnucopia of ABstractions: a language-agnostic library for abstract interpretation. https://github.com/seahorn/crab
Calcagno C, Distefano D (2011) Infer: an automatic program verifier for memory safety of C programs. In: Bobaru MG, Havelund K, Holzmann GJ, Joshi R (eds) NASA formal methods - third international symposium, NFM 2011, Pasadena, CA, USA, April 18–20, 2011. Proceedings. Lecture Notes in Computer Science, vol. 6617, pp 459–465. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-20398-5_33
9.
Amato G, Scozzari F (2013) Localizing widening and narrowing. In: Static analysis - 20th international symposium, SAS 2013, Seattle, WA, USA, June 20–22, 2013. Proceedings, pp 25–42. https://doi.org/10.1007/978-3-642-38856-9_4
10.
Kim SK, Venet AJ, Thakur AV (2020) Deterministic parallel fixpoint computation. PACMPL 4(POPL), 14–11433. https://doi.org/10.1145/3371082
11.
Jeannet B, Miné A (2009) Apron: a library of numerical abstract domains for static analysis. In: Bouajjani A, Maler O (eds) Computer aided verification, 21st international conference, CAV 2009, Grenoble, France, June 26–July 2, 2009. Proceedings. Lecture Notes in Computer Science, vol. 5643, pp. 661–667. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02658-4_52
12.
Bagnara R, Hill PM, Zaffanella E (2008) The parma polyhedra library: toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci Comput Program 72(1–2):3–21. https://doi.org/10.1016/j.scico.2007.08.001MathSciNetCrossRef
13.
Singh G, Püschel M, Vechev MT (2017) Fast polyhedra abstract domain. In: Castagna G, Gordon AD (eds) Proceedings of the 44th ACM SIGPLAN symposium on principles of programming languages, POPL 2017, Paris, France, January 18–20, pp. 46–59. ACM, New York, NY, USA (2017). https://doi.org/10.1145/3009837.3009885
14.
Gange G, Navas JA, Schachte P, Søndergaard H, Stuckey PJ (2016) An abstract domain of uninterpreted functions. In: Verification, model checking, and abstract interpretation - 17th international conference, VMCAI 2016, St. Petersburg, FL, USA, January 17–19, 2016. Proceedings, pp. 85–103. https://doi.org/10.1007/978-3-662-49122-5_4
15.
Bertrane J, Cousot P, Cousot R, Feret J, Mauborgne L, Miné A, Rival X (2011) Static analysis by abstract interpretation of embedded critical software. ACM SIGSOFT Softw Eng Notes 36(1):1–8. https://doi.org/10.1145/1921532.1921553CrossRef
16.
Heo K, Oh H, Yang H (2016) Learning a variable-clustering strategy for octagon from labeled data generated by a static analysis. In: Rival X (ed.) Static analysis - 23rd international symposium, SAS 2016, Edinburgh, UK, September 8–10, 2016, Proceedings. Lecture Notes in Computer Science, vol. 9837, pp. 237–256. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-53413-7_12
17.
Beyer D (2019) Automatic verification of C and java programs: SV-COMP 2019. In: Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 6–11, 2019, Proceedings, Part III, pp. 133–155. https://doi.org/10.1007/978-3-030-17502-3_9
Cormen TH, Leiserson CE, Rivest RL, Stein C (2009) Introduction to algorithms, 3rd edn. MIT Press, Cambridge
21.
Blanchet B, Cousot P, Cousot R, Feret J, Mauborgne L, Miné A, Monniaux D, Rival X (2002) Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software. In: Mogensen T, Schmidt DA, Sudborough IH (eds) The essence of computation, complexity, analysis, transformation. Essays Dedicated to Neil D. Jones [on Occasion of His 60th Birthday]. Lecture Notes in Computer Science, vol. 2566, pp. 85–108. Springer, Berlin. https://doi.org/10.1007/3-540-36377-7_5
22.
Okasaki C, Gill A (1998) Fast mergeable integer maps. In: Workshop on ML, pp 77–86
23.
Cousot P, Cousot R, Feret J, Mauborgne L, Miné A, Monniaux D, Rival X (2005) The astreé analyzer. In: Sagiv S (ed) Programming languages and systems, 14th European symposium on programming,ESOP 2005, held as part of the joint European conferences on theory and practice of software, ETAPS 2005, Edinburgh, UK, April 4–8, 2005, Proceedings. Lecture Notes in Computer Science, vol. 3444, pp. 21–30. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-31987-0_3
Singh G, Püschel M, Vechev MT (2018) Fast numerical program analysis with reinforcement learning. In: Computer aided verification - 30th international conference, CAV 2018, held as part of the federated logic conference, FloC 2018, Oxford, UK, July 14–17, Proceedings, Part I, pp. 211–229 (2018). https://doi.org/10.1007/978-3-319-96145-3_12
26.
Singh G, Püschel M, Vechev MT (2018) A practical construction for decomposing numerical abstract domains. In: Proceedings of the ACM programming language 2(POPL), 55–15528. https://doi.org/10.1145/3158143
Singh G, Püschel M, Vechev MT (2015) Making numerical program analysis fast. In: Proceedings of the 36th ACM SIGPLAN conference on programming language design and implementation, Portland, OR, USA, June 15–17, 2015, pp 303–313. https://doi.org/10.1145/2737924.2738000
29.
Gange G, Navas JA, Schachte P, Søndergaard H, Stuckey PJ (2016) Exploiting sparsity in difference-bound matrices. In: Rival X (ed) Static analysis - 23rd international symposium, SAS 2016, Edinburgh, UK, September 8–10, 2016, Proceedings. Lecture Notes in Computer Science, vol. 9837, pp. 189–211. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-53413-7_10
30.
Chawdhary A, King A (2017) Compact difference bound matrices. In: Chang BE (ed) Programming languages and systems - 15th Asian symposium, APLAS 2017, Suzhou, China, November 27–29, 2017, Proceedings. Lecture Notes in Computer Science, vol. 10695, pp. 471–490. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-319-71237-6_23
Halbwachs N, Henry J (2012) When the decreasing sequence fails. In: Static analysis - 19th international symposium, SAS 2012, Deauville, France, September 11–13, 2012. Proceedings, pp 198–213. https://doi.org/10.1007/978-3-642-33125-1_15
Apinis K, Seidl H, Vojdani V (2016) Enhancing top-down solving with widening and narrowing. In: Probst CW, Hankin C, Hansen RR (eds) Semantics, logics, and calculi - essays dedicated to hanne riis nielson and flemming nielson on the occasion of their 60th birthdays. Lecture Notes in Computer Science, vol. 9560, pp 272–288. Springer, Berlin. https://doi.org/10.1007/978-3-319-27810-0_14
35.
Venet A, Brat GP (2004) Precise and efficient static array bound checking for large embedded C programs. In: Proceedings of the ACM SIGPLAN 2004 conference on programming language design and implementation 2004, Washington, DC, USA, June 9–11, 2004, pp. 231–242. https://doi.org/10.1145/996841.996869
36.
Monniaux D (2005) The parallel implementation of the astrée static analyzer. In: Programming languages and systems, third Asian symposium, APLAS 2005, Tsukuba, Japan, November 2–5, 2005, Proceedings, pp 86–96. https://doi.org/10.1007/11575467_7
Rastello F (2012) On sparse intermediate representations: some structural properties and applications to just-in-time compilation. University works, Inria Grenoble Rhône-Alpes (December). Habilitation à diriger des recherches, École normale supérieure de Lyon. https://hal.inria.fr/hal-00761555
40.
Seidl H, Vogler R (2018) Three improvements to the top-down solver. In: Sabel D, Thiemann P (eds) Proceedings of the 20th international symposium on principles and practice of declarative programming, PPDP 2018, Frankfurt Am Main, Germany, September 03-05, pp. 21–12114. ACM, New York, NY, USA (2018). https://doi.org/10.1145/3236950.3236967
Reps TW, Sagiv S, Yorsh G (2004) Symbolic implementation of the best transformer. In: Steffen B, Levi G (eds) Verification, model checking, and abstract interpretation, 5th international conference, VMCAI 2004, Venice, Italy, January 11–13, 2004, Proceedings. Lecture Notes in Computer Science, vol. 2937, pp. 252–266. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24622-0_21
43.
Li Y, Albarghouthi A, Kincaid Z, Gurfinkel A, Chechik M (2014) Symbolic optimization with SMT solvers. In: Jagannathan S, Sewell P (eds) The 41st annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’14, San Diego, CA, USA, January 20–21, 2014, pp 607–618. ACM, New York, NY, USA. https://doi.org/10.1145/2535838.2535857
44.
Reps TW, Thakur AV (2016) Automating abstract interpretation. In: Jobstmann B, Leino KRM (eds) Verification, model checking, and abstract interpretation - 17th international conference, VMCAI 2016, St. Petersburg, FL, USA, January 17–19, 2016. Proceedings. Lecture Notes in Computer Science, vol. 9583, pp. 3–40. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-49122-5_1
Thakur AV, Elder M, Reps TW (2012) Bilateral algorithms for symbolic abstraction. In: Miné A, Schmidt D (eds) Static analysis - 19th international symposium, SAS 2012, Deauville, France, September 11–13, 2012. Proceedings. Lecture Notes in Computer Science, vol 7460, pp 111–128. Springer, Berlin. https://doi.org/10.1007/978-3-642-33125-1_10
47.
Thakur AV, Reps TW (2012) A method for symbolic computation of abstract operations. In: Madhusudan P, Seshia SA (eds) Computer aided verification - 24th international conference, CAV 2012, Berkeley, CA, USA, July 7–13, 2012 Proceedings. Lecture Notes in Computer Science, vol. 7358, pp 174–192. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31424-7_17
48.
Oh H, Heo K, Lee W, Lee W, Yi K (2012) Design and implementation of sparse global analyses for c-like languages. In: ACM SIGPLAN conference on programming language design and implementation, PLDI ’12, Beijing, China - June 11–16, 2012, pp 229–238. https://doi.org/10.1145/2254064.2254092
49.
Oh H, Heo K, Lee W, Lee W, Park D, Kang J, Yi K (2014) Global sparse analysis framework. ACM Trans Program Lang Syst 36(3):8–1844. https://doi.org/10.1145/2590811CrossRef
50.
Weiss C, Rubio-González C, Liblit B (2015) Database-backed program analysis for scalable error propagation. In: 37th IEEE/ACM international conference on software engineering, ICSE 2015, Florence, Italy, May 16–24, 2015, Volume 1, pp 586–597. https://doi.org/10.1109/ICSE.2015.75
51.
Reps TW, Horwitz S, Sagiv M (1995) Precise interprocedural dataflow analysis via graph reachability. In: Conference record of POPL’95: 22nd ACM SIGPLAN-SIGACT symposium on principles of programming languages, San Francisco, California, USA, January 23–25, 1995, pp. 49–61. https://doi.org/10.1145/199448.199462
52.
Bodden E (2012) Inter-procedural data-flow analysis with IFDS/IDE and soot. In: Bodden E, Hendren LJ, Lam P, Sherman E (eds.) Proceedings of the ACM SIGPLAN international workshop on state of the art in java program analysis, SOAP 2012, Beijing, China, June 14, 2012, pp. 3–8. ACM, New York, NY, USA. https://doi.org/10.1145/2259051.2259052
53.
Naeem NA, Lhoták O, Rodriguez J (2010) Practical extensions to the IFDS algorithm. In: Gupta R (ed) Compiler construction, 19th international conference, CC 2010, held as part of the joint European conferences on theory and practice of software, ETAPS 2010, Paphos, Cyprus, March 20–28, 2010. Proceedings. Lecture Notes in Computer Science, vol. 6011, pp. 124–144. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-11970-5_8
54.
Wang K, Hussain A, Zuo Z, Xu GH, Sani AA (2017) Graspan: A single-machine disk-based graph system for interprocedural static analyses of large-scale systems code. In: Proceedings of the twenty-second international conference on architectural support for programming languages and operating systems, ASPLOS 2017, Xi’an, China, April 8–12, 2017, pp. 389–404. https://doi.org/10.1145/3037697.3037744
55.
Zuo Z, Gu R, Jiang X, Wang Z, Huang Y, Wang L, Li X (2019) Bigspa: An efficient interprocedural static analysis engine in the cloud. In: 2019 IEEE international parallel and distributed processing symposium, IPDPS 2019, Rio de Janeiro, Brazil, May 20–24, 2019, pp. 771–780. https://doi.org/10.1109/IPDPS.2019.00086
in Fig. 1c. Current approaches (Sect. 2.1) allocate abstract values for each program point during fixpoint computation, check the assertions at 4 and 9 after fixpoint computation, and then deallocate all abstract values. In contrast, our approach deallocates abstract values and checks the assertions during fixpoint computation while guaranteeing that the results of the checks remain the same and that the peak-memory usage is optimal.
. The graph G typically reflects the control-flow graph of the program, though this is not always true. The aim is to find the fixpoint of the equation system \(\Phi \):
The maps \(\textsc {Pre}:V \rightarrow \mathcal {A}\) and \(\textsc {Post}:V \rightarrow \mathcal {A}\) maintain the abstract values at the beginning and end of each program point, where \(\mathcal {A}\) is an abstract domain. The abstract transformer \(\tau _v :\mathcal {A}\rightarrow \mathcal {A}\) overapproximates the semantics of program point \(v \in V\). After fixpoint computation, \(\textsc {Pre}[v]\) is an invariant for \(v \in V\).
Informally, the instruction \(\texttt{exec}\ v\) applies \(\tau _v\) for \(v \in V\); the instruction \(\texttt{repeat}\ v\ \texttt {[}P_1 \texttt {]} \) repeatedly executes the \(\texttt {FM}\) program \(P_1\) until convergence and performs widening at v; and the instruction
executes \(\texttt {FM}\) programs \(P_1\) and \(P_2\) in sequence.
. A WTO is defined using the notion of a hierarchical total ordering (HTO) of a set.
can now be defined using the notion of an HTO.
is an HTO \(\mathcal {H}(V, \preceq , \omega )\) such that for every edge \(u \rightarrow v\), either (i) \(u \prec v\), or (ii) \(v \preceq u\) and \(v \in \omega (u)\). \(\square \)
that represents the dependency graph of the equation system, Bourdoncle’s approach uses a WTO \(\mathcal {W}(V, \preceq , \omega )\) of G to derive the following recursive iteration strategy:We now show how the WTO can be represented using the syntax of our Fixpoint Machine (\(\texttt {FM}\)) defined in Eq. 2. The following function \(\texttt{genProg}:\text {WTO} \rightarrow Prog \) maps a given WTO \(\mathcal {W}\) to an \(\texttt {FM}\) program:
Each node \(v \in V\) is mapped to a single \(\texttt {FM}\) instruction by \(\texttt{genProg}\); we use \(\texttt {Inst}[v]\) to refer to this \(\texttt {FM}\) instruction corresponding to v. Note that if \(v\in V\) is a head, then \(\texttt {Inst}[v]\) is an instruction of the form \(\texttt{repeat}\ v\ \texttt {[}\ldots \texttt {]}\), else \(\texttt {Inst}[v]\) is \(\texttt{exec}\ v\).
. Note that \(\texttt {Inst}[v] = \texttt{exec}\ v\) for all \(v \in [1, 9]\). \(\square \)
. The corresponding \(\texttt {FM}\) program is
.
. \(\square \)
. The corresponding \(\texttt {FM}\) program is
. \(\square \)
and a WTO \(\mathcal {W}(V, \preceq , \omega )\).
text in Fig. 2 shows the semantics of the \(\texttt {FM}\) instructions that handle these issues. The right-hand side of \(\Rightarrow \) is executed if the left-hand side evaluates to true. Recall that the set \(V_C \subseteq V\) is the set of program points that have assertion checks. The map \(\textsc {Ck}:V_C \rightarrow \texttt {bool}\) records the result of executing the check \(\varphi _u(\textsc {Pre}[u])\) for each \(u \in V_C\). Thus, the output of the \(\texttt {FM}\) program is the map \(\textsc {Ck}\). In practice, the functions \(\varphi _u\) are expensive to compute. Furthermore, they often write the result to a database or report the output to a user. Consequently, we assume that only the first execution of \(\varphi _u\) is recorded in \(\textsc {Ck}\).
is a tuple
whereTo simplify presentation, the semantics in Fig. 2 does not make explicit the allocations of abstract values: if a \(\textsc {Post}\) or \(\textsc {Pre}\) value that has been deallocated is accessed, then it is allocated and initialized to \(\bot \).
controls the deallocation of values in \(\textsc {Post}\) that have no further use. If
, \(\textsc {Post}[u]\) is deallocated after the execution of \(\texttt {Inst}[v]\).
controls when the check function \(\varphi _u\) corresponding to \(u \in V_C\) is executed, after which the corresponding \(\textsc {Pre}\) value is deallocated. If
, assertions in u are checked and \(\textsc {Pre}[u]\) is subsequently deallocated after the execution of \(\texttt {Inst}[v]\).
control deallocation of \(\textsc {Post}\) values that are recomputed and overwritten in the loop of a \(\texttt{repeat}\) instruction before its next use. If
, \(\textsc {Post}[u]\) is deallocated in the loop of \(\texttt {Inst}[v]\).
control deallocation of \(\textsc {Pre}\) values that are recomputed and overwritten in the loop of a \(\texttt{repeat}\) instruction before its next use. If
, \(\textsc {Pre}[u]\) is deallocated in the loop of \(\texttt {Inst}[v]\).
is equivalent to
, denoted by
, iff for all \(u \in V_C\), we have \(\textsc {Ck}_1[u] = \textsc {Ck}_2[u]\), where \(\textsc {Ck}_1\) and \(\textsc {Ck}_2\) are the check maps corresponding to execution of P using
and
, respectively. \(\square \)
performs checks and deallocations at the end of the \(\texttt {FM}\) program after fixpoint has been computed.
is
for all \(v \in V\),
for all \(c \in V_C\), and
, where z is the last instruction in P. \(\square \)
for all \(v \in V\). That is, all \(\textsc {Post}\) values are deallocated at the end of the fixpoint computation. Also,
, meaning that assertion checks also happen at the end.
, so the \(\texttt {FM}\) programs do not clear abstract values whose values will be recomputed and overwritten in a loop of \(\texttt{repeat}\) instruction. \(\square \)
is valid for P iff it is equivalent to the default configuration; i.e.,
.
is optimal for a given \(\texttt {FM}\) program iff the memory footprint of
is smaller than or equal to that of
for all valid memory configuration
. The problem addressed in this paper can be stated as:
(
,
,
,
). Section 4 presents an efficient algorithm for computing
.
, the nesting relation \(\textsf {N}\) is a tuple
where
iff \(u = v\) or \(v \in \omega (u)\) for \(u, v \in V\). \(\square \)
; that is,
equals the set containing v and the heads of components in the WTO that contains v. The nesting relation
is a forest; i.e. a partial order such that for all \(v\in V\),
is a chain, as proven below.
is a forest.
is a partial order. Let x, y, z be vertices in V.Next, we show that the partial order is a forest. Suppose there exists \(v \in V\) such that
is not a chain. That is, there exists
such that
and
. Then, by definition of HTO, \(\mathcal {C}(x) \cap \mathcal {C}(y) = \emptyset \). However, this leads to a contradiction because \(v \in \mathcal {C}(x)\) and \(v \in \mathcal {C}(y)\). Thus,
is a chain. \(\square \)
. This is true by the definition of
.
and
implies
. (i) If \(x = y\),
. (ii) Otherwise, by definition of
, \(y \in \omega (x)\). Furthermore, (ii-1) if \(y = z\), \(z \in \omega (x)\); and hence,
. (ii-2) Otherwise, \(z \in \omega (y)\), and by definition of HTO, \(z \in \omega (x)\).
and
implies \(x = y\). Suppose \(x \ne y\). By definition of
and premises, \(y \in \omega (x)\) and \(x \in \omega (y)\). Then, by definition of HTO, \(x \prec y\) and \(y \prec x\). This contradicts that \(\preceq \) is a total order.
is: 
. \(\square \)
is: 
, forming a chain
. \(\square \)
implies that v is the earliest instruction at which \(\textsc {Post}[u]\) can be deallocated while ensuring that there are no subsequents reads of \(\textsc {Post}[u]\) during fixpoint computation. We cannot conclude
from a dependency
as illustrated in the following example.
is in Fig. 1c. Although there is a dependency
, memory configuration with
is not valid: \(\textsc {Post}[2]\) is read by \(\texttt {Inst}[8]\), which is executed repeatedly as part of \(\texttt {Inst}[7]\); if
, then \(\textsc {Post}[2]\) would be deallocated the first time \(\texttt {Inst}[8]\) is executed, and subsequent executions of \(\texttt {Inst}[8]\) will read \(\bot \) as the value of \(\textsc {Post}[2]\), which would be incorrect. \(\square \)
, we must find the head of maximal component that contains v but not u as the candidate for
. By choosing the head of maximal component, we remove the possibility of having a larger component whose head’s \(\texttt{repeat}\) instruction can execute \(\texttt {Inst}[v]\) after deallocating \(\textsc {Post}[u]\). If there is no component that contains v but not u, we simply use v as the candidate. The following \(\mathop {\mathrm {\texttt {Lift}}}\limits \) operator gives us the candidate of
for
:
gives us v and the heads of components that contain v. Subtracting
removes the heads of components that also contain u. We put back v to account for the case when there is no component containing v but not u and
is empty. Because
is a forest,
and
are chains, and hence,
is also a chain. Therefore, maximum is well-defined.
from Example 11. For all
, \(\mathop {\mathrm {\texttt {Lift}}}\limits (u, v) = v\). Note that there are no components in \(\mathcal {W}_1\). \(\square \)
from Example 12. \(\mathop {\mathrm {\texttt {Lift}}}\limits (2, 8)\)
. We see that 7 is the head of the maximal component containing 8 but not 2. Also,
. There is no component that contains 5 but not 4. Similarly,
. There is no component that contains 4 but not 5. \(\square \)
from Example 13. \(\mathop {\mathrm {\texttt {Lift}}}\limits (6, 3)\)
. There is no component that contains 3 but not 6. Also,
. There is no component that contains 3 but not 5. \(\square \)
, an incorrect variant of
that uses the total order \(\preceq \). Consider the \(\texttt {FM}\) program \(P_3\) from Example 9, whose graph
is in Fig. 1c and nesting relation
is in Example 13. \(\textsc {Post}[5]\) has dependencies
and
. \(\mathop {\mathrm {\texttt {Lift}}}\limits (5, 4) = 4\), \(\mathop {\mathrm {\texttt {Lift}}}\limits (5, 3) = 3\). Now,
because \(3 \preceq 4\). However, a memory configuration with
is not valid: \(\texttt {Inst}[4]\) is nested in \(\texttt {Inst}[3]\). Due to the deletion of \(\textsc {Post}[5]\) in \(\texttt {Inst}[4]\), \(\texttt {Inst}[3]\) will read \(\bot \) as the value of \(\textsc {Post}[5]\). \(\square \)
, using the total order \((V, \preceq )\) and the nesting relation
:
In the definition of
, the nesting relation
takes precedence over \(\preceq \).
is a total order.
is a total order.
or
. This follows from the connexity of the total order \(\preceq \).
and
implies
. (i) Suppose
. (i-1) If
, by transitivity of
,
. (ii-2) Otherwise,
and \(y \preceq z\). It cannot be
because transitivity of
implies
, which is a contradiction. Furthermore, it cannot be \(z \prec x\) because \(y \preceq z \prec x\) and
implies \(y \in \omega (z)\) by the definition of HTO. By connexity of \(\preceq \), \(x \preceq z\). (ii) Otherwise
and \(x \preceq y\). (ii-1) If
,
because, otherwise, transitivity of
will imply
. By connexity of \(\preceq \), it is either \(x \preceq z\) or \(z \prec x\). If \(x \preceq z\),
. If \(z \prec x\), by definition of HTO, \(z \in \omega (z)\).
and
implies \(x = y\). (i) If
, it should be
for
to be true. By anti-symmetry of
, \(x = y\). (ii) Otherwise,
and \(x \preceq y\). For
to be true,
and \(x \preceq y\). By anti-symmetry of \(\preceq \), \(x = y\).\(\square \)
moves the heads in the WTO to their corresponding closing parentheses ‘)’. In terms of the execution order and the order in which \(\textsc {Post}\) values are accessed, the total order
has the following meaning.
.
and
for \(\texttt {Inst}[v]\) to read \(\textsc {Post}[u]\). By the definition of WTO, it is either \(u \prec v'\) and \(v' \notin \omega (u)\), or \(v' \preceq u\) and \(v' \in \omega (u)\). In both cases,
. Because
, and hence
,
. \(\square \)
. That is,
. \(\square \)
. Note that \(4 \preceq 5\) while
. Postamble of \(\texttt{repeat}\ 4\ \texttt {[}\ldots \texttt {]}\) is executed after \(\texttt {Inst}[5]\), while preamble of \(\texttt{repeat}\ 4\ \texttt {[}\ldots \texttt {]}\) is executed before \(\texttt {Inst}[5]\). Similarly, \(7 \preceq 8\) while
. \(\square \)
. Note that \(3 \preceq 5\) while
. Postamble of \(\texttt{repeat}\ 3\ \texttt {[}\ldots \texttt {]}\) is executed after \(\texttt {Inst}[5]\), while preamble of \(\texttt{repeat}\ 3\ \texttt {[}\ldots \texttt {]}\) is executed before \(\texttt {Inst}[5]\). \(\square \)
. Given a nesting relation
for the graph
,
is defined as:
is in Fig. 1a and nesting relation
is in Example 11. An optimal memory configuration
defined by Eq. 6 is:
\(\mathop {\mathrm {\texttt {Lift}}}\limits (u, v) = v\) for all
and
for this case. Therefore, only \((V, \preceq )\) plays a role in determining
. \(\square \)
is in Fig. 1b and nesting relation
is in Example 12. An optimal memory configuration
defined by Eq. 6 is:
Successors of u are first lifted to compute
. For example, to compute
, 2’s successors, 3 and 8, are lifted to \(\mathop {\mathrm {\texttt {Lift}}}\limits (2, 3) = 3\) and \(\mathop {\mathrm {\texttt {Lift}}}\limits (2, 8) = 7\). Then, the maximum (as per the total order
) of the lifted successors is chosen as
. Because
,
. Thus, \(\textsc {Post}[2]\) is deleted in \(\texttt {Inst}[7]\). \(\square \)
is in Fig. 1c and nesting relation
is in Example 13.
defined by Eq. 6 is:
To compute
, 5’s successors, 3 and 4, are lifted to \(\mathop {\mathrm {\texttt {Lift}}}\limits (5, 3) = 3\) and \(\mathop {\mathrm {\texttt {Lift}}}\limits (5, 4) = 4\). Then, the maximum (as per the total order
) of the lifted successors is chosen as
. Because
,
, and \(\textsc {Post}[5]\) is deleted in \(\texttt {Inst}[3]\) instead of \(\texttt {Inst}[4]\). \(\square \)
and a map
, we use
to denote the memory configuration (
,
,
,
). Similarly,
means (
,
,
,
), and so on. For a given \(\texttt {FM}\) program P, each map X that constitutes a memory configuration is valid for P iff
is valid for every valid memory configuration
. Also, X is optimal for P iff
is optimal for an optimal memory configuration
.
is valid. That is, given an \(\texttt {FM}\) program P and a valid memory configuration
,
.
, \(\textsc {Post}[u]\) is available whenever \(\texttt {Inst}[v]\) is executed.
that violates it. Let d be
computed by our approach. Then, the execution trace of P has execution of \(\texttt {Inst}[v]\) after the deallocation of \(\textsc {Post}[u]\) in \(\texttt {Inst}[d]\), with no execution of \(\texttt {Inst}[u]\) in between.
is a total order, it is either
or
. It must be
, because
implies
, which contradicts the definition of
. Then, by definition of
, it is either
or
. In both cases, the only way \(\texttt {Inst}[v]\) can be executed after \(\texttt {Inst}[d]\) is to have another head h whose \(\texttt{repeat}\) instruction includes both \(\texttt {Inst}[d]\) and \(\texttt {Inst}[v]\). That is, when
and
.
, it is either \(u \prec v\), or
. It must be \(u \prec v\), because if
, \(\texttt {Inst}[u]\) is part of \(\texttt {Inst}[v]\), making \(\texttt {Inst}[u]\) to be executed before reading \(\textsc {Post}[u]\) in \(\texttt {Inst}[v]\). Furthermore, it must be \(u \prec h\), because if \(h \preceq u\), \(\texttt {Inst}[u]\) is executed before \(\texttt {Inst}[v]\) in each iteration over \(\mathcal {C}(h)\). However, that implies
, which combined with
, contradicts the definition of
. Therefore, no such edge
can exist and the theorem is true. \(\square \)
is optimal. That is, given an \(\texttt {FM}\) program P, memory footprint of
is smaller than or equal to that of
for all valid memory configuration
.
to be optimal, deallocation of \(\textsc {Post}\) values must be determined at earliest positions as possible with a valid memory configuration
. That is, there should not exists \(u, b \in V\) such that if
, \(b \ne d\),
is valid, and \(\texttt {Inst}[b]\) deletes \(\textsc {Post}[u]\) earlier than \(\texttt {Inst}[d]\).
, computed by our approach. Then it must be
for \(\texttt {Inst}[b]\) to be able to delete \(\textsc {Post}[u]\) earlier than \(\texttt {Inst}[d]\). Also, for all
, it must be
for \(\texttt {Inst}[v]\) to be executed before deleting \(\textsc {Post}[u]\) in \(\texttt {Inst}[b]\).
,
for all
. Also, by Theorem 3,
. Hence,
, making it either
, or
. If
, by definition of \(\mathop {\mathrm {\texttt {Lift}}}\limits \), it must be
. Therefore, it must be
, which contradicts that
. Alternative, if
, there must exist \(v \in V\) such that
and \(\mathop {\mathrm {\texttt {Lift}}}\limits (u, v) = d\). To satisfy
,
, and
, it must be
. However, this makes the analysis incorrect because when stabilization check fails for \(\mathcal {C}(d)\), \(\texttt {Inst}[v]\) gets executed again, attempting to read \(\textsc {Post}[u]\) that is already deleted by \(\texttt {Inst}[b]\). Therefore, no such u, b can exist, and the theorem is true. \(\square \)
implies that v is the earliest instruction at which the assertion check at \(u \in V_C\) can be executed so that the invariant passed to the assertion check function \(\varphi _u\) is the same as when using
. Thus, guaranteeing the same check result \(\textsc {Ck}\).
is not valid: \(\texttt {Inst}[4]\) is executed repeatedly as part of \(\texttt {Inst}[3]\), and the first value of \(\textsc {Pre}[4]\) may not be the final invariant. Consequently, executing \(\varphi _4(\textsc {Pre}[4])\) in \(\texttt {Inst}[4]\) may not give the same result as executing it in \(\texttt {Inst}[9]\) (
). \(\square \)
for the graph
,
is defined as:
Because
is a forest,
is a chain. Hence,
is well-defined.
is valid. That is, given an \(\texttt {FM}\) program P and a valid memory configuration
,
. If v is a head, by definition of
, \(\mathcal {C}(v)\) is the largest component that contains u. Therefore, once \(\mathcal {C}(v)\) is stabilized, \(\texttt {Inst}[u]\) can no longer be executed, and \(\textsc {Pre}[u]\) remains the same. If v is not a head, then \(v = u\). That is, there is no component that contains u. Therefore, \(\textsc {Pre}[u]\) remains the same after the execution of \(\texttt {Inst}[u]\). In both cases, the value passed to \(\textsc {Ck}[u]\) are the same as when using
. \(\square \)
is optimal. That is, given an \(\texttt {FM}\) program P, memory footprint of
is smaller than or equal to that of
for all valid memory configuration
.
.
. By definition of
,
. For some b to perform assertion checks of u earlier than v, it must satisfy
. However, because one cannot know in advance when a component of v would stabilize and when \(\textsc {Pre}[u]\) would converge, the assertion checks of u cannot be performed in \(\texttt {Inst}[b]\). Therefore, our approach puts the assertion checks at the earliest positions, and it leads to the minimum memory footprint. \(\square \)
implies that \(\textsc {Post}[u]\) can be deallocated at v because it is recomputed and overwritten in the loop of a \(\texttt{repeat}\) instruction before a subsequent use of \(\textsc {Post}[u]\).
must be a subset of
: only the instructions of the heads of components that contain v recompute \(\textsc {Post}[u]\). We can further rule out the instruction of the heads of components that contain
, because
deletes \(\textsc {Post}[u]\). We add back
to
when u is contained in
, because deallocation by
happens after the deallocation by
.
for the graph
,
is defined as:
where
as defined in Eq. 6, and
is the ternary conditional choice operator.
is in Fig. 1b, nesting relation
is in Example 12, and
is in Example 23.
For 7,
. Because
,
. Therefore, \(\textsc {Post}[7]\) is deleted in each iteration of the loop of \(\texttt {Inst}[7]\).
are not used in \(\texttt {Inst}[9]\). \(\square \)
is valid. That is, given an \(\texttt {FM}\) program P and a valid memory configuration
,
.
, \(\textsc {Post}[u]\) is available whenever \(\texttt {Inst}[v]\) is executed.
that violates it. Let \(d'\) be element in
that causes this violation. Then, the execution trace of P has execution of \(\texttt {Inst}[v]\) after the deallocation of \(\textsc {Post}[u]\) in \(\texttt {Inst}[d']\), with no execution of \(\texttt {Inst}[u]\) in between. Because \(\textsc {Post}[u]\) is deleted inside the loop of \(\texttt {Inst}[d']\), \(\texttt {Inst}[v]\) must be nested in \(\texttt {Inst}[d']\) or be executed after \(\texttt {Inst}[d']\) to be affected. That is, it must be either
or \(d' \prec v\). Also, because of how
is computed,
.
. By definition of WTO and
, it is either \(u \prec v\) or
. In either case, \(\texttt {Inst}[u]\) gets executed before \(\texttt {Inst}[v]\) reads \(\textsc {Post}[u]\). Therefore, deallocation of \(\textsc {Post}[u]\) in \(\texttt {Inst}[d']\) cannot cause the violation.
. Because
, \(\textsc {Post}[u]\) is generated in each iteration over \(\mathcal {C}(d')\), and the last iteration does not delete \(\textsc {Post}[u]\). Therefore, \(\textsc {Post}[u]\) will be available when executing \(\texttt {Inst}[v]\). Therefore, such \(u, d'\) does not exists, and the theorem is true. \(\square \)
is optimal. That is, given an \(\texttt {FM}\) program P, memory footprint of
is smaller than or equal to that of
for all valid memory configuration
.
,
. Because \(\textsc {Post}[u]\) is deleted in \(\texttt {Inst}[d]\), we do not have to consider components in
. Alternatively, if
,
. Because \(\textsc {Post}[u]\) is deleted \(\texttt {Inst}[d]\), we do not have to consider components in
. Therefore,
is optimal. \(\square \)
implies that \(\textsc {Pre}[u]\) can be deallocated at v because it is recomputed and overwritten in the loop of a \(\texttt{repeat}\) instruction before a subsequent use of \(\textsc {Pre}[u]\).
must be a subset of
: only the instructions of the heads of components that contain v recompute \(\textsc {Pre}[u]\). If \(\texttt {Inst}[u]\) is a \(\texttt{repeat}\) instruction, \(\textsc {Pre}[u]\) is required to perform widening. Therefore, u must not be contained in
.
is not valid, because \(\texttt {Inst}[4]\) would read \(\bot \) as the value of \(\textsc {Post}[4]\) when performing widening. \(\square \)
for the graph
,
is defined as:
is valid. That is, given an \(\texttt {FM}\) program P and a valid memory configuration
,
.
, the deletion does not affect widening.
,
. Because \(\textsc {Pre}[u]\) is not deleted when \(\mathcal {C}(v)\) is stabilized, \(\textsc {Pre}[u]\) will be available when performing assertion checks in
. Therefore,
is valid. \(\square \)
is optimal. That is, given an \(\texttt {FM}\) program P, memory footprint of
is smaller than or equal to that of
for all valid memory configuration
.
is optimal.
(
,
,
,
) is optimal.
is valid and optimal, respectively. Theorems 6 and 7 prove that
is valid and optimal, respectively. Theorems 8 and 9 prove that
is valid and optimal, respectively. Finally, Theorems 10 and 11 prove that
is valid and optimal, respectively. Therefore,
(
,
,
,
) is optimal. \(\square \)
for a given directed graph
. Algorithm 1 adapts the bottom-up WTO construction algorithm presented in Kim et al. [10]. In particular, Algorithm 1 applies the \(\texttt{genProg}\) rules (Eq. 3) to generate the \(\texttt {FM}\) program from a WTO. Line 31 generates \(\texttt{exec}\) instructions for non-heads. Line 39 generates \(\texttt{repeat}\) instructions for heads, with their bodies ([ ]) generated on Line 35. Finally, instructions are merged on Line 48 to construct the final output P.
returns the representative of the set that contains v. In Line 5, the sets are initialized to be
for all \(v \in V\). Operation
on Line 43 merges the sets containing v and
, and assigns
to be the representative for the combined set.
is the lowest common ancestor of u, v in the depth-first forest D [19]. Cross and forward edges are initially removed from
on Line 7, making the graph
reducible. Restoring it on Line 9 when
restores some reachability while keeping
reducible.
. Lines 37, 41, and 50 compute
. Due to the specific order in which the algorithm traverses G,
is overwritten with greater values (as per the total order
) on these lines, making the final value to be the maximum among the successors. \(\mathop {\mathrm {\texttt {Lift}}}\limits \) is implicitly applied when restoring the edges in
: edge
whose
is replaced to
on Line 9.
is computed using an auxiliary map
and a relation
. At the end of the algorithm,
will be the maximum element (as per
) in
. That is,
, where
. Once
is computed by lines 38, 41, and 51, the transitive reduction of
,
, is used to find all elements of
on Line 56.
is computed on Line 43. Note that
and
.
and
are computed on Lines 53 and 54, respectively.
, are removed on Line 7. Because
, the removed edge (2, 8) will be restored in Line 9 when
. It is restored as (2, 7), because the disjoint set \(\{8\}\) would have already been merged with \(\{7\}\) on Line 43 when
, making
to be 7 when
.
on Line 10 generates
, an \(\texttt {FM}\) instruction for
. When
, because the SCC whose entry is 9 is trivial, \(\texttt{exec}\ 9\) is generated in Line 32. When
, the SCC whose entry is 3 is non-trivial, with the entries of its nested SCCs,
. These entries are visited in a topological order (descending 
on Line 39. Visiting the nodes in a descending 
.
on Line 11 connects the instructions of entries of outermost SCCs, which is detected by the boolean expression
, in a topological order (descending 
and
,
is set to 3 and then to 7 on Line 50. Due to
and
,
is set to 4 and then to 3 in Line 41.
is set to 3, as
in Line 53.
is set to 2 on Line 51, and
is set to \(\{2\}\) on Line 56.
is set to 4 and then to 3 on Line 41, making
to be \(\{3, 4, 5\}\). Because
,
is set to \(\{3\}\) in Line 54. \(\square \)
,
,
: Let \(v'\) be the value of
before overwritten in Line 50, 37, or 41. Descending post DFN ordering corresponds to a topological sorting of the nested SCCs. Therefore, in Line 50 and 37, \(v' \prec v\). Also, because
for all \(v \in N_h\) in Line 41,
. In any case,
. Because
essentially performs \(\mathop {\mathrm {\texttt {Lift}}}\limits (u,v)\) when restoring the edges, the final
is the maximum of the lifted successors, and the map is correctly computed.
: The correctness follows from the correctness of
. Because the components are constructed bottom-up,
in Line 51 and Line 38 returns
. Also,
. Thus,
is correctly computed.
: At the end of the algorithm
is the head of maximal component that contains v, or v itself when v is outside of any components. Therefore,
is correctly computed.
: Using the same reasoning as in
, and because
,
is correctly computed.
The smaller the MRR, the greater reduction in peak-memory usage in \(\textsc {Mikos}\). If MRR is less than 1, \(\textsc {Mikos}\) has smaller memory footprint than \(\text {IKOS}\).
The larger the speedup, the greater reduction in runtime in \(\textsc {Mikos}\). If speedup is greater than 1, \(\textsc {Mikos}\) is faster than \(\text {IKOS}\).
