| 5 | | Concepts: |
| | 5 | 1. statically determine whether a statement is “purely local”: in any execution of that statement by a process p, no process q other than p can read/write the memory locations accessed by the statement or its guard |
| | 6 | |
| | 7 | 2. something to do with POR: given state s, and process p, determine whether there is an execution from s in which some other process q reads or writes to one of the memory locations p is about to access. Perhaps some sort of dynamic/static analysis. |
| | 8 | |
| | 9 | 3. statically: given any two statements (which might be the same statement), produce a boolean expression which, if it evaluates to true, means that if the statements are executed by two different threads/processes then they will be independent. |
| | 10 | |
| | 11 | notes from Matt based on experience with OpenMP loop independence analysis: |
| | 12 | |
| | 13 | 1) Proving that two array variables are “disjoint". I think this is more subtle than simply determining that the base addresses |
| | 14 | of the arrays are different, i.e., that they are not aliased. What is really wanted is to determine for array vars a and b, something like: |
| | 15 | (a != b) && |
| | 16 | (a < b \implies a+length(a) < b) && |
| | 17 | (b < a \implies b+length(b) < a) |
| | 18 | The problem is that one might not be able to easily capture the length in all cases. For most of the OpenMP loops I have seen |
| | 19 | it is easy to do and once one enters the loop nest there are no redefinitions of a and b, so the common case is not so bad. |
| | 20 | |
| | 21 | You need this in cases where the arrays are passed as parameters which is common, so this is pretty important and it makes |
| | 22 | this an inter-procedural analysis. |
| | 23 | |
| | 24 | 2) A workaround to avoid an inter-procedural analysis is to simply embed the above test into the model and then optimize the |
| | 25 | OpenMP loop nest if the test passes. This is the genesis of the idea of computing the non-aliasing condition if it is impossible |
| | 26 | to actually perform the aliasing. |
| | 27 | |
| | 28 | The generalization is an interesting direction, I think, and it would be good to see whether Hal agrees. The idea here would be |
| | 29 | that rather then simply performing an alias analysis, instead you perform an alias analysis and compute some additional information |
| | 30 | on the side so that you when you ask: |
| | 31 | can p1 and p2 point to the same address? |
| | 32 | it can answer: |
| | 33 | yes |
| | 34 | no |
| | 35 | maybe, but then give you a predicate that can be evaluated at run-time to give the definitive answer |
| | 36 | |
| | 37 | Note that the yes and no here are sound here. |
| | 38 | |
| | 39 | |
| | 40 | == Some Background of POR == |