Remove whitespace errors. (#15)

* Remove whitespace errors. Run `git ls-file | sed -i 's/[[:space:]]*$//'` * x
cucapra · Sep 6, 2018 · de5a4d9 · de5a4d9
1 parent cbb77f4
commit de5a4d9
Show file tree

Hide file tree

Showing 31 changed files with 171 additions and 170 deletions.
diff --git a/.gitignore b/.gitignore
@@ -4,3 +4,4 @@ _build
 seashell.wiki/*
 seashell.install
 out/
+docs/*.pdf
diff --git a/docs/appendix.md b/docs/appendix.md
@@ -5,7 +5,7 @@ title: Appendix
 3-D array examples to visualize multi-dimensional access
 --------------------------------------------------------
 
-##### Example 1 
+##### Example 1
 Consider a three-dimensional array $\text{a}$ defined like this:
 
 $$a:t[2][5][3] \text{ bank} (5)$$
@@ -14,7 +14,7 @@ The flattened version, $\text{a}_f$, would have size $N=30$. Say we make an acce
 
 Note that the banking factor is not used in this example.
 
-##### Example 2a 
+##### Example 2a
 Let's consider an access to the array we considered earlier.
 $$a:t[2][5][3] \text{ bank} (5)$$
 
@@ -28,7 +28,7 @@ $$
 (0 + 1 \times 1) \times 15 + (4 + 5 \times 0) \times 3 + (0 + 1 \times 2) \times 1 = 29
 $$
 
-##### Example 2b 
+##### Example 2b
 Let's try to access the same array as before with the dynamic index set $d=\{1,0,2\}$
 
 From the equation,
@@ -37,7 +37,7 @@ $$
 \{ (s_0 + 1 \times 1) \times 15 + (s_1 + 5 \times 0) \times 3 + (s_2 + 1 \times 2) \times 1 ~|~ s_0 \in 0..1, s_1 \in 0..5, s_2 \in 0..1 \} = \{17,20,23,26,29\}
 $$
 
-##### Example 2c 
+##### Example 2c
 Consider this program:
 
     int a[2][5][3] bank(5)
@@ -64,15 +64,15 @@ Array banking strategies with 3-D example
 
 We are interested in the indices being used to access $\text{a}_f$, so we can restrict the banks that a Seashell programmer can access. However, which banks the programmer accesses is influenced by the array banking strategy. Here are a few ways we could bank $\text{a}_f$.
 
-#### Bank Interleaving 
+#### Bank Interleaving
 We could interleave the elements of $\text{a}_f$ among its banks, like this (each rectangle represents a bank):
 
 | 0 5 10 15 20 25 | 1 6 11 16 21 26 | 2 7 12 17 22 27 | 3 8 13 18 23 28 | 4 9 14 19 24 29 |
 | --- | --- | --- | --- | --- |
 
 Then, given an index $i_f$ into $\text{a}_f$, we could determine the bank being accessed with $i \bmod b$. The index offset into the bank would be $i / b$.
 
-#### Bank Chunking 
+#### Bank Chunking
 We could simply divide $a_f$ into banks, like this:
 
 | 0 1 2 3 4 5 | 6 7 8 9 10 11 | 12 13 14 15 16 17 | 18 19 20 21 22 23 | 24 25 26 27 28 29 |
@@ -82,21 +82,21 @@ Then, we could use $i / b$ to find the relevant bank, and $i \bmod b$ to find th
 
 Both have use cases, but we won't go into those here.
 
-##### Example 3  
+##### Example 3
 Consider the array $a$ defined in example 1. Assume interleaving. If we index into $a_f$ with $i_f=29$, the bank accessed would be $29 \bmod 5 = 4$, and the index into this bank would be $29 / 5 = 5$. In other words, we would access the 5th element in the 4th bank.
 
 2-D array examples to visualize multi-dimensional access
 --------------------------------------------------------
 
 
-##### Example 1 
+##### Example 1
 Consider a two-dimensional array $\text{a}$ defined like this:
 
 $$a:t[4][2] \text{ bank} (4)$$
 
 The flattened version, $\text{a}_f$, would have size $N=8$. Say we make an access $\text{a}[3][1]$. Using our formula we defined, we'd access $\text{a}_f$ with $i_f=7$.
 
-Note that the banking factor is not used.  
+Note that the banking factor is not used.
 
 ##### Example 2.1
 Consider this program:
@@ -188,16 +188,16 @@ Both have use cases, but we won't go into those here. For the remainder of this
 Modulus proof
 -------------
 
-$$ab \bmod ac = ab - \lfloor \frac{ab}{ac} \rfloor ac   
-            = a (b - \lfloor \frac{b}{c} \rfloor c )  
-            = a (b \bmod c)  $$ 
+$$ab \bmod ac = ab - \lfloor \frac{ab}{ac} \rfloor ac
+            = a (b - \lfloor \frac{b}{c} \rfloor c )
+            = a (b \bmod c)  $$
 
 Index type array access proofs
 -------------
 
 **banked array access with unroll factor = banking factor**
 
-where $l > n$   
+where $l > n$
 
     int a[l bank(k)]
     for i in 0..n unroll k
@@ -236,11 +236,11 @@ $$
 \{ 0 .. k \}
 $$
 
-This range shows us that our index type would be accessing all $k$ distinct banks by any access, and we'd never access some non-existent bank or not access an existent bank. Allowing accesses that follow rule (1) would guarantee this access. Rule(2) would disallow any further accesses, preventing banks from being accessed multiple times.  
+This range shows us that our index type would be accessing all $k$ distinct banks by any access, and we'd never access some non-existent bank or not access an existent bank. Allowing accesses that follow rule (1) would guarantee this access. Rule(2) would disallow any further accesses, preventing banks from being accessed multiple times.
 
 **banked array access with unroll factor factor of banking factor**
 
-where $l > n$ and $m \in N$  
+where $l > n$ and $m \in N$
 
     int a[l bank(m*k)]
     for i in 0..n unroll k
@@ -275,11 +275,11 @@ $$
 k (d \bmod m) .. \left( k (d \bmod m) + k \right)
 $$
 
-This range shows us that our index type would be accessing $k$ distinct banks at any time, and we'd never access some non-existent bank. For $d=0$ we'd access $0..k$, and for $d=(m-1)$ we'd access $(mk-k)..mk$. Allowing accesses that follow rule (1) would guarantee this. Then, because we can't know what $d$ is statically, we can follow rule (2) and conservatively disallow any further accesses, preventing banks from being accessed multiple times.  
+This range shows us that our index type would be accessing $k$ distinct banks at any time, and we'd never access some non-existent bank. For $d=0$ we'd access $0..k$, and for $d=(m-1)$ we'd access $(mk-k)..mk$. Allowing accesses that follow rule (1) would guarantee this. Then, because we can't know what $d$ is statically, we can follow rule (2) and conservatively disallow any further accesses, preventing banks from being accessed multiple times.
 
 **banked array access with an unroll factor of 1**
 
-where $l > n$ and $k > 1$  
+where $l > n$ and $k > 1$
 
     int a[l bank(k)]
     for i in 0..n unroll 1
@@ -298,15 +298,15 @@ $$
 \{ ((s \bmod k) + (d \bmod k)) \bmod k ~|~ s \in 0 .. 1 \}
 $$
 
-Since we know that $s$ can take only the value $0$  
+Since we know that $s$ can take only the value $0$
 
 We have:
 
 $$
 \{ d \bmod k \}
 $$
 
-This shows us that our index type would be accessing a single bank at any time, and we'd never access some non-existent bank. For $d=0$ we'd access $0$, and for $d=k-1$ we'd access $k-1$. Allowing accesses that follow rule (1) would allow this. We can follow rule (2) and conservatively disallow any further accesses, preventing banks from being accessed multiple times. But this also limits accessing other banks, which would of course be a safe operation.  
+This shows us that our index type would be accessing a single bank at any time, and we'd never access some non-existent bank. For $d=0$ we'd access $0$, and for $d=k-1$ we'd access $k-1$. Allowing accesses that follow rule (1) would allow this. We can follow rule (2) and conservatively disallow any further accesses, preventing banks from being accessed multiple times. But this also limits accessing other banks, which would of course be a safe operation.
 
 Some basic type rules we depend on
 -----------

diff --git a/docs/hwtute-01.md b/docs/hwtute-01.md
@@ -1,6 +1,6 @@
 vector-vector add on host processor
 --------
 
-Our first attempt will be to create a host program. A host program is a regular program, written with a regular language and running on a general purpose processor. However, general purpose processor are great at running sequential programs. These programs are inherently sequential, so parallel architectures cannot exploit them. ANd general purpose processors are specialized at running these programs fast. It so happens, most control programs are very sequential. And a control program is essential to manage a heterogeneous system. 
+Our first attempt will be to create a host program. A host program is a regular program, written with a regular language and running on a general purpose processor. However, general purpose processor are great at running sequential programs. These programs are inherently sequential, so parallel architectures cannot exploit them. ANd general purpose processors are specialized at running these programs fast. It so happens, most control programs are very sequential. And a control program is essential to manage a heterogeneous system.
 
-We will run a very simple application on our host processor, which would create some arrays, initialize them and send them to a vector-vector add function. Then we can print these values to a 
+We will run a very simple application on our host processor, which would create some arrays, initialize them and send them to a vector-vector add function. Then we can print these values to a
diff --git a/docs/hwtute-intro.md b/docs/hwtute-intro.md
@@ -4,7 +4,7 @@ Tutorial on hardware programming with Seashell
 This tutorial is targeted to introduce hardware programming in high-level languages to C programmers or hardware programmers interested in moving into high level synthesis. This tutorial will use:
  * Seashell, which is a type overlay to ensure hardware safety of your program and porgram synthesis to C/C++
  * Buildbot, which is infrastructure created to submit a seashell program and receive hardware results
- 
+
 Buildbot itself hides away some other tools that can be replaced with different tools,
  * Vivado HLS, which is a C/C++ to Verilog/VHDL translator on top of Vivado synthesis tool flow
  * Xilinx Zedboard SoC development board, which has an arm CPU and a Zync FPGA with memory and interconnections which have some configurability
@@ -16,13 +16,13 @@ Buildbot itself hides away some other tools that can be replaced with different
 
 We'll be going through the following examples to get familiarized with the tools and to use the infrastructure to create interesting programs.
 
-1. [vector-vector add on host processor](hwtute-01.html)  
+1. [vector-vector add on host processor](hwtute-01.html)
    - Run a program on heterogeneous platform host processor
-2. [vector-vector add on reconfigurable hardware controlled by the host processor](hwtute-02.html)  
+2. [vector-vector add on reconfigurable hardware controlled by the host processor](hwtute-02.html)
    - Design and interface hardware module in Buildbot, Familiarize with Seashell, Run a CPU-FPGA program on a heterogeneous platform
-3. [optimized vector-vector add on reconfigurable hardware controlled by the host processor](hwtute-03.html)  
+3. [optimized vector-vector add on reconfigurable hardware controlled by the host processor](hwtute-03.html)
    - Introduce to commonly used hardware optimizations, array partition, loop unroll and pipelining
-4. [matrix multiplication]()  
-   - Usage and optimization of nested loops, Using local variables, 
-5. [convolution]()  
-   - Data transfer methods, Using memory, 
+4. [matrix multiplication]()
+   - Usage and optimization of nested loops, Using local variables,
+5. [convolution]()
+   - Data transfer methods, Using memory,
diff --git a/docs/logicalmemoryaccess.md b/docs/logicalmemoryaccess.md
@@ -4,7 +4,7 @@ title: Logical Memory Accesses
 
 This document describes Seashell's *logical access* expressions, which is to access memories using [index types][it].
 Logical access in Seashell lets programs access the logical structure of an array, even a multidimensional array, while preserving information about the underlying physical banks being accessed.
-The document goes on to introduce a set of sound typing rules that determine whether a bank access during a logical memory access is safe. 
+The document goes on to introduce a set of sound typing rules that determine whether a bank access during a logical memory access is safe.
 
 [it]: indextype.html
 
@@ -29,7 +29,7 @@ $$\tag{1}
 \{ s + |l_s .. h_s| \times d ~|~ s \in l_s .. h_s \}
 $$
 
-Given an array access with our index types, this set representation allows us to precisely identify which indices (and subsequently memory banks) are accessed. 
+Given an array access with our index types, this set representation allows us to precisely identify which indices (and subsequently memory banks) are accessed.
 
 ::: todo
 How does the implicit vs. explicit terminology differ from logical vs. physical? It sounds like it might be the same thing.
@@ -88,7 +88,7 @@ $$
 Consider a two-dimensional array $\text{a}$ defined like this:
 
 $$
-\text{a} : t[4][2] 
+\text{a} : t[4][2]
 $$
 
 The flattened version, $\text{a}_f$, has size $8$.
@@ -108,7 +108,7 @@ Logical Access with Index Types
 -------------------------------
 
 We now consider the meaning of logical accesses using Seashell's index types.
-We want to determine the *set* of elements accessed in an expression of the form 
+We want to determine the *set* of elements accessed in an expression of the form
 $\text{a}[i_0] \dots [i_n]$
 where each $i_j$ is of an index type
 $\text{idx}\langle l_{s_j} .. h_{s_j}, l_{d_j} .. h_{d_j} \rangle$.
@@ -236,7 +236,7 @@ We'll actually define this to mean the division of memory $\text{a}_f$ into $b$
 Note- Change in syntax to bank each dimension would require an update here.
 :::
 
-**Example.** 
+**Example.**
 
     memory a: int[4][2] bank(4)
 
@@ -278,8 +278,8 @@ With the knowledge of which bankes we access, we can expand on how this might be
 One dimensional arrays are a special case of array accesses, but has significance due to actual hardware being one dimensional and multi-dimensional arrays can be expanded to one dimension by the programmer.
 
 $$\tag{5}
-B = \left\{ 
-    ( s + |l_{s}..h_{s}| \times d ) \bmod b ~|~ s \in l_{s}..h_{s} 
+B = \left\{
+    ( s + |l_{s}..h_{s}| \times d ) \bmod b ~|~ s \in l_{s}..h_{s}
     \right\}
 $$
 
@@ -300,13 +300,13 @@ Our attempt now, is to determine the set of banks accessed given the unroll fact
 
 We can write such a loop as follows:
 
-where $~|~ l..h | = n$, $len > n$ and $m \in N$  
+where $~|~ l..h | = n$, $len > n$ and $m \in N$
 
     int a[len bank(m*k)]
     for i in l..h unroll k
         access a[i]
 
-Here, $i$ has type $\text{idx}\langle l_s .. h_s, l_d .. h_d \rangle$. 
+Here, $i$ has type $\text{idx}\langle l_s .. h_s, l_d .. h_d \rangle$.
 
 Since $~|~ l_s .. h_s | = k$ For any $d \in l_d .. h_d$, $\text{i}$ represents:
 
@@ -320,7 +320,7 @@ $$
 \{ s + k * d ~|~ s \in l_s .. h_s \} \bmod m * k
 $$
 
-Using the following expansion with modulus:  
+Using the following expansion with modulus:
 $(a + b) \bmod c =  (a \bmod c + b \bmod c) \bmod c$
 
 $$
@@ -330,7 +330,7 @@ $$
 We know a couple things that help us rewrite this set:
 
   - $~|~ l_s .. h_s | < mk$
-  
+
 Therefore, $s \bmod mk$ is unique
 
   - $kd \bmod mk = k (d \bmod m)$ [proof](https://capra.cs.cornell.edu/seashell/docs/appendix.html#modulus-proof), [image](https://imgur.com/a/9cEQHGr)
@@ -374,7 +374,7 @@ Moved to appendix under basic type rules we need
 --S
 :::
 
-It is evident from this rule, that our type checker is conservative about the design space of safe accesses. Our attempt through this document is to formally prove our accesses are safe, and not derive the complete design space of safe accesses. We hope to convince our index types are rigorous and flexible enough to attempt proofs with other type rules, which would make the type checker gradually less conservative.  
+It is evident from this rule, that our type checker is conservative about the design space of safe accesses. Our attempt through this document is to formally prove our accesses are safe, and not derive the complete design space of safe accesses. We hope to convince our index types are rigorous and flexible enough to attempt proofs with other type rules, which would make the type checker gradually less conservative.
 
 ::: todo
 I'm not 100% sure we need all three of these cases.
@@ -387,11 +387,11 @@ Having three proofs ends up pretty repetitive.
 :::
 
 ::: todo
-b=mk case moved higher, others moved to appendix 
+b=mk case moved higher, others moved to appendix
 --S
 :::
 
-**Note- ** We're operating on a 1-D array, so this set already represents our "flattened indices" for multi-dimensional access. In fact, we can argue 1-D as a special case of the $I_f$ definition we provided earlier. We will proceed in the next section to arrive at primitive access rules for multi-dimensional access, and gradually improve on them.  
+**Note- ** We're operating on a 1-D array, so this set already represents our "flattened indices" for multi-dimensional access. In fact, we can argue 1-D as a special case of the $I_f$ definition we provided earlier. We will proceed in the next section to arrive at primitive access rules for multi-dimensional access, and gradually improve on them.
 
 ### Type Rules for Multi-Dimensional Access
 
@@ -419,7 +419,7 @@ Intuitively, we unroll this loop $b$ times, i.e. simultaneously accessing $b$ va
  - $\text{idx}\langle 0 .. k_1, 0 .. \frac{x}{k_1} \rangle$
  - $\text{idx}\langle 0 .. k_2, 0 .. \frac{y}{k_2} \rangle$
 
-Then we can compute $I_f$ for all $d\in 0 .. \frac{x}{b}$, 
+Then we can compute $I_f$ for all $d\in 0 .. \frac{x}{b}$,
 
 $$
 I_f = \left\{
@@ -450,7 +450,7 @@ $$
 
 Therefore, each should access a different bank.
 
-The case where $j<n-1$, 
+The case where $j<n-1$,
 Since $k_j$ divides $\sigma_{j}$,
 
 $$

diff --git a/docs/seashellintro.md b/docs/seashellintro.md
@@ -8,7 +8,7 @@ In this document, we'll illustrate the capabilities of Seashell's type system by
 
 ## Memory Access
 
-Seashell supports a couple of ways to access memories. In each method, Seashell enforces _memory access safety_: that is, when the programmer accesses a memory bank, Seashell prevents the programmer from doing so again. This reflects the fact that memory banks have limited access ports. Seashell also requires that the memory banks accessed are specified _statically_, so no multiplexer will be generated in the hardware. This is in effort to make Seashell programs more explicit: multiplexers should only appear when the programmer explicitly specifies it. 
+Seashell supports a couple of ways to access memories. In each method, Seashell enforces _memory access safety_: that is, when the programmer accesses a memory bank, Seashell prevents the programmer from doing so again. This reflects the fact that memory banks have limited access ports. Seashell also requires that the memory banks accessed are specified _statically_, so no multiplexer will be generated in the hardware. This is in effort to make Seashell programs more explicit: multiplexers should only appear when the programmer explicitly specifies it.
 
 ### Banked Memory Access
 

diff --git a/examples/array1d_logical.sea b/examples/array1d_logical.sea
@@ -1,14 +1,14 @@
 /////////////////////////////////////////////
 // 1d array logical access
 // - This application uses a banked array as input
-// with regular banking, accessed logically with 
+// with regular banking, accessed logically with
 // unroll to access different banks
 ////////////////////////////////////////////
 
 func madd(a: float[1024 bank(32)], b: float) {
 
   for (let i = 0..1023) unroll 32 {
     b := a[i];
-  } 
+  }
 
 }
diff --git a/examples/array1d_physical.sea b/examples/array1d_physical.sea
@@ -1,7 +1,7 @@
 /////////////////////////////////////////////
 // 1d array physical access
 // - This application uses a banked array as input
-// with regular banking, accessed physically with 
+// with regular banking, accessed physically with
 // different banks explicitly mentioned.
 ////////////////////////////////////////////
 
@@ -10,6 +10,6 @@ func madd(a: float[1024 bank(32)], b: float, c: float) {
   for (let i = 0..31) {
     b := a{0}[i];
     c := a{1}[i];
-  } 
+  }
 
 }