Machine sets and multiprocessor tasks

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

proven

Loading review…

Natural Language Statement

Theorem

The machine-set field of a machine model on parallel machines determines which sets of machines a job may occupy. Its values are

none: a job occupies any single machine;
machine sets $M_j$ : a job occupies a single machine of a given set $M_j$ ;
fixed sets $\mathrm{fix}_j$ : a job occupies all machines of a given set $\mathrm{fix}_j$ simultaneously;
sizes in $\{1, m\}$ : a job occupies either one machine or all machines;
sizes $\mathrm{size}_j$ : a job occupies any $\mathrm{size}_j$ machines simultaneously;
general: for every job the admissible sets of machines are given explicitly.

The value none is a special case of machine sets (every $M_j$ is the set of all machines), of sizes in $\{1, m\}$ and of sizes (every size is $1$ ). Sizes in $\{1, m\}$ are a special case of sizes. Every value is a special case of the general one. Fixed sets are not comparable with the value none: a job that may use any machine is not a job bound to one set.

Theorem. Over every machine model, the machine-set field is sound.

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.

no assumptions

thm✓Lax434175.MachineSets

⊢Lax434175Proofs.MachineSets.sound

Lean source view on GitHub

Show types on hover

1	import Mathlib.Data.Finset.Card
2	import Lax434175.ParallelMachines
3
4	/-!
5	---
6	title: Machine sets and multiprocessor tasks
7	type: theorem
8	---
9	The machine-set field of a machine model on parallel machines determines
10	which sets of machines a job may occupy. Its values are
11
12	- none: a job occupies any single machine;
13	- machine sets $M_j$ : a job occupies a single machine of a given set $M_j$ ;
14	- fixed sets $\mathrm{fix}_j$ : a job occupies all machines of a given set
15	$\mathrm{fix}_j$ simultaneously;
16	- sizes in $\{1, m\}$ : a job occupies either one machine or all machines;
17	- sizes $\mathrm{size}_j$ : a job occupies any $\mathrm{size}_j$ machines
18	simultaneously;
19	- general: for every job the admissible sets of machines are given
20	explicitly.
21
22	The value none is a special case of machine sets (every $M_j$ is the set of
23	all machines), of sizes in $\{1, m\}$ and of sizes (every size is $1$ ).
24	Sizes in $\{1, m\}$ are a special case of sizes. Every value is a special
25	case of the general one. Fixed sets are not comparable with the value none:
26	a job that may use any machine is not a job bound to one set.
27
28	Theorem. Over every machine model, the machine-set field is sound.
29	-/
30
31	namespace Lax434175.MachineSets
32	open Lax434175.Kernels Lax434175.Modules Lax434175.ParallelMachines
33
34	inductive Value
35	\| none
36	\| sets
37	\| fix
38	\| sizeOneOrAll
39	\| size
40	\| general
41
42	/-- The data of a value. -/
43	def Data : Value → Inst → Type
44	\| .none, _ => Unit
45	\| .sets, x => Fin x.jobs → Fin x.machines → Prop
46	\| .fix, x => Fin x.jobs → Finset (Fin x.machines)
47	\| .sizeOneOrAll, x => Fin x.jobs → Bool
48	\| .size, x => Fin x.jobs → ℕ
49	\| .general, x => Fin x.jobs → Finset (Fin x.machines) → Prop
50
51	/-- Whether a job may occupy a set of machines. -/
52	def view {x : Inst} : (v : Value) → Data v x → Fin x.jobs → Finset (Fin x.machines) → Prop
53	\| .none, _ => fun _ S => S.card = 1
54	\| .sets, M => fun j S => S.card = 1 ∧ ∀ i ∈ S, M j i
55	\| .fix, F => fun j S => S = F j
56	\| .sizeOneOrAll, all => fun j S => S.card = if all j then x.machines else 1
57	\| .size, size => fun j S => S.card = size j
58	\| .general, allowed => allowed
59
60	def le : Value → Value → Bool
61	\| .none, .fix => false
62	\| .none, _ => true
63	\| .sets, .sets \| .sets, .general => true
64	\| .fix, .fix \| .fix, .general => true
65	\| .sizeOneOrAll, .sizeOneOrAll \| .sizeOneOrAll, .size \| .sizeOneOrAll, .general => true
66	\| .size, .size \| .size, .general => true
67	\| .general, .general => true
68	\| _, _ => false
69
70	def embed : {v w : Value} → le v w = true → (x : Inst) → Data v x → Data w x
71	\| .none, .none, _, _, _ => ()
72	\| .none, .sets, _, _, _ => fun _ _ => True
73	\| .none, .sizeOneOrAll, _, _, _ => fun _ => false
74	\| .none, .size, _, _, _ => fun _ => 1
75	\| .sets, .sets, _, _, d => d
76	\| .fix, .fix, _, _, d => d
77	\| .sizeOneOrAll, .sizeOneOrAll, _, _, d => d
78	\| .sizeOneOrAll, .size, _, x, d => fun j => if d j then x.machines else 1
79	\| .size, .size, _, _, d => d
80	\| v, .general, _, _, d => view v d
81	\| .none, .fix, h, _, _ \| .sets, .none, h, _, _ \| .sets, .fix, h, _, _
82	\| .sets, .sizeOneOrAll, h, _, _ \| .sets, .size, h, _, _ \| .fix, .none, h, _, _
83	\| .fix, .sets, h, _, _ \| .fix, .sizeOneOrAll, h, _, _ \| .fix, .size, h, _, _
84	\| .sizeOneOrAll, .none, h, _, _ \| .sizeOneOrAll, .sets, h, _, _
85	\| .sizeOneOrAll, .fix, h, _, _ \| .size, .none, h, _, _ \| .size, .sets, h, _, _
86	\| .size, .fix, h, _, _ \| .size, .sizeOneOrAll, h, _, _ \| .general, .none, h, _, _
87	\| .general, .sets, h, _, _ \| .general, .fix, h, _, _ \| .general, .sizeOneOrAll, h, _, _
88	\| .general, .size, h, _, _ => absurd h Bool.false_ne_true
89
90	/-- The machine-set field. -/
91	def module (M : Model) : Module M.kernel where
92	Value := Value
93	Data v x := Data v (M.inst x)
94	admits _ _ _ := True
95	constraint v x d σ := ∀ j S, M.uses x σ j S → view v d j S
96	le := le
97	embed h x d := embed h (M.inst x) d
98
99	axiom sound (M : Model) : (module M).Sound
100
101	end Lax434175.MachineSets
102