List scheduling on identical machines

DefinitionSchedule of a list of jobs#✓fully proved

Let \(m\) be a natural number. An assignment \(\sigma\) of a list \(\sigma(i)\) of natural numbers (processing times) to each machine \(i \in \{0, \dots, m - 1\}\) is a schedule of a list \(J\) of natural numbers when the sum over all machines \(i\) of the multisets of entries of \(\sigma(i)\) equals the multiset of entries of \(J\), that is, every number occurs in the lists \(\sigma(i)\) together exactly as often as it occurs in \(J\).

def IsScheduleOf (σ : Fin m → List ℕ) (ps : List ℕ) : Prop :=
  ∑ i, (σ i : Multiset ℕ) = (ps : Multiset ℕ)

Used by 11

Used byThe empty schedule · Every job is at most the makespan · Graham's bound for list scheduling · List scheduling schedules every job · Invariant bound for list scheduling · Graham's bound for LPT scheduling · The LPT placement step · A least-loaded machine carries at most the average load · List-scheduling state invariant · Total work is at most \(m\) times the makespan · Counting jobs when every machine is heavily loaded

DefinitionMakespan#✓fully proved

For a schedule \(\sigma\) that gives each of \(m\) machines a list of processing times, the load of a machine is the sum of its list, and the makespan of \(\sigma\) is the largest machine load (\(0\) when \(m = 0\)).

def makespan (σ : Fin m → List ℕ) : ℕ :=
  Finset.univ.sup fun i => (σ i).sum

Used by 6

Used byEvery job is at most the makespan · Graham's bound for list scheduling · Invariant bound for list scheduling · Graham's bound for LPT scheduling · The LPT placement step · Total work is at most \(m\) times the makespan

DefinitionLeast-loaded machine#✓fully proved

Let \(m \ge 1\) and let \(L\) assign a load \(L(i) \in \mathbb{N}\) to each machine \(i \in \{0, \dots, m - 1\}\). The least-loaded machine for \(L\) is the smallest index \(i\) at which \(L(i)\) is minimal.

def leastLoaded [NeZero m] (loads : Fin m → ℕ) : Fin m :=
  ((List.finRange m).argmin loads).getD 0

Used by 7

Used byGraham's bound for list scheduling · List scheduling schedules every job · List scheduling from an intermediate state · Invariant bound for list scheduling · Running time of list scheduling · The LPT placement step · A least-loaded machine carries at most the average load

DefinitionList scheduling from an intermediate state#✓fully proved

Let \(m \ge 1\). Given loads \(L(i)\) and job lists \(\sigma(i)\) for the machines \(i \in \{0, \dots, m - 1\}\) and a list of remaining jobs, list scheduling returns \(\sigma\) at cost \(0\) when no jobs remain. Otherwise it charges cost \(m\), takes the first remaining job \(p\), appends \(p\) to \(\sigma(k)\) and adds \(p\) to \(L(k)\) for the least-loaded machine \(k\) for \(L\), and continues in the same way with the other remaining jobs. The loads \(L\) are not required to be the sums of the lists \(\sigma(i)\).

def listScheduleScan [NeZero m] (loads : Fin m → ℕ) (σ : Fin m → List ℕ) :
    List ℕ → TimeM ℕ (Fin m → List ℕ)
  | [] => pure σ
  | p :: ps => do
      ✓[m]
      let i := leastLoaded loads
      listScheduleScan (Function.update loads i (loads i + p))
        (Function.update σ i (σ i ++ [p])) ps

Uses 1 · Used by 4

Statement usesLeast-loaded machine

Used byGraham's list scheduling · List scheduling schedules every job · Invariant bound for list scheduling · Running time of list scheduling

DefinitionGraham's list scheduling#✓fully proved

Given \(m \ge 1\) identical machines and a list of job processing times (natural numbers), start with every machine empty and take the jobs in the given order, appending each job to the list of a currently least-loaded machine (the first one in index order), where the load of a machine is the sum of its jobs. The result assigns to each machine its list of jobs. The cost counted is \(m\) per job, one unit for each machine load inspected.

def listSchedule (m : ℕ) [NeZero m] (ps : List ℕ) : TimeM ℕ (Fin m → List ℕ) :=
  listScheduleScan (fun _ => 0) (fun _ => []) ps

Uses 1 · Used by 5

Statement usesList scheduling from an intermediate state

Used byGraham's bound for list scheduling · List scheduling schedules every job · Running time of list scheduling · Longest processing time first (LPT) · Running time of LPT

DefinitionLongest processing time first (LPT)#✓fully proved

Given \(m \ge 1\) identical machines and a list of job processing times (natural numbers), LPT sorts the jobs into nonincreasing order by merge sort and then applies Graham's list scheduling on \(m\) machines to the sorted list. The cost counted is the number of comparisons made by merge sort plus the cost of list scheduling, \(m\) per job.

def lpt (m : ℕ) [NeZero m] (ps : List ℕ) : TimeM ℕ (Fin m → List ℕ) := do
  let sorted ← mergeSort (ps.map OrderDual.toDual)
  listSchedule m (sorted.map OrderDual.ofDual)

Uses 1 · Used by 2

Statement usesGraham's list scheduling

Used byGraham's bound for LPT scheduling · Running time of LPT

20 fully proved

Schedules

TheoremThe empty schedule#✓fully proved

For every number \(m\) of machines, the assignment of the empty list to each of the \(m\) machines is a schedule of the empty list of jobs.

theorem isScheduleOf_nil : IsScheduleOf (fun _ : Fin m => ([] : List ℕ)) []

Uses 1 · Used by 3

Statement usesSchedule of a list of jobs

Used byGraham's bound for list scheduling · List scheduling schedules every job · Graham's bound for LPT scheduling

TheoremEvery job is at most the makespan#✓fully proved

Let \(\sigma\) be a schedule on \(m\) machines of a list \(J\) of processing times. Then every entry \(x\) of \(J\) is at most the makespan of \(\sigma\).

theorem IsScheduleOf.le_makespan {σ : Fin m → List ℕ} {ps : List ℕ} (h : IsScheduleOf σ ps)
    {x : ℕ} (hx : x ∈ ps) : x ≤ makespan σ

Uses 2 · Used by 2

Statement usesSchedule of a list of jobs · Makespan

Used byGraham's bound for list scheduling · The LPT placement step

TheoremTotal work is at most \(m\) times the makespan#✓fully proved

If \(\sigma\) is a schedule of a list \(P\) of jobs on \(m\) machines, then the total processing time of \(P\) is at most \(m\) times the makespan of \(\sigma\).

theorem IsScheduleOf.sum_le {σ : Fin m → List ℕ} {ps : List ℕ} (h : IsScheduleOf σ ps) :
    ps.sum ≤ m * makespan σ

Uses 2 · Used by 2

Statement usesSchedule of a list of jobs · Makespan

Used byGraham's bound for list scheduling · The LPT placement step

The scan invariant

DefinitionList-scheduling state invariant#✓fully proved

A list \(P\) of jobs, machine loads \(\ell_i \in \mathbb{N}\) for \(i < m\), and a schedule \(\sigma\) on \(m\) machines satisfy the invariant when \(\sigma\) is a schedule of \(P\) and, for every machine \(i\), \(\ell_i\) is the load of machine \(i\) in \(\sigma\), the sum of the processing times assigned to it.

def ScanInv (P : List ℕ) (loads : Fin m → ℕ) (σ : Fin m → List ℕ) : Prop :=
  (∀ i, loads i = (σ i).sum) ∧ IsScheduleOf σ P

Uses 1 · Used by 6

Statement usesSchedule of a list of jobs

Used byGraham's bound for list scheduling · List scheduling schedules every job · Invariant bound for list scheduling · Graham's bound for LPT scheduling · The LPT placement step · A least-loaded machine carries at most the average load

TheoremInvariant bound for list scheduling#✓fully proved

Let \(m \ge 1\) and \(a, b, M \in \mathbb{N}\). Let \(\sigma\) assign job lists to the \(m\) machines so that \(\sigma\) is a schedule of a list \(P\) of jobs already placed, let \(L(i)\) be the sum of \(\sigma(i)\) for each machine \(i\), and let \(R\) be a list of remaining jobs. Assume that \(a\) times the makespan of \(\sigma\) is at most \(bM\). Assume also that whenever \(P\) followed by \(R\) equals \(P'\) followed by a job \(p\) followed by a list \(R'\), and \(\sigma'\) is any schedule of \(P'\) with loads \(L'(i)\) equal to the sum of \(\sigma'(i)\), we have \(a(L'(k) + p) \le bM\), where \(k\) is the least-loaded machine for \(L'\). Then list scheduling of \(R\) started from the loads \(L\) and machine lists \(\sigma\) produces a schedule whose makespan \(C\) satisfies \(aC \le bM\).

theorem listScheduleScan_bound [NeZero m] {a b M : ℕ} {P : List ℕ} {loads : Fin m → ℕ}
    {σ : Fin m → List ℕ} (h : ScanInv P loads σ) (rest : List ℕ)
    (h0 : a * makespan σ ≤ b * M)
    (hstep : ∀ P' p rest' (loads' : Fin m → ℕ) (σ' : Fin m → List ℕ),
      P ++ rest = P' ++ p :: rest' → ScanInv P' loads' σ' →
        a * (loads' (leastLoaded loads') + p) ≤ b * M) :
    a * makespan (listScheduleScan loads σ rest).ret ≤ b * M

Uses 5 · Used by 2

Statement usesList-scheduling state invariant · Least-loaded machine · List scheduling from an intermediate state · Makespan

Proof usesSchedule of a list of jobs

Used byGraham's bound for list scheduling · Graham's bound for LPT scheduling

TheoremA least-loaded machine carries at most the average load#✓fully proved

Let \(\sigma\) be a schedule of a list \(P\) of jobs on \(m \ge 1\) machines, with load \(\ell_i\) on machine \(i\). Then \(m\) times the load of a least-loaded machine is at most the total processing time \(T\) of the jobs in \(P\), counted with multiplicity: \(m \min_i \ell_i \le T\).

theorem mul_leastLoaded_le [NeZero m] {P : List ℕ} {loads : Fin m → ℕ} {σ : Fin m → List ℕ}
    (h : ScanInv P loads σ) : m * loads (leastLoaded loads) ≤ P.sum

Uses 3 · Used by 2

Statement usesList-scheduling state invariant · Least-loaded machine

Proof usesSchedule of a list of jobs

Used byGraham's bound for list scheduling · The LPT placement step

Graham's bound for list scheduling

TheoremGraham's bound for list scheduling#✓fully proved

Let \(m \ge 1\) and let \(J\) be a list of processing times. Let \(C\) be the makespan of the schedule that list scheduling on \(m\) machines produces from \(J\), taking the jobs in the order of \(J\), and let \(M\) be the makespan of any schedule of \(J\) on \(m\) machines. Then \(mC \le (2m - 1)M\), that is, \(C \le (2 - 1/m)M\).

theorem listSchedule_approx [NeZero m] (ps : List ℕ) (τ : Fin m → List ℕ)
    (hτ : IsScheduleOf τ ps) :
    m * makespan (listSchedule m ps).ret ≤ (2 * m - 1) * makespan τ

Sources

• Graham, "Bounds for certain multiprocessing anomalies", Bell System Technical Journal 45 (1966).

Uses 10

Statement usesSchedule of a list of jobs · Graham's list scheduling · Makespan

Proof usesEvery job is at most the makespan · Total work is at most \(m\) times the makespan · List-scheduling state invariant · The empty schedule · Least-loaded machine · Invariant bound for list scheduling · A least-loaded machine carries at most the average load

Graham's bound for LPT

TheoremCounting jobs when every machine is heavily loaded#✓fully proved

Let \(\sigma\) be a schedule of a list \(P\) of jobs on \(m\) machines, let \(p\) and \(M\) be natural numbers, and let \(d = \max(M - p, 0)\). If every job in \(P\) is at least \(p\) and every machine has load (the sum of its jobs) greater than \(d\), then \(2m \le n + k\), where \(n\) is the number of jobs in \(P\) and \(k\) is the number of jobs \(x\) in \(P\) with \(p \le x\) and \(x > d\), both counted with multiplicity.

The reason is that each machine then holds two jobs or one job longer than \(d\).

theorem two_mul_le_of_loads_gt {P : List ℕ} {σ : Fin m → List ℕ} (hσ : IsScheduleOf σ P)
    {p M : ℕ} (hP : ∀ x ∈ P, p ≤ x) (hload : ∀ i, M - p < (σ i).sum) :
    2 * m ≤ P.length + P.countP (fun x => decide (p ≤ x ∧ M - p < x))

Uses 1 · Used by 1

Statement usesSchedule of a list of jobs

Used byThe LPT placement step

TheoremAt most two long jobs per machine#✓fully proved

Let \(p\) and \(M\) be natural numbers with \(M < 3p\), and let \(\ell\) be a list of natural numbers (the jobs of one machine) whose sum is at most \(M\). Then the number of entries of \(\ell\) that are at least \(p\), plus the number of entries that are at least \(p\) and greater than \(M - p\), is at most \(2\). Here \(M - p\) is truncated subtraction, equal to \(0\) when \(M < p\). So \(\ell\) has at most two entries that are at least \(p\), and at most one if one of them is greater than \(M - p\).

theorem countP_add_countP_le {l : List ℕ} {p M : ℕ} (hl : l.sum ≤ M) (h3 : M < 3 * p) :
    l.countP (fun x => decide (p ≤ x)) + l.countP (fun x => decide (p ≤ x ∧ M - p < x)) ≤ 2

Used by 1

Used byThe LPT placement step

TheoremThe LPT placement step#✓fully proved

Let \(m \ge 1\) and let a list of job processing times, in nonincreasing order, be the concatenation of a list \(P\), a job \(p\) and a list \(R\). Let \(\sigma\) be a schedule of the jobs \(P\) on \(m\) machines, with load \(\ell_i\) on machine \(i\), and let \(L = \min_i \ell_i\) be the load of a least-loaded machine. Then for every schedule \(\tau\) of all the jobs on the \(m\) machines, with makespan \(M\), we have \(3m(L + p) \le (4m - 1)M\).

theorem lpt_step_le [NeZero m] {ps P rest : List ℕ} {p : ℕ} (hps : ps = P ++ p :: rest)
    (hsorted : ps.Pairwise (· ≥ ·)) {loads : Fin m → ℕ} {σ : Fin m → List ℕ}
    (hinv : ScanInv P loads σ) (τ : Fin m → List ℕ) (hτ : IsScheduleOf τ ps) :
    3 * m * (loads (leastLoaded loads) + p) ≤ (4 * m - 1) * makespan τ

Uses 9 · Used by 1

Statement usesSchedule of a list of jobs · List-scheduling state invariant · Least-loaded machine · Makespan

Proof usesEvery job is at most the makespan · Total work is at most \(m\) times the makespan · At most two long jobs per machine · A least-loaded machine carries at most the average load · Counting jobs when every machine is heavily loaded

Used byGraham's bound for LPT scheduling

TheoremGraham's bound for LPT scheduling#✓fully proved

Let \(m \ge 1\) and let \(J\) be a list of natural numbers (job processing times). Let \(C\) be the makespan of the schedule of \(J\) on \(m\) machines produced by the LPT algorithm, and let \(M\) be the makespan of any schedule \(\tau\) of \(J\) on \(m\) machines. Then \(3mC \le (4m - 1)M\), that is, \(C \le (4/3 - 1/(3m))M\).

theorem lpt_approx [NeZero m] (ps : List ℕ) (τ : Fin m → List ℕ) (hτ : IsScheduleOf τ ps) :
    3 * m * makespan (lpt m ps).ret ≤ (4 * m - 1) * makespan τ

Sources

• Graham, "Bounds on multiprocessing timing anomalies", SIAM J. Appl. Math. 17 (1969).

Uses 7

Statement usesSchedule of a list of jobs · Longest processing time first (LPT) · Makespan

Proof usesList-scheduling state invariant · The empty schedule · Invariant bound for list scheduling · The LPT placement step

Validity and cost

TheoremList scheduling schedules every job#✓fully proved

For \(m \ge 1\) and every list \(J\) of processing times, the assignment that list scheduling on \(m\) machines produces from \(J\) is a schedule of \(J\).

theorem listSchedule_isScheduleOf [NeZero m] (ps : List ℕ) :
    IsScheduleOf (listSchedule m ps).ret ps

Uses 6

Statement usesSchedule of a list of jobs · Graham's list scheduling

Proof usesList-scheduling state invariant · The empty schedule · Least-loaded machine · List scheduling from an intermediate state

TheoremRunning time of list scheduling#✓fully proved

For \(m \ge 1\) and every list of \(n\) jobs, list scheduling on \(m\) machines has cost exactly \(nm\), in the cost model that charges \(m\) for each job placed (one unit per machine load inspected).

@[simp]
theorem listSchedule_time [NeZero m] (ps : List ℕ) :
    (listSchedule m ps).time = ps.length * m

Uses 3 · Used by 1

Statement usesGraham's list scheduling

Proof usesLeast-loaded machine · List scheduling from an intermediate state

Used byRunning time of LPT

TheoremRunning time of LPT#✓fully proved

On \(m \ge 1\) machines and a list of \(n\) jobs, LPT costs at most \(n \lceil \log_2 n \rceil + nm\), counting merge-sort comparisons and machine load inspections.

theorem lpt_time_le [NeZero m] (ps : List ℕ) :
    (lpt m ps).time ≤ ps.length * Nat.clog 2 ps.length + ps.length * m

Uses 3

Statement usesLongest processing time first (LPT)

Proof usesGraham's list scheduling · Running time of list scheduling

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.