next up previous
Next: Program Development Up: Achievements and Misses Previous: Sequentialization Tools

Analysis of Concurrent Logic Programs

Because the preliminary schedule analysis framework proved satisfactory, work was geared towards attempting to extend sequentialization to non-sibling atoms. This incorporates aspects of Ueda and Morita's message oriented implementation of GHC [74, 73] into the conventional KL1 abstract machine. Where the optimization is applied, code is compiled to pass control directly from the producer of data to its consumer so that data can be passed in registers and some guard matching removed. Currently the optimization is only applicable to producers and consumers of single-threaded variables.

At Pisa, significant effort has been devoted to the task of extending the generalized semantics approach of (sequential) constraint logic programs to Ciao-type languages and to AKL. The aim was that of making available for these two classes of languages the analysis techniques and the abstract domains developed for the pure sequential case. The goal has been achieved, with interesting new results. In particular, we have extended a framework for the (bottom-up, goal-independent) abstract interpretation of pure Prolog (pure logic programs + Prolog control strategy) to treat the cut control primitive. The time was not enough to apply the framework to partitioning, as originally planned. However, we have studied a related application (type and groundness analysis), which shows that the application is feasible. We have also studied the application of the generalized approach to the abstract interpretation of concurrent constraint programs. For these languages the main difficulty lies in the correct approximation of the synchronization mechanism, i.e. the ask operator. After proving that there does not exist a domain independent solution to this problem, several possible solutions have been identified. The first solution is to base the abstract interpretation of concurrent constraint programs on a (non-standard) semantics, the success semantics, which models non suspended computations only. According to this semantics, concurrent constraint programs can be analyzed as if they were sequential constraint logic programs. We have shown that, for suspension-free programs, the success semantics is equivalent to the standard semantics. This justifies a two step process: first apply the suspension analysis developed in the first year of the project, then apply the existing techniques based on the generalized semantics. In particular this allows the application of existing techniques for modular analysis of programs. Another solution consists of considering a restricted class of program properties, namely the downward closed ones. We have proved that in this case a correct approximation of the synchronization mechanism can be obtained automatically by abstracting the ask constraints [75, 76], following the generalized semantics approach.

A type and alias analyzer for AKL, based on setting up and solving a set of abstract equations, was implemented and evaluated [67, 66]. Recent work at SICS has concentrated on making the analyzer a practical tool in terms of execution performance. Towards this end the analyzer was substantially rewritten and as a result speeded up about two orders of a magnitude. It was possible to do this by just improving the algorithms without changing programming language or limiting the expressiveness of the domain. The same basic structure of the system has been maintained with a strict separation between setting up the fixpoint equation, the fixpoint solver and the domain functions. The implementation is focused on a domain which handles type and alias.

A large number of benchmarks varying in size from a few lines to thousands of lines have been tested, and the results are reported in this year's deliverable. The execution time for the analysis is approximately proportional to the square of the size of the program. This means that there is a practical limit for how large programs that can be analyzed as a whole. One countermeasure is to split the program into pieces. A separate investigation has also been carried out to show the usefulness of deriving information about type and alias.

An automatic partial evaluator for AKL has been specified. It is based on a number program of transformation steps such as folding, unfolding and various evaluations. A basic partial evaluation procedure has been described which automates the application of the program transformation rules. The partial evaluator for AKL specified at SICS is not based on the meta-interpreter approach, which is otherwise common for logic programming languages. Instead, it is strictly based on a set of program transformation rules which preserve the equivalence of the program. This both simplifies proving correctness and the implementation. Such implementation is still in progress.


next up previous
Next: Program Development Up: Achievements and Misses Previous: Sequentialization Tools

<webmaster@clip.dia.fi.upm.es> Last Modified: Fri May 9 18:15:08 MET DST 1997