Parallel prefix sums

DefinitionWindow product#✓fully proved

For a sequence \(x : \mathbb{N} \to M\) in a monoid \(M\) and \(a, b \in \mathbb{N}\), the window product is the ordered product \(x_a x_{a+1} \cdots x_{b-1}\) of the terms with indices \(a \le j < b\); it is the empty product \(1\) when \(b \le a\).

def seg (x : ℕ → M) (a b : ℕ) : M := ((List.range' a (b - a)).map x).prod

Used by 6

Used byBlelloch's scan computes the exclusive prefix products · The list implementation computes the exclusive prefix products · The scan computes all prefix products · What the scan holds after each round · Prefix product · Products of adjacent windows

DefinitionPrefix product#✓fully proved

For a sequence \(x_0, x_1, \dots\) in a monoid \(M\) and a natural number \(i\), the prefix product at \(i\) is \(x_0 x_1 \cdots x_i\), the factors taken in increasing order of index.

def prefixProd (x : ℕ → M) (i : ℕ) : M := seg x 0 (i + 1)

Uses 1 · Used by 3

Statement usesWindow product

Used byThe tabulated scan computes all prefix products · The scan computes all prefixes in logarithmically many rounds · The scan computes all prefix products

TheoremProducts of adjacent windows#✓fully proved

Let \(M\) be a monoid and \(x : \mathbb{N} \to M\) a sequence, and for \(a, b \in \mathbb{N}\) let \(x_{[a, b)}\) be the ordered product \(x_a x_{a+1} \cdots x_{b-1}\) (equal to \(1\) if \(b \le a\)). For all \(a \le b \le c\), \(x_{[a, b)} \, x_{[b, c)} = x_{[a, c)}\).

theorem seg_mul_seg (x : ℕ → M) {a b c : ℕ} (hab : a ≤ b) (hbc : b ≤ c) :
    seg x a b * seg x b c = seg x a c

Uses 1 · Used by 2

Statement usesWindow product

Used byBlelloch's scan computes the exclusive prefix products · What the scan holds after each round

DefinitionThe Kogge–Stone scan#✓fully proved

Given a sequence \(x_0, x_1, \dots\) in a monoid \(M\), the value \(s_k(i)\) at position \(i\) after \(k\) rounds is defined by \(s_0(i) = x_i\) and, for each \(k\), \(s_{k+1}(i) = s_k(i - 2^k) \, s_k(i)\) if \(2^k \le i\) and \(s_{k+1}(i) = s_k(i)\) otherwise.

def koggeStone (x : ℕ → M) : ℕ → ℕ → M
  | 0, i => x i
  | k + 1, i => if 2 ^ k ≤ i then koggeStone x k (i - 2 ^ k) * koggeStone x k i
      else koggeStone x k i

Used by 5

Used byThe tabulated scan agrees with the round recursion · The tabulated scan computes all prefix products · The scan computes all prefixes in logarithmically many rounds · The scan computes all prefix products · What the scan holds after each round

TheoremWhat the scan holds after each round#✓fully proved

Let \(x_0, x_1, \dots\) be a sequence in a monoid \(M\), let \(k\) and \(i\) be natural numbers, and let \(m = \min(i + 1, 2^k)\). After \(k\) rounds of the Kogge–Stone scan, position \(i\) holds the product \(x_{i+1-m} \cdots x_i\) of the \(m\) consecutive inputs ending at \(i\), taken in increasing order of index.

theorem koggeStone_eq_seg (x : ℕ → M) :
    ∀ k i, koggeStone x k i = seg x (i + 1 - min (i + 1) (2 ^ k)) (i + 1)

Uses 3 · Used by 1

Statement usesThe Kogge–Stone scan · Window product

Proof usesProducts of adjacent windows

Used byThe scan computes all prefix products

TheoremThe scan computes all prefix products#✓fully proved

Let \(x_0, x_1, \dots\) be a sequence in a monoid \(M\) and let \(n\) and \(K\) be natural numbers with \(n \le 2^K\). After \(K\) rounds of the Kogge–Stone scan, every position \(i < n\) holds the prefix product \(x_0 x_1 \cdots x_i\).

theorem koggeStone_eq_prefix (x : ℕ → M) {n K : ℕ} (hn : n ≤ 2 ^ K) {i : ℕ} (hi : i < n) :
    koggeStone x K i = prefixProd x i

Uses 4 · Used by 2

Statement usesThe Kogge–Stone scan · Prefix product

Proof usesWhat the scan holds after each round · Window product

Used byThe tabulated scan computes all prefix products · The scan computes all prefixes in logarithmically many rounds

DefinitionWork of a scan round#✓fully proved

The work of round \(k\) on \(n\) positions is \(\max(n - 2^k, 0)\), the number of positions \(i < n\) with \(i \ge 2^k\), each of which performs one multiplication.

def roundWork (n k : ℕ) : ℕ := n - 2 ^ k

Used by 3

Used byThe work of a round counts its combining positions · Work of the Kogge–Stone scan · Work bound for the Kogge–Stone scan

TheoremThe work of a round counts its combining positions#✓fully proved

For natural numbers \(n\) and \(k\), the work of round \(k\) on \(n\) positions equals the number of positions \(i\) with \(2^k \le i < n\).

theorem roundWork_eq_card (n k : ℕ) :
    roundWork n k = ((Finset.range n).filter fun i => 2 ^ k ≤ i).card

Uses 1

Statement usesWork of a scan round

DefinitionWork of the Kogge–Stone scan#✓fully proved

The total work of \(K\) rounds on \(n\) positions is \(\sum_{k=0}^{K-1} \max(n - 2^k, 0)\), the sum over the rounds \(k < K\) of the work \(\max(n - 2^k, 0)\) of round \(k\).

def work (n K : ℕ) : ℕ := ∑ k ∈ Finset.range K, roundWork n k

Uses 1 · Used by 1

Statement usesWork of a scan round

Used byWork bound for the Kogge–Stone scan

TheoremWork bound for the Kogge–Stone scan#✓fully proved

For all \(n, K \in \mathbb{N}\), the total work of \(K\) rounds of the scan on \(n\) positions is at most \(nK\).

theorem work_le (n K : ℕ) : work n K ≤ n * K

Uses 2

Statement usesWork of the Kogge–Stone scan

Proof usesWork of a scan round

DefinitionSpan of the Kogge–Stone scan#✓fully proved

The span of \(K\) rounds of the scan is \(K\): each round is one parallel step.

def span (K : ℕ) : ℕ := K

TheoremThe scan computes all prefixes in logarithmically many rounds#✓fully proved

Let \(x_0, x_1, \dots\) be a sequence in a monoid \(M\) and let \(n\) be a natural number. After \(\lceil \log_2 n \rceil\) rounds of the Kogge–Stone scan (the least \(K\) with \(n \le 2^K\)), every position \(i < n\) holds the prefix product \(x_0 x_1 \cdots x_i\).

theorem koggeStone_clog_eq_prefix (x : ℕ → M) {n i : ℕ} (hi : i < n) :
    koggeStone x (Nat.clog 2 n) i = prefixProd x i

Uses 3

Statement usesThe Kogge–Stone scan · Prefix product

Proof usesThe scan computes all prefix products

DefinitionOne round of the scan on a list#✓fully proved

Given a list \(y_0, \dots, y_{n-1}\) in a monoid \(M\) and a natural number \(k\), one round produces the list of length \(n\) whose entry \(i\) is \(y_{i - 2^k} \, y_i\) when \(2^k \le i\) and \(y_i\) when \(i < 2^k\).

The list is traversed in lockstep with its own suffix starting at position \(2^k\), so a round costs \(O(n)\).

def roundList (k : ℕ) (ys : List M) : List M :=
  ys.take (2 ^ k) ++ List.zipWith (· * ·) ys (ys.drop (2 ^ k))

Used by 2

Used byThe tabulated scan agrees with the round recursion · Tabulated Kogge–Stone scan

DefinitionTabulated Kogge–Stone scan#✓fully proved

For a list \(y = (y_0, \dots, y_{n-1})\) in a monoid \(M\), the list after \(K\) rounds is defined by recursion on \(K\): after \(0\) rounds it is \(y\), and after \(K + 1\) rounds it is round \(K\) applied to the list after \(K\) rounds. Here round \(k\) sends a list \((z_0, \dots, z_{n-1})\) to the list of length \(n\) whose entry \(i\) is \(z_i\) for \(i < 2^k\) and \(z_{i - 2^k} z_i\) for \(2^k \le i < n\).

def scanList : ℕ → List M → List M
  | 0, ys => ys
  | K + 1, ys => roundList K (scanList K ys)

Uses 1 · Used by 2

Statement usesOne round of the scan on a list

Used byThe tabulated scan agrees with the round recursion · The tabulated scan computes all prefix products

TheoremThe tabulated scan agrees with the round recursion#✓fully proved

Let \(x_0, \dots, x_{n-1}\) be a list of elements of a monoid \(M\), extended to a sequence by \(x_j = 1\) for \(j \ge n\). For every number of rounds \(K\) and every position \(i < n\), entry \(i\) of the list produced by \(K\) rounds of the tabulated scan equals the value at position \(i\) after \(K\) rounds of the Kogge–Stone scan applied to the sequence \(x\).

theorem getD_scanList (xs : List M) : ∀ (K i : ℕ), i < xs.length →
    (scanList K xs).getD i 1 = koggeStone (fun j => xs.getD j 1) K i

Uses 3 · Used by 1

Statement usesThe Kogge–Stone scan · Tabulated Kogge–Stone scan

Proof usesOne round of the scan on a list

Used byThe tabulated scan computes all prefix products

TheoremThe tabulated scan computes all prefix products#✓fully proved

Let \(x_0, \dots, x_{n-1}\) be a list of elements of a monoid \(M\) and let \(K\) be a natural number with \(n \le 2^K\). Then for every \(i < n\), entry \(i\) of the list produced by \(K\) rounds of the tabulated scan equals the prefix product \(x_0 x_1 \cdots x_i\).

theorem getD_scanList_eq_prefix (xs : List M) {K : ℕ} (hK : xs.length ≤ 2 ^ K) {i : ℕ}
    (hi : i < xs.length) : (scanList K xs).getD i 1 = prefixProd (fun j => xs.getD j 1) i

Uses 5

Statement usesPrefix product · Tabulated Kogge–Stone scan

Proof usesThe tabulated scan agrees with the round recursion · The Kogge–Stone scan · The scan computes all prefix products

DefinitionAdjacent pair products of a sequence#✓fully proved

For a sequence \(x \colon \mathbb{N} \to M\) in a monoid \(M\), the sequence of adjacent pair products is the sequence whose term at \(i\) is \(x(2i) \cdot x(2i+1)\).

def pairUp (x : ℕ → M) : ℕ → M := fun i => x (2 * i) * x (2 * i + 1)

Used by 3

Used byBlelloch's scan · Blelloch's scan computes the exclusive prefix products · The list implementation computes Blelloch's scan

DefinitionBlelloch's scan#✓fully proved

Let \(M\) be a monoid. For a natural number \(k\) and a sequence \(x = (x_0, x_1, \dots)\) in \(M\), the scan \(B_k(x)\) is the sequence in \(M\) defined by recursion on \(k\): \(B_0(x)\) is constantly \(1\), and \(B_{k+1}(x)\) is obtained from the scan \(y = B_k(p)\) of the pair products \(p_i = x_{2i} x_{2i+1}\) by setting \(B_{k+1}(x)_{2i} = y_i\) and \(B_{k+1}(x)_{2i+1} = y_i x_{2i}\) for every \(i\).

def blelloch : ℕ → (ℕ → M) → ℕ → M
  | 0, _ => fun _ => 1
  | k + 1, x => fun j =>
      if j % 2 = 0 then blelloch k (pairUp x) (j / 2) else blelloch k (pairUp x) (j / 2) * x (j - 1)

Uses 1 · Used by 3

Statement usesAdjacent pair products of a sequence

Used byBlelloch's scan computes the exclusive prefix products · The list implementation computes Blelloch's scan · The list implementation computes the exclusive prefix products

TheoremBlelloch's scan computes the exclusive prefix products#✓fully proved

Let \(M\) be a monoid, \(k\) a natural number and \(x = (x_0, x_1, \dots)\) a sequence in \(M\). For every \(j < 2^k\), the value at position \(j\) of Blelloch's scan of \(x\) on \(2^k\) positions is the exclusive prefix product \(x_0 x_1 \cdots x_{j-1}\) (equal to \(1\) when \(j = 0\)).

theorem blelloch_eq_seg : ∀ (k : ℕ) (x : ℕ → M) (j : ℕ), j < 2 ^ k → blelloch k x j = seg x 0 j

Uses 4 · Used by 1

Statement usesBlelloch's scan · Window product

Proof usesAdjacent pair products of a sequence · Products of adjacent windows

Used byThe list implementation computes the exclusive prefix products

DefinitionWork of Blelloch's scan#✓fully proved

The number \(W(k)\) of monoid multiplications Blelloch's scan performs on \(2^k\) positions is defined by \(W(0) = 0\) and \(W(k+1) = 2^k + W(k) + 2^k\): on \(2^{k+1}\) positions, \(2^k\) pair products, the recursive scan on the \(2^k\) pair products, and \(2^k\) products for the odd positions.

def blellochWork : ℕ → ℕ
  | 0 => 0
  | k + 1 => 2 ^ k + blellochWork k + 2 ^ k

Used by 1

Used byBlelloch's scan is work-efficient

DefinitionParallel steps of Blelloch's scan#✓fully proved

The span \(S(k)\) of Blelloch's scan on \(2^k\) positions is defined by \(S(0) = 0\) and \(S(k+1) = S(k) + 2\): one parallel step for the pair products, the recursive scan, and one parallel step for the odd positions.

def blellochSpan : ℕ → ℕ
  | 0 => 0
  | k + 1 => blellochSpan k + 2

Used by 1

Used byBlelloch's scan has logarithmic span

TheoremBlelloch's scan is work-efficient#✓fully proved

For every natural number \(k\), the number \(W(k)\) of monoid multiplications Blelloch's scan performs on \(n = 2^k\) positions satisfies \(W(k) + 2 = 2^{k+1}\), so \(W(k) = 2^{k+1} - 2 < 2n\).

theorem blellochWork_eq : ∀ k, blellochWork k + 2 = 2 ^ (k + 1)

Uses 1

Statement usesWork of Blelloch's scan

TheoremBlelloch's scan has logarithmic span#✓fully proved

For every natural number \(k\), the span of Blelloch's scan on \(n = 2^k\) positions is \(2k = 2 \log_2 n\).

theorem blellochSpan_eq : ∀ k, blellochSpan k = 2 * k

Uses 1

Statement usesParallel steps of Blelloch's scan

DefinitionAdjacent pair products of a list#✓fully proved

For a list \([a_0, a_1, \ldots, a_{n-1}]\) of elements of a monoid \(M\), the list of adjacent pair products is \([a_0 a_1, a_2 a_3, \ldots]\): it has length \(\lfloor n/2 \rfloor\), its \(i\)-th entry is \(a_{2i} a_{2i+1}\), and when \(n\) is odd the last element \(a_{n-1}\) is dropped.

def pairList : List M → List M
  | a :: b :: xs => (a * b) :: pairList xs
  | _ => []

Used by 2

Used byBlelloch's scan on lists · The list implementation computes Blelloch's scan

DefinitionInterleaving step of Blelloch's list scan#✓fully proved

Let \(M\) be a monoid. For lists \(z = (z_0, z_1, \dots)\) and \(x = (x_0, x_1, \dots)\) in \(M\), the expansion of \(z\) along \(x\) is the list \((z_0, z_0 x_0, z_1, z_1 x_2, z_2, z_2 x_4, \dots)\): each \(z_i\) is followed by \(z_i x_{2i}\), and the list stops at the first \(i\) for which \(z_i\) or \(x_{2i+1}\) does not exist.

def expand : List M → List M → List M
  | z :: zs, a :: _ :: xs => z :: (z * a) :: expand zs xs
  | _, _ => []

Used by 2

Used byBlelloch's scan on lists · The list implementation computes Blelloch's scan

DefinitionBlelloch's scan on lists#✓fully proved

Let \(M\) be a monoid. For a natural number \(k\) and a list \(xs = (x_0, x_1, \dots)\) in \(M\), the list scan \(L_k(xs)\) is defined by recursion on \(k\): \(L_0(xs)\) is the one-element list \((1)\), and \(L_{k+1}(xs)\) is obtained from the list scan \(z = L_k(p)\) of the pair products \(p = (x_0 x_1, x_2 x_3, \dots)\) of \(xs\) (a trailing unpaired entry is dropped) by interleaving: \(L_{k+1}(xs) = (z_0, z_0 x_0, z_1, z_1 x_2, \dots)\), where each \(z_i\) is followed by \(z_i x_{2i}\) and the list stops at the first \(i\) for which \(z_i\) or \(x_{2i+1}\) does not exist.

On a list of length \(2^k\) this takes \(O(2^k)\) time.

def blellochList : ℕ → List M → List M
  | 0, _ => [1]
  | k + 1, xs => expand (blellochList k (pairList xs)) xs

Uses 2 · Used by 2

Statement usesInterleaving step of Blelloch's list scan · Adjacent pair products of a list

Used byThe list implementation computes Blelloch's scan · The list implementation computes the exclusive prefix products

TheoremThe list implementation computes Blelloch's scan#✓fully proved

Let \(M\) be a monoid, \(k\) a natural number and \(xs = (x_0, \dots, x_{2^k - 1})\) a list in \(M\) of length \(2^k\). For every \(j < 2^k\), the entry at position \(j\) of Blelloch's list scan of \(xs\) in \(k\) rounds equals the value at position \(j\) of Blelloch's scan on \(2^k\) positions of the sequence \(x_0, \dots, x_{2^k - 1}, 1, 1, \dots\) obtained by extending \(xs\) by \(1\).

theorem getD_blellochList : ∀ (k : ℕ) (xs : List M), xs.length = 2 ^ k → ∀ j, j < 2 ^ k →
    (blellochList k xs).getD j 1 = blelloch k (fun i => xs.getD i 1) j

Uses 5 · Used by 1

Statement usesBlelloch's scan · Blelloch's scan on lists

Proof usesInterleaving step of Blelloch's list scan · Adjacent pair products of a list · Adjacent pair products of a sequence

Used byThe list implementation computes the exclusive prefix products

TheoremThe list implementation computes the exclusive prefix products#✓fully proved

Let \(M\) be a monoid, \(k\) a natural number and \(xs = (x_0, \dots, x_{2^k - 1})\) a list in \(M\) of length \(2^k\). For every \(j < 2^k\), the entry at position \(j\) of Blelloch's list scan of \(xs\) in \(k\) rounds is the exclusive prefix product \(x_0 x_1 \cdots x_{j-1}\) (equal to \(1\) when \(j = 0\)).

theorem getD_blellochList_eq_seg (k : ℕ) (xs : List M) (h : xs.length = 2 ^ k) (j : ℕ)
    (hj : j < 2 ^ k) : (blellochList k xs).getD j 1 = seg (fun i => xs.getD i 1) 0 j

Uses 5

Statement usesBlelloch's scan on lists · Window product

Proof usesBlelloch's scan · Blelloch's scan computes the exclusive prefix products · The list implementation computes Blelloch's scan

28 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.