1module Compiler.Planning.Resources
2
3import Execution.ResourceGraph
4import Compiler.Planning.Liveness
5import Model.Config
6import Model.Parameter
7import Model.Word32
8import Model.Word64
9import Std.Physical
10import Std.Foundation
11import Std.List
12import Std.Natural
13
14-- This explicit collection planner is for bounded deployment descriptions.
15-- It admits no transfer merely from vendor, host or failure-domain affinity.
16-- Its duplicate and interval checks are quadratic in description entries;
17-- callers bound entry count and its square (a work estimate, not CPU time).
18-- The square is checked by division without overflowing a runtime word. This is not
19-- the eventual sharded fleet search/index implementation.
20family ResourceUsage : Type 0
21constructor ResourceUsageWithin
22field unrestricted resourceUsageAmount : Nat
23constructor ResourceUsageOverflow
24
25end-family
26
27def resourceWordLimit =
28 18446744073709551615
29
30def resourceCount =
31 (lambda erased element : Type 0 .
32 (lambda unrestricted predicate : (pi unrestricted value : element . Nat) .
33 (stdListFold
34 element
35 Nat
36 (lambda unrestricted value : element .
37 (lambda unrestricted total : Nat . (naturalAdd (naturalNonzero (predicate value)) total)))
38 0)))
39
40def resourceAll =
41 (lambda erased element : Type 0 .
42 (lambda unrestricted predicate : (pi unrestricted value : element . Nat) .
43 (stdListFold
44 element
45 Nat
46 (lambda unrestricted value : element .
47 (lambda unrestricted valid : Nat . (naturalAnd (predicate value) valid)))
48 1)))
49
50def resourceDistinct =
51 (lambda erased element : Type 0 .
52 (lambda unrestricted same : (pi unrestricted left : element . (pi unrestricted right : element . Nat)) .
53 (lambda unrestricted values : (family StdList element) .
54 (eliminate
55 StdList
56 (lambda unrestricted current : (family StdList element) . Nat)
57 values
58 (branch StdListEmpty . 1)
59 (branch
60 StdListCons
61 head
62 tail
63 induction
64 .
65 (naturalAnd (naturalIsZero (resourceCount element (same head) tail)) induction))))))
66
67def resourceRequire =
68 (lambda erased value : Type 0 .
69 (lambda unrestricted condition : Nat .
70 (lambda unrestricted reason : (family ResourceFailure) .
71 (lambda unrestricted next : (family StdResult (family ResourceFailure) value) .
72 (nat-eliminate
73 (lambda unrestricted flag : Nat . (family StdResult (family ResourceFailure) value))
74 (constructor StdResult StdFailure (family ResourceFailure) value reason)
75 (lambda unrestricted prior : Nat .
76 (lambda unrestricted ignored : (family StdResult (family ResourceFailure) value) .
77 next))
78 condition)))))
79
80def resourceUnitCode =
81 (lambda unrestricted unit : (family ResourceUnit) .
82 (eliminate
83 ResourceUnit
84 (lambda unrestricted current : (family ResourceUnit) . Nat)
85 unit
86 (branch ResourceMemoryBytes . 0)
87 (branch ResourceBandwidthBytesPerSecond . 1)))
88
89def resourceFactValid =
90 (lambda unrestricted fact : (family ResourceFact) .
91 (eliminate
92 ResourceFact
93 (lambda unrestricted current : (family ResourceFact) . Nat)
94 fact
95 (branch ResourceAbsent reason . (naturalNonzero (bytes-length reason)))
96 (branch
97 ResourceEstablished
98 limit
99 reference
100 .
101 (naturalAnd
102 (naturalLessOrEqual limit resourceWordLimit)
103 (naturalNonzero (bytes-length reference))))))
104
105def resourceFactKnown =
106 (lambda unrestricted fact : (family ResourceFact) .
107 (eliminate
108 ResourceFact
109 (lambda unrestricted current : (family ResourceFact) . Nat)
110 fact
111 (branch ResourceAbsent reason . 0)
112 (branch ResourceEstablished limit reference . 1)))
113
114def resourceFactAllows =
115 (lambda unrestricted fact : (family ResourceFact) .
116 (lambda unrestricted amount : Nat .
117 (eliminate
118 ResourceFact
119 (lambda unrestricted current : (family ResourceFact) . Nat)
120 fact
121 (branch ResourceAbsent reason . 0)
122 (branch ResourceEstablished limit reference . (naturalLessOrEqual amount limit)))))
123
124def resourceDomainValid =
125 (lambda unrestricted domain : (family ResourceDomain) .
126 (eliminate
127 ResourceDomain
128 (lambda unrestricted current : (family ResourceDomain) . Nat)
129 domain
130 (branch
131 ResourceCapacityDomain
132 id
133 name
134 unit
135 fact
136 .
137 (naturalAnd
138 (naturalLessOrEqual id resourceWordLimit)
139 (naturalAnd (naturalNonzero (bytes-length name)) (resourceFactValid fact))))
140 (branch
141 ResourceRelationDomain
142 id
143 name
144 .
145 (naturalAnd (naturalLessOrEqual id resourceWordLimit) (naturalNonzero (bytes-length name))))))
146
147def resourceDomainUnitMatches =
148 (lambda unrestricted domain : (family ResourceDomain) .
149 (lambda unrestricted expected : (family ResourceUnit) .
150 (eliminate
151 ResourceDomain
152 (lambda unrestricted current : (family ResourceDomain) . Nat)
153 domain
154 (branch
155 ResourceCapacityDomain
156 id
157 name
158 unit
159 fact
160 .
161 (naturalEqual (resourceUnitCode unit) (resourceUnitCode expected)))
162 (branch ResourceRelationDomain id name . 0))))
163
164def resourceDomainKnown =
165 (lambda unrestricted domain : (family ResourceDomain) .
166 (eliminate
167 ResourceDomain
168 (lambda unrestricted current : (family ResourceDomain) . Nat)
169 domain
170 (branch ResourceCapacityDomain id name unit fact . (resourceFactKnown fact))
171 (branch ResourceRelationDomain id name . 0)))
172
173def resourceDomainAllows =
174 (lambda unrestricted domain : (family ResourceDomain) .
175 (lambda unrestricted amount : Nat .
176 (eliminate
177 ResourceDomain
178 (lambda unrestricted current : (family ResourceDomain) . Nat)
179 domain
180 (branch ResourceCapacityDomain id name unit fact . (resourceFactAllows fact amount))
181 (branch ResourceRelationDomain id name . 0))))
182
183def resourceHasEndpoint =
184 (lambda unrestricted graph : (family ResourceGraph) .
185 (lambda unrestricted id : Nat .
186 (naturalNonzero
187 (resourceCount
188 (family ResourceEndpoint)
189 (lambda unrestricted e : (family ResourceEndpoint) .
190 (naturalEqual id (resourceEndpointId e)))
191 (resourceGraphEndpoints graph)))))
192
193def resourceHasDomain =
194 (lambda unrestricted graph : (family ResourceGraph) .
195 (lambda unrestricted id : Nat .
196 (naturalNonzero
197 (resourceCount
198 (family ResourceDomain)
199 (lambda unrestricted d : (family ResourceDomain) . (naturalEqual id (resourceDomainId d)))
200 (resourceGraphDomains graph)))))
201
202def resourceEndpointValid =
203 (lambda unrestricted graph : (family ResourceGraph) .
204 (lambda unrestricted endpoint : (family ResourceEndpoint) .
205 (naturalAnd
206 (naturalLessOrEqual (resourceEndpointId endpoint) resourceWordLimit)
207 (naturalAnd
208 (naturalNonzero (bytes-length (resourceEndpointIdentity endpoint)))
209 (naturalAnd
210 (naturalNonzero (bytes-length (resourceEndpointRealization endpoint)))
211 (naturalAnd
212 (resourceAll
213 Bytes
214 (lambda unrestricted cap : Bytes . (naturalNonzero (bytes-length cap)))
215 (resourceEndpointCapabilities endpoint))
216 (naturalAnd
217 (resourceDistinct
218 Bytes
219 (lambda unrestricted a : Bytes .
220 (lambda unrestricted b : Bytes . (bytes-equal a b)))
221 (resourceEndpointCapabilities endpoint))
222 (naturalAnd
223 (resourceAll
224 Nat
225 (lambda unrestricted id : Nat . (resourceHasDomain graph id))
226 (resourceEndpointDomains endpoint))
227 (naturalAnd
228 (resourceDistinct
229 Nat
230 (lambda unrestricted a : Nat .
231 (lambda unrestricted b : Nat . (naturalEqual a b)))
232 (resourceEndpointDomains endpoint))
233 1)))))))))
234
235def resourceLinkValid =
236 (lambda unrestricted graph : (family ResourceGraph) .
237 (lambda unrestricted link : (family ResourceLink) .
238 (naturalAnd
239 (naturalLessOrEqual (resourceLinkId link) resourceWordLimit)
240 (naturalAnd
241 (naturalNonzero (bytes-length (resourceLinkRealization link)))
242 (naturalAnd
243 (resourceHasEndpoint graph (resourceLinkSource link))
244 (naturalAnd
245 (resourceHasEndpoint graph (resourceLinkDestination link))
246 (naturalAnd
247 (naturalIsZero
248 (naturalEqual (resourceLinkSource link) (resourceLinkDestination link)))
249 (naturalAnd (resourceFactValid (resourceLinkEnvelope link)) 1))))))))
250
251def resourceGraphValid =
252 (lambda unrestricted graph : (family ResourceGraph) .
253 (naturalAnd
254 (naturalNonzero (stdListLength (family ResourceEndpoint) (resourceGraphEndpoints graph)))
255 (naturalAnd
256 (resourceDistinct
257 (family ResourceEndpoint)
258 (lambda unrestricted a : (family ResourceEndpoint) .
259 (lambda unrestricted b : (family ResourceEndpoint) .
260 (naturalOr
261 (naturalEqual (resourceEndpointId a) (resourceEndpointId b))
262 (bytes-equal (resourceEndpointIdentity a) (resourceEndpointIdentity b)))))
263 (resourceGraphEndpoints graph))
264 (naturalAnd
265 (resourceDistinct
266 (family ResourceDomain)
267 (lambda unrestricted a : (family ResourceDomain) .
268 (lambda unrestricted b : (family ResourceDomain) .
269 (naturalOr
270 (naturalEqual (resourceDomainId a) (resourceDomainId b))
271 (bytes-equal (resourceDomainName a) (resourceDomainName b)))))
272 (resourceGraphDomains graph))
273 (naturalAnd
274 (resourceDistinct
275 (family ResourceLink)
276 (lambda unrestricted a : (family ResourceLink) .
277 (lambda unrestricted b : (family ResourceLink) .
278 (naturalEqual (resourceLinkId a) (resourceLinkId b))))
279 (resourceGraphLinks graph))
280 (naturalAnd
281 (resourceAll (family ResourceDomain) resourceDomainValid (resourceGraphDomains graph))
282 (naturalAnd
283 (resourceAll
284 (family ResourceEndpoint)
285 (resourceEndpointValid graph)
286 (resourceGraphEndpoints graph))
287 (naturalAnd
288 (resourceAll
289 (family ResourceLink)
290 (resourceLinkValid graph)
291 (resourceGraphLinks graph))
292 1))))))))
293
294def resourcePlacementValid =
295 (lambda unrestricted graph : (family ResourceGraph) .
296 (lambda unrestricted placement : (family ResourcePlacement) .
297 (naturalAnd
298 (naturalLessOrEqual (resourcePlacementRole placement) resourceWordLimit)
299 (naturalAnd
300 (naturalNonzero
301 (resourceCount
302 (family ResourceEndpoint)
303 (lambda unrestricted endpoint : (family ResourceEndpoint) .
304 (naturalAnd
305 (naturalEqual (resourceEndpointId endpoint) (resourcePlacementEndpoint placement))
306 (naturalAnd
307 (naturalNonzero
308 (resourceCount
309 Bytes
310 (lambda unrestricted cap : Bytes .
311 (bytes-equal cap (resourcePlacementCapability placement)))
312 (resourceEndpointCapabilities endpoint)))
313 1)))
314 (resourceGraphEndpoints graph)))
315 1))))
316
317def resourceLeaseValid =
318 (lambda unrestricted graph : (family ResourceGraph) .
319 (lambda unrestricted lease : (family ResourceLease) .
320 (naturalAnd
321 (naturalNonzero (bytes-length (resourceLeaseIdentity lease)))
322 (naturalAnd
323 (naturalNonzero (resourceLeaseAmount lease))
324 (naturalAnd
325 (naturalLessOrEqual (resourceLeaseAmount lease) resourceWordLimit)
326 (naturalAnd
327 (naturalLess (resourceLeaseBegin lease) (resourceLeaseUntil lease))
328 (naturalAnd
329 (naturalLessOrEqual (resourceLeaseUntil lease) resourceWordLimit)
330 (naturalAnd
331 (naturalNonzero
332 (resourceCount
333 (family ResourceEndpoint)
334 (lambda unrestricted endpoint : (family ResourceEndpoint) .
335 (naturalAnd
336 (naturalEqual (resourceEndpointId endpoint) (resourceLeaseEndpoint lease))
337 (naturalAnd
338 (naturalNonzero
339 (resourceCount
340 Nat
341 (lambda unrestricted id : Nat .
342 (naturalEqual id (resourceLeaseDomain lease)))
343 (resourceEndpointDomains endpoint)))
344 1)))
345 (resourceGraphEndpoints graph)))
346 (naturalAnd
347 (naturalNonzero
348 (resourceCount
349 (family ResourceDomain)
350 (lambda unrestricted domain : (family ResourceDomain) .
351 (naturalAnd
352 (naturalEqual (resourceDomainId domain) (resourceLeaseDomain lease))
353 (naturalAnd
354 (resourceDomainUnitMatches domain (resourceLeaseUnit lease))
355 1)))
356 (resourceGraphDomains graph)))
357 1)))))))))
358
359def resourceUsageAdd =
360 (lambda unrestricted total : (family ResourceUsage) .
361 (lambda unrestricted amount : Nat .
362 (eliminate
363 ResourceUsage
364 (lambda unrestricted current : (family ResourceUsage) . (family ResourceUsage))
365 total
366 (branch
367 ResourceUsageWithin
368 value
369 .
370 (eliminate
371 StdBool
372 (lambda unrestricted flag : (family StdBool) . (family ResourceUsage))
373 (stdBoolFromNatural
374 (naturalLessOrEqual amount (naturalSaturatingSubtract resourceWordLimit value)))
375 (branch
376 StdTrue
377 .
378 (constructor ResourceUsage ResourceUsageWithin (naturalAdd value amount)))
379 (branch StdFalse . (constructor ResourceUsage ResourceUsageOverflow))))
380 (branch ResourceUsageOverflow . (constructor ResourceUsage ResourceUsageOverflow)))))
381
382-- A peak occurs at a lease start: amounts are nonnegative and only those
383-- events add reservations. Ends are exclusive; device completion alone cannot
384-- end a lease still extended by a transport read.
385def resourceUsageAt =
386 (lambda unrestricted leases : (family StdList (family ResourceLease)) .
387 (lambda unrestricted domain : Nat .
388 (lambda unrestricted event : Nat .
389 (stdListFold
390 (family ResourceLease)
391 (family ResourceUsage)
392 (lambda unrestricted lease : (family ResourceLease) .
393 (lambda unrestricted total : (family ResourceUsage) .
394 (resourceUsageAdd
395 total
396 (naturalSelect
397 (naturalAnd
398 (naturalEqual domain (resourceLeaseDomain lease))
399 (naturalAnd
400 (naturalLessOrEqual (resourceLeaseBegin lease) event)
401 (naturalLess event (resourceLeaseUntil lease))))
402 (resourceLeaseAmount lease)
403 0))))
404 (constructor ResourceUsage ResourceUsageWithin 0)
405 leases))))
406
407def resourceLeaseKnown =
408 (lambda unrestricted graph : (family ResourceGraph) .
409 (lambda unrestricted lease : (family ResourceLease) .
410 (naturalNonzero
411 (resourceCount
412 (family ResourceDomain)
413 (lambda unrestricted domain : (family ResourceDomain) .
414 (naturalAnd
415 (naturalEqual (resourceDomainId domain) (resourceLeaseDomain lease))
416 (naturalAnd (resourceDomainKnown domain) 1)))
417 (resourceGraphDomains graph)))))
418
419def resourceLeaseFits =
420 (lambda unrestricted graph : (family ResourceGraph) .
421 (lambda unrestricted leases : (family StdList (family ResourceLease)) .
422 (lambda unrestricted lease : (family ResourceLease) .
423 (eliminate
424 ResourceUsage
425 (lambda unrestricted current : (family ResourceUsage) . Nat)
426 (resourceUsageAt leases (resourceLeaseDomain lease) (resourceLeaseBegin lease))
427 (branch
428 ResourceUsageWithin
429 total
430 .
431 (naturalNonzero
432 (resourceCount
433 (family ResourceDomain)
434 (lambda unrestricted domain : (family ResourceDomain) .
435 (naturalAnd
436 (naturalEqual (resourceDomainId domain) (resourceLeaseDomain lease))
437 (resourceDomainAllows domain total)))
438 (resourceGraphDomains graph))))
439 (branch ResourceUsageOverflow . 0)))))
440
441def resourceGraphEntries =
442 (lambda unrestricted graph : (family ResourceGraph) .
443 (naturalAdd
444 (stdListLength (family ResourceDomain) (resourceGraphDomains graph))
445 (naturalAdd
446 (stdListLength (family ResourceLink) (resourceGraphLinks graph))
447 (stdListFold
448 (family ResourceEndpoint)
449 Nat
450 (lambda unrestricted endpoint : (family ResourceEndpoint) .
451 (lambda unrestricted total : Nat .
452 (naturalAdd
453 total
454 (naturalAdd
455 1
456 (naturalAdd
457 (stdListLength Bytes (resourceEndpointCapabilities endpoint))
458 (stdListLength Nat (resourceEndpointDomains endpoint)))))))
459 0
460 (resourceGraphEndpoints graph)))))
461
462def resourceScheduleEntries =
463 (lambda unrestricted schedule : (family ResourceSchedule) .
464 (naturalAdd
465 (resourceGraphEntries (resourceScheduleGraph schedule))
466 (naturalAdd
467 (stdListLength (family ResourcePlacement) (resourceSchedulePlacements schedule))
468 (stdListLength (family ResourceLease) (resourceScheduleLeases schedule)))))
469
470def admitResourceSchedule =
471 (lambda unrestricted entryBudget : Nat .
472 (lambda unrestricted pairBudget : Nat .
473 (lambda unrestricted schedule : (family ResourceSchedule) .
474 (let unrestricted graph =
475 (resourceScheduleGraph schedule)
476 in
477 (let unrestricted placements =
478 (resourceSchedulePlacements schedule)
479 in
480 (let unrestricted leases =
481 (resourceScheduleLeases schedule)
482 in
483 (let unrestricted entries =
484 (resourceScheduleEntries schedule)
485 in
486 (resourceRequire
487 (family ResourceSchedule)
488 (naturalAnd
489 (naturalLessOrEqual entries entryBudget)
490 (naturalLessOrEqual
491 entries
492 (naturalDivideUnchecked
493 pairBudget
494 (naturalSelect (naturalNonzero entries) entries 1))))
495 (constructor ResourceFailure ResourceBudgetExceeded)
496 (resourceRequire
497 (family ResourceSchedule)
498 (resourceGraphValid graph)
499 (constructor ResourceFailure ResourceMalformedGraph)
500 (resourceRequire
501 (family ResourceSchedule)
502 (naturalAnd
503 (resourceDistinct
504 (family ResourcePlacement)
505 (lambda unrestricted a : (family ResourcePlacement) .
506 (lambda unrestricted b : (family ResourcePlacement) .
507 (naturalEqual (resourcePlacementRole a) (resourcePlacementRole b))))
508 placements)
509 (naturalAnd
510 (resourceAll
511 (family ResourcePlacement)
512 (resourcePlacementValid graph)
513 placements)
514 1))
515 (constructor ResourceFailure ResourceInvalidPlacement)
516 (resourceRequire
517 (family ResourceSchedule)
518 (naturalAnd
519 (resourceDistinct
520 (family ResourceLease)
521 (lambda unrestricted a : (family ResourceLease) .
522 (lambda unrestricted b : (family ResourceLease) .
523 (bytes-equal (resourceLeaseIdentity a) (resourceLeaseIdentity b))))
524 leases)
525 (naturalAnd
526 (resourceAll (family ResourceLease) (resourceLeaseValid graph) leases)
527 1))
528 (constructor ResourceFailure ResourceInvalidLease)
529 (resourceRequire
530 (family ResourceSchedule)
531 (resourceAll (family ResourceLease) (resourceLeaseKnown graph) leases)
532 (constructor ResourceFailure ResourceCapacityUnavailable)
533 (resourceRequire
534 (family ResourceSchedule)
535 (resourceAll
536 (family ResourceLease)
537 (resourceLeaseFits graph leases)
538 leases)
539 (constructor ResourceFailure ResourceCapacityExceeded)
540 (constructor
541 StdResult
542 StdSuccess
543 (family ResourceFailure)
544 (family ResourceSchedule)
545 schedule))))))))))))))
546
547-- These lookups consume an admitted schedule. Resolve each logical role once;
548-- nesting full collection scans for every candidate would make routing cubic.
549def resourcePlacementForRole =
550 (lambda unrestricted role : Nat .
551 (stdListFold
552 (family ResourcePlacement)
553 (family StdOption Nat)
554 (lambda unrestricted placement : (family ResourcePlacement) .
555 (lambda unrestricted next : (family StdOption Nat) .
556 (eliminate
557 StdBool
558 (lambda unrestricted flag : (family StdBool) . (family StdOption Nat))
559 (stdBoolFromNatural (naturalEqual (resourcePlacementRole placement) role))
560 (branch
561 StdTrue
562 .
563 (constructor StdOption StdSome Nat (resourcePlacementEndpoint placement)))
564 (branch StdFalse . next))))
565 (constructor StdOption StdNone Nat)))
566
567def resourceRouteAllowed =
568 (lambda unrestricted schedule : (family ResourceSchedule) .
569 (lambda unrestricted sourceRole : Nat .
570 (lambda unrestricted destinationRole : Nat .
571 (lambda unrestricted linkId : Nat .
572 (lambda unrestricted realization : Bytes .
573 (lambda unrestricted bytes : Nat .
574 (eliminate
575 StdOption
576 (lambda unrestricted current : (family StdOption Nat) . Nat)
577 (resourcePlacementForRole sourceRole (resourceSchedulePlacements schedule))
578 (branch StdNone . 0)
579 (branch
580 StdSome
581 source
582 .
583 (eliminate
584 StdOption
585 (lambda unrestricted current : (family StdOption Nat) . Nat)
586 (resourcePlacementForRole destinationRole (resourceSchedulePlacements schedule))
587 (branch StdNone . 0)
588 (branch
589 StdSome
590 destination
591 .
592 (naturalNonzero
593 (resourceCount
594 (family ResourceLink)
595 (lambda unrestricted link : (family ResourceLink) .
596 (naturalAnd
597 (naturalEqual (resourceLinkId link) linkId)
598 (naturalAnd
599 (naturalEqual (resourceLinkSource link) source)
600 (naturalAnd
601 (naturalEqual (resourceLinkDestination link) destination)
602 (naturalAnd
603 (bytes-equal (resourceLinkRealization link) realization)
604 (resourceFactAllows (resourceLinkEnvelope link) bytes))))))
605 (resourceGraphLinks (resourceScheduleGraph schedule))))))))))))))
606
607-- Lifetimes use inclusive last-use events. Leases are half-open: retain bytes
608-- through lastUse, including any extension made by the transfer planner. The
609-- lifetime owner is U32, so adding one here fits the resource event word.
610def resourceLeaseFromLifetime =
611 (lambda unrestricted identity : Bytes .
612 (lambda unrestricted endpoint : Nat .
613 (lambda unrestricted domain : Nat .
614 (lambda unrestricted lifetime : (family Lifetime) .
615 (eliminate
616 Lifetime
617 (lambda unrestricted current : (family Lifetime) . (family ResourceLease))
618 lifetime
619 (branch
620 LifetimeValue
621 tensor
622 first
623 last
624 bytes
625 alignment
626 .
627 (constructor
628 ResourceLease
629 ResourceLeaseOf
630 identity
631 endpoint
632 domain
633 (constructor ResourceUnit ResourceMemoryBytes)
634 (modelWord64Natural (stdByteCountValue bytes))
635 (modelWord32ToNatural first)
636 (naturalAdd (modelWord32ToNatural last) 1))))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.