Static performance guarantees for programs with Run-time Checks

Klemen, Maximiliano and Stulova, Nataliia and López García, Pedro and Morales Caballero, José Francisco and Hermenegildo, Manuel V. (2018). Static performance guarantees for programs with Run-time Checks. In: "20th International Symposium on Principles and Practice of Declarative Programming (PPDP '18)", 03-05 Sep 2018, Frankfurt. ISBN 978-1-4503-6441-6. pp. 1-13. https://doi.org/10.1145/3236950.3236970.

Description

Title: Static performance guarantees for programs with Run-time Checks
Author/s:
  • Klemen, Maximiliano
  • Stulova, Nataliia
  • López García, Pedro
  • Morales Caballero, José Francisco
  • Hermenegildo, Manuel V.
Item Type: Presentation at Congress or Conference (Article)
Event Title: 20th International Symposium on Principles and Practice of Declarative Programming (PPDP '18)
Event Dates: 03-05 Sep 2018
Event Location: Frankfurt
Title of Book: PPDP '18 Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming
Date: 2018
ISBN: 978-1-4503-6441-6
Subjects:
Freetext Keywords: Run-time Checks; Assertions; Abstract Interpretation; Resource Usage Analysis; Program Analysis; (Constraint) Logic Programming
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 (2MB) | Preview

Abstract

Instrumenting programs for performing run-time checking of properties, such as regular shapes, is a common and useful technique that helps programmers detect incorrect program behaviors. This is specially true in dynamic languages such as Prolog. However, such run-time checks inevitably introduce run-time overhead (in execution time, memory, energy, etc.). Several approaches have been proposed for reducing this overhead, such as eliminating the checks that can statically be proved to always succeed, and/or optimizing the way in which the (remaining) checks are performed. However, there are cases in which it is not possible to remove all checks statically (e.g., open libraries which must check their interfaces, complex properties, unknown code, etc.) and in which, even after optimizations, these remaining checks may still introduce an unacceptable level of overhead. It is thus important for programmers to be able to determine the additional cost due to the run-time checks and compare it to some notion of admissible cost. The common practice used for estimating run-time checking overhead is profiling, which is not exhaustive by nature. Instead, we propose a method that uses static analysis to estimate such overhead, with the advantage that the estimations are functions parameterized by input data sizes. Unlike profiling, this approach can provide guarantees for all possible execution traces, and allows assessing how the overhead grows as the size of the input grows. Our method also extends an existing assertion verification framework to express “admissible” overheads, and statically and automatically checks whether the instrumented program conforms with such specifications. Finally, we present an experimental evaluation of our approach that suggests that our method is feasible and promising.

More information

Item ID: 52828
DC Identifier: http://oa.upm.es/52828/
OAI Identifier: oai:oa.upm.es:52828
DOI: 10.1145/3236950.3236970
Official URL: https://dl.acm.org/citation.cfm?id=3236970
Deposited by: Biblioteca Facultad de Informatica
Deposited on: 26 Oct 2018 09:51
Last Modified: 26 Oct 2018 09:51
  • 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