Practical run-time checking via unobtrusive property caching

Stulova, Nataliia and Morales Caballero, José Francisco and Hermenegildo, Manuel V. (2015). Practical run-time checking via unobtrusive property caching. In: "31st International Conference on Logic Programming (ICLP ’15)", 31 Aug-04 Sep 2015, Cork, Irlanda. pp. 726-741. https://doi.org/10.1017/S1471068415000344.

Description

Title: Practical run-time checking via unobtrusive property caching
Author/s:
  • Stulova, Nataliia
  • Morales Caballero, José Francisco
  • Hermenegildo, Manuel V.
Item Type: Presentation at Congress or Conference (Article)
Event Title: 31st International Conference on Logic Programming (ICLP ’15)
Event Dates: 31 Aug-04 Sep 2015
Event Location: Cork, Irlanda
Title of Book: Theory and Practice of Logic Programming
Date: July 2015
Volume: 15
Subjects:
Faculty: E.T.S. de Ingenieros Informáticos (UPM)
Department: Inteligencia Artificial
Creative Commons Licenses: Recognition - No derivative works - Non commercial

Full text

[img]
Preview
PDF - Requires a PDF viewer, such as GSview, Xpdf or Adobe Acrobat Reader
Download (684kB) | Preview

Abstract

The use of annotations, referred to as assertions or contracts, to describe program properties for which run-time tests are to be generated, has become frequent in dynamic programing languages. However, the frameworks proposed to support such run-time testing generally incur high time and/or space overheads over standard program execution. We present an approach for reducing this overhead that is based on the use of memoization to cache intermediate results of check evaluation, avoiding repeated checking of previously verified properties. Compared to approaches that reduce checking frequency, our proposal has the advantage of being exhaustive (i.e., all tests are checked at all points) while still being much more efficient than standard run-time checking. Compared to the limited previous work on memoization, it performs the task without requiring modifications to data structure representation or checking code. While the approach is general and system-independent, we present it for concreteness in the context of the Ciao run-time checking framework, which allows us to provide an operational semantics with checks and caching. We also report on a prototype implementation and provide some experimental results that support that using a relatively small cache leads to significant decreases in run-time checking overhead.

  • Logo InvestigaM (UPM)
  • Logo GEOUP4
  • Logo Open Access
  • Open Access
  • Logo Sherpa/Romeo
    Check whether the anglo-saxon journal in which you have published an article allows you to also publish it under open access.
  • Logo Dulcinea
    Check whether the spanish journal in which you have published an article allows you to also publish it under open access.
  • Logo de Recolecta
  • Logo del Observatorio I+D+i UPM
  • Logo de OpenCourseWare UPM