Practical Machine-Checked Formalization of Change Impact Analysis
CC Attribution 3.0 Germany:
You are free to use, adapt and copy, distribute and transmit the work or content in adapted or unchanged form for any legal purpose as long as the work is attributed to the author in the manner specified by the author or licensor.
Palmskog, Karl
Change impact analysis techniques determine the components affected by a change to a software system, and are used as part of many program analysis techniques and tools, e.g., in regression test selection, build systems, and compilers. The correctness of such analyses usually depends both on domain-specific properties and change impact analysis, and is rarely established formally, which is detrimental to trustworthiness. We present a formalization of change impact analysis with machine-checked proofs of correctness in the Coq proof assistant. Our formal model factors out domain-specific concerns and captures system components and their interrelations in terms of dependency graphs. Using compositionality, we also capture hierarchical impact analysis formally for the first time, which, e.g., can capture when impacted files are used to locate impacted tests inside those files. We refined our verified impact analysis for performance, extracted it to efficient executable OCaml code, and integrated it with a regression test selection tool, one regression proof selection tool, and one build system, replacing their existing impact analyses. We then evaluated the resulting toolchains on several open source projects, and our results show that the toolchains run with only small differences compared to the original running time. We believe our formalization can provide a basis for formally proving domain-specific techniques using change impact analysis correct, and our verified code can be integrated with additional tools to increase their reliability.
 Welcome to this presentation for the paper Practical Machine Check Formalization of Change Impact Analysis. I'm Carl and this is joint work with my colleagues Akmet at Facebook and Miloš at UT Austin. Before I tell you about our formalization, let me give you some context for this work. What we're considering is building and testing a software development. In a typical workflow, a programmer submits a diff or a change to a software system through a version control system. The version control system in turn invokes a continuous integration system, which builds the software and performs other tasks such as running tests and other things. Typically, this continuous integration system uses build systems like Make, Bersal, Dune or Cloudmake. Anno may also use regression test selection tools like Ecstasy and Starts. The key point of using these kinds of tools is to scale over the size of the change rather than the size of the code base. You don't want this to take a really long time just because you have a lot of code. You want it to be because the change was large. One way to deal with this is to perform change impact analysis. We take this as the activity of identifying potential consequences to change the software system. Also, after this analysis, we want to use this information to perform fewer tasks than we might have to do without this analysis. So we save some effort. This kind of analysis is at the core of a lot of these build systems and tools. Usually, when you want to reason that your build system, for example, is correct, you will have to reason both about the domain you're applying it to, and also the general parts of change impact analysis. The question we asked in this work was whether we could separate out the reasoning on the change impact analysis so that this can be done once and for all, and then a domain expert can solve the other problems, for example, for the Java language where you might do test selection and say that this is correct. Our contribution is that we present this form of model of change impact analysis, and this is done in the Cookproof system. So we provide a library of definitions and proofs. And from this code in Cook, we also produce a verified tool called chip, and then we evaluated chip by integrating it with building and testing tools. And so now we're getting to this part where we present our model, and the basic concept in our model is of a component. So a component can be thought of, for example, as a file name, and we think of the set of components before and after a change is enacted to a system. So we call the set of components before v, and then we call it v prime afterwards. And then we have a set of artifacts, and the intuition for this is that this is the content of a file, and this may, of course, change when a change is done. So we track this with two functions called f and f prime that map these components to artifacts before and after the change is made. So and then we have some kind of dependencies between these components, and this is stated by these dependency graphs, g and g prime, and these are just binary relations on these component sets. And then we have some set of checkable components that we can run some operation on. So in this case, we call this operation check, and we assume that it's side effect free. So this might be running a test case or invoking some kind of test running program. And based on this kind of initial concepts, we can define some derived concepts like a modified vertex, and we say that a matrix is modified if the artifact changed. So we can use this by evoking these functions. And then we can define what it means for vertex to be impacted. So this means that it's reachable in the inverse graph. So we sort of take the graph and then we flip all edges, and then we see whether we can reach something from a modified vertex, and then we say it's impacted. So of course, a modified vertex is going to be impacted. And then finally, we have the set of fresh vertices. So these are vertices that were added in this revision that were not present before. And the key idea here is that when we take this set of both impacted and the fresh vertices, and then run this check on all the executable vertices in the union of these two sets, then we have done all the work required. So that's kind of the main idea here. So let me give you an example here. So here we have a dependency graph on the left-hand side in the before state. And it has six components, out of which two, these five and six are executable. And then we perform a change, namely we change the artifact for this vertex one or this component one. And then we sort of flip the edges of the graph and we see that oh, one, three, and five are actually impacted by this. And then in this case, it was only five that needed to be executed or checked. So all we need to do here is to run check five. So we don't, for example, have to run check six. So we might save a lot of time and money by doing this analysis. Okay. So the correctness, of course, we have formal statements, which I will not show you, but the intuition behind it is this, that if we only execute impact and fresh vertices, this is actually sound and complete. So we are checking precisely the vertices we need to check and all the other things that we did not do have the same results as before. So this, of course, we cannot prove this out of thin air. So we have to assume some kind of sanity properties. So specifically for example, we have this property that the direct dependencies of a vertex are the same in both revisions if the artifact is the same. So if kind of your dependencies or a vertex direct dependency is changed, then you also have to change the vertex. And this is kind of typically what happens in most programming languages. And a vertex with the same artifact in both revisions is checkable in both revisions, checkable in new revisions, if and only if it's checkable in the older revisions. So basically you can turn something into a checkable vertex or non-checkable vertex if it was checkable without changing the artifact. So this is again, sanity property. And finally, we have that outcome of executing a checkable vertices is the same in both revisions if everything kind of in the closure is the same. And this, of course, does not hold in practice sometimes. For example, if you run a test two times with exactly the same system, it might return different salt because of non-determinism and so on. Your test is flaky. So every, we assume that this does not happen. So this sort of key assumption to prove correctness. Now we're moving to a hierarchical analysis. So and usually this is when you run make, this is what you usually have in mind. So you have a set of coarse-grained components or files in this case. And then these are connected inside these files or some kind of fine-grained components like methods or other kinds of structures. And the files, of course, are somehow contained in or the methods are contained in these files. So our model sort of extends to this by we have these now two sets of components. And one is the coarse-grained set, one is the fine-grained set. And then there's a partition from the coarse-grained to the fine-grained ones. So and then, of course, we have two dependency graphs. And we have, we can use the graph to analyze the components V and the graph, this key bottom here. So we have two key strategies to do this. We have the over-approximation strategy, which is kind of running everything in, we sort of figure out which files have been impacted and then we sort of execute everything inside those files regardless of whether that changed. And this is sort of what makes us or typically what makes us. And then we have the compositional strategy where we're a little bit more clever. So we sort of do this, we find the impacted vertices in this U set. And then we sort of figure out a subgraph on the V set. And then we perform change-effect analysis in this subgraph. And then we can sort of avoid running check on these these kind of fine-grained components that did not change while getting some kind of boost from our analysis of the U sets. And the correctness is the same here as essentially the same here as for the basic model. And of course, there are some assumptions here that are kind of sanity properties on this partitioning. So for example, if we have two different coarse-grained components and there are two fine-grained components that live in each of these and they are related, then of course the coarse-grained components have to be related as well. So this is again, if you're using file system analogy, this would absolutely hold. And you also have that if these functions for the coarse-grained, if the artifacts for the coarse-grained sets are the same, then they have the same partitioning. So again, this would absolutely hold in a file system world, but maybe not in other domains. And finally, if you have the same artifacts for the coarse-grained sets, and then you, for all of the things inside this coarse-grained component, then they have to be unchanged as well. So you can't have a method that's changed when the file is unchanged, for example. And let me give you some idea of what the encoding code is. So I want to give you too many details, but it's around two thin lines of specification and five thousand lines of proofs. And it uses finite sets and graphs. And the definitions are quite similar to what I just show you in terms of all sets and so on. But you have some notations like connect here, which is transducer closure. That's a little bit different. And we use some kind of predicate here to define whether something is fresh or not. And this is the union operator. And to evaluate our formalization, so again, we prove these things under the assumption. So now we extracted some executable code from this, and we defined a general interface and the tool called chip. And then we integrated chip with three tools. So one regression testing tool, one regression proof selection, one regression test selection tool, one regression proof selection tool, and a build tool. Just to kind of show, to cover all bases. And then we compare the results and the time taken to run chip, the tool with the chip and without chip on a bunch of projects. So here is the list of projects we use. For example, here we use a set of Java projects for Ecstasy, which is a Java tool. And it's quite big projects. You can see URLs here on GitHub. And then for Coq, we used three quite big projects, or at least three big projects and one smaller one. And for the build system top, we used these projects, which used top as a build system. We used a bunch of revisions to run chip on. And here you can see the results for Ecstasy and chip. So you can see that the time increases a bit. So we went, for example, here from 188.67 seconds to about 195 seconds. So a bit slower. And you can see the change of the analysis time also went up a bit. But the results were actually all the same. So we selected the exact same things. So this was some kind of validation. And overall, the time was not that much worse. So we did not have to pay too much to get the verified components. And here are the results for ICOC, the regression proof selection tool and chip. And again, we have the story where we increase a bit in the time and sometimes a bit more. But overall, the results were the same and the increase was not, in most cases, not too bad. And finally, we have the build system. And here we have quite small changes in most. So here we only report the change impact analysis time. You can see that the changes were quite small. In most cases, this is milliseconds. But the results were all the same. So in conclusion, we represented this conversation of change impact analysis using the code persistent. And we integrated, we took a verified code, integrated it with build and test tools. And we sort of validated that in some sense that this model is capturing something that we think it is. And we provide all the code on GitHub. And feel free to ask questions after the presentation. Also feel free to contact me or open issues on GitHub if you have questions specifically about, for example, the COC code, which I did not go into detail all that much.
 Welcome to this presentation for the paper Practical Machine Check  Formalization of Change Impact Analysis.  I'm Carl and this is joint work with my colleagues Akmet at Facebook and Miloš at UT Austin.  Before I tell you about our formalization,  let me give you some context for this work.  What we're considering is building and testing a software development.  In a typical workflow, a programmer submits a diff or a change to  a software system through a version control system.  The version control system in turn invokes a continuous integration system,  which builds the software and performs other tasks such as running tests and other things.  Typically, this continuous integration system uses build systems like  Make, Bersal, Dune or Cloudmake.  Anno may also use regression test selection tools like Ecstasy and Starts.  The key point of using these kinds of tools is to scale over  the size of the change rather than the size of the code base.  You don't want this to take a really long time just because you have a lot of code.  You want it to be because the change was large.  One way to deal with this is to perform change impact analysis.  We take this as the activity of  identifying potential consequences to change the software system.  Also, after this analysis,  we want to use this information to perform fewer tasks  than we might have to do without this analysis.  So we save some effort.  This kind of analysis is at the core of a lot of these build systems and tools.  Usually, when you want to reason that your build system, for example, is correct,  you will have to reason both about the domain you're applying it to,  and also the general parts of change impact analysis.  The question we asked in this work was whether we could separate out  the reasoning on the change impact analysis so that this can be done once and for all,  and then a domain expert can solve the other problems,  for example, for the Java language where you might do test selection and say that this is correct.  Our contribution is that we present this form of model of change impact analysis,  and this is done in the Cookproof system.  So we provide a library of definitions and proofs.  And from this code in Cook, we also produce a verified tool called chip,  and then we evaluated chip by integrating it with building and testing tools.  And so now we're getting to this part where we present our model,  and the basic concept in our model is of a component.  So a component can be thought of, for example, as a file name,  and we think of the set of components before and after a change is enacted to a system.  So we call the set of components before v, and then we call it v prime afterwards.  And then we have a set of artifacts, and the intuition for this is that this is the content of a file,  and this may, of course, change when a change is done.  So we track this with two functions called f and f prime that map these components  to artifacts before and after the change is made.  So and then we have some kind of dependencies between these components,  and this is stated by these dependency graphs, g and g prime,  and these are just binary relations on these component sets.  And then we have some set of checkable components that we can run some operation on.  So in this case, we call this operation check, and we assume that it's side effect free.  So this might be running a test case or invoking some kind of test running program.  And based on this kind of initial concepts, we can define some derived concepts  like a modified vertex, and we say that a matrix is modified if the artifact changed.  So we can use this by evoking these functions.  And then we can define what it means for vertex to be impacted.  So this means that it's reachable in the inverse graph.  So we sort of take the graph and then we flip all edges,  and then we see whether we can reach something from a modified vertex,  and then we say it's impacted. So of course, a modified vertex is going to be impacted.  And then finally, we have the set of fresh vertices.  So these are vertices that were added in this revision that were not present before.  And the key idea here is that when we take this set of both impacted and the fresh vertices,  and then run this check on all the executable vertices in the union of these two sets,  then we have done all the work required. So that's kind of the main idea here.  So let me give you an example here. So here we have a dependency graph on the left-hand side  in the before state. And it has six components, out of which two, these five and six are executable.  And then we perform a change, namely we change the artifact for this vertex one or this component one.  And then we sort of flip the edges of the graph and we see that oh, one, three, and five are actually  impacted by this. And then in this case, it was only five that needed to be executed or checked.  So all we need to do here is to run check five. So we don't, for example, have to run check six.  So we might save a lot of time and money by doing this analysis. Okay. So the correctness,  of course, we have formal statements, which I will not show you, but the intuition behind it is this,  that if we only execute impact and fresh vertices, this is actually sound and complete.  So we are checking precisely the vertices we need to check and all the other things that we did not do  have the same results as before. So this, of course, we cannot prove this out of thin air.  So we have to assume some kind of sanity properties. So specifically for example,  we have this property that the direct dependencies of a vertex are the same in both revisions if the  artifact is the same. So if kind of your dependencies or a vertex direct dependency is changed,  then you also have to change the vertex. And this is kind of typically what happens in most  programming languages. And a vertex with the same artifact in both revisions is checkable in  both revisions, checkable in new revisions, if and only if it's checkable in the older revisions. So  basically you can turn something into a checkable vertex or non-checkable vertex if it was checkable  without changing the artifact. So this is again, sanity property. And finally, we have that outcome  of executing a checkable vertices is the same in both revisions if everything kind of in the  closure is the same. And this, of course, does not hold in practice sometimes. For example, if you  run a test two times with exactly the same system, it might return different salt because of  non-determinism and so on. Your test is flaky. So every, we assume that this does not happen.  So this sort of key assumption to prove correctness. Now we're moving to a hierarchical analysis.  So and usually this is when you run make, this is what you usually have in mind. So you have a set of  coarse-grained components or files in this case. And then these are connected inside these files or  some kind of fine-grained components like methods or other kinds of structures. And the files, of  course, are somehow contained in or the methods are contained in these files. So our model sort of  extends to this by we have these now two sets of components. And one is the coarse-grained set,  one is the fine-grained set. And then there's a partition from the coarse-grained to the fine-grained  ones. So and then, of course, we have two dependency graphs. And we have, we can use the  graph to analyze the components V and the graph, this key bottom here. So we have two key strategies  to do this. We have the over-approximation strategy, which is kind of running everything in, we sort  of figure out which files have been impacted and then we sort of execute everything inside those  files regardless of whether that changed. And this is sort of what makes us or typically what  makes us. And then we have the compositional strategy where we're a little bit more clever.  So we sort of do this, we find the impacted vertices in this U set. And then we sort of figure out  a subgraph on the V set. And then we perform change-effect analysis in this subgraph. And then  we can sort of avoid running check on these these kind of fine-grained components that did not change  while getting some kind of boost from our analysis of the U sets. And the correctness is the same  here as essentially the same here as for the basic model. And of course, there are some assumptions  here that are kind of sanity properties on this partitioning. So for example, if we  have two different coarse-grained components and there are two fine-grained components that  live in each of these and they are related, then of course the coarse-grained components have to  be related as well. So this is again, if you're using file system analogy, this would absolutely  hold. And you also have that if these functions for the coarse-grained, if the artifacts for  the coarse-grained sets are the same, then they have the same partitioning. So again,  this would absolutely hold in a file system world, but maybe not in other domains. And finally,  if you have the same artifacts for the coarse-grained sets, and then you, for all of the things  inside this coarse-grained component, then they have to be unchanged as well. So you can't have  a method that's changed when the file is unchanged, for example. And let me give you some idea of  what the encoding code is. So I want to give you too many details, but it's around two  thin lines of specification and five thousand lines of proofs. And it uses finite sets and graphs.  And the definitions are quite similar to what I just show you in terms of all sets and so on.  But you have some notations like connect here, which is transducer closure. That's a little bit  different. And we use some kind of predicate here to define whether something is fresh or not.  And this is the union operator. And to evaluate our formalization, so again, we prove these things  under the assumption. So now we extracted some executable code from this, and we defined a  general interface and the tool called chip. And then we integrated chip with three tools. So one  regression testing tool, one regression proof selection, one regression test selection tool,  one regression proof selection tool, and a build tool. Just to kind of show, to cover all bases.  And then we compare the results and the time taken to run chip, the tool with the chip and  without chip on a bunch of projects. So here is the list of projects we use. For example,  here we use a set of Java projects for Ecstasy, which is a Java tool. And it's quite big projects.  You can see URLs here on GitHub. And then for Coq, we used three quite big projects, or at least  three big projects and one smaller one. And for the build system top, we used these projects,  which used top as a build system. We used a bunch of revisions to run chip on.  And here you can see the results for Ecstasy and chip. So you can see that the time increases a  bit. So we went, for example, here from 188.67 seconds to about 195 seconds. So a bit slower.  And you can see the change of the analysis time also went up a bit. But the results were actually  all the same. So we selected the exact same things. So this was some kind of validation.  And overall, the time was not that much worse. So we did not have to pay too much to get the  verified components. And here are the results for ICOC, the regression proof selection tool  and chip. And again, we have the story where we increase a bit in the time and sometimes a bit  more. But overall, the results were the same and the increase was not, in most cases, not too bad.  And finally, we have the build system. And here we have quite small changes in most. So here we  only report the change impact analysis time. You can see that the changes were quite small.  In most cases, this is milliseconds. But the results were all the same.  So in conclusion, we represented this conversation of change impact analysis using the  code persistent. And we integrated, we took a verified code, integrated it with build and test  tools. And we sort of validated that in some sense that this model is capturing something  that we think it is. And we provide all the code on GitHub. And feel free to ask questions  after the presentation. Also feel free to contact me or open issues on GitHub if you have  questions specifically about, for example, the COC code, which I did not go into detail all that  much.
604907f51a80aac83ca25da4_0_419.png 604907f51a80aac83ca25da4_420_2075.png 604907f51a80aac83ca25da4_2076_2255.png 604907f51a80aac83ca25da4_2256_2303.png 604907f51a80aac83ca25da4_2304_3035.png 604907f51a80aac83ca25da4_3036_3755.png 604907f51a80aac83ca25da4_3756_3815.png 604907f51a80aac83ca25da4_3816_3887.png 604907f51a80aac83ca25da4_3888_4487.png 604907f51a80aac83ca25da4_4488_6539.png 604907f51a80aac83ca25da4_6540_6995.png 604907f51a80aac83ca25da4_6996_7511.png 604907f51a80aac83ca25da4_7512_8231.png 604907f51a80aac83ca25da4_8232_9347.png 604907f51a80aac83ca25da4_9348_10079.png 604907f51a80aac83ca25da4_10080_10619.png 604907f51a80aac83ca25da4_10620_11891.png 604907f51a80aac83ca25da4_11892_12635.png 604907f51a80aac83ca25da4_12636_13631.png 604907f51a80aac83ca25da4_13632_14183.png 604907f51a80aac83ca25da4_14184_15179.png 604907f51a80aac83ca25da4_15180_15227.png 604907f51a80aac83ca25da4_15228_16379.png 604907f51a80aac83ca25da4_16380_16943.png 604907f51a80aac83ca25da4_16944_17927.png 604907f51a80aac83ca25da4_17928_18971.png 604907f51a80aac83ca25da4_18972_19823.png 604907f51a80aac83ca25da4_19824_21107.png 604907f51a80aac83ca25da4_21108_21407.png 604907f51a80aac83ca25da4_21408_21623.png 604907f51a80aac83ca25da4_21624_22619.png 604907f51a80aac83ca25da4_22620_22640.png