Lax Lean Archive

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

Preemption with restarts on parallel machines

Lax434175.Restarts · concepts/Lax434175/Restarts.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

    With restarts a job may be interrupted, but then its processing is lost and it has to be processed again from the beginning. A schedule is a finite list of pieces as in preemptive scheduling. It is feasible for the kernel if two different pieces that share a machine or a job are disjoint in time and every job has a complete piece, whose length is the full time the job needs on the machines of the piece. A job starts when its first piece starts and completes when its first complete piece ends.

    Theorem. In every feasible schedule, every job starts no later than it completes.

    Concept map
    5 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 Lax434175.Preemptive
    2
    3/-!
    4---
    5title: Preemption with restarts on parallel machines
    6type: theorem
    7---
    8With restarts a job may be interrupted, but then its processing is lost and
    9it has to be processed again from the beginning. A schedule is a finite list
    10of pieces as in preemptive scheduling. It is feasible for the kernel if two
    11different pieces that share a machine or a job are disjoint in time and
    12every job has a complete piece, whose length is the full time the job needs
    13on the machines of the piece. A job starts when its first piece starts and
    14completes when its first complete piece ends.
    15
    16**Theorem.** In every feasible schedule, every job starts no later than it
    17completes.
    18-/
    19
    20namespace Lax434175.Restarts
    21open Lax434175.Kernels Lax434175.ParallelMachines Lax434175.Preemptive
    22
    23/-- A piece processes its job entirely. -/
    24def Complete {x : Inst} (q : Piece x) : Prop :=
    25 q.length = (duration x q.job q.machines : NNRat)
    26
    27instance {x : Inst} (q : Piece x) : Decidable (Complete q) :=
    28 inferInstanceAs (Decidable (q.length = _))
    29
    30/-- The complete pieces of a job. -/
    31def completePieces {x : Inst} (σ : Sched x) (j : Fin x.jobs) : List (Piece x) :=
    32 (piecesOf σ j).filter (fun q => decide (Complete q))
    33
    34def feasible (x : Inst) (σ : Sched x) : Prop :=
    35 (∀ q ∈ σ.pieces, q.machines.Nonempty) ∧
    36 σ.pieces.Pairwise (fun a b => (¬ Disjoint a.machines b.machines ∨ a.job = b.job) → Apart a b) ∧
    37 ∀ j, completePieces σ j ≠ []
    38
    39/-- The end of the first complete piece of a job. -/
    40def completion (x : Inst) (σ : Sched x) (j : Fin x.jobs) : NNRat :=
    41 (((completePieces σ j).map Piece.finish).min?).getD 0
    42
    43/-- The kernel of scheduling with restarts on parallel machines. -/
    44def kernel : Kernel where
    45 Inst := Inst
    46 jobs := Inst.jobs
    47 release := Inst.r
    48 Sched := Sched
    49 feasible := feasible
    50 start := start
    51 completion := completion
    52
    53/-- Scheduling with restarts as a machine model. -/
    54def model : Model where
    55 kernel := kernel
    56 inst x := x
    57 jobs_eq _ := rfl
    58 uses _ σ j S := ∃ q ∈ piecesOf σ j, q.machines = S
    59
    60axiom startsBeforeCompletion : kernel.StartsBeforeCompletion
    61
    62end Lax434175.Restarts
    63
    Show Proof
    Builds on
    Used by
    From Mathlib

    none

    Discussion

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

    Loading discussion…