1module Compiler.Planning.VA
2
3import Model.Parameter
4import Model.Word64
5import Std.Natural
6import Std.Physical
7
8family VAAlignment : Type 0
9constructor VAAlignment64KiB
10constructor VAAlignment2MiB
11
12end-family
13
14family VAOptionalAlignment : Type 0
15constructor VANoAlignment
16constructor VASomeAlignment
17field unrestricted vaSelectedAlignment : (family VAAlignment)
18
19end-family
20
21family VAAllocator : Type 0
22constructor VAAllocatorValue
23field unrestricted vaNextAddress : DeviceAddress
24
25end-family
26
27family VAAllocation : Type 0
28constructor VAAllocationValue
29field unrestricted vaAllocationStart : DeviceAddress
30field unrestricted vaAllocationExtent : ByteCount
31field unrestricted vaAllocationAlignment : (family VAAlignment)
32field unrestricted vaAllocationNext : (family VAAllocator)
33
34end-family
35
36family VAErrorCode : Type 0
37constructor VARequestZero
38constructor VAAllocatorBelowBase
39constructor VAAlignmentOverflow
40constructor VAAllocatorOverflow
41constructor VAReceiptStartMismatch
42constructor VAReceiptExtentMismatch
43constructor VANativeReservationRejected
44constructor VAHostFallbackObserved
45
46end-family
47
48family VAResult : Type 0
49constructor VASucceeded
50field unrestricted vaResultAllocation : (family VAAllocation)
51constructor VAFailed
52field unrestricted vaResultError : (family VAErrorCode)
53
54end-family
55
56family VAAlignResult : Type 0
57constructor VAAligned
58-- Internal checked word alignment. Callers wrap the result according to
59-- whether the aligned word is an address or a byte extent.
60field unrestricted vaAlignedAddress : (family ModelWord64)
61constructor VAAlignFailed
62
63end-family
64
65family VAOptionalError : Type 0
66constructor VANoError
67constructor VASomeError
68field unrestricted vaTelemetryError : (family VAErrorCode)
69
70end-family
71
72family VATelemetry : Type 0
73constructor VATelemetryValue
74field unrestricted vaTelemetryEventIndex : Nat
75field unrestricted vaTelemetryInputNext : DeviceAddress
76field unrestricted vaTelemetryRequestedBytes : ByteCount
77field unrestricted vaTelemetryAlignment : (family VAOptionalAlignment)
78field unrestricted vaTelemetryStart : DeviceAddress
79field unrestricted vaTelemetryExtent : ByteCount
80field unrestricted vaTelemetryStartPadding : ByteCount
81field unrestricted vaTelemetryExtentPadding : ByteCount
82field unrestricted vaTelemetryOutputNext : DeviceAddress
83field unrestricted vaTelemetrySucceeded : Nat
84field unrestricted vaTelemetryError : (family VAOptionalError)
85field unrestricted vaTelemetryHostFallbacks : Nat
86
87end-family
88
89family VAObservedResult : Type 0
90constructor VAObservedResultValue
91field unrestricted vaObservedAllocationResult : (family VAResult)
92field unrestricted vaObservedTelemetry : (family VATelemetry)
93
94end-family
95
96-- Two-phase reservation prevents failed native reservations from committing an
97-- allocator cursor that could later be mistaken for owned VA.
98family VAPendingReservation : Type 0
99constructor VAPendingReservationValue
100field unrestricted vaPendingEventIndex : Nat
101field unrestricted vaPendingInputAllocator : (family VAAllocator)
102field unrestricted vaPendingAllocation : (family VAAllocation)
103
104end-family
105
106family VAPrepareResult : Type 0
107constructor VAPrepared
108field unrestricted vaPreparedReservation : (family VAPendingReservation)
109field unrestricted vaPreparedTelemetry : (family VATelemetry)
110constructor VAPrepareFailed
111field unrestricted vaPrepareError : (family VAErrorCode)
112field unrestricted vaPrepareFailureTelemetry : (family VATelemetry)
113
114end-family
115
116family VANativeReservationReceipt : Type 0
117constructor VANativeReservationReceiptValue
118field unrestricted vaReceiptEventIndex : Nat
119field unrestricted vaReceiptStart : DeviceAddress
120field unrestricted vaReceiptExtent : ByteCount
121field unrestricted vaReceiptSucceeded : Nat
122field unrestricted vaReceiptHostFallbacks : Nat
123
124end-family
125
126family VACommitResult : Type 0
127constructor VACommitted
128field unrestricted vaCommittedAllocator : (family VAAllocator)
129field unrestricted vaCommitTelemetry : (family VATelemetry)
130constructor VACommitFailed
131field unrestricted vaCommitError : (family VAErrorCode)
132field unrestricted vaUnchangedAllocator : (family VAAllocator)
133field unrestricted vaCommitFailureTelemetry : (family VATelemetry)
134
135end-family
136
137def vaErrorCodeBytes =
138 (lambda unrestricted code : (family VAErrorCode) .
139 (eliminate
140 VAErrorCode
141 (lambda unrestricted current : (family VAErrorCode) . Bytes)
142 code
143 (branch VARequestZero . b"ALPHA-GAIA-VA-001")
144 (branch VAAllocatorBelowBase . b"ALPHA-GAIA-VA-002")
145 (branch VAAlignmentOverflow . b"ALPHA-GAIA-VA-003")
146 (branch VAAllocatorOverflow . b"ALPHA-GAIA-VA-004")
147 (branch VAReceiptStartMismatch . b"ALPHA-GAIA-VA-005")
148 (branch VAReceiptExtentMismatch . b"ALPHA-GAIA-VA-006")
149 (branch VANativeReservationRejected . b"ALPHA-GAIA-VA-007")
150 (branch VAHostFallbackObserved . b"ALPHA-GAIA-VA-008")))
151
152def vaBase : DeviceAddress =
153 (stdDeviceAddress 0x0000_0008_0000_0000)
154
155-- the base as a natural, and a buffer's place after the one before it:
156-- `address` + `bytes`, rounded up to `alignment` (a plan places its buffers
157-- in the card's address space one after another from the base)
158def vaBaseNatural : Nat =
159 (modelWord64Natural (stdDeviceAddressValue vaBase))
160
161def vaPlaceAfter =
162 (lambda unrestricted address : Nat .
163 (lambda unrestricted bytes : Nat .
164 (lambda unrestricted alignment : Nat .
165 (naturalMultiply
166 (naturalDivideUnchecked (naturalAdd (naturalAdd address bytes) (naturalSaturatingSubtract alignment 1)) alignment)
167 alignment))))
168
169def va64KiB : ByteAlignment =
170 (stdByteAlignment 0x1_0000)
171
172def va2MiB : ByteAlignment =
173 (stdByteAlignment 0x20_0000)
174
175def vaNewAllocator =
176 (constructor VAAllocator VAAllocatorValue vaBase)
177
178def vaAlignmentBytes =
179 (lambda unrestricted alignment : (family VAAlignment) .
180 (eliminate
181 VAAlignment
182 (lambda unrestricted current : (family VAAlignment) . ByteAlignment)
183 alignment
184 (branch VAAlignment64KiB . va64KiB)
185 (branch VAAlignment2MiB . va2MiB)))
186
187def vaSelectAlignment =
188 (lambda unrestricted size : ByteCount .
189 (nat-eliminate
190 (lambda unrestricted current : Nat . (family VAAlignment))
191 (constructor VAAlignment VAAlignment2MiB)
192 (lambda unrestricted predecessor : Nat .
193 (lambda unrestricted induction : (family VAAlignment) .
194 (constructor VAAlignment VAAlignment64KiB)))
195 (modelWord64LessThan (stdByteCountValue size) (stdByteAlignmentValue va2MiB))))
196
197def vaAlignUp =
198 (lambda unrestricted value : (family ModelWord64) .
199 (lambda unrestricted alignment : (family VAAlignment) .
200 (app
201 (lambda unrestricted alignmentBytes : (family ModelWord64) .
202 (app
203 (lambda unrestricted alignmentMask : (family ModelWord64) .
204 (eliminate
205 ModelWord64CheckedResult
206 (lambda unrestricted result : (family ModelWord64CheckedResult) .
207 (family VAAlignResult))
208 (modelWord64AddChecked value alignmentMask)
209 (branch
210 ModelWord64CheckedSucceeded
211 candidate
212 .
213 (constructor
214 VAAlignResult
215 VAAligned
216 (modelWord64And candidate (modelWord64Complement alignmentMask))))
217 (branch ModelWord64CheckedFailed error . (constructor VAAlignResult VAAlignFailed))))
218 (modelWord64Subtract alignmentBytes modelWord64One)))
219 (stdByteAlignmentValue (vaAlignmentBytes alignment)))))
220
221def vaTake =
222 (lambda unrestricted size : ByteCount .
223 (lambda unrestricted allocator : (family VAAllocator) .
224 (eliminate
225 VAAllocator
226 (lambda unrestricted current : (family VAAllocator) . (family VAResult))
227 allocator
228 (branch
229 VAAllocatorValue
230 next
231 .
232 (nat-eliminate
233 (lambda unrestricted requestIsZero : Nat . (family VAResult))
234 (nat-eliminate
235 (lambda unrestricted belowBase : Nat . (family VAResult))
236 (app
237 (lambda unrestricted alignment : (family VAAlignment) .
238 (eliminate
239 VAAlignResult
240 (lambda unrestricted result : (family VAAlignResult) . (family VAResult))
241 (vaAlignUp (stdDeviceAddressValue next) alignment)
242 (branch
243 VAAligned
244 start
245 .
246 (eliminate
247 VAAlignResult
248 (lambda unrestricted result : (family VAAlignResult) . (family VAResult))
249 (vaAlignUp (stdByteCountValue size) alignment)
250 (branch
251 VAAligned
252 extent
253 .
254 (eliminate
255 ModelWord64CheckedResult
256 (lambda unrestricted result : (family ModelWord64CheckedResult) .
257 (family VAResult))
258 (modelWord64AddChecked start extent)
259 (branch
260 ModelWord64CheckedSucceeded
261 nextAddress
262 .
263 (constructor
264 VAResult
265 VASucceeded
266 (constructor
267 VAAllocation
268 VAAllocationValue
269 (stdDeviceAddress start)
270 (stdByteCount extent)
271 alignment
272 (constructor
273 VAAllocator
274 VAAllocatorValue
275 (stdDeviceAddress nextAddress)))))
276 (branch
277 ModelWord64CheckedFailed
278 error
279 .
280 (constructor
281 VAResult
282 VAFailed
283 (constructor VAErrorCode VAAllocatorOverflow)))))
284 (branch
285 VAAlignFailed
286 .
287 (constructor
288 VAResult
289 VAFailed
290 (constructor VAErrorCode VAAlignmentOverflow)))))
291 (branch
292 VAAlignFailed
293 .
294 (constructor VAResult VAFailed (constructor VAErrorCode VAAlignmentOverflow)))))
295 (vaSelectAlignment size))
296 (lambda unrestricted predecessor : Nat .
297 (lambda unrestricted induction : (family VAResult) .
298 (constructor VAResult VAFailed (constructor VAErrorCode VAAllocatorBelowBase))))
299 (modelWord64LessThan (stdDeviceAddressValue next) (stdDeviceAddressValue vaBase)))
300 (lambda unrestricted predecessor : Nat .
301 (lambda unrestricted induction : (family VAResult) .
302 (constructor VAResult VAFailed (constructor VAErrorCode VARequestZero))))
303 (modelWord64IsZero (stdByteCountValue size)))))))
304
305def vaUsed =
306 (lambda unrestricted allocator : (family VAAllocator) .
307 (eliminate
308 VAAllocator
309 (lambda unrestricted current : (family VAAllocator) . (family ModelWord64CheckedResult))
310 allocator
311 (branch
312 VAAllocatorValue
313 next
314 .
315 (modelWord64SubtractChecked (stdDeviceAddressValue next) (stdDeviceAddressValue vaBase)))))
316
317def vaTelemetryFailed =
318 (lambda unrestricted eventIndex : Nat .
319 (lambda unrestricted inputNext : DeviceAddress .
320 (lambda unrestricted requestedBytes : ByteCount .
321 (lambda unrestricted error : (family VAErrorCode) .
322 (constructor
323 VATelemetry
324 VATelemetryValue
325 eventIndex
326 inputNext
327 requestedBytes
328 (constructor VAOptionalAlignment VANoAlignment)
329 (stdDeviceAddress modelWord64Zero)
330 (stdByteCount modelWord64Zero)
331 (stdByteCount modelWord64Zero)
332 (stdByteCount modelWord64Zero)
333 inputNext
334 zero
335 (constructor VAOptionalError VASomeError error)
336 zero)))))
337
338def vaTelemetrySucceededFor =
339 (lambda unrestricted eventIndex : Nat .
340 (lambda unrestricted inputNext : DeviceAddress .
341 (lambda unrestricted requestedBytes : ByteCount .
342 (lambda unrestricted allocation : (family VAAllocation) .
343 (eliminate
344 VAAllocation
345 (lambda unrestricted current : (family VAAllocation) . (family VATelemetry))
346 allocation
347 (branch
348 VAAllocationValue
349 start
350 extent
351 alignment
352 nextAllocator
353 .
354 (eliminate
355 VAAllocator
356 (lambda unrestricted current : (family VAAllocator) . (family VATelemetry))
357 nextAllocator
358 (branch
359 VAAllocatorValue
360 outputNext
361 .
362 (constructor
363 VATelemetry
364 VATelemetryValue
365 eventIndex
366 inputNext
367 requestedBytes
368 (constructor VAOptionalAlignment VASomeAlignment alignment)
369 start
370 extent
371 (stdByteCount
372 (modelWord64Subtract
373 (stdDeviceAddressValue start)
374 (stdDeviceAddressValue inputNext)))
375 (stdByteCount
376 (modelWord64Subtract
377 (stdByteCountValue extent)
378 (stdByteCountValue requestedBytes)))
379 outputNext
380 (succ zero)
381 (constructor VAOptionalError VANoError)
382 zero)))))))))
383
384def vaTakeObserved =
385 (lambda unrestricted eventIndex : Nat .
386 (lambda unrestricted size : ByteCount .
387 (lambda unrestricted allocator : (family VAAllocator) .
388 (eliminate
389 VAAllocator
390 (lambda unrestricted current : (family VAAllocator) . (family VAObservedResult))
391 allocator
392 (branch
393 VAAllocatorValue
394 inputNext
395 .
396 (app
397 (lambda unrestricted result : (family VAResult) .
398 (eliminate
399 VAResult
400 (lambda unrestricted current : (family VAResult) . (family VAObservedResult))
401 result
402 (branch
403 VASucceeded
404 allocation
405 .
406 (constructor
407 VAObservedResult
408 VAObservedResultValue
409 result
410 (vaTelemetrySucceededFor eventIndex inputNext size allocation)))
411 (branch
412 VAFailed
413 error
414 .
415 (constructor
416 VAObservedResult
417 VAObservedResultValue
418 result
419 (vaTelemetryFailed eventIndex inputNext size error)))))
420 (vaTake size allocator)))))))
421
422def vaPrepareReservation =
423 (lambda unrestricted eventIndex : Nat .
424 (lambda unrestricted size : ByteCount .
425 (lambda unrestricted allocator : (family VAAllocator) .
426 (eliminate
427 VAAllocator
428 (lambda unrestricted current : (family VAAllocator) . (family VAPrepareResult))
429 allocator
430 (branch
431 VAAllocatorValue
432 inputNext
433 .
434 (eliminate
435 VAResult
436 (lambda unrestricted result : (family VAResult) . (family VAPrepareResult))
437 (vaTake size allocator)
438 (branch
439 VASucceeded
440 allocation
441 .
442 (constructor
443 VAPrepareResult
444 VAPrepared
445 (constructor
446 VAPendingReservation
447 VAPendingReservationValue
448 eventIndex
449 allocator
450 allocation)
451 (vaTelemetrySucceededFor eventIndex inputNext size allocation)))
452 (branch
453 VAFailed
454 error
455 .
456 (constructor
457 VAPrepareResult
458 VAPrepareFailed
459 error
460 (vaTelemetryFailed eventIndex inputNext size error)))))))))
461
462def vaCommitFailure =
463 (lambda unrestricted pending : (family VAPendingReservation) .
464 (lambda unrestricted code : (family VAErrorCode) .
465 (eliminate
466 VAPendingReservation
467 (lambda unrestricted current : (family VAPendingReservation) . (family VACommitResult))
468 pending
469 (branch
470 VAPendingReservationValue
471 eventIndex
472 original
473 allocation
474 .
475 (eliminate
476 VAAllocator
477 (lambda unrestricted current : (family VAAllocator) . (family VACommitResult))
478 original
479 (branch
480 VAAllocatorValue
481 inputNext
482 .
483 (eliminate
484 VAAllocation
485 (lambda unrestricted current : (family VAAllocation) . (family VACommitResult))
486 allocation
487 (branch
488 VAAllocationValue
489 start
490 extent
491 alignment
492 following
493 .
494 (constructor
495 VACommitResult
496 VACommitFailed
497 code
498 original
499 (vaTelemetryFailed eventIndex inputNext extent code))))))))))
500
501def vaCommitReservation =
502 (lambda unrestricted pending : (family VAPendingReservation) .
503 (lambda unrestricted receipt : (family VANativeReservationReceipt) .
504 (eliminate
505 VAPendingReservation
506 (lambda unrestricted current : (family VAPendingReservation) . (family VACommitResult))
507 pending
508 (branch
509 VAPendingReservationValue
510 eventIndex
511 original
512 allocation
513 .
514 (eliminate
515 VAAllocation
516 (lambda unrestricted current : (family VAAllocation) . (family VACommitResult))
517 allocation
518 (branch
519 VAAllocationValue
520 start
521 extent
522 alignment
523 following
524 .
525 (eliminate
526 VANativeReservationReceipt
527 (lambda unrestricted current : (family VANativeReservationReceipt) .
528 (family VACommitResult))
529 receipt
530 (branch
531 VANativeReservationReceiptValue
532 receiptEvent
533 receiptStart
534 receiptExtent
535 succeeded
536 fallbacks
537 .
538 (nat-eliminate
539 (lambda unrestricted noFallbacks : Nat . (family VACommitResult))
540 (vaCommitFailure pending (constructor VAErrorCode VAHostFallbackObserved))
541 (lambda unrestricted fallbackPredecessor : Nat .
542 (lambda unrestricted fallbackInduction : (family VACommitResult) .
543 (nat-eliminate
544 (lambda unrestricted nativeSucceeded : Nat . (family VACommitResult))
545 (vaCommitFailure
546 pending
547 (constructor VAErrorCode VANativeReservationRejected))
548 (lambda unrestricted successPredecessor : Nat .
549 (lambda unrestricted successInduction : (family VACommitResult) .
550 (nat-eliminate
551 (lambda unrestricted startMatches : Nat . (family VACommitResult))
552 (vaCommitFailure
553 pending
554 (constructor VAErrorCode VAReceiptStartMismatch))
555 (lambda unrestricted startPredecessor : Nat .
556 (lambda unrestricted startInduction : (family VACommitResult) .
557 (nat-eliminate
558 (lambda unrestricted extentMatches : Nat .
559 (family VACommitResult))
560 (vaCommitFailure
561 pending
562 (constructor VAErrorCode VAReceiptExtentMismatch))
563 (lambda unrestricted extentPredecessor : Nat .
564 (lambda unrestricted extentInduction : (family VACommitResult) .
565 (eliminate
566 VAAllocator
567 (lambda unrestricted current : (family VAAllocator) .
568 (family VACommitResult))
569 original
570 (branch
571 VAAllocatorValue
572 inputNext
573 .
574 (constructor
575 VACommitResult
576 VACommitted
577 following
578 (vaTelemetrySucceededFor
579 eventIndex
580 inputNext
581 extent
582 allocation))))))
583 (modelWord64Equal
584 (stdByteCountValue receiptExtent)
585 (stdByteCountValue extent)))))
586 (modelWord64Equal
587 (stdDeviceAddressValue receiptStart)
588 (stdDeviceAddressValue start)))))
589 succeeded)))
590 (naturalIsZero fallbacks))))))))))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.