1module Runtime.NativeResourcePlan
2
3import Runtime.NativePhysicalMemory
4import Runtime.NativePhysicalProgram
5import Execution.ResourceGraph
6import Compiler.Planning.Resources
7import Model.Parameter
8import Model.Word64
9import Std.Foundation
10import Std.List
11import Std.Natural
12
13-- Deployment facts and existing allocations are separate from the program.
14-- This context admits only the interpreter's owned mapping. Image/stack,
15-- syscall-created mappings and target buffers require their own derived leases.
16family NativeResourceContext : Type 0
17constructor NativeResourceContextOf
18field unrestricted nativeResourceSchedule : (family ResourceSchedule)
19field unrestricted nativeResourceAllocationIdentity : Bytes
20field unrestricted nativeResourceEndpoint : Nat
21field unrestricted nativeResourceDomain : Nat
22field unrestricted nativeResourceMappingQuantum : Nat
23field unrestricted nativeResourceEntryBudget : Nat
24field unrestricted nativeResourcePairBudget : Nat
25
26end-family
27
28family NativeResourceFailure : Type 0
29constructor NativeResourceMemoryFailed
30field unrestricted nativeResourceMemoryFailure : (family NativePhysicalMemoryFailure)
31constructor NativeResourceAdmissionFailed
32field unrestricted nativeResourceAdmissionFailure : (family ResourceFailure)
33
34end-family
35
36def nativePhysicalProgramMemory =
37 (lambda unrestricted program : (family NativePhysicalProgram) .
38 (eliminate
39 NativePhysicalProgram
40 (lambda unrestricted current : (family NativePhysicalProgram) .
41 (family StdResult (family NativePhysicalMemoryFailure) (family NativePhysicalMemoryLayout)))
42 program
43 (branch
44 NativePhysicalProgramValue
45 state
46 slots
47 commands
48 expected
49 identity
50 fallbacks
51 .
52 (planNativePhysicalMemory (modelWord64Natural state) (modelWord64Natural slots)))))
53
54-- Charge one owned allocation, rounded independently of its neighbors. An
55-- alias is not an allocation; target inventories omit it before this step.
56def nativeMemoryLease =
57 (lambda unrestricted identity : Bytes .
58 (lambda unrestricted endpoint : Nat .
59 (lambda unrestricted domain : Nat .
60 (lambda unrestricted quantum : Nat .
61 (lambda unrestricted extent : Nat .
62 (eliminate
63 StdResult
64 (lambda unrestricted current : (family StdResult (family NativePhysicalMemoryFailure) Nat) .
65 (family StdResult (family NativePhysicalMemoryFailure) (family ResourceLease)))
66 (nativeMemoryMappedBytes quantum extent)
67 (branch
68 StdFailure
69 error
70 .
71 (constructor
72 StdResult
73 StdFailure
74 (family NativePhysicalMemoryFailure)
75 (family ResourceLease)
76 error))
77 (branch
78 StdSuccess
79 bytes
80 .
81 (constructor
82 StdResult
83 StdSuccess
84 (family NativePhysicalMemoryFailure)
85 (family ResourceLease)
86 (constructor
87 ResourceLease
88 ResourceLeaseOf
89 identity
90 endpoint
91 domain
92 (constructor ResourceUnit ResourceMemoryBytes)
93 bytes
94 0
95 1)))))))))
96
97def nativeResourceContextAddLeases =
98 (lambda unrestricted context : (family NativeResourceContext) .
99 (lambda unrestricted additional : (family StdList (family ResourceLease)) .
100 (eliminate
101 NativeResourceContext
102 (lambda unrestricted current : (family NativeResourceContext) .
103 (family NativeResourceContext))
104 context
105 (branch
106 NativeResourceContextOf
107 schedule
108 identity
109 endpoint
110 domain
111 quantum
112 entries
113 pairs
114 .
115 (constructor
116 NativeResourceContext
117 NativeResourceContextOf
118 (constructor
119 ResourceSchedule
120 ResourceScheduleOf
121 (resourceScheduleGraph schedule)
122 (resourceSchedulePlacements schedule)
123 (stdListAppend (family ResourceLease) additional (resourceScheduleLeases schedule)))
124 identity
125 endpoint
126 domain
127 quantum
128 entries
129 pairs)))))
130
131-- One allocation is charged once, including holes/alignment and result/scratch
132-- storage. Frame and checkpoint residents are already inside the state extent:
133-- summing them again would double-charge the same physical pages.
134-- The conservative [0,1) epoch is the whole cooperating execution, not host time.
135def nativePhysicalInterpreterLease =
136 (lambda unrestricted identity : Bytes .
137 (lambda unrestricted endpoint : Nat .
138 (lambda unrestricted domain : Nat .
139 (lambda unrestricted quantum : Nat .
140 (lambda unrestricted program : (family NativePhysicalProgram) .
141 (stdResultBind
142 (family NativePhysicalMemoryFailure)
143 (family NativePhysicalMemoryLayout)
144 (family ResourceLease)
145 (nativePhysicalProgramMemory program)
146 (lambda unrestricted layout : (family NativePhysicalMemoryLayout) .
147 (nativeMemoryLease
148 identity
149 endpoint
150 domain
151 quantum
152 (nativePhysicalMemoryBytes layout)))))))))
153
154def admitNativePhysicalResources =
155 (lambda unrestricted context : (family NativeResourceContext) .
156 (lambda unrestricted program : (family NativePhysicalProgram) .
157 (eliminate
158 NativeResourceContext
159 (lambda unrestricted current : (family NativeResourceContext) .
160 (family StdResult (family NativeResourceFailure) (family ResourceSchedule)))
161 context
162 (branch
163 NativeResourceContextOf
164 schedule
165 identity
166 endpoint
167 domain
168 quantum
169 entries
170 pairs
171 .
172 (eliminate
173 StdResult
174 (lambda unrestricted current : (family StdResult (family NativePhysicalMemoryFailure) (family ResourceLease)) .
175 (family StdResult (family NativeResourceFailure) (family ResourceSchedule)))
176 (nativePhysicalInterpreterLease identity endpoint domain quantum program)
177 (branch
178 StdFailure
179 reason
180 .
181 (constructor
182 StdResult
183 StdFailure
184 (family NativeResourceFailure)
185 (family ResourceSchedule)
186 (constructor NativeResourceFailure NativeResourceMemoryFailed reason)))
187 (branch
188 StdSuccess
189 lease
190 .
191 (eliminate
192 StdResult
193 (lambda unrestricted current : (family StdResult (family ResourceFailure) (family ResourceSchedule)) .
194 (family StdResult (family NativeResourceFailure) (family ResourceSchedule)))
195 (admitResourceSchedule
196 entries
197 pairs
198 (constructor
199 ResourceSchedule
200 ResourceScheduleOf
201 (resourceScheduleGraph schedule)
202 (resourceSchedulePlacements schedule)
203 (constructor
204 StdList
205 StdListCons
206 (family ResourceLease)
207 lease
208 (resourceScheduleLeases schedule))))
209 (branch
210 StdFailure
211 reason
212 .
213 (constructor
214 StdResult
215 StdFailure
216 (family NativeResourceFailure)
217 (family ResourceSchedule)
218 (constructor NativeResourceFailure NativeResourceAdmissionFailed reason)))
219 (branch
220 StdSuccess
221 admitted
222 .
223 (constructor
224 StdResult
225 StdSuccess
226 (family NativeResourceFailure)
227 (family ResourceSchedule)
228 admitted)))))))))
229
230def nativePhysicalResourcesAdmitted =
231 (lambda unrestricted context : (family NativeResourceContext) .
232 (lambda unrestricted program : (family NativePhysicalProgram) .
233 (stdBoolToNatural
234 (stdResultIsSuccess
235 (family NativeResourceFailure)
236 (family ResourceSchedule)
237 (admitNativePhysicalResources context program)))))
238
239-- One native host process reserving `budget` bytes for its interpreter
240-- mapping: the context a single-participant host pairing admits against.
241-- `kind` names the executor (for example b"x86-64-native" or
242-- b"aarch64-native"); it is evidence naming the target, not a capability the
243-- admission checks.
244def nativeSingleHostResources =
245 (lambda unrestricted name : Bytes .
246 (lambda unrestricted kind : Bytes .
247 (lambda unrestricted budget : Nat .
248 (constructor
249 NativeResourceContext
250 NativeResourceContextOf
251 (constructor
252 ResourceSchedule
253 ResourceScheduleOf
254 (constructor
255 ResourceGraph
256 ResourceGraphOf
257 (constructor
258 StdList
259 StdListCons
260 (family ResourceEndpoint)
261 (constructor
262 ResourceEndpoint
263 ResourceEndpointOf
264 0
265 name
266 kind
267 (constructor
268 StdList
269 StdListCons
270 Bytes
271 b"native-interpreter"
272 (constructor StdList StdListEmpty Bytes))
273 (constructor StdList StdListCons Nat 0 (constructor StdList StdListEmpty Nat)))
274 (constructor StdList StdListEmpty (family ResourceEndpoint)))
275 (constructor
276 StdList
277 StdListCons
278 (family ResourceDomain)
279 (constructor
280 ResourceDomain
281 ResourceCapacityDomain
282 0
283 (bytes-append name b"-interpreter-reservation")
284 (constructor ResourceUnit ResourceMemoryBytes)
285 (constructor
286 ResourceFact
287 ResourceEstablished
288 budget
289 b"qualification-process-reservation"))
290 (constructor StdList StdListEmpty (family ResourceDomain)))
291 (constructor StdList StdListEmpty (family ResourceLink)))
292 (constructor StdList StdListEmpty (family ResourcePlacement))
293 (constructor StdList StdListEmpty (family ResourceLease)))
294 (bytes-append name b"-interpreter")
295 0
296 0
297 4096
298 16
299 256))))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.