Experimental evaluation of optimal abstract operators for sharing and linearity analysis

Technical Summary: Experimental Evaluation of Optimal Abstract Operators for Sharing and Linearity Analysis

Problem Statement
In the static analysis of logic programs, the optimality of abstract operators is a valuable theoretical property that defines the maximum precision achievable within an abstract domain. However, a practical trade-off exists: implementing optimal operators is often complex and computationally expensive, potentially degrading performance. While the theoretical benefits of optimality are well-understood, their practical impact on the accuracy and efficiency of real-world analyses remains less clear. Specifically, it is uncertain whether the increased precision of optimal operators justifies the computational cost, or if higher precision might paradoxically reduce overall analysis costs by producing smaller abstract objects.

Methodology
The authors experimentally investigate this trade-off within the context of sharing and linearity analysis using the PLAI static analyzer, part of the CiaoPP preprocessor for the Ciao Prolog system. The study focuses on three abstract domains:

1. Sharing: The basic domain for (set) sharing analysis.
2. ShLin: A reduced product combining sharing and linearity information.
3. ShLin2: An enhanced domain annotating sharing groups with specific linearity information per variable.

For each domain, the authors implemented both standard operators (as described in existing literature, e.g., Hans and Winkler 1992) and optimal operators (the most precise correct abstractions of their concrete counterparts, as defined by Amato and Scozzari 2009; 2010; 2014; 2024). The implementation distinguishes between two strategies for backward unification:

• Unification-based: Using the standard most general unifier (mgu) for both forward and backward steps.
• Matching-based: Using mgu for forward unification and an optimal matching (match) operator for backward unification, exploiting the fact that exit substitutions are more instantiated than call substitutions.

The evaluation was conducted on a suite of 33 Prolog programs from the SWI-Prolog benchmark suite. The experiments measured execution time and precision (quantified by the number of sharing groups and linear variables) across 15 different configurations, including built-in CiaoPP domains and the authors' custom implementations with varying combinations of standard/optimal operators and unification/matching strategies.

Key Contributions

1. Implementation of Optimal Operators: The authors provide a modular implementation of optimal abstract operators for unification and matching within the Sharing, ShLin, and ShLin2 domains, integrated into the PLAI analyzer.
2. First Implementation of ShLin2: This work presents the first implementation and experimental evaluation of the ShLin2 abstract domain.
3. Empirical Trade-off Analysis: The paper offers a comprehensive empirical study comparing standard versus optimal operators and unification versus matching strategies, challenging the assumption that optimal operators invariably incur a performance penalty.
4. Optimization of Algorithms: The authors address the implementation challenges of optimal operators, moving beyond naive "generate-and-test" approaches (which are exponential in complexity) to optimized procedures that incrementally build results, making the operators practically usable.

Experimental Results

• Feasibility and Performance: The use of optimal operators does not compromise the feasibility of the analysis. In many cases, optimal operators lead to faster analyses. This is attributed to the fact that higher precision often results in smaller abstract objects (fewer sharing groups), which reduces the computational cost of subsequent operations.
• Impact of Matching: The use of the matching operator for backward unification consistently outperforms unification-only approaches. Matching improves both precision and performance and, in several critical cases (e.g., chat_parser, reducer), enables analyses to complete within the timeout where unification-based approaches fail.
• Precision Gains: Optimal operators and matching strategies yield clearer increases in precision for the ShLin domain. For ShLin2, the most precise configuration (optimal mgu and optimal matching) generally yields the most precise results among all tested domains, with the exception of programs where the analysis fails to terminate due to complexity.
• Termination Behavior: Increasing operator precision can lead to non-termination in specific cases (e.g., reducer with ShLin, flatten with ShLin2), likely due to the complexity of the abstract objects. However, in other cases, increased precision allows the analysis to terminate where standard operators fail.
• Correlation with Metrics: Analysis failures (timeouts or out-of-memory conditions) are most strongly correlated with the maximum number of variables in a clause (max vars), rather than other program size metrics.

Significance and Claims
The paper claims that the theoretical property of optimality translates effectively into practice. The authors conclude that optimal abstract operators can be implemented efficiently and, contrary to intuition, often improve overall analysis performance by reducing the size of abstract objects. Furthermore, the use of matching for backward unification is identified as a particularly effective choice, offering superior precision and performance compared to standard unification. The work demonstrates that the ShLin2 domain, when combined with optimal operators and matching, provides the highest precision, though it requires careful implementation to manage computational costs. The authors note that while the benefits are not uniform across all programs, the approach is viable and often advantageous, particularly for domains where precision directly influences the size of the abstract state.