Work–span model and Brent's theorem

StructureComputation DAG#✓fully proved

A computation DAG on \(n\) unit-time tasks, numbered \(0, \dots, n - 1\), assigns to each task \(v\) a list of predecessors (the tasks \(v\) waits for), each numbered below \(v\); so the numbering is a topological order.

structure Dag (n : ℕ) where
  /-- The tasks each task waits for. -/
  preds : Fin n → List (Fin n)
  /-- Predecessors come first. -/
  topo : ∀ v, ∀ u ∈ preds v, u < v
Used by 35
Used byBrent's theorem with the work and span laws · Depth of a task in a computation DAG · No step of Brent's level schedule mixes levels · Depth bounds the step of a task · Predecessors have smaller depth · Table of depths · Depths of an initial segment of tasks · Every step of a schedule has a task running at or after it · The table of depths is correct · Greedy schedule · Greediness need only be checked at the steps of the schedule · The work-span bound for greedy schedules · The greedy scheduling bound · Number of incomplete steps · A greedy schedule has at most \(D\) incomplete steps · Each incomplete step advances the critical path · Length of a schedule · Level size · Level \(0\) is empty · Brent's level schedule · Brent's theorem · Steps of a level · Step of a task in Brent's schedule · Load of a step · Complete steps are bounded by the work · First step of a level · A greedy schedule never idles · Rank within a level · Ranks increase within a level · Ready task · Schedule of a computation DAG · Span of a computation DAG · The span law · The step loads add up to the number of tasks · The work law

DefinitionDepth of a task in a computation DAG#✓fully proved

The depth of a task \(v\) is the number of tasks on a longest path ending at \(v\): it is \(1\) plus the largest depth of a predecessor of \(v\), or \(1\) if \(v\) has no predecessors.

def depth (v : Fin n) : ℕ :=
  1 + ((G.preds v).attach.map fun u => depth u.1).foldr max 0
termination_by v.val
decreasing_by exact G.topo v u.1 u.2
Uses 1 · Used by 15
Statement usesComputation DAG
Used byNo step of Brent's level schedule mixes levels · Depth bounds the step of a task · Predecessors have smaller depth · The table of depths is correct · A greedy schedule has at most \(D\) incomplete steps · Each incomplete step advances the critical path · Level size · Level \(0\) is empty · Brent's level schedule · Brent's theorem · Step of a task in Brent's schedule · Rank within a level · Ranks increase within a level · Span of a computation DAG · The span law

DefinitionSpan of a computation DAG#✓fully proved

The span of a computation DAG is the number of tasks on a longest path, that is, the largest depth of a task, and \(0\) when there are no tasks.

def span : ℕ := Finset.univ.sup (depth G)
Uses 2 · Used by 6
Statement usesComputation DAG · Depth of a task in a computation DAG
Used byBrent's theorem with the work and span laws · The work-span bound for greedy schedules · The greedy scheduling bound · A greedy schedule has at most \(D\) incomplete steps · Brent's theorem · The span law

TheoremPredecessors have smaller depth#✓fully proved

In a computation DAG, if \(u\) is a predecessor of \(v\), then the depth of \(u\) is strictly less than the depth of \(v\).

theorem depth_lt_of_mem {u v : Fin n} (hu : u ∈ G.preds v) : depth G u < depth G v
Uses 2 · Used by 2
Statement usesComputation DAG · Depth of a task in a computation DAG
Used byEach incomplete step advances the critical path · Brent's level schedule

DefinitionDepths of an initial segment of tasks#✓fully proved

For \(k \le n\), the list of the depths of tasks \(0, \dots, k - 1\) of a computation DAG on \(n\) tasks, computed in topological order: the empty list for \(k = 0\), and for \(k + 1\) the list for \(k\) followed by \(1\) plus the largest entry of that list at a predecessor of task \(k\) (or \(1\) if task \(k\) has no predecessors).

def depthsUpTo : (k : ℕ) → k ≤ n → List ℕ
  | 0, _ => []
  | k + 1, h =>
      let acc := depthsUpTo k (Nat.le_of_succ_le h)
      acc ++ [1 + ((G.preds ⟨k, h⟩).map fun u => acc.getD u.val 0).foldr max 0]
Uses 1 · Used by 2
Statement usesComputation DAG
Used byTable of depths · The table of depths is correct

DefinitionTable of depths#✓fully proved

The list of the depths of tasks \(0, \dots, n - 1\) of a computation DAG on \(n\) tasks, computed once each in topological order: the entry for task \(k\) is \(1\) plus the largest entry at a predecessor of \(k\), or \(1\) if \(k\) has no predecessors.

With lists (appending and indexed reads take linear time) this costs \(O(n^2 + n|E|)\), where \(|E|\) is the total number of predecessor entries; evaluating the depth directly from its recursive definition instead recomputes shared subpaths exponentially often.

def depthTable : List ℕ := depthsUpTo G n (Nat.le_refl n)
Uses 2 · Used by 1
Statement usesComputation DAG · Depths of an initial segment of tasks
Used byThe table of depths is correct

TheoremThe table of depths is correct#✓fully proved

For every task \(v\) of a computation DAG, the entry of the table of depths at position \(v\) equals the depth of \(v\).

theorem getD_depthTable (v : Fin n) : (depthTable G).getD v.val 0 = depth G v
Uses 4
Statement usesComputation DAG · Depth of a task in a computation DAG · Table of depths
Proof usesDepths of an initial segment of tasks

StructureSchedule of a computation DAG#✓fully proved

A schedule of a computation DAG on \(n\) tasks on \(p\) processors assigns to each task \(v\) a step \(t(v) \in \mathbb{N}\) in which it runs, such that \(t(u) < t(v)\) whenever \(u\) is a predecessor of \(v\), and for every step \(s\) at most \(p\) tasks \(v\) have \(t(v) = s\).

structure Schedule (p : ℕ) where
  /-- The step in which each task runs. -/
  time : Fin n → ℕ
  /-- Predecessors run earlier. -/
  prec : ∀ v, ∀ u ∈ G.preds v, time u < time v
  /-- At most `p` tasks per step. -/
  cap : ∀ t, (Finset.univ.filter fun v => time v = t).card ≤ p
Uses 1 · Used by 20
Statement usesComputation DAG
Used byBrent's theorem with the work and span laws · Depth bounds the step of a task · Every step of a schedule has a task running at or after it · Greedy schedule · Greediness need only be checked at the steps of the schedule · The work-span bound for greedy schedules · The greedy scheduling bound · Number of incomplete steps · A greedy schedule has at most \(D\) incomplete steps · Each incomplete step advances the critical path · Length of a schedule · Brent's level schedule · Brent's theorem · Load of a step · Complete steps are bounded by the work · A greedy schedule never idles · Ready task · The span law · The step loads add up to the number of tasks · The work law

DefinitionLength of a schedule#✓fully proved

The length of a schedule is the number of steps it takes: one more than the latest step in which a task runs (steps are numbered from \(0\)), or \(0\) if there are no tasks.

def Schedule.length {p : ℕ} (S : Schedule G p) : ℕ := Finset.univ.sup fun v => S.time v + 1
Uses 2 · Used by 12
Statement usesComputation DAG · Schedule of a computation DAG
Used byBrent's theorem with the work and span laws · Every step of a schedule has a task running at or after it · Greediness need only be checked at the steps of the schedule · The work-span bound for greedy schedules · The greedy scheduling bound · A greedy schedule has at most \(D\) incomplete steps · Brent's theorem · Complete steps are bounded by the work · A greedy schedule never idles · The span law · The step loads add up to the number of tasks · The work law

TheoremThe work law#✓fully proved

For a computation DAG on \(n\) tasks, every schedule of it on \(p\) processors that takes \(T\) steps satisfies \(n \le p T\). In particular, for \(p > 0\) the schedule takes at least \(n / p\) steps.

theorem Schedule.work_le {p : ℕ} (S : Schedule G p) : n ≤ p * S.length
Uses 3 · Used by 1
Statement usesComputation DAG · Schedule of a computation DAG · Length of a schedule
Used byBrent's theorem with the work and span laws

TheoremDepth bounds the step of a task#✓fully proved

For every schedule of a computation DAG on \(p\) processors, with steps numbered from \(0\), every task \(v\) runs in a step \(t\) with \(\operatorname{depth}(v) \le t + 1\).

theorem Schedule.depth_le_time {p : ℕ} (S : Schedule G p) (v : Fin n) :
    depth G v ≤ S.time v + 1
Uses 3 · Used by 1
Statement usesComputation DAG · Schedule of a computation DAG · Depth of a task in a computation DAG
Used byThe span law

TheoremThe span law#✓fully proved

No schedule is shorter than the span.

theorem Schedule.span_le {p : ℕ} (S : Schedule G p) : span G ≤ S.length
Uses 6 · Used by 1
Statement usesComputation DAG · Schedule of a computation DAG · Length of a schedule · Span of a computation DAG
Proof usesDepth bounds the step of a task · Depth of a task in a computation DAG
Used byBrent's theorem with the work and span laws

DefinitionLevel size#✓fully proved

For a computation DAG and a natural number \(d\), the size of level \(d\) is the number of tasks of depth \(d\).

def levelCard (d : ℕ) : ℕ := (Finset.univ.filter fun v => depth G v = d).card
Uses 2 · Used by 5
Statement usesComputation DAG · Depth of a task in a computation DAG
Used byNo step of Brent's level schedule mixes levels · Level \(0\) is empty · Brent's level schedule · Brent's theorem · Steps of a level

DefinitionSteps of a level#✓fully proved

For a computation DAG and natural numbers \(p\) and \(d\), let \(L_d\) be the number of tasks of depth \(d\). The number of steps of level \(d\) on \(p\) processors is \(\lceil L_d / p \rceil\) if \(p \ge 1\), and \(0\) if \(p = 0\).

def levelSteps (p d : ℕ) : ℕ := (levelCard G d + p - 1) / p
Uses 2 · Used by 4
Statement usesComputation DAG · Level size
Used byNo step of Brent's level schedule mixes levels · Brent's level schedule · Brent's theorem · First step of a level

DefinitionFirst step of a level#✓fully proved

For a computation DAG and natural numbers \(p\) and \(d\), let \(s_e\) be the number of steps of level \(e\) on \(p\) processors: \(\lceil L_e / p \rceil\) if \(p \ge 1\) and \(0\) if \(p = 0\), where \(L_e\) is the number of tasks of depth \(e\). The first step of level \(d\) is \(\sum_{e < d} s_e\).

def offset (p d : ℕ) : ℕ := ∑ e ∈ Finset.range d, levelSteps G p e
Uses 2 · Used by 4
Statement usesComputation DAG · Steps of a level
Used byNo step of Brent's level schedule mixes levels · Brent's level schedule · Brent's theorem · Step of a task in Brent's schedule

DefinitionRank within a level#✓fully proved

In a computation DAG, the rank of a task \(v\) is the number of tasks of the same depth as \(v\) with a smaller number than \(v\). Taken in numbering order, the tasks of a level have ranks \(0, 1, 2, \dots\)

def rank (v : Fin n) : ℕ := (Finset.univ.filter fun u => depth G u = depth G v ∧ u < v).card
Uses 2 · Used by 5
Statement usesComputation DAG · Depth of a task in a computation DAG
Used byNo step of Brent's level schedule mixes levels · Brent's level schedule · Brent's theorem · Step of a task in Brent's schedule · Ranks increase within a level

DefinitionStep of a task in Brent's schedule#✓fully proved

Let \(G\) be a computation DAG and \(p\) a natural number. If \(p \ge 1\), for each \(d\) let \(L_d\) be the number of tasks of depth \(d\) and \(o_d = \sum_{e < d} \lceil L_e / p \rceil\), and for each task \(v\) let \(r(v)\) be the number of tasks of the same depth as \(v\) with a smaller number; the step of a task \(v\) is \(o_{\operatorname{depth}(v)} + \lfloor r(v) / p \rfloor\). If \(p = 0\), the step of every task is \(0\).

For \(p \ge 1\) this runs the tasks level by level, each level of \(L_d\) tasks in \(\lceil L_d / p \rceil\) steps of at most \(p\) tasks.

def levelTime (p : ℕ) (v : Fin n) : ℕ := offset G p (depth G v) + rank G v / p
Uses 4 · Used by 3
Statement usesComputation DAG · Depth of a task in a computation DAG · First step of a level · Rank within a level
Used byNo step of Brent's level schedule mixes levels · Brent's level schedule · Brent's theorem

TheoremNo step of Brent's level schedule mixes levels#✓fully proved

Let \(G\) be a computation DAG and \(p \ge 1\). If two tasks \(u\) and \(v\) run in the same step of Brent's level-by-level schedule on \(p\) processors, then \(u\) and \(v\) have the same depth.

theorem depth_eq_of_levelTime_eq {p : ℕ} (hp : 1 ≤ p) {u v : Fin n}
    (h : levelTime G p u = levelTime G p v) : depth G u = depth G v
Uses 7 · Used by 1
Statement usesComputation DAG · Depth of a task in a computation DAG · Step of a task in Brent's schedule
Proof usesLevel size · Steps of a level · First step of a level · Rank within a level
Used byBrent's level schedule

TheoremRanks increase within a level#✓fully proved

In a computation DAG, if tasks \(u\) and \(v\) have the same depth and \(u\) has a smaller number than \(v\), then the rank of \(u\) is smaller than the rank of \(v\), where the rank of a task is the number of tasks of the same depth with a smaller number. In particular, ranks are distinct within a level.

theorem rank_lt_rank {u v : Fin n} (hd : depth G u = depth G v) (h : u < v) :
    rank G u < rank G v
Uses 3 · Used by 1
Statement usesComputation DAG · Depth of a task in a computation DAG · Rank within a level
Used byBrent's level schedule

DefinitionBrent's level schedule#✓fully proved

Let \(G\) be a computation DAG and \(p \ge 1\). For each \(d\) let \(L_d\) be the number of tasks of depth \(d\) and \(o_d = \sum_{e < d} \lceil L_e / p \rceil\), and for each task \(v\) let \(r(v)\) be the number of tasks of the same depth as \(v\) with a smaller number. Brent's level schedule is the schedule of \(G\) on \(p\) processors that runs each task \(v\) at step \(o_{\operatorname{depth}(v)} + \lfloor r(v) / p \rfloor\).

It runs the tasks level by level, in order of depth, each level of \(L_d\) tasks in \(\lceil L_d / p \rceil\) steps of at most \(p\) tasks.

Cslib.Algorithms.Lean.Parallel.Brent.levelSchedule · 41 lines 
def levelSchedule {p : ℕ} (hp : 1 ≤ p) : Schedule G p where
  time := levelTime G p
  prec v u hu := by
    have hlt := depth_lt_of_mem G hu
    have h1 := levelTime_lt G hp u
    have h2 := offset_add_le G (p := p) hlt
    have h3 : offset G p (depth G v) ≤ levelTime G p v := Nat.le_add_right _ _
    omega
  cap t := by
    by_cases hne : (Finset.univ.filter fun v => levelTime G p v = t).Nonempty
    · obtain ⟨w, hw⟩ := hne
      have hwt : levelTime G p w = t := (Finset.mem_filter.1 hw).2
      set j := rank G w / p
      -- every task in step `t` has rank in `[j p, j p + p)`
      have hmaps : ∀ v ∈ Finset.univ.filter (fun v => levelTime G p v = t),
          rank G v ∈ Finset.Ico (j * p) (j * p + p) := fun v hv => by
        have hvt : levelTime G p v = t := (Finset.mem_filter.1 hv).2
        have hd := depth_eq_of_levelTime_eq G hp (hvt.trans hwt.symm)
        have hj : rank G v / p = j := by
          have := hvt.trans hwt.symm
          unfold levelTime at this
          rw [hd] at this
          omega
        rw [Finset.mem_Ico]
        constructor
        · rw [← hj]; exact Nat.div_mul_le_self _ _
        · rw [← hj]
          have := Nat.lt_div_mul_add (a := rank G v) (show 0 < p by omega)
          omega
      have hinj : Set.InjOn (rank G) (Finset.univ.filter fun v => levelTime G p v = t) :=
        fun u hu v hv huv => by
          have hd := depth_eq_of_levelTime_eq G hp
            ((Finset.mem_filter.1 hu).2.trans (Finset.mem_filter.1 hv).2.symm)
          by_contra hne
          rcases lt_or_gt_of_ne hne with h | h
          · exact absurd huv (Nat.ne_of_lt (rank_lt_rank G hd h))
          · exact absurd huv (Nat.ne_of_gt (rank_lt_rank G hd.symm h))
      have := Finset.card_le_card_of_injOn (rank G) hmaps hinj
      rwa [Nat.card_Ico, Nat.add_sub_cancel_left] at this
    · rw [Finset.not_nonempty_iff_eq_empty.1 hne, Finset.card_empty]
      exact Nat.zero_le _
Uses 11 · Used by 2
Statement usesComputation DAG · Schedule of a computation DAG · Depth of a task in a computation DAG · No step of Brent's level schedule mixes levels · Predecessors have smaller depth · Level size · Steps of a level · Step of a task in Brent's schedule · First step of a level · Rank within a level · Ranks increase within a level
Used byBrent's theorem with the work and span laws · Brent's theorem

TheoremLevel \(0\) is empty#✓fully proved

In every computation DAG no task has depth \(0\), so the number of tasks of depth \(0\) is \(0\).

theorem levelCard_zero : levelCard G 0 = 0
Uses 3 · Used by 1
Statement usesComputation DAG · Level size
Proof usesDepth of a task in a computation DAG
Used byBrent's theorem

TheoremBrent's theorem#✓fully proved

Let \(G\) be a computation DAG with \(n\) tasks and span \(D\), and let \(p \ge 1\). If Brent's level schedule of \(G\) on \(p\) processors takes \(T\) steps, then \(pT \le n + (p - 1) D\), that is, \(T \le (n - D)/p + D\).

theorem levelSchedule_length {p : ℕ} (hp : 1 ≤ p) :
    p * (levelSchedule G hp).length ≤ n + (p - 1) * span G
Uses 12 · Used by 1
Statement usesComputation DAG · Length of a schedule · Brent's level schedule · Span of a computation DAG
Proof usesSchedule of a computation DAG · Depth of a task in a computation DAG · Level size · Level \(0\) is empty · Steps of a level · Step of a task in Brent's schedule · First step of a level · Rank within a level
Used byBrent's theorem with the work and span laws

TheoremBrent's theorem with the work and span laws#✓fully proved

Let \(G\) be a computation DAG on \(n\) unit-time tasks with span \(D\), and let \(p \ge 1\). Then some schedule of \(G\) on \(p\) processors has length \(T\) with \(pT \le n + (p - 1)D\), and every schedule of \(G\) on \(p\) processors has a length \(T'\) with \(n \le pT'\) (the work law) and \(D \le T'\) (the span law).

theorem brent {p : ℕ} (hp : 1 ≤ p) :
    ∃ S : Schedule G p, p * S.length ≤ n + (p - 1) * span G ∧
      ∀ S' : Schedule G p, n ≤ p * S'.length ∧ span G ≤ S'.length
Uses 8
Statement usesComputation DAG · Schedule of a computation DAG · Length of a schedule · Span of a computation DAG
Proof usesThe span law · The work law · Brent's level schedule · Brent's theorem

DefinitionLoad of a step#✓fully proved

The load of step \(t\) in a schedule \(S\) of a computation DAG is the number of tasks that \(S\) runs in step \(t\).

def Schedule.load (S : Schedule G p) (t : ℕ) : ℕ := (Finset.univ.filter fun v => S.time v = t).card
Uses 2 · Used by 9
Statement usesComputation DAG · Schedule of a computation DAG
Used byGreedy schedule · Greediness need only be checked at the steps of the schedule · The greedy scheduling bound · Number of incomplete steps · A greedy schedule has at most \(D\) incomplete steps · Each incomplete step advances the critical path · Complete steps are bounded by the work · A greedy schedule never idles · The step loads add up to the number of tasks

DefinitionReady task#✓fully proved

In a schedule \(S\) of a task graph, a task \(v\) is ready at step \(t\) if \(v\) runs in a step later than \(t\) and every predecessor of \(v\) runs in a step earlier than \(t\).

def Schedule.Ready (S : Schedule G p) (t : ℕ) (v : Fin n) : Prop :=
  t < S.time v ∧ ∀ u ∈ G.preds v, S.time u < t
Uses 2 · Used by 4
Statement usesComputation DAG · Schedule of a computation DAG
Used byGreedy schedule · Greediness need only be checked at the steps of the schedule · Each incomplete step advances the critical path · A greedy schedule never idles

DefinitionGreedy schedule#✓fully proved

A schedule \(S\) of a computation DAG on \(p\) processors is greedy if, for every step \(t\) and every task that is ready at step \(t\), exactly \(p\) tasks run in step \(t\): a step leaves a ready task waiting only when all \(p\) processors are busy.

def Schedule.Greedy (S : Schedule G p) : Prop := ∀ t v, S.Ready t v → S.load t = p
Uses 4 · Used by 6
Statement usesComputation DAG · Schedule of a computation DAG · Ready task · Load of a step
Used byGreediness need only be checked at the steps of the schedule · The work-span bound for greedy schedules · The greedy scheduling bound · A greedy schedule has at most \(D\) incomplete steps · Each incomplete step advances the critical path · A greedy schedule never idles

TheoremGreediness need only be checked at the steps of the schedule#✓fully proved

Let \(S\) be a schedule of a computation DAG on \(p\) processors taking \(T\) steps. Then \(S\) is greedy if and only if, for every step \(t < T\) and every task \(v\) that is ready at step \(t\), exactly \(p\) tasks run in step \(t\).

This holds because a task is never ready at or after the last step.

theorem Schedule.greedy_iff (S : Schedule G p) :
    S.Greedy ↔ ∀ t < S.length, ∀ v, S.Ready t v → S.load t = p
Uses 6
Statement usesComputation DAG · Schedule of a computation DAG · Greedy schedule · Ready task · Length of a schedule · Load of a step

DefinitionNumber of incomplete steps#✓fully proved

For a schedule \(S\) of a computation DAG on \(p\) processors and a natural number \(t\), the number of incomplete steps before step \(t\) is the number of steps \(s < t\) in which \(S\) runs fewer than \(p\) tasks.

def Schedule.incomplete (S : Schedule G p) (t : ℕ) : ℕ :=
  ((Finset.range t).filter fun s => S.load s < p).card
Uses 3 · Used by 2
Statement usesComputation DAG · Schedule of a computation DAG · Load of a step
Used byA greedy schedule has at most \(D\) incomplete steps · Each incomplete step advances the critical path

TheoremEach incomplete step advances the critical path#✓fully proved

In a greedy schedule, fewer than depth v incomplete steps precede the step of task v.

theorem Schedule.incomplete_lt_depth (S : Schedule G p) (hS : S.Greedy) :
    ∀ (t : ℕ) (v : Fin n), S.time v = t → S.incomplete t < depth G v
Uses 8 · Used by 1
Statement usesComputation DAG · Schedule of a computation DAG · Greedy schedule · Number of incomplete steps · Depth of a task in a computation DAG
Proof usesReady task · Load of a step · Predecessors have smaller depth
Used byA greedy schedule has at most \(D\) incomplete steps

TheoremThe step loads add up to the number of tasks#✓fully proved

For a schedule \(S\) of a task graph with \(n\) tasks that takes \(T\) steps, the numbers of tasks run in the steps \(0, 1, \dots, T - 1\) add up to \(n\).

theorem Schedule.sum_load (S : Schedule G p) :
    ∑ t ∈ Finset.range S.length, S.load t = n
Uses 4 · Used by 2
Statement usesComputation DAG · Schedule of a computation DAG · Length of a schedule · Load of a step
Used byThe greedy scheduling bound · Complete steps are bounded by the work

TheoremComplete steps are bounded by the work#✓fully proved

Let \(G\) be a computation DAG with \(n\) tasks, and let \(S\) be a schedule of \(G\) on \(p\) processors taking \(T\) steps. If \(C\) is the number of steps \(t < T\) in which \(S\) runs at least \(p\) tasks (the complete steps, where all \(p\) processors are busy), then \(pC \le n\).

theorem Schedule.mul_complete_le (S : Schedule G p) :
    p * ((Finset.range S.length).filter fun s => ¬ S.load s < p).card ≤ n
Uses 5
Statement usesComputation DAG · Schedule of a computation DAG · Length of a schedule · Load of a step
Proof usesThe step loads add up to the number of tasks

TheoremA greedy schedule has at most \(D\) incomplete steps#✓fully proved

Let \(G\) be a computation DAG with span \(D\), and let \(S\) be a greedy schedule of \(G\) on \(p\) processors taking \(T\) steps. Then at most \(D\) of the steps \(t < T\) are incomplete, that is, run fewer than \(p\) tasks.

theorem Schedule.incomplete_length_le (S : Schedule G p) (hS : S.Greedy) :
    S.incomplete S.length ≤ span G
Uses 9 · Used by 1
Statement usesComputation DAG · Schedule of a computation DAG · Greedy schedule · Number of incomplete steps · Length of a schedule · Span of a computation DAG
Proof usesEach incomplete step advances the critical path · Load of a step · Depth of a task in a computation DAG
Used byThe greedy scheduling bound

TheoremEvery step of a schedule has a task running at or after it#✓fully proved

Let \(S\) be a schedule of a computation DAG on \(p\) processors taking \(T\) steps, numbered from \(0\). For every step \(t < T\) there is a task that \(S\) runs at step \(t\) or later.

theorem Schedule.exists_le_time (S : Schedule G p) {t : ℕ} (ht : t < S.length) :
    ∃ v, t ≤ S.time v
Uses 3 · Used by 1
Statement usesComputation DAG · Schedule of a computation DAG · Length of a schedule
Used byA greedy schedule never idles

TheoremA greedy schedule never idles#✓fully proved

Let \(S\) be a greedy schedule of a task graph on \(p\) processors that takes \(T\) steps, numbered \(0, \dots, T - 1\). Then every step \(t < T\) of \(S\) runs at least one task.

The task that runs earliest among those not run before step \(t\) has all its predecessors done before step \(t\). If step \(t\) ran no task, this task would be ready at step \(t\), while a greedy step with a ready task keeps all \(p\) processors busy.

theorem Schedule.one_le_load (S : Schedule G p) (hS : S.Greedy) {t : ℕ} (ht : t < S.length) :
    1 ≤ S.load t
Uses 7 · Used by 1
Statement usesComputation DAG · Schedule of a computation DAG · Greedy schedule · Length of a schedule · Load of a step
Proof usesReady task · Every step of a schedule has a task running at or after it
Used byThe greedy scheduling bound

TheoremThe greedy scheduling bound#✓fully proved

Let \(G\) be a computation DAG with \(n\) tasks and span \(D\), and let \(S\) be a greedy schedule of \(G\) on \(p\) processors taking \(T\) steps. Then \(pT \le n + (p - 1)D\).

Each complete step runs \(p\) tasks, and each of the at most \(D\) incomplete steps runs at least one.

theorem Schedule.greedy_length_le (S : Schedule G p) (hS : S.Greedy) :
    p * S.length ≤ n + (p - 1) * span G
Sources
  • the unit-task case of Graham's list-scheduling argument, Graham, Bounds for certain multiprocessing anomalies, Bell System Tech. J. 45, 1966.
Uses 9 · Used by 1
Statement usesComputation DAG · Schedule of a computation DAG · Greedy schedule · Length of a schedule · Span of a computation DAG
Proof usesA greedy schedule has at most \(D\) incomplete steps · Load of a step · A greedy schedule never idles · The step loads add up to the number of tasks
Used byThe work-span bound for greedy schedules

TheoremThe work-span bound for greedy schedules#✓fully proved

Let \(G\) be a computation DAG with \(n\) tasks and span \(D\), and let \(S\) be a greedy schedule of \(G\) on \(p\) processors taking \(T\) steps. Then \(pT \le n + pD\), that is, \(T \le n/p + D\) when \(p \ge 1\).

This is a weakening of the greedy scheduling bound \(pT \le n + (p - 1)D\).

theorem Schedule.greedy_length (S : Schedule G p) (hS : S.Greedy) :
    p * S.length ≤ n + p * span G
Sources
  • CLRS, third edition, Theorem 27.1.
Uses 6
Statement usesComputation DAG · Schedule of a computation DAG · Greedy schedule · Length of a schedule · Span of a computation DAG
Proof usesThe greedy scheduling bound
36 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.