Differences between version 12 and predecessor to the previous major change of Stage 3 for TM analysis.

Other diffs: Previous Revision, Previous Author

Newer page: version 12 Last edited on February 25, 2007 10:00 pm. by EricBodden
Older page: version 6 Last edited on February 13, 2007 2:49 pm. by EricBodden
@@ -10,8 +10,12 @@
  
 # a state of the TM automaton 
  
 # a mapping from variables to tuples <o,unique,Must,May,~MustNot> 
+  
+!! There seems to be a mistake in the description of the focus operation  
+  
+[Pathological case | Pathological case Fink et al. paper]  
  
 ---- 
  
 !! About their different analyses 
@@ -52,4 +56,39 @@
  
 * *Multithreading* is not handled at all. Hence, we still need a way to at least tell if a disjunct holds possibly shared objects or not. 
  
 * According to Stephen Fink (personal communication with Eric) they use a special join operator: When merging facts A and B and A implies B then A will be the sole result of the merge. 
+  
+----  
+  
+!! Invariant methods  
+  
+[Formal Definition of Invariant Methods]  
+  
+  
+Interestingly, there are, for example, some enumerations which clearly do not escape the method they are created in but apparently context information is not good enough to distinguish them from other enumerations. For those cases we found the following solution. Assume this example:  
+  
+<pre>  
+void foo() {  
+ Enumeration e = v.elements();  
+ while(e.hasMoreElements()) {  
+ Object o = e.nextElement();  
+ }  
+}  
+</pre>  
+  
+Assume the pattern "hasNextElem", i.e. "always call hasNextElem() before nextElement()". Further assume that enumeration e is aliased with enumerations used in other methods due to imprecision. Then we can still decide that the method foo() is "invariant" with respect to the tracematch, because when leaving foo() we are in the initial state configuration, assuming we have local must-alias information and hence can do strong updates. Because we are in this initial configuration, it does not matter what happens after execution foo() so even if e is aliased with something else, we don't have to care. Note however, that it is crucial that we really get back to the initial configuration. For instance in the following case, we would not reach a final state but also *not* end up in the initial configuration...  
+  
+<pre>  
+void foo() {  
+ Enumeration e = v.elements();  
+ Object o = e.nextElement();  
+}  
+</pre>  
+  
+In this case, foo() is *not* invariant and hence we could not rule out the shadows in foo().  
+  
+Determining invariant methods generally means a shift from the shadow-group centric view to a shadow centric view.  
+  
+----  
+  
+!! [Agenda for the conference call Feb 27th]