Evaluation of the Implementation of an Abstract Interpretation Algorithm using Tabled CLP

Joaquin Arias - joaquin.arias@imdea.org
Manuel Carro - manuel.carro@imdea.org

Abstract

Abstract interpretation of programs requires a fixpoint computation. PLAI is a fixpoint algorithm implemented by the abstract interpreter of CiaoPP, an analyzer and optimizer suite for logic programs, part of the Ciao development environment.

In this paper, we adapt the existing PLAI implementation in CiaoPP using tabled constraint logic programming. The tabling engine is used to compute the fixpoint and the constraint interface computes the LUB of the abstract substitutions of different clauses. That provides, on one hand, a much simpler code as the fixpoint computation is taken care of by the underlying machinery, and in most cases performance gains, since some crucial operations (such as branch switching and resumption) are executed by the tabling engine.

Determining that the fixpoint has been reached uses semantic equivalence, e.g., whether syntactically different representations of an abstract substitution actually refer to the same element in the abstract domain. This is delegated to the abstract domain operations, transparently to the analyzer. As a result, the tabling analyzer can reuse more answers than if syntactical equality were used and better performance, even with the additional cost associated to these checks, is achieved.

The implementation presented is based on the TCLP framework available in Ciao Prolog and has been evaluated by analysing several programs with different abstract domains.

Resources available

We are including here the files related to our ICLP 2019 submission:

The original code for the implementation of the abstract interpretation fixpoint algorithm (PLAI) available in Ciao/CiaoPP.
The code for the modified version of the fixpoint using tabling.
The benchmarks used in the paper, together with instructions to use them.
The Ciao/CiaoPP distribution with which the abstract interpretation fixpoint algorithm was tested, ready to be compiled and executed.

Fixpoint implementation: tabling version

Below you can find a link to the code corresponding to the re-implementation of PLAI using tabling with constraints. The aim of this file is not to explain the algorithm or the code, but rather to compare the complexity and verbosity of the original implementation of PLAI in CiaoPP with ours.

fixpo_plai_tabling.pl

Ciao/CiaoPP version

We include here the original implementation of the PLAI algorithm in Ciao/CiaoPP using plain Prolog.

fixpo_plai_with_comments.pl

Benchmarks

Besides showing the simplicity of the implementation using tabling, we evaluated and compared its performance with that of the original one. We used a series of standard benchmarks, ranging from small to moderately-sized programs, which are available in the file linked below. With them, the tabling implementation showed an average speedup of 30%.

benchmarks-fixpo-plai.tar.gz

To execute the benchmarks, please follow the instructions included at the end of this page to install the Ciao/CiaoPP distribution, download and untar the file above, cd to the directory, and execute:

$ ./go

Note: the figures reported in the paper were obtained by running every analysis 40 times and discarded the 10 slower executions to neutralize the effect of noise due to O.S. scheduling, cache behavior, etc. The script we include in the above link only executes every analysis twice and does not discard any timing measure. Therefore the results are likely to be different (for example, in stability) from those in the paper.

The results are stored as .csv files under the folder temp_csv_files.

Ciao/CiaoPP Distribution

We include here a tar.gz file with the Ciao distribution including both fixpo_plai_xxx.pl versions.

Ciao-1.18-474-g4762bb60a-CiaoPP.tar.gz

To install the distribution, untar the file and execute:

$ ./quick_install.sh
$ source ~/.bashrc # To add the path of the Ciao executables