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-- every driver branch whose ioctl layouts it carries (the host selects
135-- among them, and refuses any other branch by name, at run time:
136-- PlanHost.phSelectDriverInterface) -- so a profile must hold evidence for
137-- each branch a host may run on, not just one of them -- the compute class
138-- it allocates, and unified memory when its lifecycle is UVM
139def nvidiaDriverDemands =
140  (lambda unrestricted drivers : (family NvidiaDriverInterfaces) .
141    (lambda unrestricted rest : (family StdList (family NvidiaDemand)) .
142      (let unrestricted demand =
143        (lambda unrestricted driver : (family NvidiaDriverInterface) .
144          (lambda unrestricted later : (family StdList (family NvidiaDemand)) .
145            (nvidiaDemand b"driver-branch" (constructor NvidiaDemandKind NvidiaDemandABI) (constructor NvidiaDemandBound NvidiaDemandExactly)
146              (nvidiaDriverInterfacePrefixWord driver) later))) in
147      (eliminate NvidiaDriverInterfaces (lambda unrestricted current : (family NvidiaDriverInterfaces) . (family StdList (family NvidiaDemand))) drivers
148        (branch NvidiaDriverInterfacesLast final . (demand final rest))
149        (branch NvidiaDriverInterfacesNext head tail induction . (demand head induction))))))
150
151def nvidiaHostDemands =
152  (lambda unrestricted layout : (family NvidiaPlanHostLayout) .
153    (lambda unrestricted rest : (family StdList (family NvidiaDemand)) .
154      (eliminate NvidiaPlanHostLayout (lambda unrestricted current : (family NvidiaPlanHostLayout) . (family StdList (family NvidiaDemand))) layout
155        (branch NvidiaPlanHostLayoutValue gpfifo push sem program qmd userd data abi lifecycle expectedName errorHost .
156          (eliminate NvidiaPlanHostABI (lambda unrestricted current : (family NvidiaPlanHostABI) . (family StdList (family NvidiaDemand))) abi
157            (branch NvidiaPlanHostABIValue drivers channelClass computeClass usermodeClass engineType userdMemory channelFlags directDMAFlags .
158              (nvidiaDriverDemands drivers
159                (nvidiaDemand b"compute-class" (constructor NvidiaDemandKind NvidiaDemandFeature) (constructor NvidiaDemandBound NvidiaDemandExactly) computeClass
160                  (eliminate NvidiaPlanHostLifecycle (lambda unrestricted current : (family NvidiaPlanHostLifecycle) . (family StdList (family NvidiaDemand))) lifecycle
161                    (branch NvidiaPlanHostDirectRM entries . rest)
162                    (branch NvidiaPlanHostUVM base extent .
163                      (nvidiaDemand b"unified-memory" (constructor NvidiaDemandKind NvidiaDemandFeature) (constructor NvidiaDemandBound NvidiaDemandAtLeast) 1 rest)))))))))))
164
165-- ---- what a plan's kernels demand ----
166-- the most registers, threads and shared bytes any of its device regions
167-- declares, per thread and per block
168def nvidiaRegionsMaximum =
169  (lambda unrestricted field : (pi unrestricted region : (family NvidiaDeviceRegion) . Nat) .
170    (lambda unrestricted regions : (family NvidiaDeviceRegions) .
171      (eliminate NvidiaDeviceRegions (lambda unrestricted current : (family NvidiaDeviceRegions) . Nat) regions
172        (branch NvidiaDeviceRegionsEnd . 0)
173        (branch NvidiaDeviceRegionsNext head tail induction .
174          (naturalSelect (naturalLess induction (field head)) (field head) induction)))))
175
176def nvidiaRegionRegisters =
177  (lambda unrestricted region : (family NvidiaDeviceRegion) .
178    (eliminate NvidiaDeviceRegion (lambda unrestricted current : (family NvidiaDeviceRegion) . Nat) region
179      (branch NvidiaDeviceRegionValue identity material registers blockX shared . registers)
180      (branch NvidiaDeviceRegionSM121 identity material registers blockX shared barriers . registers)
181      (branch NvidiaDeviceRegionSM90 identity material registers blockX shared barriers . registers)
182      (branch NvidiaDeviceProgramRegion identity program registers blockX shared realization . registers)
183      (branch NvidiaDeviceAllocatedProgramRegion identity program registers blockX shared realization . registers)))
184def nvidiaRegionThreads =
185  (lambda unrestricted region : (family NvidiaDeviceRegion) .
186    (eliminate NvidiaDeviceRegion (lambda unrestricted current : (family NvidiaDeviceRegion) . Nat) region
187      (branch NvidiaDeviceRegionValue identity material registers blockX shared . blockX)
188      (branch NvidiaDeviceRegionSM121 identity material registers blockX shared barriers . blockX)
189      (branch NvidiaDeviceRegionSM90 identity material registers blockX shared barriers . blockX)
190      (branch NvidiaDeviceProgramRegion identity program registers blockX shared realization . blockX)
191      (branch NvidiaDeviceAllocatedProgramRegion identity program registers blockX shared realization . blockX)))
192def nvidiaRegionShared =
193  (lambda unrestricted region : (family NvidiaDeviceRegion) .
194    (eliminate NvidiaDeviceRegion (lambda unrestricted current : (family NvidiaDeviceRegion) . Nat) region
195      (branch NvidiaDeviceRegionValue identity material registers blockX shared . shared)
196      (branch NvidiaDeviceRegionSM121 identity material registers blockX shared barriers . shared)
197      (branch NvidiaDeviceRegionSM90 identity material registers blockX shared barriers . shared)
198      (branch NvidiaDeviceProgramRegion identity program registers blockX shared realization . shared)
199      (branch NvidiaDeviceAllocatedProgramRegion identity program registers blockX shared realization . shared)))
200
201-- a plan's demands: its instruction set (10 x major + minor), its kernels'
202-- resources, the video memory its arena occupies, then the host's
203def nvidiaPlanDemands =
204  (lambda unrestricted instructionSet : Nat .
205    (lambda unrestricted regions : (family NvidiaDeviceRegions) .
206      (lambda unrestricted videoMemory : Nat .
207        (lambda unrestricted rest : (family StdList (family NvidiaDemand)) .
208          (nvidiaDemand b"instruction-set" (constructor NvidiaDemandKind NvidiaDemandFeature) (constructor NvidiaDemandBound NvidiaDemandExactly) instructionSet
209            (nvidiaDemand b"registers-per-thread" (constructor NvidiaDemandKind NvidiaDemandResource) (constructor NvidiaDemandBound NvidiaDemandAtLeast) (nvidiaRegionsMaximum nvidiaRegionRegisters regions)
210              (nvidiaDemand b"threads-per-block" (constructor NvidiaDemandKind NvidiaDemandResource) (constructor NvidiaDemandBound NvidiaDemandAtLeast) (nvidiaRegionsMaximum nvidiaRegionThreads regions)
211                (nvidiaDemand b"shared-bytes-per-block" (constructor NvidiaDemandKind NvidiaDemandResource) (constructor NvidiaDemandBound NvidiaDemandAtLeast) (nvidiaRegionsMaximum nvidiaRegionShared regions)
212                  (nvidiaDemand b"video-memory-bytes" (constructor NvidiaDemandKind NvidiaDemandResource) (constructor NvidiaDemandBound NvidiaDemandAtLeast) videoMemory
213                    rest)))))))))
214
215-- a little-endian word of text (a driver version's first four bytes)
216def nvidiaCompatibilityTextWord =
217  (lambda unrestricted text : Bytes .
218    (bytes-eliminate
219      (lambda unrestricted current : Bytes . Nat)
220      0
221      (lambda unrestricted head : Byte . (lambda unrestricted tail : Bytes . (lambda unrestricted induction : Nat .
222        (naturalAdd (byte-to-nat head) (naturalMultiply 256 induction)))))
223      text))
224
225-- the instruction set a QMD architecture word names (0x86: 8.6, as 86)
226def nvidiaInstructionSetOf =
227  (lambda unrestricted architecture : Nat .
228    (naturalAdd (naturalMultiply 10 (naturalDivideUnchecked architecture 16)) (naturalModuloUnchecked architecture 16)))
229
230-- a profile with one supply dropped (what the contract's refusals are
231-- stated against)
232def nvidiaSuppliesWithout =
233  (lambda unrestricted name : Bytes .
234    (lambda unrestricted supplies : (family StdList (family NvidiaSupply)) .
235      (stdListFold (family NvidiaSupply) (family StdList (family NvidiaSupply))
236        (lambda unrestricted supply : (family NvidiaSupply) .
237          (lambda unrestricted rest : (family StdList (family NvidiaSupply)) .
238            (eliminate NvidiaSupply (lambda unrestricted current : (family NvidiaSupply) . (family StdList (family NvidiaSupply))) supply
239              (branch NvidiaSupplyValue supplied amount evidence .
240                (nat-eliminate (lambda unrestricted same : Nat . (family StdList (family NvidiaSupply)))
241                  (constructor StdList StdListCons (family NvidiaSupply) supply rest)
242                  (lambda unrestricted p : Nat . (lambda unrestricted ignored : (family StdList (family NvidiaSupply)) . rest))
243                  (bytes-equal name supplied))))))
244        nvidiaNoSupplies
245        supplies)))