Differences

This shows you the differences between two versions of the page.

--- tutorial_forward_substitution [2024/09/22 15:03]
sanjay [How to really thoroughly check the very first equational program]
+++ tutorial_forward_substitution [2024/09/26 07:56] (current)
sanjay [How to check more thoroughly]
@@ Line 1: / Line 1: @@
+=====Getting started with Alpha and AlphaZ=====
+Alpha is a polyhedral equational language, and AlphaZ is its "IDE:"  tools to read, write, edit, and analyze Alpha Programs, and also to compile them to executable code.
+=====Your first Alpha program (not hello world)=====
 In this tutorial, which complements Section 1.1 from [[https://www.cs.colostate.edu/~cs560/Fall2015/Lectures/foundations1.pdf | Foundations 1]], we will walk through a simple Alpha program that solves the equation Lx=b where L is a lower triangular matrix with unit diagonals, b is a known vector and x is the unknown vector, using the forward substitution algorithm.  With a little bit of algebraic reasoning, we derived a mathematical identity with x on the left hand side LHS.  We now want to write it as an equational program in Alpha.  You will see that it is surprisingly simple.
-=====Writing Alpha=====
 ====Step 1: Affine System and Parameters ====
 Let's start from an empty alpha file  “forward_sub".ab, in which with “FS" is the name of the system, and a positive integer N as its parameter.
@@ Line 19: / Line 24: @@
 affine FS {N|N>0}
 input // "given" is also a legal keyword for input
-   float L {i,j|1<=j<i<N};
+   float L {i,j|1<=j<i<=N};
    float b {j|1<=j<=N};
 output // or "returns"
@@ Line 161: / Line 166: @@
 ==make verify==
-This only becomes useful if you have a known, correct implementation of the function.  For this first tutorial, it does not make sense (it ends up comparing the outputs of two identical functions).  Later, when you produce different versions using scheduling directives, it becomes useful to validate the correctness agains the original equations,
+This only becomes useful if you have a known, correct implementation of the function.  For this first tutorial, it does not make sense (it ends up comparing the outputs of two identical functions).  Later, when you produce different versions using scheduling directives, it becomes useful to validate the correctness against the original equations,
-Compiles the code with another code named ''xxx_verify.c'' that defines a function ''xxx_verify'' (''xxx'' is the system name).
+Compiles the code with another code named ''xxx_verify.c'' that defines another function with the same signature, ''xxx_verify'' (''xxx'' is the system name).
 Users can provide different programs as ''xxx_verify'' to compare outputs.
 ==make verify-rand==
@@ Line 174: / Line 179: @@
 It idea is to write additional (simpler) equational programs that are easier to verify and trust and use them to build up the verification.  For example, you could first write an Alpha program to multiply a (triangular or otherwise) matrix with a vector, and verify it.  Let's assume that you have done this.
-Then you can extend the FS system itself, to write an additional equation to compute the matrix-vector product of L and x, subtract b from it, and compute the max of the absolute value of all entries of this,  If this is below a certain threshold, then the program is correct  (note that we are using floating point values and there may be roundoff errors).  We can return this in the Boolean variable ''C''.
+Then you can extend the FS system itself, to write an additional equation to compute the matrix-vector product of L and x, subtract b from it,=, v=giving a vector or error values.  Now all we need to do is to check that some given threshold is greater than the absolute values of each all elements of the error  (Alpha does not have an operator abs, so you can use a trick; ''abs(x)'' equals ''max(x, -x)'' of all ''x'').  We can return this in the Boolean variable ''C'' defined as follows.
 <sxh alphabets; gutter:true>
-C = reduce(and, [i], abs(b - reduce(+, [j], L[i,j]*x[j]) < THRESHOLD) ;
+error [i] =
+    case
+        {|i==1}: b[i] - x[i];
+        {|i>1} : b[i] - x[i] - reduce(+, [j], L[i,j]*x[j]);
+	esac;
+C[] = reduce(and, [i], max(error[i], - error[i])<0.000000001);
+      //you may also do a max reduction and/or use a different threshold
 </sxh>
-Actually the above equation has to be corrected, because the (unit) diagonal elements of L are not explicitly stored.  You may want to define/use an auxiliary variables like bp.
+Note how we account for the (unit) diagonal elements of L (which are not explicitly part of the array L.
-But how to provide sufficiently large number of (random) inputs to the code if we don't use the verify option?  The answer is to create a sufficiently large file of rand inputs, and then use file redirection in linux to feed this file to ''xxx_check'' (make sure that the boolean output is either first or last, or even the only one).
-Alpha allows for user-defined operators by declaring them as an external function in the header
 <sxh alphabets; gutter:true>
-float abs (float),
+float abs (float);
 </sxh>
+But how to provide sufficiently large number of (random) inputs to the code if we don't use the verify option?  The answer is to create a sufficiently large file of random inputs, and then use file redirection in linux to feed this file to ''xxx_check'' (make sure that the boolean output is either first or last, or even the only one).

AlphaZ

User Tools

Site Tools

Differences

Page Tools