Cargando…
Run-time Complexity Bounds Using Squeezers
Determining upper bounds on the time complexity of a program is a fundamental problem with a variety of applications, such as performance debugging, resource certification, and compile-time optimizations. Automated techniques for cost analysis excel at bounding the resource complexity of programs th...
Autores principales: | , , , |
---|---|
Formato: | Online Artículo Texto |
Lenguaje: | English |
Publicado: |
2021
|
Materias: | |
Acceso en línea: | https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7984564/ http://dx.doi.org/10.1007/978-3-030-72019-3_12 |
_version_ | 1783668092258222080 |
---|---|
author | Ish-Shalom, Oren Itzhaky, Shachar Rinetzky, Noam Shoham, Sharon |
author_facet | Ish-Shalom, Oren Itzhaky, Shachar Rinetzky, Noam Shoham, Sharon |
author_sort | Ish-Shalom, Oren |
collection | PubMed |
description | Determining upper bounds on the time complexity of a program is a fundamental problem with a variety of applications, such as performance debugging, resource certification, and compile-time optimizations. Automated techniques for cost analysis excel at bounding the resource complexity of programs that use integer values and linear arithmetic. Unfortunately, they fall short when execution traces become more involved, esp. when data dependencies may affect the termination conditions of loops. In such cases, state-of-the-art analyzers have shown to produce loose bounds, or even no bound at all. We propose a novel technique that generalizes the common notion of recurrence relations based on ranking functions. Existing methods usually unfold one loop iteration, and examine the resulting relations between variables. These relations assist in establishing a recurrence that bounds the number of loop iterations. We propose a different approach, where we derive recurrences by comparing whole traces with whole traces of a lower rank, avoiding the need to analyze the complexity of intermediate states. We offer a set of global properties, defined with respect to whole traces, that facilitate such a comparison, and show that these properties can be checked efficiently using a handful of local conditions. To this end, we adapt state squeezers, an induction mechanism previously used for verifying safety properties. We demonstrate that this technique encompasses the reasoning power of bounded unfolding, and more. We present some seemingly innocuous, yet intricate, examples where previous tools based on cost relations and control flow analysis fail to solve, and that our squeezer-powered approach succeeds. |
format | Online Article Text |
id | pubmed-7984564 |
institution | National Center for Biotechnology Information |
language | English |
publishDate | 2021 |
record_format | MEDLINE/PubMed |
spelling | pubmed-79845642021-03-23 Run-time Complexity Bounds Using Squeezers Ish-Shalom, Oren Itzhaky, Shachar Rinetzky, Noam Shoham, Sharon Programming Languages and Systems Article Determining upper bounds on the time complexity of a program is a fundamental problem with a variety of applications, such as performance debugging, resource certification, and compile-time optimizations. Automated techniques for cost analysis excel at bounding the resource complexity of programs that use integer values and linear arithmetic. Unfortunately, they fall short when execution traces become more involved, esp. when data dependencies may affect the termination conditions of loops. In such cases, state-of-the-art analyzers have shown to produce loose bounds, or even no bound at all. We propose a novel technique that generalizes the common notion of recurrence relations based on ranking functions. Existing methods usually unfold one loop iteration, and examine the resulting relations between variables. These relations assist in establishing a recurrence that bounds the number of loop iterations. We propose a different approach, where we derive recurrences by comparing whole traces with whole traces of a lower rank, avoiding the need to analyze the complexity of intermediate states. We offer a set of global properties, defined with respect to whole traces, that facilitate such a comparison, and show that these properties can be checked efficiently using a handful of local conditions. To this end, we adapt state squeezers, an induction mechanism previously used for verifying safety properties. We demonstrate that this technique encompasses the reasoning power of bounded unfolding, and more. We present some seemingly innocuous, yet intricate, examples where previous tools based on cost relations and control flow analysis fail to solve, and that our squeezer-powered approach succeeds. 2021-03-23 /pmc/articles/PMC7984564/ http://dx.doi.org/10.1007/978-3-030-72019-3_12 Text en © The Author(s) 2021 Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. |
spellingShingle | Article Ish-Shalom, Oren Itzhaky, Shachar Rinetzky, Noam Shoham, Sharon Run-time Complexity Bounds Using Squeezers |
title | Run-time Complexity Bounds Using Squeezers |
title_full | Run-time Complexity Bounds Using Squeezers |
title_fullStr | Run-time Complexity Bounds Using Squeezers |
title_full_unstemmed | Run-time Complexity Bounds Using Squeezers |
title_short | Run-time Complexity Bounds Using Squeezers |
title_sort | run-time complexity bounds using squeezers |
topic | Article |
url | https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7984564/ http://dx.doi.org/10.1007/978-3-030-72019-3_12 |
work_keys_str_mv | AT ishshalomoren runtimecomplexityboundsusingsqueezers AT itzhakyshachar runtimecomplexityboundsusingsqueezers AT rinetzkynoam runtimecomplexityboundsusingsqueezers AT shohamsharon runtimecomplexityboundsusingsqueezers |