Item


Resource Analysis driven by (Conditional) Termination Proofs

When programs feature a complex control flow, existing techniques for resource analysis produce cost relation systems (CRS) whose cost functions retain the complex flow of the program and, consequently, might not be solvable into closed-form upper bounds. This paper presents a novel approach to resource analysis that is driven by the result of a termination analysis. The fundamental idea is that the termination proof encapsulates the flows of the program which are relevant for the cost computation so that, by driving the generation of the CRS using the termination proof, we produce a linearly-bounded CRS (LB-CRS). A LB-CRS is composed of cost functions that are guaranteed to be locally bounded by linear ranking functions and thus greatly simplify the process of CRS solving. We have built a new resource analysis tool, named MaxCore, that is guided by the VeryMax termination analyzer and uses CoFloCo and PUBS as CRS solvers. Our experimental results on the set of benchmarks from the Complexity and Termination Competition 2019 for C Integer programs show that MaxCore outperforms all other resource analysis tools

This work was funded partially by the Spanish MICINN/FEDER, UE projects RTI2018-094403-BC31, RTI2018-094403-B-C33 and RTI2018-095609-B-I00, the MINECO project TIN2015-69175-C4-2-R, the MINECO/FEDER, UE projects TIN2015-69175-C4-3-R and TIN2015-66293-R, and by the CM project S2018/TCS-4314

Cambridge University Press (CUP)

Manager: Ministerio de Economía y Competitividad (Espanya)
Author: Albert, Elvira
Bofill Arasa, Miquel
Borralleras, Cristina
Martín-Martín, Enrique
Rubio, Albert
Abstract: When programs feature a complex control flow, existing techniques for resource analysis produce cost relation systems (CRS) whose cost functions retain the complex flow of the program and, consequently, might not be solvable into closed-form upper bounds. This paper presents a novel approach to resource analysis that is driven by the result of a termination analysis. The fundamental idea is that the termination proof encapsulates the flows of the program which are relevant for the cost computation so that, by driving the generation of the CRS using the termination proof, we produce a linearly-bounded CRS (LB-CRS). A LB-CRS is composed of cost functions that are guaranteed to be locally bounded by linear ranking functions and thus greatly simplify the process of CRS solving. We have built a new resource analysis tool, named MaxCore, that is guided by the VeryMax termination analyzer and uses CoFloCo and PUBS as CRS solvers. Our experimental results on the set of benchmarks from the Complexity and Termination Competition 2019 for C Integer programs show that MaxCore outperforms all other resource analysis tools
This work was funded partially by the Spanish MICINN/FEDER, UE projects RTI2018-094403-BC31, RTI2018-094403-B-C33 and RTI2018-095609-B-I00, the MINECO project TIN2015-69175-C4-2-R, the MINECO/FEDER, UE projects TIN2015-69175-C4-3-R and TIN2015-66293-R, and by the CM project S2018/TCS-4314
Format: application/pdf
Document access: http://hdl.handle.net/10256/18110
Language: eng
Publisher: Cambridge University Press (CUP)
Collection: info:eu-repo/semantics/altIdentifier/doi/10.1017/S1471068419000152
info:eu-repo/semantics/altIdentifier/issn/1471-0684
info:eu-repo/semantics/altIdentifier/eissn/1475-3081
info:eu-repo/grantAgreement/MINECO//TIN2015-66293-R/ES/LOGICA PARA PROBLEMAS COMBINATORIOS/
Rights: Tots els drets reservats
Subject: Programació lògica
Logic programming
Programació (Matemàtica)
Programming (Mathematics)
Title: Resource Analysis driven by (Conditional) Termination Proofs
Type: info:eu-repo/semantics/article
Repository: DUGiDocs

Subjects

Authors


Warning: Unknown: write failed: No space left on device (28) in Unknown on line 0

Warning: Unknown: Failed to write session data (files). Please verify that the current setting of session.save_path is correct (/var/lib/php5) in Unknown on line 0