Changes between Version 12 and Version 13 of AliasAnalysis

Timestamp:

04/26/16 22:15:53 (10 years ago)

Author:

zmanchun

Comment:

--

AliasAnalysis

@@ -33 +33 @@
 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.
+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 ===
+
+=== Example 1: decides purely local statements statically ===
 
 {{{
@@ -118 +120 @@
 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`.
 
 
 
+
+
+
+
+