= Alias Analysis =

Goal:

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

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.

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.

notes from Matt based on experience with OpenMP loop independence analysis:

1) Proving that two array variables are “disjoint".  I think this is more subtle than simply determining that the base addresses 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:
          (a != b) &&
          (a < b \implies a+length(a) < b) &&
          (b < a \implies b+length(b) < a)
    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 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.

    You need this in cases where the arrays are passed as parameters which is common, so this is pretty important and it makes this an inter-procedural analysis.

2) A workaround to avoid an inter-procedural analysis is to simply embed the above test into the model and then optimize the OpenMP loop nest if the test passes.    This is the genesis of the idea of computing the non-aliasing condition if it is impossible to actually perform the aliasing.

    The generalization is an interesting direction, I think, and it would be good to see whether Hal agrees.   The idea here would be that rather then simply performing an alias analysis, instead you perform an alias analysis and compute some additional information on the side so that you when you ask: can p1 and p2 point to the same address?
    it can answer:\\
        yes\\
        no\\
        maybe, but then give you a predicate that can be evaluated at run-time to give the definitive answer\\

    Note that the yes and no here are sound here.


== Examples ==

Assume that all statements are "atomic" actions, for simplicity.

dyscope: a dynamic instance of a lexical scope, with values assigned to each variable declared in the lexical scope

call frame: a call frame contains a function and a location of the function (and the corresponding dyscope of the location can be obtained)

call stack: a stack of call frames

process: the state of a process includes its call stacks and its current program location (and thus the current dyscope)

state: a state contains a dyscope tree and a number of processes

independent statements: two statements `s1` and `s2` are said to be independent if for any state `S` where `s1` and `s2` are enabled, 
1. `s2` is still enabled in `exec(S, s1)` and vice versa; and
2. `exec(exec(S, s1), s2) = exec(exec(S, s2), s1) `
where `exec(S, s)` denotes the state resulted by executing statement `s` at state `S`.
Two independent statements commute.

ample set: a set of processes at a certain state such that for all processes not in the ample set, all their reachable statements commute with any enabled statement of any process in the ample set

The key of the POR is to find out the minimal ample set for a state. Usually, the dependency of statements 


Let `s` be a statement, and `p` be a pointer, let `L(s)` be the source location of `s`, let `O(p, s)` be the set of objects that `p` may alias to at `L(s)`.\\
Let `LR(s)` be the set of locations reachable from `s`, let `OR(p, s)` be the set of objects that `p` may alias to at any location of `LR(s)`. \\
Note that each statement has a unique source location.\\
Let a state `S` be a tuple `(p0: s0, p1: s1, ...)`, which contains the statement that maybe enabled for each process. \\
For simplicity, the dyscope tree and the call stacks are omitted and we assume that the execution of each process is always deterministic.\\
Let `AMP(S)` be the set of possible ample sets of `S`.


=== Example 1: decides purely local statements statically ===

{{{
int x=0, y=0;

void f(int *q) {
  *q = 1; //s1: would like to know p!=q here
}

int main() {
  int *p = &x;//s0'

  $proc p1 = $spawn f(&y);
  *p = 99; //s0: would like to know p!=q here
  $wait(p1);
}
}}}

Suppose `p0` is the process executes the main function, and `p1` is the spawned process that executes `f`.

Then the alias analysis result of statements `s0` and `s1` would be:

`O(p, s0)={x}`
`O(q, s1)={y}`

and
`OR(p, s0)={x}`
`OR(q, s1)={y}`

Suppose the current state is `S=(p0: s0, p1:s1)`, i.e., the enable statement of `p0` and `p1` is `s0` and `s1`, respectively. Since we know **statically** that `O(p, s0)` never intersect with `O(q, s1)`, then we know that `s0` and `s1` commute. So the ample set at `S` is either `{p0}` or `{p1}`.

In fact, the ample set of any reachable state of this program is always `{p0}` and `{p1}`.
For example, if the current state is `S=(p0: s0', p1: s1)`, the POR algorithm looks at all reachable statements of `p0` and finds that `OR(p0, s0')` is `{x}` and similarly `OR(p1, s1)` is `{y}`, thus the `{p0}` or `{p1}` is an ample set.

=== Example 2 ===
Now let's look at a more complicated example which is obtained by modifying **Example 1**.

{{{
int x=0, y=0;

void f(int *q) {
  *q = 1; //s1: would like to know p!=q here
  q = &x; //s2
  *q = 1; //s3
}

int main() {
  int *p = &x;//s0'

  $proc p1 = $spawn f(&y);
  *p = 99; //s0
  $wait(p1);
}
}}}

alias analysis result:

`O(p, s0')={}`\\
`OR(p, s0')={x}`

`O(p, s0)={x}`\\
`OR(p, s0)={x}`

`O(q, s1)={y}`\\
`OR(q, s1)={x,y}`

`O(q, s2)={y}`//maybe this should be `{}` because the value of `q` is going to be changed and s2 never access the memory unit pointed to by `q`.//\\
`OR(q, s2)={x, y}`//maybe this should be `{x}`//

`O(q, s3)={x}`\\
`OR(q, s3)={x}`

case 1: `S=(p0:s0', p1:s1)`, then we have `AMP(S)={{p0}, {p1}}`.
rationale: `p` is local variable of `p0` and is never aliased, which implies that `{p0}` can be an ample set.
For `{p1}`,  since `OR(q, s1)={x,y}`, and `s0'` only writes to `p`, `{p1}` can be an ample set.

case 2: `S=(p0:s0, p1:s1)`, then `{p1} \in AMP(S)` but not `{p0}`.
The current referenced object of `p1` at `L(s1)` is `y` and `y` can never be aliased by `p0`.

case 3: `S=(p0:s0, p1:s2)`, then `{p1} \in AMP(S)` but not `{p0}`. 

case 4: `S=(p0:s0, p1:s3)`, then `{p0, p1} \in AMP(S)`.

=== Example 3: decides two independent transitions with thread-specific variables ===
process-specific variables: process ID, arguments used when creating the process

{{{
int x,y,z;

void f(int *q){
  *q = 2; // s1
}

int main(){
  int *p=&x;

  $proc p1=$spawn f(&y);
  $proc p2=$spawn f(&z);

  *p=1; //s0
  $wait(p1);
  $wait(p2);  
}
}}}

process-specific variables: `q`, let `vq` be the value of `q` when the process is created

alias analysis result:

`O(p, s0)={x}`\\
`OR(p, s0)={x}`

`O(q, s1)={vq}`\\
`OR(q, s1)={vq}`

let `S=(p0:s0, p1:s1, p2:s1)`, since `vq(p1)=&y`, `vq(p2)=&z`, we can conclude that `AMP(S)={{p0}, {p1}, {p2}}`, i.e., each process forms an ample set at `S`.