1module Runtime.NativePhysicalMemory
2
3import Data.Bytes
4import Model.Parameter
5import Model.Word64
6import Std.Foundation
7import Std.Natural
8
9-- The interpreter's allocation contains program state, result words, then
10-- repeat and wait state. Both native hosts implement this same layout.
11-- Keep this ABI independent of the program/target owners so admission, memory
12-- reservations and machine emitters share one calculation. The scratch extent
13-- depends on the repeat nesting depth the interpreter is built for (see
14-- nativePhysicalRepeatScratchBytes), so every reservation takes that depth.
15family NativePhysicalMemoryLayout : Type 0
16constructor NativePhysicalMemoryLayoutOf
17field unrestricted nativePhysicalMemoryStateBytes : Nat
18field unrestricted nativePhysicalMemorySlotBytes : Nat
19field unrestricted nativePhysicalMemoryScratchOffset : Nat
20field unrestricted nativePhysicalMemoryAllocationBytes : Nat
21
22end-family
23
24family NativePhysicalMemoryFailure : Type 0
25constructor NativePhysicalMemoryEmpty
26constructor NativePhysicalMemoryOverflow
27constructor NativePhysicalMemoryPageInvalid
28
29end-family
30
31def nativePhysicalMemoryWordLimit =
32 18446744073709551615
33
34def nativePhysicalMemoryWordBytes =
35 (bytes-length (dataBytesWord64LE (modelWord64FromNaturalTruncated 0)))
36
37-- The ISA shift implementing multiplication by one ABI word; checked below.
38def nativePhysicalMemoryWordShift =
39 3
40
41def nativePhysicalMemoryIterationOffset =
42 0
43
44def nativePhysicalMemoryCountOffset =
45 (naturalAdd nativePhysicalMemoryIterationOffset nativePhysicalMemoryWordBytes)
46
47def nativePhysicalMemoryBodyOffset =
48 (naturalAdd nativePhysicalMemoryCountOffset nativePhysicalMemoryWordBytes)
49
50def nativePhysicalMemoryBodyCountOffset =
51 (naturalAdd nativePhysicalMemoryBodyOffset nativePhysicalMemoryWordBytes)
52
53def nativePhysicalMemoryWaitSecondsOffset =
54 (naturalAdd nativePhysicalMemoryBodyCountOffset nativePhysicalMemoryWordBytes)
55
56def nativePhysicalMemoryWaitNanosOffset =
57 (naturalAdd nativePhysicalMemoryWaitSecondsOffset nativePhysicalMemoryWordBytes)
58
59-- The depth-independent part of the scratch: the active repeat frame's four
60-- words and the fence wait's timespec. A program without repeats needs only
61-- this (nativePhysicalRepeatScratchBytes 0).
62def nativePhysicalMemoryScratchBytes =
63 (naturalAdd nativePhysicalMemoryWaitNanosOffset nativePhysicalMemoryWordBytes)
64
65-- Repeat frames extend that scratch: the depth word follows the wait timespec,
66-- then one saved frame per nesting level, each holding the iteration, count,
67-- first body record and body record count. Both interpreters (x86-64
68-- Runtime.NativePhysicalNative, AArch64 Platform.AArch64.NativePhysicalRuntime)
69-- address these offsets and allocate exactly nativePhysicalRepeatScratchBytes
70-- for the depth they are built for.
71def nativePhysicalRepeatDepthAt : Nat =
72 nativePhysicalMemoryScratchBytes
73
74def nativePhysicalRepeatFramesAt : Nat =
75 (naturalAdd nativePhysicalRepeatDepthAt nativePhysicalMemoryWordBytes)
76
77def nativePhysicalRepeatFrameBytes : Nat =
78 (naturalSaturatingSubtract
79 nativePhysicalMemoryWaitSecondsOffset
80 nativePhysicalMemoryIterationOffset)
81
82-- Depth zero has no depth word and no saved frame: the interpreter for a
83-- repeat-free program allocates only the base scratch.
84def nativePhysicalRepeatScratchBytes =
85 (lambda unrestricted depth : Nat .
86 (naturalSelect
87 (naturalEqual depth 0)
88 nativePhysicalRepeatDepthAt
89 (naturalAdd
90 nativePhysicalRepeatFramesAt
91 (naturalMultiply depth nativePhysicalRepeatFrameBytes))))
92
93-- Admission and reservation charge the scratch of the interpreter that will
94-- run the program, i.e. of its maximum repeat depth, never a fixed extent:
95-- a reservation smaller than the allocation would let a nested program map
96-- more than it was admitted for.
97def nativePhysicalMemoryAdmitted =
98 (lambda unrestricted state : Nat .
99 (lambda unrestricted slots : Nat .
100 (lambda unrestricted depth : Nat .
101 (let unrestricted scratch =
102 (nativePhysicalRepeatScratchBytes depth)
103 in
104 (naturalAnd
105 (naturalNonzero state)
106 (naturalAnd
107 (naturalLessOrEqual
108 state
109 (naturalSaturatingSubtract nativePhysicalMemoryWordLimit scratch))
110 (naturalLessOrEqual
111 slots
112 (naturalDivideUnchecked
113 (naturalSaturatingSubtract
114 (naturalSaturatingSubtract nativePhysicalMemoryWordLimit scratch)
115 state)
116 nativePhysicalMemoryWordBytes))))))))
117
118def planNativePhysicalMemory =
119 (lambda unrestricted state : Nat .
120 (lambda unrestricted slots : Nat .
121 (lambda unrestricted depth : Nat .
122 (eliminate
123 StdBool
124 (lambda unrestricted flag : (family StdBool) .
125 (family
126 StdResult
127 (family NativePhysicalMemoryFailure)
128 (family NativePhysicalMemoryLayout)))
129 (stdBoolFromNatural (naturalNonzero state))
130 (branch
131 StdTrue
132 .
133 (eliminate
134 StdBool
135 (lambda unrestricted flag : (family StdBool) .
136 (family
137 StdResult
138 (family NativePhysicalMemoryFailure)
139 (family NativePhysicalMemoryLayout)))
140 (stdBoolFromNatural (nativePhysicalMemoryAdmitted state slots depth))
141 (branch
142 StdTrue
143 .
144 (let unrestricted slotBytes =
145 (naturalMultiply slots nativePhysicalMemoryWordBytes)
146 in
147 (let unrestricted scratch =
148 (naturalAdd state slotBytes)
149 in
150 (constructor
151 StdResult
152 StdSuccess
153 (family NativePhysicalMemoryFailure)
154 (family NativePhysicalMemoryLayout)
155 (constructor
156 NativePhysicalMemoryLayout
157 NativePhysicalMemoryLayoutOf
158 state
159 slotBytes
160 scratch
161 (naturalAdd scratch (nativePhysicalRepeatScratchBytes depth)))))))
162 (branch
163 StdFalse
164 .
165 (constructor
166 StdResult
167 StdFailure
168 (family NativePhysicalMemoryFailure)
169 (family NativePhysicalMemoryLayout)
170 (constructor NativePhysicalMemoryFailure NativePhysicalMemoryOverflow)))))
171 (branch
172 StdFalse
173 .
174 (constructor
175 StdResult
176 StdFailure
177 (family NativePhysicalMemoryFailure)
178 (family NativePhysicalMemoryLayout)
179 (constructor NativePhysicalMemoryFailure NativePhysicalMemoryEmpty)))))))
180
181def nativePhysicalMemoryBytes =
182 (lambda unrestricted layout : (family NativePhysicalMemoryLayout) .
183 (eliminate
184 NativePhysicalMemoryLayout
185 (lambda unrestricted current : (family NativePhysicalMemoryLayout) . Nat)
186 layout
187 (branch NativePhysicalMemoryLayoutOf state slots scratch bytes . bytes)))
188
189-- Mapping granularity is a platform/deployment fact, never guessed from a
190-- neighboring host. This accepts a positive declared quantum; its provenance
191-- and agreement with the actual OS mapping remain the target's responsibility.
192def nativeMemoryMappedBytes =
193 (lambda unrestricted quantum : Nat .
194 (lambda unrestricted bytes : Nat .
195 (eliminate
196 StdBool
197 (lambda unrestricted flag : (family StdBool) .
198 (family StdResult (family NativePhysicalMemoryFailure) Nat))
199 (stdBoolFromNatural
200 (naturalAnd
201 (naturalNonzero quantum)
202 (naturalAnd
203 (naturalLessOrEqual quantum nativePhysicalMemoryWordLimit)
204 (naturalAnd
205 (naturalNonzero bytes)
206 (naturalLessOrEqual bytes nativePhysicalMemoryWordLimit)))))
207 (branch
208 StdTrue
209 .
210 (let unrestricted pages =
211 (naturalAdd (naturalDivideUnchecked (naturalSaturatingSubtract bytes 1) quantum) 1)
212 in
213 (eliminate
214 StdBool
215 (lambda unrestricted flag : (family StdBool) .
216 (family StdResult (family NativePhysicalMemoryFailure) Nat))
217 (stdBoolFromNatural
218 (naturalLessOrEqual
219 pages
220 (naturalDivideUnchecked nativePhysicalMemoryWordLimit quantum)))
221 (branch
222 StdTrue
223 .
224 (constructor
225 StdResult
226 StdSuccess
227 (family NativePhysicalMemoryFailure)
228 Nat
229 (naturalMultiply pages quantum)))
230 (branch
231 StdFalse
232 .
233 (constructor
234 StdResult
235 StdFailure
236 (family NativePhysicalMemoryFailure)
237 Nat
238 (constructor NativePhysicalMemoryFailure NativePhysicalMemoryOverflow))))))
239 (branch
240 StdFalse
241 .
242 (constructor
243 StdResult
244 StdFailure
245 (family NativePhysicalMemoryFailure)
246 Nat
247 (constructor NativePhysicalMemoryFailure NativePhysicalMemoryPageInvalid))))))
248
249def nativePhysicalMemoryMappedBytes =
250 (lambda unrestricted quantum : Nat .
251 (lambda unrestricted layout : (family NativePhysicalMemoryLayout) .
252 (nativeMemoryMappedBytes quantum (nativePhysicalMemoryBytes layout))))
253
254def nativePhysicalMemoryWordShiftLaw :
255 (equal Nat (naturalPowerOfTwo nativePhysicalMemoryWordShift) nativePhysicalMemoryWordBytes) =
256 (refl Nat 8)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.