===== LICENSE =====
Our tool is licensed under MIT license (see LICENSE)
It uses Eclipse and its related tools released under Eclipse Public License (see LICENSE.EPL)
It also uses Integer Set Library for polyhedral operations (see LICENSE.ISL)

===== COPY RIGHT =====
Colorado State University, December 2012
Author: Tomofumi Yuki

===== mini-X10 Syntax =====
Program := Program [<List of Program Parameters>] {
   <ArrayDeclaration>+
   <Statement>?
}


Statement := 
   <Loop> |
   <Finish> |
   <Async> |
   <Assignment> |
   <StatementBlock>
   
Loop := for (<Iterator Name>=<AffineExpression>:<AffineExpression>) <Statement>

Finish := finish <Statement>

Async := async <Statement>

Assignment := <ArrayAccess> <Statement Name>(<ArrayAccess>*);

StatementBlock := { <Statement>+ }


List of Program Parameters is a comma delimited list of symbols, which are
treated as program parameters.  Iterator Name is also a symbol, and we require
that all symbol names are unique.  Thus, two separate loop nests cannot share
the same iterator name. (This is purely a restriction of our parser, and not of
our analysis.) AffineExpression may use program parameters and surrounding loop
indices.

====== Usage (Console) =====
java -jar polyX10.jar filepath [options]

Valid options are:
  -d : Enable debug output
  -e : Enable existential quantifier support

The console output includes the input program, with path labels
(discussed in paper) encoded as comments, and DFA results.

===== Usage (Eclipse) =====
You can right click on the file and run our analysis through
"Polyhedral X10 Analyzer" menu item. This invokes the analyzer with both
the options turned off.

You may also call static methods in PolyhedralX10Analyzer class.
See MainClassTest in the test project for how it can be used.

===== Output =====
The output is usually a Quast (Quasi-Affine Solution Tree) that
give instance- and element-wise producer for each read reference.
The analysis result may be accompanied with data-race reports.

For example, "examplePaper1.x10p" produces the following;

[Ambiguous Source] S2(B[k]) has two sources S0[k] and S1[k] at [N] -> {[k] : (k + -1*N = 0) and (-1 + N >= 0)}

Question (S2, B[k]):
   S0[k]
      IF {k|k-1>=0 && -k+2N>=0 && -k+N>=0}
   S1[k]
      IF {k|k-1>=0 && -k+2N>=0 && k-N>=0}

However, there is a case where analysis terminates before computing the full
Quast, since a data-race was already found. When a data-race is found by just
analyzing a pair of read and write statement, we report it as Read-Write Race
and terminate the analysis.  For example, analyzing "examplePaper1.x10p"
produces the following:

[Read-Write Race] S1(A[j]) -> S0 at {j|j>=0 && -j+N>=0}
[DFA Output] DFA results unavailable due to races found in the program.

Existential quantifiers require special handling due to technical reasons.  If
the tool terminates with a RuntimeException reporting some expression is not
affine, it is likely that the support for existential quantifiers is needed.
For example, analyzing "examplePaper3.x10p" without the "-e" option should fail.
Using the option it should produce the following quast:

Question (S2, C[k]):
   S0[k]
      IF [N] -> { [k] : exists (e0 = [(k)/2]: 2e0 = k and k >= 2 and k <= 2N) }
      THEN [N] -> { [k] -> [k'] : 2k' = k and k >= 2 and k <= 2N }
   S1[k]
      IF [N] -> { [k] : exists (e0 = [(-1 + k)/2]: 2e0 = -1 + k and k >= 3 and k <= -1 + 2N) }
      THEN [N] -> { [k] -> [k'] : 2k' = -1 + k and k >= 3 and k <= -1 + 2N }

The IF clause in the above tests for existential quantifiers. The one for S0[k]
tests if k is even (divisible by 2,) and the one for S1[k] tests if k is odd.
The producer for cases when the existential quantifier exists is represented as
a relation in THEN clause.


