[Javapathfinder-svn] SF.net SVN: javapathfinder:[1898] branches/mango/Mango/Mango/src/mango

[<fra...@us...>]

Revision: 1898
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1898&view=rev
Author:   frankrimlinger
Date:     2009-09-09 04:52:43 +0000 (Wed, 09 Sep 2009)

Log Message:
-----------
Blowups introduce an interesting complication.  A blowup component has two special vertices, alpha and omega.  Every path from alpha to omega is a case of the blown up loop.  What stratification buys you in MangoBasline is a means of detecting and bundling all these cases into a single predicate transformer, which the rewriter must then disentangle.  But in Mango, jpf is supposed to be in charge.

Mathematically, the "methods" and "loops" dichotomy is unnatural.  The natural object is the component graph, and the issue is to compute universal connector predicate transformers at component sources in terms of the place-holders at component sinks.  This is the function that stratification performed at a high level of abstraction, without actually interpreting the individual instructions.  The rewriter then had to struggle heroically to open up interpretations in a sensible order in order to give the user some hope of understanding and moderating the process.  

The rewriter is now relieved of this responsibility, but now it falls to jpf to execute the paths in an order that makes sense to the user.  The really nice thing about this is that jpf is on the outside looking in, and gets to see the whole graph at once, whereas the rewriter is unable to see the forest for the trees.

So what exactly is the "looking from the outside in" algorithm.  First, component sources are categorized as 

method entrypoint
component entrypoint
alpha

Component sinks are categorized as

method exit
component exit
omega

In this context, innermost loop graphs are just linear graphs beginning with alpha and ending with omega.  The loop subdivision algorithm makes the following guarantees:

1. A component either has exactly one alpha and one omega vertex, or it has no alpha or omega vertex.  
2. No edge enters alpha, no edge leaves omega.
3. A "connector" entering a component entrypoint has its source in a more dependent component. Likewise, an connector exiting a component exit has a destination is a less dependent graph.  In otherwise, the "total graph" of subgraphs and connectors is acyclic.
4. The paths from an alpha to an omega within the total graph are actually contained within the component containing alpha and omega, and constitute the case of the corresponding loop.
5. Now consider the quotient of the total graph obtained by identifying alpha and omega pairs.  The paths in this graph from method entrypoint to method exit points which contain no loop case are the cases for the method.  Such a path will contain an alpha-omega vertex exactly once or not at all (i.e. because the loop is inside another loop).  Likewise, the paths from alpha-omega to itself which comprise the loop cases will meet other alpha-omega vertices exactly once or not at all.   The predicate transformer for the alpha-omega vertex is the recursive function corresponding to the loop, which must be punched in when executing a path through alpha-omega for some less dependent loop or method.

Having stated these facts, the algorithm for jpf is now clear.
1. get a most dependent component containing an alpha omega pair, if none, go to 4
2. execute the paths from alpha to omega, and specify the loop.
3. go to 1
4. execute the paths from method entrypoint to method exit points, crossing over connectors as needed.  At this point, jpf no longer needs to respect the component boundaries.  When all paths are specified, on to the next method.

One final point, in full generality, method must be replaced by "co-recursive system of methods" and in this context there could be multiple entry points.

OK, need to sleep on this and do some engineering to get jpf up to speed on the search strategy and the various activities that must occur at the special times.

Modified Paths:
--------------
    branches/mango/Mango/Mango/src/mango/graph/data/supervertex/SuperLoopData.java
    branches/mango/Mango/Mango/src/mango/worker/mangoModel/BackupAlg.java
    branches/mango/Mango/Mango/src/mango/worker/mangoModel/graph/LoopGraph.java
    branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/superVertex/SuperLoopSym.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.