Changes between Version 3 and Version 4 of AliasAnalysis

Timestamp:

04/22/16 13:29:43 (10 years ago)

Author:

zmanchun

Comment:

--

AliasAnalysis

@@ -2 +2 @@
 
 Goal: help POR to be more precise
+
+Concepts:
+
+Assume that all statements are "atomic" actions, for simplicity.
+
+dyscope: a dynamic instance of a lexical scope, with values assigned to each variable declared in the lexical scope
+
+call frame: a call frame contains a function and a location of the function (and the corresponding dyscope of the location can be obtained)
+
+call stack: a stack of call frames
+
+process: the state of a process includes its call stacks and its current program location (and thus the current dyscope)
+
+state: a state contains a dyscope tree and a number of processes
+
+independent statements: two statements `s1` and `s2` are said to be independent if for any state `S` where `s1` and `s2` are enabled, 
+1. `s2` is still enabled in `exec(S, s1)` and vice versa; and
+2. `exec(exec(S, s1), s2) = exec(exec(S, s2), s1) `
+where `exec(S, s)` denotes the state resulted by executing statement `s` at state `S`.
+Two independent statements commute.
+
+ample set: a set of processes at a certain state such that for all processes not in the ample set, all their reachable statements commute with any enabled statement of any process in the ample set
+
+The key of the POR is to find out the minimal ample set for a state. Usually, the dependency of statements 
 
 == Examples ==
@@ -18 +42 @@
 
 int main() {
-  int *p = &x;
+  int *p = &x;//s0'
 
   $proc p1 = $spawn f(&y);
@@ -36 +60 @@
 
 In fact, the ample set of any reachable state of this program is always `{p0}` and `{p1}`.
-
+For example, if the current state is `S=(p0: s0', p1: s1)`, the POR algorithm looks at all reachable statements of `p0` and finds that `OR(p0, s0')` is `{x}` and similarly `OR(p1, s1)` is `{y}`, thus the `{p0}` or `{p1}` is an ample set.
 
 === Example 2 ===
@@ -44 +68 @@
 
 
-