Blocks and arrays

../_images/block-primitives-montage.png

CertSAFE’s mechanism for representing arrays is called blocks. Using blocks, a single wire can carry an array of many values. Arrays can be indexed on one or more dimensions, and the index types can be fixed-size integer types, integer interval types, or enumeration types. Blocks are also compatible with the other notations in CertSAFE: applying a diagram full of ordinary logic to input variables that have block dimensions will automatically map the logic over the input arrays.

To help illustrate how to write models using blocks notation, this page includes a number of examples. Each example shows C code for a simple program, together with the analogous CertSAFE logic that performs the same function.

Note

For a walkthrough of how to use arrays when modeling and simulating real-world systems, see the Blocks and Arrays Tutorial.

For information on using array-typed variables in simulations, see the article on working with blocks in simulations.

Concept

If you are familiar with matrix-based programming environments such as MATLAB or NumPy, the blocks notation in CertSAFE can often be thought of as a statically-typed version of the same idea. Standard logic is automatically mapped pointwise over input arrays, producing output arrays of the same size. This works for arithmetic, Boolean operators, and even stateful components such as the One Frame Delay.

Note

The term blocks is chosen by analogy with clocks, which is a feature for conditional execution present in some other dataflow languages such as Lustre. Blocks are similar to clocks in that they are a property of a network at the type level that propagates across the model automatically. However, whereas clocks allow logic to be executed less frequently, blocks allow logic to be executed more frequently.

Be careful not to confuse the term blocks with the common use of the word “block” to refer to a diagram component in other dataflow languages. In this documentation, the word “blocks” always refers to the CertSAFE arrays feature.

Example: Pointwise multiplication by 2

#define SIZE 100
void multiplyAllBy2(int input[SIZE], int output[SIZE]) {
   for (int k = 0; k < SIZE; k++)
      output[k] = 2 * input[k];
}
../_images/pointwise-multiplication.png

Note that there is no explicit loop in the CertSAFE diagram. The Inline Multiplier component is automatically vectorized over the entire input array—whatever size it may be—without any additional notation. The block key type annotation [0..99], together with the scalar type annotation Int32, tells CertSAFE that the diagram above accepts any array of Int32 values that has an innermost dimension whose key type is the integer interval type [0..99]. Block key types are the most common use case for integer interval types, because they allow specifying an array with a specific arbitrary integer size. Block key types are discussed in more detail in subsequent sections of this page.

Example: Dot product

double dotProduct(int size, double u[], double v[]) {
   double o = 0.0;
   for (int k = 0; k < size; k++)
      o += u[k] * v[k];
   return o;
}
../_images/dot-product.png

Here is an example of a diagram that uses the standard multiplication component together with a Block Sum component to compute the dot product of two vectors of the same length. The multiplication component is automatically vectorized to operate over matching pairs of input array indices. The λ (lambda) symbol on the single input of the Sum primitive indicates that the sum is taken over all of the values of the input array along the innermost dimension.

Unlike the C code, in the CertSAFE model the size of the arrays does not have to be passed in as an explicit parameter. Instead, the size is a polymorphic type parameter that is inferred by the type system from the surrounding context when this diagram is used as a custom component. The type system infers that the two arrays must have the same size and the same number of dimensions, because they are both being fed into the multiplication component to get a single output array of that size.

Warning

An important difference between CertSAFE and most matrix-based languages is that arrays with different numbers of dimensions cannot be mixed freely in general. For example, attempting to add a vector to a matrix will not automatically expand the vector with an extra dimension; it is simply a static type error. Missing dimensions must instead be explicitly added using the Capture component. This restriction allows CertSAFE to automatically infer the dimensionality of all arrays in a model, while preserving the flexibility to use logic with different array sizes. The details of when explicit dimension conversion is necessary are discussed later in this page.

Block primitives

Array dimensions—commonly called block dimensions in the context of CertSAFE—are introduced and eliminated by special primitive components. There are a handful of dedicated primitives for manipulating block dimensions, while the rest is handled by special modes of the standard primitives.

Varargs folds

../_images/varargs-folds.png

All varargs components (primitives that have a variable number of input pins, such as the Boolean gates) have an Inputs property. By default, this is set to allow two or more individual inputs pins. However, by selecting the block button, the component will instead take a single array-valued input and fold over a dimension of the input, eliminating it from the output. For example, an AND gate set to block level 1, given as input a 1-dimensional array, will output a single Boolean value that is True if and only if all of the values in the input array are True.

All varargs fold components have an identity value, which is produced when the folded dimension is empty—that is, when the folded dimension’s key type is a data type with no values. The identity value is the mathematical identity for the binary operation applied by the fold. For example, the identity value for an AND Gate is True, the identity value for an OR Gate is False, the identity value for a Min Selector is the maximum value of the scalar data type, etc.

Note

All primitives that eliminate a block dimension, such as the varargs folds and the Block Switch, are marked with a λ (lambda) symbol on one of their input pins. This is because these components correspond in a formal sense to the lambda expressions from functional programming languages.

Capture

../_images/capture.png

The Capture primitive adds a new array dimension by replicating the input value repeatedly. The size of the new dimension on the output of the Capture component is automatically inferred by the type system in order to match whatever the output wire is connected to. If the output array is inferred to be of size 10, then giving an input value of 5.0 to the Capture component results in the output array [5.0, 5.0, 5.0, 5.0, 5.0, 5.0, 5.0, 5.0, 5.0, 5.0].

The Capture primitive is often used when mixing scalar-typed variables with array-typed variables, or mixing array-typed variables having different numbers of dimensions. Since CertSAFE requires all inputs to have identical array dimensions when applying a pointwise operation with multiple inputs, it is necessary to use the Capture component to adapt the input values to have the correct dimensionality. If the pointwise operation is conceptualized as performing a scalar operation in a loop, the Capture component can be thought of as capturing a variable from outside the loop and bringing it into the scope of the loop, similar to how nested functions can capture variables from enclosing scopes in functional programming languages.

Index

../_images/index.png

The Index primitive outputs an array whose value at each position is the current array index along the chosen dimension. For example, for a single-dimensional array whose key type is the integer interval type [1..10], the Index primitive will output the array [1, 2, 3, 4, 5, 6, 7, 8, 9, 10]. This can be used to perform different logic depending on the current loop index.

Pack Block and Unpack Block

../_images/pack-unpack-block.png

The Pack Block primitive provides a convienient syntax for combining multiple scalar values into a one-dimensional array, or assembling a multi-dimensional array out of lower-dimensional arrays. Similarly, the Unpack Block primitive provides a convienient syntax for extracting one or more scalar values from an array, or slicing lower-dimensional arrays out of a multi-dimensional array. These components work similarly to the Switch primitive, in that the key data type and list of keys to pack/unpack are selected through the Properties view. The Pack Block component also requires all entries to be covered by its input cases, similar to the Switch primitive and the inputs of case tables.

Warning

When using a Pack Block or Unpack Block primitive to assemble or disassemble a multidimensional array, be careful of which array dimension the primitive is operating on. Remember that the types of the input and output networks are shown in tooltips on mouseover. As with other block primitives, the dimension on which a Pack Block or Unpack Block component operates can be modified by editing the Block Level property in the Properties view.

Block Switch and Compose

../_images/block-switch-compose.png

The Block Switch and Compose primitives are used to access arrays at indices defined by a variable. The Block Switch takes an array and an index and outputs the value of the array at that index. The Compose component uses the array(s) on the top of the component to reindex the array on the left of the component, composing the arrays together (like function composition).

The only difference between the Block Switch and Compose primitives is the choice of dimensions being indexed. The Block Switch component eliminates a single array dimension, which can be at any depth in the block stack, by slicing to a chosen position. The Compose component reindexes an input array by accessing one input array at the locations determined by the values of another group of input arrays. Try different property values and check the type signatures in the tooltips to see which primitive is appropriate for any given situation.

One Index Delay and Fold End

../_images/one-index-delay-fold-end.png

The One Index Delay and Fold End primitives are used for writing custom scan and fold operations that perform more general loops than can be expressed using only pointwise operations, adding and removing block levels, and the built-in varargs folds. These primitives are covered in more detail in later sections.

Block prefixes and key types

When the mouse is hovered over a wire in a diagram, CertSAFE will display type information for that variable. This includes the block prefix of the variable, which describes the variable’s block dimensions, and the scalar type of the variable, which is the type of the actual values contained in the array.

../_images/instance-types-tooltip.png

The block prefix consists of the symbol ℕ, followed by a list of zero or more additional key types, which are the index types of the variable’s block dimensions. Following the block prefix, CertSAFE displays the symbol ⊢ (the “turnstile”), then the scalar type of the variable. For example, in the image above, the variable is a two-dimensional array of Float64 values, where the first dimension’s key type is [0..3] and the second dimension’s key type is Color.

CertSAFE models are always executed repeatedly at a fixed global frame rate. This can be thought of like an additional block dimension, called the time dimension. The time dimension is represented by the symbol ℕ (“natural numbers”) at the beginning of the block prefix, corresponding to the infinite list of frame numbers {0, 1, 2, ...}. This reflects how a CertSAFE variable is never really a single value, but rather an unbounded stream of values that can be produced for as long as desired in a simulation.

Constness

Variables whose values are inferred to not change over time are indicated in the user interface by prefixing the symbol ℕ with const. Similarly, CertSAFE also tries to infer when a variable’s value does not change when moving along a block dimension, and prefixes such dimensions with const. For example, the following variable is a 1-dimensional array indexed on [1..5], where the contents of the array may change over time, but at any given time all five of the slots in the array have the same value as each other.

../_images/constant-dimension.png

The block stack

By default, primitive components that manipulate the block dimensions of variables always act upon the innermost dimension of the block prefix—that is, the dimension closest to the right-hand end. This makes the block prefix behave as a sort of last-in-first-out block stack.

../_images/block-sum-primitive.png

For example, the component shown to the right sums the values of an array across the innermost block dimension. If given as input a 3-dimensional array with key types [0..3], [1..10], and [1..5], it will return as output a 2-dimensional array with key types [0..3] and [1..10], with each value in the output array being the sum of 5 values from the input array.

All block primitives provide one or more parameters that determine the dimension(s) on which the primitive operates. Dimension parameters are indexed from the right, so that the innermost dimension is numbered 1, the next-innermost dimension is numbered 2, etc. In the example above, the Block Sum primitive has a Block Level parameter that by default is set to 1, meaning that it operates on the innermost block dimension.

../_images/block-sum-2-primitive.png

Changing the Block Level parameter to 2 (using the Properties view) results in the modified component shown to the right. If given as input a 3-dimensional array with key types [0..3], [1..10], and [1..5], this modified component will return as output a 2-dimensional array with key types [0..3] and [1..5], with each value in the output array being the sum of 10 values from the input array.

Note

Currently, there is a maximum depth limit of 16 levels in any block prefix. That is, no array can have more than 16 dimensions. This is unlikely to be a constraint for most real-world models—it is the equivalent of writing 16 pairs of square brackets in a variable declaration in C.

Block prefix variables

When viewed in definition mode, block prefix types contain block prefix variables. A block prefix variable is a placeholder in a block prefix where additional dimensions may be inserted. Block prefix variables enable block polymorphism, where the number and types of array dimensions can vary between different instances of a component. This is similar to ordinary data type polymorphism, but with lists of array dimensions instead of individual data types.

A block prefix variable is represented in the user interface by Γ (uppercase Greek letter gamma), possibly followed by a number to distinguish the variable from other block prefix variables that may be substituted with different lists of key types. In a definition-mode block prefix, the block prefix variable always appears between the ℕ symbol and the leftmost key type. Additional array dimensions can be inserted at this location through type inference from the surrounding context in which the component is used. This produces the “block stack” behavior discussed above.

All CertSAFE components, including user-defined custom components, are block polymorphic in the sense of having block prefix variables in their types. This means that any component that works on scalar values can also be applied pointwise to 1-D arrays, 2-D arrays, etc. This also means that any component that works on 1-D arrays can be applied to 2-D arrays, in which case it will operate pointwise across the outer array dimension. This concept generalizes no matter how many dimensions appear in the type of the component and how many additional dimensions are substituted for the block prefix variable.

Example: Block Switch

../_images/definition-types-block-switch-tooltip.png

This Block Switch component can be applied to a one-dimensional input array with a scalar selector value to produce a scalar output. It could have the following types:

Inputs Outputs
selector : ℕ ⊢ Int8 o : ℕ ⊢ Float32
i : ℕ, Int8 ⊢ Float32

However, it can also be applied to a two-dimensional input array with a one-dimensional array input on the selector pin to produce a one-dimensional array as output. This applies the Block Switch pointwise with respect to the outer dimension of the two-dimensional input array. The types might look like this:

Inputs Outputs
selector : ℕ, [1..5] ⊢ Int8 o : ℕ, [1..5] ⊢ Float32
i : ℕ, [1..5], Int8 ⊢ Float32

Example: Literal

../_images/definition-types-literal-tooltip.png

The block prefix of any pure logic is simply “pure ℕ, Γ”. This means that pure logic does not depend on the time dimension, and can be applied to zero or more array dimensions indexed on any types. As a particular case of the general principle, the Literal primitive is pure, so it can be applied to any number of block dimensions to generate an array filled with a single literal value. For example, connecting a Literal component with a value of 9 directly to logic that requires an array of size 10 will automatically produce the array [9, 9, 9, 9, 9, 9, 9, 9, 9, 9]. Effectively, the 9 Literal component is being replicated 10 times, or executed 10 times in a loop.

Writing arbitrary loops with One Index Delay

It is possible to model many different types of logic using only the basic operations of adding and removing block levels and applying built-in folds such as the AND Gate or Sum primitives. However, some behaviors cannot be expressed using only these operations. To address such situations, CertSAFE provides another, very general block primitive called the One Index Delay. Using the One Index Delay primitive together with the other block primitives, it is possible to write any logic that can be expressed using bounded loops.

Note

CertSAFE does not currently provide any mechanism for writing unbounded loops, or loops whose maximum length is not known until the loop executes. This is intentional: it ensures that a single frame of execution cannot run forever, which is an important constraint for real-time systems. Using the One Index Delay component together with switching logic, it is possible to emulate loops whose length varies at runtime, as long as an upper bound on the length of the loop is known at modeling time.

The One Index Delay component is analogous to the One Frame Delay component—in fact, they are the same primitive, just with the Block Level parameter set differently. Whereas the One Frame Delay outputs the value of the input delayed by one frame along the time dimension, the One Index Delay outputs the value of the input delayed by one index along a block dimension. When a One Index Delay component is inserted into a dependency cycle, the effect is that values at later indices in the array are defined in terms of values at earlier indices in the array.

Example: Generalized Fibonacci numbers

#define SIZE 10
void generalizedFibonacciNumbers(int f0, int f1, int fibs[SIZE]) {
   fibs[0] = f0;
   fibs[1] = f1;
   for (int k = 2; k < SIZE; k++)
      fibs[k] = fibs[k - 1] + fibs[k - 2];
}
../_images/generalized-fibonacci.png

This code computes the first 10 terms of a generalized Fibonacci sequence, where \(f_0\) and \(f_1\) are parameters and then the rest of the terms are defined by \(f_{k+2} = f_k + f_{k+1}\). The CertSAFE diagram uses the One Index Delay component twice to look up the previous and second-previous values of the array as it is being produced. Note that we need Capture components on the initial condition pins of the One Index Delays to make these pins scalar-typed. Without the Capture components, the f0 and f1 input variables would be inferred as array-typed and the One Index Delays would access their first indices for the IC values (similarly to how a One Frame Delay accesses the value of its IC pin on the first frame).

Extracting the last value with Fold End

When using the One Index Delay component, sometimes you just want the final value computed by the loop (a fold operation) rather than the entire history of intermediate values (a scan operation). It is possible to extract the last value from the array produced by the One Index Delay component using a Block Switch with a Literal value on the selector pin; however, this does not work polymorphically for arrays indexed on different key types. The Fold End primitive handles this automatically. A Fold End component behaves like a Block Switch with a Literal selector input that polymorphically changes to the appropriate value for any non-empty array key type. This allows the final value of a loop to be extracted without needing the index of the final value to be written into the diagram as an explicit Literal.

Example: Babylonian square root

double babylonianSqrt(double x) {
   double y = x;
   for (int k = 1; k <= 10; k++)
      y = 0.5 * (y + (x / y));
   return y;
}
../_images/babylonian-sqrt.png

This code computes an approximation to the square root of \(x\) by applying 10 iterations of the Babylonian method. It starts with \(y_0 = x\) and then iterates \(y_{k+1} = \frac{1}{2} \left(y_k + \frac{x}{y_k}\right)\). In the C code, it is not necessary to store all of the intermediate values \(y_1, \dots, y_{10}\) during the computation; instead, a single mutable y variable is repeatedly overwritten. CertSAFE uses immutable variables rather than mutable variables, so in the CertSAFE diagram, the variable yk is an array containing all of the values \(y_1, \dots, y_{10}\), and a Fold End component is used to extract the final value.

Block dependencies

Similar to how the One Frame Delay component can break an illegal dependency cycle in a diagram, the One Index Delay component can also break certain illegal dependency cycles. Specifically, a One Index Delay can break a dependency cycle only if any fold operation in the dependency cycle is over a dimension further to the right in the block prefix than the dimension that the One Index Delay component is delaying across. The time dimension ℕ is considered to be the leftmost dimension in the block prefix, so a One Frame Delay component can break any dependency cycle regardless of what block operations it contains.

Example: Dependency cycles

../_images/dependency-cycle-illegal.png

The diagram above is illegal because the Block Sum eliminates the dimension that the One Index Delay is delaying across, before the Capture component reintroduces it in a cycle.

../_images/dependency-cycle-legal.png

However, this similar diagram is legal because the Capture component introduces a new dimension that is eliminated by the Block Sum component, and the new dimension is further to the right in the block prefix from the dimension that the One Index Delay is delaying across.

Dependency line labels

When mousing over the pins of a component, CertSAFE will display numeric labels on the dependency lines between pairs of pins that involve block operations.

  • For a solid blue line, the number is the largest N such that a loopback in the containing diagram with a level N index delay is illegal. If no number is displayed, then there are no folds along the dependency, so any delay makes the loopback legal.
  • For a dashed gray line, the number is the smallest N such that a loopback in the containing diagram with a level N fold is illegal. If no number is displayed, then there is a time delay along the dependency, so the loopback is legal no matter what fold is added in the containing diagram.
../_images/dependency-line-labels.png