Platform.Linux.Nvidia.Compatibility

1module Platform.Linux.Nvidia.Compatibility
2
3import Hardware.Nvidia.SM86.Command.WholeProgramPlan
4import Platform.Linux.Nvidia.PlanHost
5import Std.List
6import Std.Natural
7
8-- The compatibility contract (docs/PRD-ALPHA-REMAINING.md item 5, [12]):
9-- what an artifact assumes of the card and the driver, set against what a
10-- device profile states the card supplies, each supply with the kind of
11-- evidence behind it.
12--
13--   * a DEMAND is the plan's: an ABI it was built against (the driver
14--     branch whose ioctl layouts the host encodes), a feature it uses (the
15--     instruction set, unified memory, the compute class), or a resource it
16--     needs (registers per thread, threads and shared memory per block,
17--     video memory) -- with the amount, derived from the plan, and whether
18--     the supply must be exactly that (an ABI, an instruction set) or at
19--     least that (a resource);
20--   * a SUPPLY is the profile's, named as the demand is, with its amount
21--     and its evidence: an ARCHITECTURAL constraint (what the architecture
22--     defines, named by its source), a MEASUREMENT (what a qualified run on
23--     that card recorded, named by the record), or a VALIDATED MODEL (what
24--     a model the gates hold to the card says, named by the model).
25--
26-- Admission takes the demands in order; the first with no supply of its
27-- name, or a supply that does not meet it, refuses the pairing BY NAME
28-- (nvidiaCompatibilityRefusal is that name; empty = admitted).  A profile
29-- that drops a supply is refused at the demand that needed it
30-- (scripts/ci/compatibility-contract.sh).
31
32family NvidiaEvidence : Type 0
33constructor NvidiaEvidenceArchitectural
34field unrestricted nvidiaEvidenceArchitecturalSource : Bytes
35constructor NvidiaEvidenceMeasured
36field unrestricted nvidiaEvidenceMeasuredRecord : Bytes
37constructor NvidiaEvidenceModelled
38field unrestricted nvidiaEvidenceModel : Bytes
39end-family
40
41family NvidiaDemandKind : Type 0
42constructor NvidiaDemandABI
43constructor NvidiaDemandFeature
44constructor NvidiaDemandResource
45end-family
46
47-- a demand's comparison: the supply exactly the amount, or at least it
48family NvidiaDemandBound : Type 0
49constructor NvidiaDemandExactly
50constructor NvidiaDemandAtLeast
51end-family
52
53family NvidiaDemand : Type 0
54constructor NvidiaDemandValue
55field unrestricted nvidiaDemandName : Bytes
56field unrestricted nvidiaDemandKind : (family NvidiaDemandKind)
57field unrestricted nvidiaDemandBound : (family NvidiaDemandBound)
58field unrestricted nvidiaDemandAmount : Nat
59end-family
60
61family NvidiaSupply : Type 0
62constructor NvidiaSupplyValue
63field unrestricted nvidiaSupplyName : Bytes
64field unrestricted nvidiaSupplyAmount : Nat
65field unrestricted nvidiaSupplyEvidence : (family NvidiaEvidence)
66end-family
67
68def nvidiaDemand =
69  (lambda unrestricted name : Bytes .
70    (lambda unrestricted kind : (family NvidiaDemandKind) .
71      (lambda unrestricted bound : (family NvidiaDemandBound) .
72        (lambda unrestricted amount : Nat .
73          (lambda unrestricted rest : (family StdList (family NvidiaDemand)) .
74            (constructor StdList StdListCons (family NvidiaDemand) (constructor NvidiaDemand NvidiaDemandValue name kind bound amount) rest))))))
75
76def nvidiaSupply =
77  (lambda unrestricted name : Bytes .
78    (lambda unrestricted amount : Nat .
79      (lambda unrestricted evidence : (family NvidiaEvidence) .
80        (lambda unrestricted rest : (family StdList (family NvidiaSupply)) .
81          (constructor StdList StdListCons (family NvidiaSupply) (constructor NvidiaSupply NvidiaSupplyValue name amount evidence) rest)))))
82
83def nvidiaNoDemands : (family StdList (family NvidiaDemand)) = (constructor StdList StdListEmpty (family NvidiaDemand))
84def nvidiaNoSupplies : (family StdList (family NvidiaSupply)) = (constructor StdList StdListEmpty (family NvidiaSupply))
85
86-- whether a supply meets a demand of the same name (0 when the names differ)
87def nvidiaSupplyMeets =
88  (lambda unrestricted demand : (family NvidiaDemand) .
89    (lambda unrestricted supply : (family NvidiaSupply) .
90      (eliminate NvidiaDemand (lambda unrestricted current : (family NvidiaDemand) . Nat) demand
91        (branch NvidiaDemandValue name kind bound amount .
92          (eliminate NvidiaSupply (lambda unrestricted current : (family NvidiaSupply) . Nat) supply
93            (branch NvidiaSupplyValue supplied available evidence .
94              (naturalAnd (bytes-equal name supplied)
95                (eliminate NvidiaDemandBound (lambda unrestricted current : (family NvidiaDemandBound) . Nat) bound
96                  (branch NvidiaDemandExactly . (naturalEqual available amount))
97                  (branch NvidiaDemandAtLeast . (naturalLessOrEqual amount available))))))))))
98
99def nvidiaDemandMet =
100  (lambda unrestricted supplies : (family StdList (family NvidiaSupply)) .
101    (lambda unrestricted demand : (family NvidiaDemand) .
102      (stdListFold (family NvidiaSupply) Nat
103        (lambda unrestricted supply : (family NvidiaSupply) .
104          (lambda unrestricted rest : Nat . (naturalOr (nvidiaSupplyMeets demand supply) rest)))
105        0
106        supplies)))
107
108def nvidiaDemandName =
109  (lambda unrestricted demand : (family NvidiaDemand) .
110    (eliminate NvidiaDemand (lambda unrestricted current : (family NvidiaDemand) . Bytes) demand
111      (branch NvidiaDemandValue name kind bound amount . name)))
112
113-- the first demand the supplies do not meet, by name; empty when all are met
114def nvidiaCompatibilityRefusal =
115  (lambda unrestricted demands : (family StdList (family NvidiaDemand)) .
116    (lambda unrestricted supplies : (family StdList (family NvidiaSupply)) .
117      (stdListFold (family NvidiaDemand) Bytes
118        (lambda unrestricted demand : (family NvidiaDemand) .
119          (lambda unrestricted later : Bytes .
120            (nat-eliminate (lambda unrestricted met : Nat . Bytes)
121              (nvidiaDemandName demand)
122              (lambda unrestricted p : Nat . (lambda unrestricted ignored : Bytes . later))
123              (nvidiaDemandMet supplies demand))))
124        b""
125        demands)))
126
127-- 1 when admitted
128def nvidiaCompatibilityAdmitted =
129  (lambda unrestricted demands : (family StdList (family NvidiaDemand)) .
130    (lambda unrestricted supplies : (family StdList (family NvidiaSupply)) .
131      (naturalIsZero (bytes-length (nvidiaCompatibilityRefusal demands supplies)))))
132
133-- ---- what a request host demands ----
134-- the driver branch its ioctl layouts are for (the host also refuses
135-- another branch by name at run time: PlanHost.phRootAndDriverBranch), the
136-- compute class it allocates, and unified memory when its lifecycle is UVM
137def nvidiaHostDemands =
138  (lambda unrestricted layout : (family NvidiaPlanHostLayout) .
139    (lambda unrestricted rest : (family StdList (family NvidiaDemand)) .
140      (eliminate NvidiaPlanHostLayout (lambda unrestricted current : (family NvidiaPlanHostLayout) . (family StdList (family NvidiaDemand))) layout
141        (branch NvidiaPlanHostLayoutValue gpfifo push sem program qmd userd data abi lifecycle expectedName errorHost .
142          (eliminate NvidiaPlanHostABI (lambda unrestricted current : (family NvidiaPlanHostABI) . (family StdList (family NvidiaDemand))) abi
143            (branch NvidiaPlanHostABIValue mapIoctl nvos46Size dmaOffset status channelClass computeClass usermodeClass engineType driverBranch scheduleParams userdMemory channelFlags directDMAFlags .
144              (nvidiaDemand b"driver-branch" (constructor NvidiaDemandKind NvidiaDemandABI) (constructor NvidiaDemandBound NvidiaDemandExactly) driverBranch
145                (nvidiaDemand b"compute-class" (constructor NvidiaDemandKind NvidiaDemandFeature) (constructor NvidiaDemandBound NvidiaDemandExactly) computeClass
146                  (eliminate NvidiaPlanHostLifecycle (lambda unrestricted current : (family NvidiaPlanHostLifecycle) . (family StdList (family NvidiaDemand))) lifecycle
147                    (branch NvidiaPlanHostDirectRM . rest)
148                    (branch NvidiaPlanHostUVM base extent .
149                      (nvidiaDemand b"unified-memory" (constructor NvidiaDemandKind NvidiaDemandFeature) (constructor NvidiaDemandBound NvidiaDemandAtLeast) 1 rest)))))))))))
150
151-- ---- what a plan's kernels demand ----
152-- the most registers, threads and shared bytes any of its device regions
153-- declares, per thread and per block
154def nvidiaRegionsMaximum =
155  (lambda unrestricted field : (pi unrestricted region : (family NvidiaDeviceRegion) . Nat) .
156    (lambda unrestricted regions : (family NvidiaDeviceRegions) .
157      (eliminate NvidiaDeviceRegions (lambda unrestricted current : (family NvidiaDeviceRegions) . Nat) regions
158        (branch NvidiaDeviceRegionsEnd . 0)
159        (branch NvidiaDeviceRegionsNext head tail induction .
160          (naturalSelect (naturalLess induction (field head)) (field head) induction)))))
161
162def nvidiaRegionRegisters =
163  (lambda unrestricted region : (family NvidiaDeviceRegion) .
164    (eliminate NvidiaDeviceRegion (lambda unrestricted current : (family NvidiaDeviceRegion) . Nat) region
165      (branch NvidiaDeviceRegionValue identity material registers blockX shared . registers)
166      (branch NvidiaDeviceRegionSM121 identity material registers blockX shared barriers . registers)
167      (branch NvidiaDeviceProgramRegion identity program registers blockX shared realization . registers)))
168def nvidiaRegionThreads =
169  (lambda unrestricted region : (family NvidiaDeviceRegion) .
170    (eliminate NvidiaDeviceRegion (lambda unrestricted current : (family NvidiaDeviceRegion) . Nat) region
171      (branch NvidiaDeviceRegionValue identity material registers blockX shared . blockX)
172      (branch NvidiaDeviceRegionSM121 identity material registers blockX shared barriers . blockX)
173      (branch NvidiaDeviceProgramRegion identity program registers blockX shared realization . blockX)))
174def nvidiaRegionShared =
175  (lambda unrestricted region : (family NvidiaDeviceRegion) .
176    (eliminate NvidiaDeviceRegion (lambda unrestricted current : (family NvidiaDeviceRegion) . Nat) region
177      (branch NvidiaDeviceRegionValue identity material registers blockX shared . shared)
178      (branch NvidiaDeviceRegionSM121 identity material registers blockX shared barriers . shared)
179      (branch NvidiaDeviceProgramRegion identity program registers blockX shared realization . shared)))
180
181-- a plan's demands: its instruction set (10 x major + minor), its kernels'
182-- resources, the video memory its arena occupies, then the host's
183def nvidiaPlanDemands =
184  (lambda unrestricted instructionSet : Nat .
185    (lambda unrestricted regions : (family NvidiaDeviceRegions) .
186      (lambda unrestricted videoMemory : Nat .
187        (lambda unrestricted rest : (family StdList (family NvidiaDemand)) .
188          (nvidiaDemand b"instruction-set" (constructor NvidiaDemandKind NvidiaDemandFeature) (constructor NvidiaDemandBound NvidiaDemandExactly) instructionSet
189            (nvidiaDemand b"registers-per-thread" (constructor NvidiaDemandKind NvidiaDemandResource) (constructor NvidiaDemandBound NvidiaDemandAtLeast) (nvidiaRegionsMaximum nvidiaRegionRegisters regions)
190              (nvidiaDemand b"threads-per-block" (constructor NvidiaDemandKind NvidiaDemandResource) (constructor NvidiaDemandBound NvidiaDemandAtLeast) (nvidiaRegionsMaximum nvidiaRegionThreads regions)
191                (nvidiaDemand b"shared-bytes-per-block" (constructor NvidiaDemandKind NvidiaDemandResource) (constructor NvidiaDemandBound NvidiaDemandAtLeast) (nvidiaRegionsMaximum nvidiaRegionShared regions)
192                  (nvidiaDemand b"video-memory-bytes" (constructor NvidiaDemandKind NvidiaDemandResource) (constructor NvidiaDemandBound NvidiaDemandAtLeast) videoMemory
193                    rest)))))))))
194
195-- a little-endian word of text (a driver version's first four bytes)
196def nvidiaCompatibilityTextWord =
197  (lambda unrestricted text : Bytes .
198    (bytes-eliminate
199      (lambda unrestricted current : Bytes . Nat)
200      0
201      (lambda unrestricted head : Byte . (lambda unrestricted tail : Bytes . (lambda unrestricted induction : Nat .
202        (naturalAdd (byte-to-nat head) (naturalMultiply 256 induction)))))
203      text))
204
205-- the instruction set a QMD architecture word names (0x86: 8.6, as 86)
206def nvidiaInstructionSetOf =
207  (lambda unrestricted architecture : Nat .
208    (naturalAdd (naturalMultiply 10 (naturalDivideUnchecked architecture 16)) (naturalModuloUnchecked architecture 16)))
209
210-- a profile with one supply dropped (what the contract's refusals are
211-- stated against)
212def nvidiaSuppliesWithout =
213  (lambda unrestricted name : Bytes .
214    (lambda unrestricted supplies : (family StdList (family NvidiaSupply)) .
215      (stdListFold (family NvidiaSupply) (family StdList (family NvidiaSupply))
216        (lambda unrestricted supply : (family NvidiaSupply) .
217          (lambda unrestricted rest : (family StdList (family NvidiaSupply)) .
218            (eliminate NvidiaSupply (lambda unrestricted current : (family NvidiaSupply) . (family StdList (family NvidiaSupply))) supply
219              (branch NvidiaSupplyValue supplied amount evidence .
220                (nat-eliminate (lambda unrestricted same : Nat . (family StdList (family NvidiaSupply)))
221                  (constructor StdList StdListCons (family NvidiaSupply) supply rest)
222                  (lambda unrestricted p : Nat . (lambda unrestricted ignored : (family StdList (family NvidiaSupply)) . rest))
223                  (bytes-equal name supplied))))))
224        nvidiaNoSupplies
225        supplies)))