Interruption as a field of parallel-machine scheduling
Lax434175.Interruption · concepts/Lax434175/Interruption.lean · lax-434175
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
Non-preemptive scheduling, preemptive scheduling and scheduling with restarts on parallel machines share one machine model, in which a schedule is a finite list of pieces as in preemptive scheduling. A schedule is feasible for this model if every piece occupies some machine and two different pieces that share a machine or a job are disjoint in time. A job starts when its first piece starts and completes when its last piece ends.
How a job may be interrupted is a field with four values:
- none: every job has exactly one piece, it starts at an integral time, and its length is the full time the job needs on its machines;
- restarts: some piece of the job is complete, that is, its length is the full time the job needs on its machines, no piece of the job ends later, and every complete piece of the job ends at the same time;
- preemption: the fractions of the job that its pieces complete sum to , or one of its pieces is on machines on which it needs time ;
- preemption without migration: preemption, and all pieces of the job occupy the same set of machines.
No value is a special case of another: the same instance may have different optimal costs with and without preemption, and with and without migration.
Theorem. The field is sound, and in every schedule every job starts no later than it completes.
Concept map
Evidence
Lean source view on GitHub
| 1 | import Lax434175.Restarts |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: Interruption as a field of parallel-machine scheduling |
| 6 | type: theorem |
| 7 | --- |
| 8 | Non-preemptive scheduling, preemptive scheduling and scheduling with |
| 9 | restarts on parallel machines share one machine model, in which a schedule |
| 10 | is a finite list of pieces as in preemptive scheduling. A schedule is |
| 11 | feasible for this model if every piece occupies some machine and two |
| 12 | different pieces that share a machine or a job are disjoint in time. A job |
| 13 | starts when its first piece starts and completes when its last piece ends. |
| 14 | |
| 15 | How a job may be interrupted is a field with four values: |
| 16 | |
| 17 | - none: every job has exactly one piece, it starts at an integral time, and |
| 18 | its length is the full time the job needs on its machines; |
| 19 | - restarts: some piece of the job is complete, that is, its length is the |
| 20 | full time the job needs on its machines, no piece of the job ends later, |
| 21 | and every complete piece of the job ends at the same time; |
| 22 | - preemption: the fractions of the job that its pieces complete sum to , |
| 23 | or one of its pieces is on machines on which it needs time ; |
| 24 | - preemption without migration: preemption, and all pieces of the job occupy |
| 25 | the same set of machines. |
| 26 | |
| 27 | No value is a special case of another: the same instance may have different |
| 28 | optimal costs with and without preemption, and with and without migration. |
| 29 | |
| 30 | **Theorem.** The field is sound, and in every schedule every job starts no |
| 31 | later than it completes. |
| 32 | -/ |
| 33 | |
| 34 | namespace Lax434175.Interruption |
| 35 | open Lax434175.Kernels Lax434175.Modules Lax434175.ParallelMachines Lax434175.Preemptive |
| 36 | |
| 37 | inductive Mode |
| 38 | | none |
| 39 | | restarts |
| 40 | | pmtn |
| 41 | /-- Preemption without migration: all pieces of a job, or of an operation, |
| 42 | occupy the same set of machines. -/ |
| 43 | | pmtnNoMigration |
| 44 | deriving DecidableEq |
| 45 | |
| 46 | /-- The schedules that respect a way of interruption. -/ |
| 47 | def Mode.holds : Mode → (x : Inst) → Sched x → Prop |
| 48 | | .none, x, σ => ∀ j, ∃ q, piecesOf σ j = [q] ∧ |
| 49 | q.length = (duration x j q.machines : NNRat) ∧ ∃ n : ℕ, q.start = (n : NNRat) |
| 50 | | .restarts, _, σ => ∀ j, ∃ q ∈ piecesOf σ j, Restarts.Complete q ∧ |
| 51 | ∀ q' ∈ piecesOf σ j, q'.finish ≤ q.finish ∧ (Restarts.Complete q' → q'.finish = q.finish) |
| 52 | | .pmtn, x, σ => ∀ j, fraction x σ j = 1 ∨ ∃ q ∈ piecesOf σ j, duration x j q.machines = 0 |
| 53 | | .pmtnNoMigration, x, σ => ∀ j, |
| 54 | (fraction x σ j = 1 ∨ ∃ q ∈ piecesOf σ j, duration x j q.machines = 0) ∧ |
| 55 | ∀ q ∈ piecesOf σ j, ∀ q' ∈ piecesOf σ j, q.machines = q'.machines |
| 56 | |
| 57 | /-- Every piece occupies some machine, and two different pieces that share a |
| 58 | machine or a job do not overlap. -/ |
| 59 | def 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 | |
| 63 | /-- The kernel of scheduling on parallel machines with pieces. -/ |
| 64 | def kernel : Kernel where |
| 65 | Inst := Inst |
| 66 | jobs := Inst.jobs |
| 67 | release := Inst.r |
| 68 | Sched := Sched |
| 69 | feasible _ σ := feasible σ |
| 70 | start := start |
| 71 | completion := completion |
| 72 | |
| 73 | /-- Scheduling with pieces as a machine model. -/ |
| 74 | def model : Model where |
| 75 | kernel := kernel |
| 76 | inst x := x |
| 77 | jobs_eq _ := rfl |
| 78 | uses _ σ j S := ∃ q ∈ piecesOf σ j, q.machines = S |
| 79 | |
| 80 | /-- The interruption field. -/ |
| 81 | def module : Module kernel where |
| 82 | Value := Mode |
| 83 | Data _ _ := Unit |
| 84 | admits _ _ _ := True |
| 85 | constraint v x _ σ := v.holds x σ |
| 86 | le v w := decide (v = w) |
| 87 | embed _ _ _ := () |
| 88 | |
| 89 | axiom sound : module.Sound |
| 90 | |
| 91 | axiom startsBeforeCompletion : kernel.StartsBeforeCompletion |
| 92 | |
| 93 | end Lax434175.Interruption |
| 94 |
Builds on
From Mathlib
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments