<html><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; ">
Ted,<div> very interesting...</div><div><br></div><div>when I worked at Sun Microsystems, I invented a generalization to the traditional Iterative-Dataflow-Analysis</div><div>algorithm that might provide a useful way to select within the memory-verses-accuracy tradeoff space.</div><div><br></div><div>-Peter Lawrence.</div><div><br></div><div><br></div><div><br><div><div>On May 19, 2011, at 12:28 PM, <a href="mailto:cfe-dev-request@cs.uiuc.edu">cfe-dev-request@cs.uiuc.edu</a> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><p style="margin: 0.0px 0.0px 0.0px 0.0px; font: 12.0px Monaco; min-height: 16.0px"><br></p> <p style="margin: 0.0px 0.0px 0.0px 0.0px"><font face="Monaco" size="3" style="font: 12.0px Monaco">Hi Lei,</font></p> <p style="margin: 0.0px 0.0px 0.0px 0.0px; font: 12.0px Monaco; min-height: 16.0px"><br></p> <p style="margin: 0.0px 0.0px 0.0px 0.0px"><font face="Monaco" size="3" style="font: 12.0px Monaco">Running out of memory is a real problem that needs a general solution.<span class="Apple-converted-space"> </span>I have been mulling this over myself, and have a few ideas that match with #2 and #3.</font></p> <p style="margin: 0.0px 0.0px 0.0px 0.0px; font: 12.0px Monaco; min-height: 16.0px"><br></p> <p style="margin: 0.0px 0.0px 0.0px 0.0px"><font face="Monaco" size="3" style="font: 12.0px Monaco">Before I get into those, I think it is worth pondering the fact that unless we force the path exploration to combine paths, there will always be cases where we don't exhaustively explore all paths.<span class="Apple-converted-space"> </span>For example, consider the kind of dataflow analysis done in many compiler analyses: paths are always merged at confluence points, guaranteeing convergence and bounding memory usage.<span class="Apple-converted-space"> </span>The path-sensitive analysis doesn't force this kind of convergence (although paths converge when the states are the same), so if you are interested in forcing convergence I think we'll need something else in the analyzer that isn't there right now.</font></p> <p style="margin: 0.0px 0.0px 0.0px 0.0px; font: 12.0px Monaco; min-height: 16.0px"><br></p> <p style="margin: 0.0px 0.0px 0.0px 0.0px"><font face="Monaco" size="3" style="font: 12.0px Monaco">Let's talk about #2.<span class="Apple-converted-space"> </span>Essentially, the wordlist algorithm (which currently is either BFS or DFS) is all about prioritizing what part of the state space gets explored first. My goal is that we eventually have other intelligent algorithms besides BFS and DFS, that allow us to exploit even more information.<span class="Apple-converted-space"> </span>Thus, switching between BFS and DFS to solve this problem isn't the answer.<span class="Apple-converted-space"> </span>Switching between those should help if, say, you want to bound the amount of work done by the analyzer (which we do) and want to prioritize that some types of paths are prioritized over others.<span class="Apple-converted-space"> </span>This may help you find different kinds of bugs more effectively.<span class="Apple-converted-space"> </span>For "all paths" checkers, like yours, BFS will tend to cover paths that end sooner, but it won't explore paths that require going deeper into the state space (like DFS does).<span class="Apple-converted-space"> </span>This will directly impact the results you get from your checker, but those are just tradeoffs in the results.<span class="Apple-converted-space"> </span>It doesn't actually solve the scalability problem.<span class="Apple-converted-space"> </span>If th!</font></p> <p style="margin: 0.0px 0.0px 0.0px 0.0px"><font face="Monaco" size="3" style="font: 12.0px Monaco"><span class="Apple-converted-space"> </span>e number of paths to explore are too costly to enumerate, we are going to run into memory problems regardless.<span class="Apple-converted-space"> </span>Put another way, DFS and BFS are just enumerating paths in a different order.<span class="Apple-converted-space"> </span>The cost to enumerate all of them is the same.</font></p> <p style="margin: 0.0px 0.0px 0.0px 0.0px; font: 12.0px Monaco; min-height: 16.0px"><br></p> <p style="margin: 0.0px 0.0px 0.0px 0.0px"><font face="Monaco" size="3" style="font: 12.0px Monaco">To tackle memory scalability, the direction I have been gradually pushing the analyzer is to have the ability to gradually reclaim ExplodedNodes<span class="Apple-converted-space"> </span>(and states) as the graph grows larger.<span class="Apple-converted-space"> </span>It use to be that we would just generate GRStates, many which would just get thrown away and not included in ExplodedNodes, and not reclaim that memory until we reclaimed all the memory for an analysis.<span class="Apple-converted-space"> </span>Now GRStates are reference counted, so we can reclaim some of the memory more eagerly.<span class="Apple-converted-space"> </span>To take this further, we can possibly prune out parts of the ExplodedGraph as it grows if we can deem those parts "uninteresting."<span class="Apple-converted-space"> </span>I think this is very doable, but it's a lot trickier than it sounds, and it requires consulting which ExplodedNodes are currently referenced by BugReports.<span class="Apple-converted-space"> </span>If we can identify paths that are essentially uninteresting, nor are deemed critical by a checker, then we can potentially throw away those nodes.<span class="Apple-converted-space"> </span>Note that when we do this, we are throwing away analysis state.<span class="Apple-converted-space"> </span>If we th!</font></p> <p style="margin: 0.0px 0.0px 0.0px 0.0px"><font face="Monaco" size="3" style="font: 12.0px Monaco"><span class="Apple-converted-space"> </span>row away a path, only to explore another path that would have merged with the discarded path, we are going to end up analyzing the same path again.<span class="Apple-converted-space"> </span>That's an inherit time-space tradeoff.</font></p> <p style="margin: 0.0px 0.0px 0.0px 0.0px; font: 12.0px Monaco; min-height: 16.0px"><br></p> <p style="margin: 0.0px 0.0px 0.0px 0.0px"><font face="Monaco" size="3" style="font: 12.0px Monaco">So, I think the solution to your problem requires a combination of several approaches:</font></p> <p style="margin: 0.0px 0.0px 0.0px 0.0px; font: 12.0px Monaco; min-height: 16.0px"><br></p> <p style="margin: 0.0px 0.0px 0.0px 0.0px"><font face="Monaco" size="3" style="font: 12.0px Monaco">a) Make path analysis more scalable in general by more eagerly reclaiming memory when the ExplodedGraph starts to get large.<span class="Apple-converted-space"> </span>This is essentially a "garbage collection" of uninteresting paths.</font></p> <p style="margin: 0.0px 0.0px 0.0px 0.0px; font: 12.0px Monaco; min-height: 16.0px"><br></p> <p style="margin: 0.0px 0.0px 0.0px 0.0px"><font face="Monaco" size="3" style="font: 12.0px Monaco">b) Because (a) doesn't completely "solve" the path explosion problem (i.e., it doesn't guarantee that all paths are explored), if exploring all paths matters to you we will need to devise a strategy where we can (optionally) merge paths.<span class="Apple-converted-space"> </span>This requires being able to define a merge operation for everything in GRState, including checker-specific state.<span class="Apple-converted-space"> </span>It will then be up to some policy to decide when the merge takes place, as merging too frequently will cause us to discard too much information (i.e., it basically reduces to a flow-sensitive analysis).</font></p> <p style="margin: 0.0px 0.0px 0.0px 0.0px; font: 12.0px Monaco; min-height: 16.0px"><br></p> <p style="margin: 0.0px 0.0px 0.0px 0.0px"><font face="Monaco" size="3" style="font: 12.0px Monaco">Ted</font></p> <p style="margin: 0.0px 0.0px 0.0px 0.0px"><font face="Monaco" size="3" style="font: 12.0px Monaco">-------------- next part --------------</font></p> </blockquote></div><br></div></body></html>