= Alias Analysis =

Goal: help POR to be more precise

== Examples ==

Let `s` be a statement, and `p` be a pointer, let `O(p, s)` be the set of objects that `p` may alias to at the location where `s` may be enabled. 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, we ignore the value of variables here and assume that the execution of each process is always deterministic.

=== Example 1 ===

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

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

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

  $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 result of statements `s0` and `s1` would be:

`O(p, s0)={x}`
`O(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}`.