2/4/2011
Simultaneous points-to using arrays:
a[1] = p
a[2] = q
*(a[1]) = a[2]
Experiments we want to do:
- Generate witnesses handling dynamic memory with summary nodes
- Generate witnesses handling dynamic memory with non-summary (concrete) nodes
- Check aliasing with or without client
Possible client from Manu : check locals from the same method to see if they are aliased; can be used for optimization
Data to collect for each benchmark:
- number of witnesses
- number of refutations (should be easy to collect)
- number of witnesses of length i (for all i)
- number of witnesses with i mallocs (for all i)
- percent of witnesses that are flow compatible [triaging cost may be too high]
Roles: Sam, Sriram perform experiments, collect and analyze data. Manu, Evan rewrite paper.
Other questions that are interesting, but probably aren't worth looking into because they are too obscure and "pointer analysis-y":
- Explain more formally how program statements like *a=a that lead to simultaneous points-to are "weird"/"contrived" and give intuition for why they are not found in real programs
- What biasing effects might transforming a program to Andersen-style statements have? (for example, with Andersen-style statements, the largest simultaneous points-to set that can occur is of size two, but with multiple dereferences we can have larger simultaneous points-to sets)
Explanation of Angelic Debugging (by Chandra et al., ICSE 2011)
Say you are given a program P with a bug, a failing test case that exposes the bug, and a set of passing test cases. Furthermore, assume the bug can be fixed by changing a single expression e in P to some other expression e’. The problem being solved is to determine a small set of repair candidate expressions R from P such that e is in R. R is useful since it narrows the scope for the programmer searching for a fix.
Angelic debugging computes R as follows. First, for each expression e in P, it is determined if there exists a value v such that replacing e with v causes the failing test to pass. If this condition does not hold, clearly e need not be in R.
Second, for each expression e that passes the first condition, and each passing test input U, let v_U be the value of e when P is run with U (assume no loops / procedures). It is determined for each such U whether there exists a value v_n such that v_n != v_U and P still passes the test with input U when v_n is substituted for e. In essence, this is checking that for each passing test, the value of e can be changed without breaking the test. While it is possible that e can be the correct fix point without satisfying this condition, given a sufficient number of passing tests this becomes less and less likely. The expressions satisfying both conditions are the final set of repair candidates R.
The paper describes how angelic execution is used to do the checks for existence of values and describes an initial evaluation.
1/21/2011
Explaining the lack of refutations with Andersen’s
- taking it further: trying to explain it
- Manu’s conjecture: With Andersen-style statements, if typable with recursive types, then Andersen’s precise
-Hack CIL so it does not separate multiple dereferences (test Chakavarti [sp?] paper) OR aliases
-Throw out dynamic memory, introduction to witnesses
-Paper is about an experiment to determine if Andersen’s is precise in practice
Witnesses for Abstract Interpretation
-Deal with imprecision of join and widening
-Deal with imprecision in abstract domain
Semantic slice-universe of everything than can be involved in that bug
-isolate statements that modify the properties you are interested in
-Rival Understanding the Sources of Alarms in Astree
-Rajamani
-Sriram’s POPL’10 bibliography
-Angelic Debugging
Examples where tools will give a horrible explanation but a simpler explanation (ie, change 1-2 statements) is possible
1/14/2011
Small refutable example:
a = &b;
a = &c;
*a = a; (refutable b |-> c)
Manu's conjecture: If you have no recursive types (i.e., no cycles) and Andersen-style statements (i.e., no multiple dereference), then Andersen's is precise. If this conjecture is true, can we focus only the recursive parts.
Evan's proposal: Do SSA (say on all locals where address is not taken) to separate out reuse of variables. Then look at points-to set sizes from Andersen's. Will never get refutations for variables split by SSA. Also know that if each variable can only point to one thing, then Andersen's is precise.
SAS paper is about elucidating the why Andersen's seems precise.
Future directions. (1) A practical application like race condition checking, (2) a more generic framework for witness generation (abstract interpretation).
12/3/2010
Dilig et al. OOPSLA'10 paper uses simultaneous points-to
Two directions:
TODO
Informal Meeting Notes:
Region-based pointer analysis (useful for race detection)
Array to do work on, split into n pieces, n threads, one to work on each piece
Threads hit barrier, wait, then join
Need this for graphics, other data-parallel clients
Problem: many races in such applications are benign. Need a way to weed these out
Argument: Does the design of GPU's prevent them from having races altogether if they are used correctly (ie, input data partitioned into disjoint sets)? (Sriram yes vs Manu no, I think)
TODO:
read/look into:
Briding gap between pointer analysis and shape analysis - Alan Deutsch (sp?)
GPU Programming -- communications of the ACM (http://portal.acm.org/citation.cfm?id=1839694)
IBM LiquidMetal -- code in -> {CPU, GPU, FPGA} out (https://researcher.ibm.com/researcher/view_project.php?id=122)
do:
Learn llvm: ocaml bindings, clang, pointer analysis
Ask people in the know about nasty bugs in GPU's--what are they and how can we help them?
Manu's e-mail 10/29/2010
I just wanted to email out thoughts on the experiments we could perform, based on our meeting today. In the flow-insensitive world, two possible queries of interest would be points-to queries and alias queries. Let's assume for simplicity that for each type of query, the pointer(s) have to be variables. These queries can obviously be answered by Andersen's analysis. An open question is, how many points-to / alias relationships reported by Andersen's could be filtered through combinations of the following precisions:
1. reasoning about simultaneous points-to
2. precise reasoning about dynamic memory allocation
3. field sensitivity
4. array sensitivity (i.e., reasoning separately about different array indices)
As of now, we've done an experiment where we checked if 1 is helpful for points-to queries, and found that it is not. Checking other combinations of precision and alias queries would be interesting.
For 2, 3, and 4, one can do a limit study of how much benefit they could possibly introduce by simply treating the corresponding memory as concrete rather than as a summary; clearly, a precise analysis could filter no more than what is filtered by this unsound handling. So, if unsound concretization doesn't yield any filtering, a precise algorithm won't either. Note that some filtering may only occur when precisions are combined; e.g., we may get filtering with both dynamic memory and field sensitivity reasoning, but not with either alone.
In the flow-sensitive world, one can still ask flow-insensitive points-to and alias queries to see if we get any improvement. One could also introduce queries at particular program points, but it seems hard to experiment with this facility without an actual client (unless we have some client-independent way of guessing what program points would be good for raising queries). Also note that we have the weak flow sensitivity (only reasoning about statement order) and a stronger flow sensitivity (adding reasoning about interfering updates).
Anyway, it would be good to see what kind of experiments we can push through by PLDI. Also, I should probably go re-read that client-driven pointer analysis paper to remember what they did along these lines.
Possible directions based on 9/3 meeting: