Interval-based resource usage verification by translation into Horn clauses and an application to energy consumption

López García, Pedro and Darmawan, Luthfi and Liqat, Umer and Bueno Carrillo, Francisco and Hermenegildo, Manuel V. (2018). Interval-based resource usage verification by translation into Horn clauses and an application to energy consumption. In: "34th International Conference on Logic Programming", 14-17 Jul 2018, Oxford. pp. 167-223. https://doi.org/10.1017/S1471068418000042.

Description

Title: Interval-based resource usage verification by translation into Horn clauses and an application to energy consumption
Author/s:
  • López García, Pedro
  • Darmawan, Luthfi
  • Liqat, Umer
  • Bueno Carrillo, Francisco
  • Hermenegildo, Manuel V.
Item Type: Presentation at Congress or Conference (Article)
Event Title: 34th International Conference on Logic Programming
Event Dates: 14-17 Jul 2018
Event Location: Oxford
Title of Book: Theory and Practice of Logic Programming
Date: 2018
Volume: 18
Subjects:
Freetext Keywords: Static Analysis; Resource Usage Analysis and Verification; Horn Clause-based Analysis and Verification; Energy Consumption; Program Verification and Debugging
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 (3MB) | Preview

Abstract

In many applications it is important to ensure conformance with respect to specifications that constrain the use of resources such as execution time, energy, bandwidth, etc. We present a configurable framework for static resource usage verifi cation where specifications can include data size-dependent resource usage functions, expressing both lower and upper bounds. Ensuring conformance with respect to such specifications is an undecidable problem. Therefore, our framework infers resource usage functions (of the same type as the specifications, i.e., data-size dependent, and providing upper and lower bounds), which safely approximate the actual resource usage of the program, and which are safely compared against the specification. We start by reviewing how this framework is parametric with respect to the programming language by a) translating programs to an intermediate representation based on Horn clauses, and b) using the configurability of the framework to describe the resource semantics of the input language. We then provide a more detailed formalization of the approach and extend the framework so that the outcome of the static checking of assertions can generate intervals of the input data sizes for which assertions hold or not, i.e., a given specification can be proved for some intervals but disproved for others. We also generalize the specifications to support preconditions expressing intervals within which the input data size of a program is supposed to lie. Most importantly, we provide new techniques which extend the classes of resource usage functions that can be checked, such as functions containing logarithmic or summation expressions, or some functions with multiple variables. We also report on and provide results from an implementation within the Ciao/CiaoPP framework, as well as on a practical tool built by instantiating this framework for the verification of energy consumption specifications for imperative/embedded programs written in the XC language and running on the XS1-L architecture. Finally, we illustrate with an example how embedded software developers can use this tool, in particular for determining values for program parameters that ensure meeting a given energy budget while minimizing the loss in quality of service.

  • 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