Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Preemptive scheduling on parallel machines

Lax434175.Preemptive · concepts/Lax434175/Preemptive.lean · lax-434175

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    A preemptive schedule is a finite list of pieces. A piece processes one job on a nonempty set of machines during an interval given by a start time and a length, both nonnegative rational numbers.

    A piece of length ℓ\ell of job jj on a set of machines on which the job needs time pp completes the fraction ℓ/p\ell / p of the job. A schedule is feasible for the kernel if

    • two different pieces that share a machine or a job are disjoint in time, so a machine processes one job at a time and a job is processed in one place at a time, and
    • every job is completed: its fractions sum to 11, or one of its pieces is on machines on which it needs time 00.

    A job starts when its first piece starts and completes when its last piece ends.

    Theorem. Every job starts no later than it completes.

    Concept map
    4 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Mathlib.Algebra.Order.Field.Rat
    2import Mathlib.Algebra.Order.Ring.Rat
    3import Lax434175.ParallelMachines
    4
    5/-!
    6---
    7title: Preemptive scheduling on parallel machines
    8type: theorem
    9---
    10A preemptive schedule is a finite list of pieces. A piece processes one job
    11on a nonempty set of machines during an interval given by a start time and a
    12length, both nonnegative rational numbers.
    13
    14A piece of length ℓ\ell of job jj on a set of machines on which the job
    15needs time pp completes the fraction ℓ/p\ell / p of the job. A schedule is
    16feasible for the kernel if
    17
    18- two different pieces that share a machine or a job are disjoint in time,
    19 so a machine processes one job at a time and a job is processed in one
    20 place at a time, and
    21- every job is completed: its fractions sum to 11, or one of its pieces is
    22 on machines on which it needs time 00.
    23
    24A job starts when its first piece starts and completes when its last piece
    25ends.
    26
    27**Theorem.** Every job starts no later than it completes.
    28-/
    29
    30namespace Lax434175.Preemptive
    31open Lax434175.Kernels Lax434175.ParallelMachines
    32
    33/-- A job is processed on a set of machines from `start` for `length` time
    34units. -/
    35structure Piece (x : Inst) where
    36 job : Fin x.jobs
    37 machines : Finset (Fin x.machines)
    38 start : NNRat
    39 length : NNRat
    40
    41/-- The time at which a piece ends. -/
    42def Piece.finish {x : Inst} (q : Piece x) : NNRat := q.start + q.length
    43
    44structure Sched (x : Inst) where
    45 pieces : List (Piece x)
    46
    47/-- The pieces of a job. -/
    48def piecesOf {x : Inst} (σ : Sched x) (j : Fin x.jobs) : List (Piece x) :=
    49 σ.pieces.filter (fun q => decide (q.job = j))
    50
    51/-- The fraction of a job that a schedule completes. -/
    52def fraction (x : Inst) (σ : Sched x) (j : Fin x.jobs) : NNRat :=
    53 ((piecesOf σ j).map (fun q => q.length / (duration x j q.machines : NNRat))).sum
    54
    55/-- Two pieces do not overlap in time. -/
    56def Apart {x : Inst} (a b : Piece x) : Prop :=
    57 a.finish ≤ b.start ∨ b.finish ≤ a.start
    58
    59def feasible (x : Inst) (σ : Sched x) : Prop :=
    60 (∀ q ∈ σ.pieces, q.machines.Nonempty) ∧
    61 σ.pieces.Pairwise (fun a b => (¬ Disjoint a.machines b.machines ∨ a.job = b.job) → Apart a b) ∧
    62 ∀ j, fraction x σ j = 1 ∨ ∃ q ∈ piecesOf σ j, duration x j q.machines = 0
    63
    64/-- The start of the first piece of a job. -/
    65def start (x : Inst) (σ : Sched x) (j : Fin x.jobs) : NNRat :=
    66 (((piecesOf σ j).map Piece.start).min?).getD 0
    67
    68/-- The end of the last piece of a job. -/
    69def completion (x : Inst) (σ : Sched x) (j : Fin x.jobs) : NNRat :=
    70 (((piecesOf σ j).map Piece.finish).max?).getD 0
    71
    72/-- The kernel of preemptive scheduling on parallel machines. -/
    73def kernel : Kernel where
    74 Inst := Inst
    75 jobs := Inst.jobs
    76 release := Inst.r
    77 Sched := Sched
    78 feasible := feasible
    79 start := start
    80 completion := completion
    81
    82/-- Preemptive scheduling as a machine model. -/
    83def model : Model where
    84 kernel := kernel
    85 inst x := x
    86 jobs_eq _ := rfl
    87 uses _ σ j S := ∃ q ∈ piecesOf σ j, q.machines = S
    88
    89axiom startsBeforeCompletion : kernel.StartsBeforeCompletion
    90
    91end Lax434175.Preemptive
    92
    Show Proof
    Builds on
    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…