Non-failure analysis for (logic) programs

May 11, 2010

Pedro López-Garcia


Non-failure analysis for (logic) programs

Time:   11:00am
Location:   Meeting room 302 (Mountain View), level 3

Non-failure analysis aims at inferring that procedure calls in a program will never fail. This type of information has many applications in logic/functional programming, such as error detection, program transformations and parallel execution optimization, avoiding speculative parallelism and estimating lower bounds on the computational costs of goals, which can be used for resource usage analysis, granularity control, abstract carrying code, etc. We provide a method that uses mode and (upper approximation) type information to detect calls and procedures in a program that can be guaranteed to produce at least one solution or not terminate. The technique is based on an intuitively very simple notion, that of a (set of) tests “covering” the type of a set of variables (i.e. for any element that belongs to the type, at least one test will succeed). We give sound algorithms for determining coverings that are precise and efficient in practice. Based on this information, we show how to identify calls and procedures that can be guaranteed to not fail at runtime. Finally, we report on an implementation of our method and show that better results are obtained than with previously proposed approaches.