Changes between Initial Version and Version 1 of AliasAnalysis

Timestamp:

04/22/16 12:20:41 (10 years ago)

Author:

zmanchun

Comment:

--

AliasAnalysis

@@ +1 @@
+= 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}`.
+
+
+
+
+