(L. Araujo) Correctness Proof of a Distributed Implementation of Prolog by Means of Abstract State Machines

Abstract: This work provides both a specification and a proof of correctness for the system PDP (Prolog Distributed Processor) which make use of Abstract State Machines (ASMs). PDP is a recomputation-based model for parallel execution of Prolog on distributed memory. The system exploits OR_parallelism, Independent AND_parallelism as well as the combination of both. The verification process starts from the SLD trees, which define the execution of a Prolog program, and going through the parallel model, it arrives to the abstract machine designed for PDP, an extension of the WAM (Warren Abstract Machine), the most common sequential implementation of Prolog. The first step of this process consists in defining parallel SLD subtrees, which are a kind of partition of the SLD tree for programs whose clauses are annotated with parallelism. In a subsequent step the parallel execution approach of PDP is modeled by means of an OR_TASK ASM. In this ASM each task is associated with the execution of a parallel SLD subtree. The execution of the parallel SLD subtree corresponding to each task is modeled by a NODE submachine which is an extension of the one proposed by Börger and Rosenzweig to verify the sequential execution of Prolog. Accordingly, the verification leans on the results of this work in order to avoid the verification of the common points with the sequential execution. The new elements of the execution due to parallelism exploitation are modeled at successive steps of the verification process, finally leading to the extended WAM which implements PDP. The PDP verification proves correctness for this particular system but it can readily be adapted to prove it in other related parallel systems exploiting AND, OR or both kinds of parallelism.