Calculating the differential cost of code changes

{"value":"Making changes to computer code may have unintended consequences for program performance. For instance, modifying loops or changing data structures in a specific program could cause an increase in execution time or in memory or disk usage. We refer to changes in such performance measures as the differential cost of modifying the code.\n\nThe ability to reason about the cost of code changes is called differential cost analysis. Being able to perform such an analysis before deploying a new version of program code is of particular interest to Amazon, as it not only enables a better customer experience but can also reduce resource usage and carbon footprint.\n\n\n\nDifferential cost analysis measures the cost of code changes in terms of some performance metric such as execution time or memory or disk usage.\n\nBut bounding the cost of a code change is an undecidable problem, meaning there’s no algorithm guaranteed to give you an answer. Previous approaches have focused on estimating the cost of a single version of the code, or they assumed the ability to align code changes in a syntactic way.\n\nAt this year’s ACM SIGPLAN Conference on Programming Language Design and Implementation (++[PLDI 2022](https://pldi22.sigplan.org/)++), we ++[presented a paper](https://www.amazon.science/publications/differential-cost-analysis-with-simultaneous-potentials-and-anti-potentials)++ on differential cost analysis that overcomes some of these challenges. Our approach is based on the idea of jointly computing a potential function and an anti-potential function that provide, respectively, the upper and lower bounds for changes in cost.\n\nUnlike previous approaches, our implementation can compute tight bounds on the costs of code changes between pairs of program versions collected from the literature. In particular, we are able to provide tight bounds on 14 out of 19 examples, which include both variations that have an impact on cost and variations that do not impact the cost but require complex analysis to establish as much.\n\n#### **Thresholds**\n\nThe ability to reason about cost changes in code is of fundamental importance in most software applications, but particularly for Prime Video: the Prime Video app runs on a range of devices, some of them with very limited memory and processing power. As our colleague Alex Ene ++[has described](https://www.amazon.science/blog/how-prime-video-updates-its-app-for-more-than-8-000-device-types)++, efficiency is a key concern for Prime Video: not only do we need to provide code that runs fast, with very tight bounds on startup time, but we also need to address the memory limitations of USB-powered streaming devices.\n\nWhile new architectures can help with achieving these goals, the approach we propose in this paper is finer-grained. It is a form of ++[automated reasoning](https://www.amazon.science/blog/a-gentle-introduction-to-automated-reasoning)++ that allows us to provide feedback to developers on every code change, in a workflow similar to the one we presented in ++[an earlier blog post](https://www.amazon.science/blog/how-automated-reasoning-improves-the-prime-video-experience)++.\n\nIn particular, we address the following code analysis problem: given two versions of a program, old and new, and given a cost we are interested in (e.g., run time, memory, number of threads, disk space), we want to compute a numerical bound, the threshold t, such that\n\ncostnew - costold ≤ t.\n\nWe focus on imperative programs — the most familiar type of program, with explicit specification of every computational step — with integer variables and polynomial arithmetic. The programs may also have nondeterministic elements, meaning that the same inputs may yield different outputs.\n\nThe anti-potential function — which calculates the lower bound — captures the minimum cost to be “paid” for a program to run. If we indicate with ϕ the potential function of a program and with χ its anti-potential function, then the threshold in cost variation between an old and a new version of a program can be approximated by ϕnew - χold.\n\nAs a concrete example, consider the two versions of the program below, where lines in yellow model the cost, text in red is the code that is removed, and text in green is the code that is added. This program encodes a common join operation over two sequences, with an operator f having some cost per pair of elements.\n\nThe formulas in boxes are, respectively, the values of the anti-potential and the potential functions. For instance, the anti-potential value in the box labeled ℓ0 encodes the fact that the cost to terminate the program is at least equal to the product of the size of the two sequences. As a result, the difference between ϕnew and χold is lenB ⋅ lenA, which is the desired threshold.\n\n\n\nIn the paper, we show that it is possible to compute both ϕ and χ by working with polynomial expressions over program variables at each program location, as shown in the example above. We represent the program versions as transition systems, a model of computation that consists of a set of program states and a set of valid transitions between states. We assume that the transition systems terminate — i.e., there’s no input that will cause them to run forever.\n\nWe fix a symbolic variable for the threshold t, and by traversing the two transition systems, we obtain a system of constraints that can be solved to obtain concrete values for the threshold and for the potential functions.\n\n#### **Constraint satisfaction**\n\nA key aspect of our approach is obtaining a simultaneous system of constraints for both the potential function of the new program version and the anti-potential function of the old program.\n\nUnfortunately, the resulting system of constraints is hard to solve, as it involves universal quantifiers and polynomial constraints over variables. We solve it by employing the results of ++[Handelman’s theorem](https://en.wikipedia.org/wiki/Positive_polynomial)++ to convert these constraints into a system of purely existentially quantified linear constraints. That is, we convert constraints of the form “for all X’s, P(X)” (a universal quantifier) to constraints of the form “there exist X’s such that Q(X)” (an existential quantifier), where Q is linear, meaning its variables are not squared, cubed, etc.\n\nSuch systems of constraints can be solved efficiently via an off-the-shelf linear-programming solver. This constraint representation has the additional benefit of enabling either the verification of a symbolic threshold or the optimization of a concrete one, which results in a threshold t that is as tight as possible.\n\nWe have validated this approach using 19 benchmarks in C from the current literature. We convert these programs to transition systems, and for 17 of them, we are able to compute a value for the threshold. The threshold is optimal in 14 cases, and more importantly, we can provide a threshold value in less that five seconds in all cases.\n\nAcknowledgements: Djordje Zikelic, ++[Pauline Bolignano](https://www.amazon.science/author/pauline-bolignano)++, Daniel Schoepe, Ilina Stoilkovska.\n\nABOUT THE AUTHOR\n\n#### **[Franco Raimondi](https://www.amazon.science/author/franco-raimondi)**\nFranco Raimondi is an Amazon Scholar and a professor of computer science at Middlesex University, London.\n\n#### **[Bor-Yuh Evan Chang](https://www.amazon.science/author/bor-yuh-evan-chang)**\nBor-Yuh Evan Chang is an Amazon Scholar and an associate professor of computer science at the University of Colorado Boulder.","render":"<p>Making changes to computer code may have unintended consequences for program performance. For instance, modifying loops or changing data structures in a specific program could cause an increase in execution time or in memory or disk usage. We refer to changes in such performance measures as the differential cost of modifying the code.</p>\n<p>The ability to reason about the cost of code changes is called differential cost analysis. Being able to perform such an analysis before deploying a new version of program code is of particular interest to Amazon, as it not only enables a better customer experience but can also reduce resource usage and carbon footprint.</p>\n<p><img src=\"https://dev-media.amazoncloud.cn/40e66d4da18c41378311abc6d04281c2_%E4%B8%8B%E8%BD%BD.gif\" alt=\"下载.gif\" /></p>\n<p>Differential cost analysis measures the cost of code changes in terms of some performance metric such as execution time or memory or disk usage.</p>\n<p>But bounding the cost of a code change is an undecidable problem, meaning there’s no algorithm guaranteed to give you an answer. Previous approaches have focused on estimating the cost of a single version of the code, or they assumed the ability to align code changes in a syntactic way.</p>\n<p>At this year’s ACM SIGPLAN Conference on Programming Language Design and Implementation (<ins><a href=\"https://pldi22.sigplan.org/\" target=\"_blank\">PLDI 2022</a></ins>), we <ins><a href=\"https://www.amazon.science/publications/differential-cost-analysis-with-simultaneous-potentials-and-anti-potentials\" target=\"_blank\">presented a paper</a></ins> on differential cost analysis that overcomes some of these challenges. Our approach is based on the idea of jointly computing a potential function and an anti-potential function that provide, respectively, the upper and lower bounds for changes in cost.</p>\n<p>Unlike previous approaches, our implementation can compute tight bounds on the costs of code changes between pairs of program versions collected from the literature. In particular, we are able to provide tight bounds on 14 out of 19 examples, which include both variations that have an impact on cost and variations that do not impact the cost but require complex analysis to establish as much.</p>\n<h4><a id=\"Thresholds_14\"></a><strong>Thresholds</strong></h4>\n<p>The ability to reason about cost changes in code is of fundamental importance in most software applications, but particularly for Prime Video: the Prime Video app runs on a range of devices, some of them with very limited memory and processing power. As our colleague Alex Ene <ins><a href=\"https://www.amazon.science/blog/how-prime-video-updates-its-app-for-more-than-8-000-device-types\" target=\"_blank\">has described</a></ins>, efficiency is a key concern for Prime Video: not only do we need to provide code that runs fast, with very tight bounds on startup time, but we also need to address the memory limitations of USB-powered streaming devices.</p>\n<p>While new architectures can help with achieving these goals, the approach we propose in this paper is finer-grained. It is a form of <ins><a href=\"https://www.amazon.science/blog/a-gentle-introduction-to-automated-reasoning\" target=\"_blank\">automated reasoning</a></ins> that allows us to provide feedback to developers on every code change, in a workflow similar to the one we presented in <ins><a href=\"https://www.amazon.science/blog/how-automated-reasoning-improves-the-prime-video-experience\" target=\"_blank\">an earlier blog post</a></ins>.</p>\n<p>In particular, we address the following code analysis problem: given two versions of a program, old and new, and given a cost we are interested in (e.g., run time, memory, number of threads, disk space), we want to compute a numerical bound, the threshold t, such that</p>\n<p>costnew - costold ≤ t.</p>\n<p>We focus on imperative programs — the most familiar type of program, with explicit specification of every computational step — with integer variables and polynomial arithmetic. The programs may also have nondeterministic elements, meaning that the same inputs may yield different outputs.</p>\n<p>The anti-potential function — which calculates the lower bound — captures the minimum cost to be “paid” for a program to run. If we indicate with ϕ the potential function of a program and with χ its anti-potential function, then the threshold in cost variation between an old and a new version of a program can be approximated by ϕnew - χold.</p>\n<p>As a concrete example, consider the two versions of the program below, where lines in yellow model the cost, text in red is the code that is removed, and text in green is the code that is added. This program encodes a common join operation over two sequences, with an operator f having some cost per pair of elements.</p>\n<p>The formulas in boxes are, respectively, the values of the anti-potential and the potential functions. For instance, the anti-potential value in the box labeled ℓ0 encodes the fact that the cost to terminate the program is at least equal to the product of the size of the two sequences. As a result, the difference between ϕnew and χold is lenB ⋅ lenA, which is the desired threshold.</p>\n<p><img src=\"https://dev-media.amazoncloud.cn/2e5242c9ee754c03a0fe8cf46ef1f46d_%E4%B8%8B%E8%BD%BD.jpg\" alt=\"下载.jpg\" /></p>\n<p>In the paper, we show that it is possible to compute both ϕ and χ by working with polynomial expressions over program variables at each program location, as shown in the example above. We represent the program versions as transition systems, a model of computation that consists of a set of program states and a set of valid transitions between states. We assume that the transition systems terminate — i.e., there’s no input that will cause them to run forever.</p>\n<p>We fix a symbolic variable for the threshold t, and by traversing the two transition systems, we obtain a system of constraints that can be solved to obtain concrete values for the threshold and for the potential functions.</p>\n<h4><a id=\"Constraint_satisfaction_38\"></a><strong>Constraint satisfaction</strong></h4>\n<p>A key aspect of our approach is obtaining a simultaneous system of constraints for both the potential function of the new program version and the anti-potential function of the old program.</p>\n<p>Unfortunately, the resulting system of constraints is hard to solve, as it involves universal quantifiers and polynomial constraints over variables. We solve it by employing the results of <ins><a href=\"https://en.wikipedia.org/wiki/Positive_polynomial\" target=\"_blank\">Handelman’s theorem</a></ins> to convert these constraints into a system of purely existentially quantified linear constraints. That is, we convert constraints of the form “for all X’s, P(X)” (a universal quantifier) to constraints of the form “there exist X’s such that Q(X)” (an existential quantifier), where Q is linear, meaning its variables are not squared, cubed, etc.</p>\n<p>Such systems of constraints can be solved efficiently via an off-the-shelf linear-programming solver. This constraint representation has the additional benefit of enabling either the verification of a symbolic threshold or the optimization of a concrete one, which results in a threshold t that is as tight as possible.</p>\n<p>We have validated this approach using 19 benchmarks in C from the current literature. We convert these programs to transition systems, and for 17 of them, we are able to compute a value for the threshold. The threshold is optimal in 14 cases, and more importantly, we can provide a threshold value in less that five seconds in all cases.</p>\n<p>Acknowledgements: Djordje Zikelic, <ins><a href=\"https://www.amazon.science/author/pauline-bolignano\" target=\"_blank\">Pauline Bolignano</a></ins>, Daniel Schoepe, Ilina Stoilkovska.</p>\n<p>ABOUT THE AUTHOR</p>\n<h4><a id=\"Franco_Raimondihttpswwwamazonscienceauthorfrancoraimondi_52\"></a><strong><a href=\"https://www.amazon.science/author/franco-raimondi\" target=\"_blank\">Franco Raimondi</a></strong></h4>\n<p>Franco Raimondi is an Amazon Scholar and a professor of computer science at Middlesex University, London.</p>\n<h4><a id=\"BorYuh_Evan_Changhttpswwwamazonscienceauthorboryuhevanchang_55\"></a><strong><a href=\"https://www.amazon.science/author/bor-yuh-evan-chang\" target=\"_blank\">Bor-Yuh Evan Chang</a></strong></h4>\n<p>Bor-Yuh Evan Chang is an Amazon Scholar and an associate professor of computer science at the University of Colorado Boulder.</p>\n"}