Coppelius.Build.PhysicalComponents

1module Coppelius.Build.PhysicalComponents
2
3import Coppelius.Build.DeviceImages
4import Coppelius.Build.Graph
5import Coppelius.ArenaPlan
6import Coppelius.Build.Placement
7import Data.Bytes
8import Hardware.Nvidia.SM86.Command.WholeProgramPlan
9import Model.Config
10import Model.Word64
11import Std.Physical
12
13-- The source closure retains device images and the typed launch description.
14-- The compiler realizes their wire representation only after target
15-- specialization and proof erasure; no file path or intermediate executable
16-- participates in this construction.
17family CoppeliusPhysicalComponents : Type 0
18constructor CoppeliusPhysicalComponentsReady
19field unrestricted coppeliusPhysicalProgram : BytesBuilder
20field unrestricted coppeliusPhysicalQMD : BytesBuilder
21field unrestricted coppeliusPhysicalPushbuffer : BytesBuilder
22field unrestricted coppeliusPhysicalGPFIFO : BytesBuilder
23constructor CoppeliusPhysicalComponentsFailed
24end-family
25
26-- The device placement of the plan's tables and of the host's other
27-- buffers outside the video arena: the plan encodes launches against these
28-- bases and the host (Coppelius.Build.NativeHost) allocates the buffers at
29-- them.
30
31-- over a submission schedule: the plan's own (coppeliusSubmissionSchedule)
32-- or the same one profiled (coppeliusProfiledSubmissionSchedule)
33def coppeliusWholeProgramPlanFor =
34  (lambda unrestricted submissions : (family NvidiaSubmissionSchedule) .
35  (lambda unrestricted component : (family NvidiaWholeProgramComponent) .
36    (lambda unrestricted architecture : (family ModelWord32) .
37      (lambda unrestricted computeClass : (family ModelWord32) .
38        (lambda unrestricted spaVersion : (family ModelWord32) .
39        (lambda unrestricted qmdTableBytes : Nat .
40          (constructor
41            NvidiaWholeProgramPlan
42            NvidiaWholeProgramPlanValue
43            component
44            architecture
45            computeClass
46            spaVersion
47            (modelWord64FromNaturalTruncated coppeliusProgramBase)
48            (modelWord64FromNaturalTruncated coppeliusQMDBase)
49            (modelWord64FromNaturalTruncated coppeliusPushbufferBase)
50            (modelWord64FromNaturalTruncated coppeliusSemaphoreBase)
51            256
52            coppeliusSM86CompatProgramBytesNatural
53            coppeliusWholeProgramDeviceRegions
54            coppeliusLaunchSchedule
55            coppeliusLaunchCount
56            qmdTableBytes
57            submissions
58            coppeliusSubmissionCount
59            coppeliusSubmissionReferenceCount)))))))
60
61def coppeliusWholeProgramPlan = (coppeliusWholeProgramPlanFor coppeliusSubmissionSchedule)
62
63def coppeliusWholeProgramComponentFor =
64  (lambda unrestricted submissions : (family NvidiaSubmissionSchedule) .
65  (lambda unrestricted component : (family NvidiaWholeProgramComponent) .
66    (lambda unrestricted architecture : (family ModelWord32) .
67      (lambda unrestricted computeClass : (family ModelWord32) .
68        (lambda unrestricted spaVersion : (family ModelWord32) .
69        (lambda unrestricted qmdTableBytes : Nat .
70          (bytes-builder-chunk
71            (compiler-native-encode
72              (family NvidiaWholeProgramPlan)
73              (coppeliusWholeProgramPlanFor submissions
74                component architecture computeClass spaVersion qmdTableBytes)))))))))
75
76def coppeliusWholeProgramComponent = (coppeliusWholeProgramComponentFor coppeliusSubmissionSchedule)
77
78def coppeliusPhysicalComponents =
79  (lambda unrestricted architecture : (family ModelWord32) .
80    (lambda unrestricted computeClass : (family ModelWord32) .
81      (lambda unrestricted spaVersion : (family ModelWord32) .
82      (lambda unrestricted qmdTableBytes : Nat .
83        (constructor
84          CoppeliusPhysicalComponents
85          CoppeliusPhysicalComponentsReady
86          (coppeliusWholeProgramComponent
87            (constructor NvidiaWholeProgramComponent NvidiaWholeProgramProgram)
88            architecture computeClass spaVersion qmdTableBytes)
89          (coppeliusWholeProgramComponent
90            (constructor NvidiaWholeProgramComponent NvidiaWholeProgramQMD)
91            architecture computeClass spaVersion qmdTableBytes)
92          (coppeliusWholeProgramComponent
93            (constructor NvidiaWholeProgramComponent NvidiaWholeProgramPushbuffer)
94            architecture computeClass spaVersion qmdTableBytes)
95          (coppeliusWholeProgramComponent
96            (constructor NvidiaWholeProgramComponent NvidiaWholeProgramGPFIFO)
97            architecture computeClass spaVersion qmdTableBytes))))))