Finch Notation

Finch programs are written in Julia, but they are not Julia programs. Instead, they are an abstraction description of a tensor computation.

Finch programs are blocks of tensor operations, joined by control flow. Finch is an imperative language. The AST is separated into statements and expressions, where statements can modify the state of the program but expressions cannot.

The core Finch expressions are:

And the core Finch statements are:

  • declare e.g. tns .= init
  • assign e.g. lhs[idxs...] <<op>>= rhs
  • loop e.g. for i = _; ... end
  • define e.g. let var = val; ... end
  • sieve e.g. if cond; ... end
  • block e.g. begin ... end
Finch.FinchNotation.value — Constant
value(val, type)

Finch AST expression for host code val expected to evaluate to a value of type type.

Finch.FinchNotation.index — Constant
index(name)

Finch AST expression for an index named name. Each index must be quantified by a corresponding loop which iterates over all values of the index.

Finch.FinchNotation.variable — Constant
variable(name)

Finch AST expression for a variable named name. The variable can be looked up in the context.

Finch.FinchNotation.call — Constant
call(op, args...)

Finch AST expression for the result of calling the function op on args....

Finch.FinchNotation.access — Constant
access(tns, mode, idx...)

Finch AST expression representing the value of tensor tns at the indices idx.... The mode differentiates between reads or updates and whether the access is in-place.

Finch.FinchNotation.define — Constant
define(lhs, rhs, body)

Finch AST statement that defines lhs as having the value rhs in body. A new scope is introduced to evaluate body.

Finch.FinchNotation.assign — Constant
assign(lhs, op, rhs)

Finch AST statement that updates the value of lhs to op(lhs, rhs). Overwriting is accomplished with the function overwrite(lhs, rhs) = rhs.

Finch.FinchNotation.loop — Constant
loop(idx, ext, body)

Finch AST statement that runs body for each value of idx in ext. Tensors in body must have ranges that agree with ext. A new scope is introduced to evaluate body.

Finch.FinchNotation.sieve — Constant
sieve(cond, body)

Finch AST statement that only executes body if cond is true. A new scope is introduced to evaluate body.

Finch.FinchNotation.block — Constant
block(bodies...)

Finch AST statement that executes each of it's arguments in turn. If the body is not a block, replaces accesses to tensors in the body with instantiate.

Scoping

Finch programs are scoped. Scopes contain variable definitions and tensor declarations. Loops and sieves introduce new scopes. The following program has four scopes, each of which is numbered to the left of the statements it contains.

@finch begin
1   y .= 0
1   for j = _
1   2   t .= 0
1   2   for i = _
1   2   3   t[] += A[i, j] * x[i]
1   2   end
1   2   for i = _
1   2   4   y[i] += A[i, j] * t[]
1   2   end
1   end
end

Variables refer to their defined values in the innermost containing scope. If variables are undefined, they are assumed to have global scope (they may come from the surrounding program).

Tensor Lifecycle

Tensors have two modes: Read and Update. Tensors in read mode may be read, but not updated. Tensors in update mode may be updated, but not read. A tensor declaration initializes and possibly resizes the tensor, setting it to update mode. Also, Finch will automatically change the mode of tensors as they are used. However, tensors may only change their mode within scopes that contain their declaration. If a tensor has not been declared, it is assumed to have global scope.

Tensor declaration is different than variable definition. Declaring a tensor initializes the memory (usually to zero) and sets the tensor to update mode. Defining a tensor simply gives a name to that memory. A tensor may be declared multiple times, but it may only be defined once.

Tensors are assumed to be in read mode when they are defined. Tensors must enter and exit scope in read mode. Finch inserts freeze and thaw statements to ensure that tensors are in the correct mode. Freezing a tensor prevents further updates and allows reads. Thawing a tensor allows further updates and prevents reads.

Tensor lifecycle statements consist of:

Finch.FinchNotation.declare — Constant
declare(tns, init)

Finch AST statement that declares tns with an initial value init in the current scope.

Dimensionalization

Finch loops have dimensions. Accessing a tensor with an unmodified loop index "hints" that the loop should have the same dimension as the corresponding axis of the tensor. Finch will automatically dimensionalize loops that are hinted by tensor accesses. One may refer to the automatically determined dimension using a variable named _ or :.

Similarly, tensor declarations also set the dimensions of a tensor. Accessing a tensor with an unmodified loop index "hints" that the tensor axis should have the same dimension as the corresponding loop. Finch will automatically dimensionalize declarations based on all updates up to the first read.

Array Combinators

Finch includes several array combinators that modify the behavior of arrays. For example, the OffsetArray type wraps an existing array, but shifts its indices. The PermissiveArray type wraps an existing array, but allows out-of-bounds reads and writes. When an array is accessed out of bounds, it produces Missing.

Array combinators introduce some complexity to the tensor lifecycle, as wrappers may contain multiple or different arrays that could potentially be in different modes. Any array combinators used in a tensor access must reference a single global variable which holds the root array. The root array is the single array that gets declared, and changes modes from read to update, or vice versa.

Fancy Indexing

Finch supports arbitrary indexing of arrays, but certain indexing operations have first class support through array combinators. Before dimensionalization, the following transformations are performed:

    A[i + c] =>        OffsetArray(A, c)[i]
    A[i + j] =>      ToeplitzArray(A, 1)[i, j]
       A[~i] => PermissiveArray(A, true)[i]

Note that these transformations may change the behavior of dimensionalization, since they often result in unmodified loop indices (the index i will participate in dimensionalization, but an index expression like i + 1 will not).