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}.