Changes between Version 4 and Version 5 of AliasAnalysis

Timestamp:

04/22/16 13:38:49 (10 years ago)

Author:

zmanchun

Comment:

--

AliasAnalysis

@@ -29 +29 @@
 == 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.
+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.
 
 === Example 1 ===
@@ -57 +60 @@
 `O(q, s1)={y}`
 
+and
+`OR(p, s0)={x}`
+`OR(1, 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}`.
 
@@ -65 +72 @@
 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: would like to know p!=q here
+  $wait(p1);
+}
+}}}
+
+case 1: current state `S=(p0:s0', p1:s1)`
 
 
 
+