Exploiting Multiple Abstract Call Patterns for Optimizing Run-Time Checks
For developers of dynamically typed languages like Prolog, this reduces the performance cost of using expressive assertions for type and property checking.
This work reduces run-time overhead of assertion checking in dynamic languages by integrating run-time semantics into abstract interpretation and exploiting multiple inferred calling patterns. The approach achieves better performance than prior techniques, as demonstrated in the Ciao system.
In strongly-typed languages, types are verified at compile time, while dynamically typed languages, such as Prolog, perform type consistency checks entirely at run-time. Extending dynamic languages with assertions allows expressing both classical types and more general properties, providing high expressiveness, but at the cost of run-time overhead. Abstract interpretation allows safely approximating such program properties at compile time, which has been used to reduce the number of properties that require run-time checks, while still reporting unverified properties that can guide further static analyses, testing, or domain refinement. In this work, we first study how to selectively integrate the run-time semantics of assertion properties into a multivariant, top-down, goal-directed abstract interpretation algorithm. We then show how multiple inferred calling patterns can be exploited to reduce the number of properties that must be checked at run-time, thus minimizing the overhead. Finally, we report on an implementation of our approach in the Ciao system and provide performance results supporting that better results can be obtained than with the previously reported techniques.