Improving run-time checking in dynamic programming language

• Autores: Nataliia Stulova
• Directores de la Tesis: Manuel de Hermenegildo Salinas (dir. tes.) , José Francisco Morales Caballero (codir. tes.)
• Lectura: En la Universidad Politécnica de Madrid ( España ) en 2018
• Idioma: español
• Tribunal Calificador de la Tesis: Germán Vidal Oriola (presid.) , Manuel Carro Liñares (secret.) , Alessandra Gorla (voc.) , Viktor Kuncak (voc.) , Tom Schrijvers (voc.)
• Enlaces
  • Tesis en acceso abierto en: Archivo Digital UPM
• Resumen

  • Detecting incorrect program behaviors is an important part of the software development life cycle. It is also a complex and tedious one, in which dynamic languages bring special challenges. A number of techniques have been proposed to aid in the process, among which we center our attention on the use of language-level constructs to describe expected program behavior, and of associated tools to compare actual program behavior against expectations, such as static code analyzers/verifiers and run-time verification frameworks.

    In practice, however, the run-time overhead associated with these tools often remains impractically high, specially for non-trivial properties, or complex data structure tests. This reduces the attractiveness of run-time checking to programmers, who may allow sporadic checking of very simple conditions, but will tend to turn off run-time checking for more complex properties in favor of faster execution. Some approaches even opt for limiting the expressiveness of the assertion language in order to reduce the overhead.

    Our research objective in this thesis is twofold: * first, we aim to enhance the expressiveness of the assertion language to reflect all the features of the related programming language, including, e.g., higher-order constructs, and to do so in a way that allows the programmer to write precise program specifications while not imposing a learning or programming burden on them; * at the same time, our goal is to efficiently check specifications, mitigating the associated run-time overhead as much as possible without compromising the safety guarantees that the checks provide.

    With respect to checking specifications efficiently this dissertation presents several improvements for run-time specification checking, including: * a mechanism for unobtrusive caching of intermediate run-time checking results so that they can be re-used in the checking process instead of being re-evaluated, contributing to undesirable (and unnecessary) run-time overhead; * a technique of combining compile- and run-time checking in a way that uses the properties from the program specification as an additional information source during static specification checking, which results in more properties checked statically and fewer of them turned into run-time checks; * and another technique for improving term shape inference during static program analysis, exploiting term visibility rules of the underlying module system, which allows to simplify property checks in a program in a way that constant run-time over- head is achievable in relevant cases.

    Finally, to address the limited expressiveness of the specification languages, this dissertation targets the concrete case of providing detailed specifications for higher-order program routines.

    The techniques and tools discussed in this thesis are presented for concreteness in the context of the Ciao run-time checking framework. Nevertheless, these results are general and system-independent, and we believe they can be straightforwardly transferred to the contexts of other declarative languages. In addition, given the recent advances in verification of a wide class of programming languages, including imperative ones, by translation into Horn clauses and proving properties at this level, and the fact that this approach is fully supported in the Ciao system, we argue that our results can easily be adapted to a much broader spectrum of languages.