1module Runtime.RegionTransfer
2
3import Learning.Transition
4import Representation.Partition
5import Std.Foundation
6import Std.Natural
7
8-- Logical identity, before choosing transport or encoding. A matching byte
9-- count alone cannot authorize a receive. Digests and authentication belong
10-- to the wire boundary; process pointers never belong in a logical message.
11family RegionTransferIdentity : Type 0
12constructor RegionTransferIdentityOf
13field unrestricted transferComposition : Bytes
14field unrestricted transferRun : Bytes
15field unrestricted transferRegion : Bytes
16field unrestricted transferRepresentation : Bytes
17field unrestricted transferRound : (family LearningRound)
18field unrestricted transferOperation : Nat
19field unrestricted transferSender : Nat
20field unrestricted transferReceiver : Nat
21field unrestricted transferInterval : (family LogicalInterval)
22
23end-family
24
25family TransferPhase : Type 0
26constructor TransferDeclared
27constructor TransferSourceReading
28constructor TransferSourceReleased
29constructor TransferPayloadReceived
30constructor TransferDestinationVisible
31constructor TransferConsumed
32constructor TransferAborted
33
34end-family
35
36family TransferEvent : Type 0
37constructor TransferBeginRead
38constructor TransferFinishRead
39constructor TransferValidatePayload
40constructor TransferEstablishVisibility
41constructor TransferConsume
42constructor TransferAbort
43
44end-family
45
46family TransferFailure : Type 0
47constructor TransferIdentityMismatch
48constructor TransferPayloadSizeMismatch
49constructor TransferIllegalPhase
50
51end-family
52
53def regionTransferIdentityEqual =
54 (lambda unrestricted expected : (family RegionTransferIdentity) .
55 (lambda unrestricted actual : (family RegionTransferIdentity) .
56 (eliminate
57 RegionTransferIdentity
58 (lambda unrestricted current : (family RegionTransferIdentity) . Nat)
59 expected
60 (branch
61 RegionTransferIdentityOf
62 expectedComposition
63 expectedRun
64 expectedRegion
65 expectedRepresentation
66 expectedRound
67 expectedOperation
68 expectedSender
69 expectedReceiver
70 expectedInterval
71 .
72 (eliminate
73 RegionTransferIdentity
74 (lambda unrestricted current : (family RegionTransferIdentity) . Nat)
75 actual
76 (branch
77 RegionTransferIdentityOf
78 actualComposition
79 actualRun
80 actualRegion
81 actualRepresentation
82 actualRound
83 actualOperation
84 actualSender
85 actualReceiver
86 actualInterval
87 .
88 (naturalAnd
89 (bytes-equal expectedComposition actualComposition)
90 (naturalAnd
91 (bytes-equal expectedRun actualRun)
92 (naturalAnd
93 (bytes-equal expectedRegion actualRegion)
94 (naturalAnd
95 (bytes-equal expectedRepresentation actualRepresentation)
96 (naturalAnd
97 (learningRoundEqual expectedRound actualRound)
98 (naturalAnd
99 (naturalEqual expectedOperation actualOperation)
100 (naturalAnd
101 (naturalEqual expectedSender actualSender)
102 (naturalAnd
103 (naturalEqual expectedReceiver actualReceiver)
104 (naturalAnd
105 (naturalEqual
106 (intervalBegin expectedInterval)
107 (intervalBegin actualInterval))
108 (naturalEqual
109 (intervalEnd expectedInterval)
110 (intervalEnd actualInterval)))))))))))))))))
111
112def transferPhaseCode =
113 (lambda unrestricted phase : (family TransferPhase) .
114 (eliminate
115 TransferPhase
116 (lambda unrestricted current : (family TransferPhase) . Nat)
117 phase
118 (branch TransferDeclared . 0)
119 (branch TransferSourceReading . 1)
120 (branch TransferSourceReleased . 2)
121 (branch TransferPayloadReceived . 3)
122 (branch TransferDestinationVisible . 4)
123 (branch TransferConsumed . 5)
124 (branch TransferAborted . 6)))
125
126def transferRequirePhase =
127 (lambda unrestricted expected : Nat .
128 (lambda unrestricted next : (family TransferPhase) .
129 (lambda unrestricted actual : (family TransferPhase) .
130 (nat-eliminate
131 (lambda unrestricted flag : Nat .
132 (family StdResult (family TransferFailure) (family TransferPhase)))
133 (constructor
134 StdResult
135 StdFailure
136 (family TransferFailure)
137 (family TransferPhase)
138 (constructor TransferFailure TransferIllegalPhase))
139 (lambda unrestricted previous : Nat .
140 (lambda unrestricted ignored : (family StdResult (family TransferFailure) (family TransferPhase)) .
141 (constructor
142 StdResult
143 StdSuccess
144 (family TransferFailure)
145 (family TransferPhase)
146 next)))
147 (naturalEqual expected (transferPhaseCode actual))))))
148
149-- These are protocol states, not claims of physical DMA completion. A native
150-- realization must obtain events from its actual transport and visibility
151-- primitives. One edge's state has one execution owner.
152def advanceTransferPhase =
153 (lambda unrestricted phase : (family TransferPhase) .
154 (lambda unrestricted event : (family TransferEvent) .
155 (eliminate
156 TransferEvent
157 (lambda unrestricted current : (family TransferEvent) .
158 (family StdResult (family TransferFailure) (family TransferPhase)))
159 event
160 (branch
161 TransferBeginRead
162 .
163 (transferRequirePhase 0 (constructor TransferPhase TransferSourceReading) phase))
164 (branch
165 TransferFinishRead
166 .
167 (transferRequirePhase 1 (constructor TransferPhase TransferSourceReleased) phase))
168 (branch
169 TransferValidatePayload
170 .
171 (transferRequirePhase 2 (constructor TransferPhase TransferPayloadReceived) phase))
172 (branch
173 TransferEstablishVisibility
174 .
175 (transferRequirePhase 3 (constructor TransferPhase TransferDestinationVisible) phase))
176 (branch
177 TransferConsume
178 .
179 (transferRequirePhase 4 (constructor TransferPhase TransferConsumed) phase))
180 (branch
181 TransferAbort
182 .
183 (nat-eliminate
184 (lambda unrestricted flag : Nat .
185 (family StdResult (family TransferFailure) (family TransferPhase)))
186 (constructor
187 StdResult
188 StdFailure
189 (family TransferFailure)
190 (family TransferPhase)
191 (constructor TransferFailure TransferIllegalPhase))
192 (lambda unrestricted previous : Nat .
193 (lambda unrestricted ignored : (family StdResult (family TransferFailure) (family TransferPhase)) .
194 (constructor
195 StdResult
196 StdSuccess
197 (family TransferFailure)
198 (family TransferPhase)
199 (constructor TransferPhase TransferAborted))))
200 (naturalLess (transferPhaseCode phase) 5))))))
201
202-- Aborting does not establish that in-flight DMA has stopped. Teardown must
203-- drain those reads before reclaiming resources.
204def transferSourceReusable =
205 (lambda unrestricted phase : (family TransferPhase) .
206 (let unrestricted code =
207 (transferPhaseCode phase)
208 in
209 (naturalAnd (naturalLessOrEqual 2 code) (naturalLessOrEqual code 5))))
210
211def transferDestinationUsable =
212 (lambda unrestricted phase : (family TransferPhase) .
213 (let unrestricted code =
214 (transferPhaseCode phase)
215 in
216 (naturalAnd (naturalLessOrEqual 4 code) (naturalLessOrEqual code 5))))
217
218def receiveRegionTransfer =
219 (lambda unrestricted expected : (family RegionTransferIdentity) .
220 (lambda unrestricted actual : (family RegionTransferIdentity) .
221 (lambda unrestricted expectedBytes : Nat .
222 (lambda unrestricted actualBytes : Nat .
223 (lambda unrestricted phase : (family TransferPhase) .
224 (nat-eliminate
225 (lambda unrestricted flag : Nat .
226 (family StdResult (family TransferFailure) (family TransferPhase)))
227 (constructor
228 StdResult
229 StdFailure
230 (family TransferFailure)
231 (family TransferPhase)
232 (constructor TransferFailure TransferIdentityMismatch))
233 (lambda unrestricted previous : Nat .
234 (lambda unrestricted ignored : (family StdResult (family TransferFailure) (family TransferPhase)) .
235 (nat-eliminate
236 (lambda unrestricted flag : Nat .
237 (family StdResult (family TransferFailure) (family TransferPhase)))
238 (constructor
239 StdResult
240 StdFailure
241 (family TransferFailure)
242 (family TransferPhase)
243 (constructor TransferFailure TransferPayloadSizeMismatch))
244 (lambda unrestricted before : Nat .
245 (lambda unrestricted rest : (family StdResult (family TransferFailure) (family TransferPhase)) .
246 (advanceTransferPhase
247 phase
248 (constructor TransferEvent TransferValidatePayload))))
249 (naturalEqual expectedBytes actualBytes))))
250 (regionTransferIdentityEqual expected actual)))))))
251
252-- Route projection reads the same identity that the wire header encodes;
253-- participant programs must not keep a second, independently chosen route.
254def regionTransferSender =
255 (lambda unrestricted identity : (family RegionTransferIdentity) .
256 (eliminate
257 RegionTransferIdentity
258 (lambda unrestricted current : (family RegionTransferIdentity) . Nat)
259 identity
260 (branch
261 RegionTransferIdentityOf
262 composition
263 run
264 region
265 representation
266 round
267 operation
268 sender
269 receiver
270 interval
271 .
272 sender)))
273
274def regionTransferReceiver =
275 (lambda unrestricted identity : (family RegionTransferIdentity) .
276 (eliminate
277 RegionTransferIdentity
278 (lambda unrestricted current : (family RegionTransferIdentity) . Nat)
279 identity
280 (branch
281 RegionTransferIdentityOf
282 composition
283 run
284 region
285 representation
286 round
287 operation
288 sender
289 receiver
290 interval
291 .
292 receiver)))
293
294-- Change only the route of a logical transfer; all scope, version and region
295-- fields survive. Used when a single decision is disseminated along a tree.
296
297def regionTransferWithRoute =
298(lambda unrestricted identity : (family RegionTransferIdentity) .
299(lambda unrestricted sender : Nat .
300(lambda unrestricted receiver : Nat .
301(eliminate RegionTransferIdentity (lambda unrestricted current : (family RegionTransferIdentity) . (family RegionTransferIdentity)) identity
302(branch RegionTransferIdentityOf composition run region representation round operation oldSender oldReceiver interval .
303(constructor RegionTransferIdentity RegionTransferIdentityOf composition run region representation round operation sender receiver interval))))))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.