Runtime.ArenaCertificate

1module Runtime.ArenaCertificate
2
3import Std.Natural
4
5-- A placement certificate for a static arena: not a byte total but the
6-- actual placement.  Every resident names its offset, extent and alignment;
7-- the certificate holds when each resident is aligned, non-empty and inside
8-- the arena, and every pair of residents is disjoint.  Residents here are
9-- all live for the whole program, so disjointness is the whole aliasing
10-- rule; lifetimes and happens-before come later, with the event graph.  The
11-- checker decides the certificate on a concrete plan by normalization.
12
13family ArenaResident : Type 0
14constructor ArenaResidentValue
15field unrestricted arenaResidentIdentity : Bytes
16field unrestricted arenaResidentOffset : Nat
17field unrestricted arenaResidentExtent : Nat
18field unrestricted arenaResidentAlignment : Nat
19end-family
20
21family ArenaResidents : Type 0
22constructor ArenaResidentsEnd
23constructor ArenaResidentsNext
24field unrestricted arenaResidentsHead : (family ArenaResident)
25recursive unrestricted arenaResidentsTail
26end-family
27
28-- the schedule's events and the pending ranges (below)
29family ArenaEvent : Type 0
30constructor ArenaHostWrite
31field unrestricted arenaHostWriteOffset : Nat
32field unrestricted arenaHostWriteExtent : Nat
33constructor ArenaHostRead
34field unrestricted arenaHostReadOffset : Nat
35field unrestricted arenaHostReadExtent : Nat
36constructor ArenaAwait
37field unrestricted arenaAwaitGeneration : Nat
38constructor ArenaObserve
39field unrestricted arenaObserveGeneration : Nat
40end-family
41
42family ArenaEvents : Type 0
43constructor ArenaEventsEnd
44constructor ArenaEventsNext
45field unrestricted arenaEventsHead : (family ArenaEvent)
46recursive unrestricted arenaEventsTail
47end-family
48
49-- the pending host writes, as [start, stop)
50family ArenaRanges : Type 0
51constructor ArenaRangesNone
52constructor ArenaRangesNext
53field unrestricted arenaRangeStart : Nat
54field unrestricted arenaRangeStop : Nat
55recursive unrestricted arenaRangesTail
56end-family
57
58-- the schedule certificate's state after a prefix of events: the next
59-- event's index (from 1), the last generation awaited, the pending writes,
60-- the first hazard (0: none yet)
61family ArenaScheduleState : Type 0
62constructor ArenaScheduleStateValue
63field unrestricted arenaStateIndex : Nat
64field unrestricted arenaStateLast : Nat
65field unrestricted arenaStatePending : (family ArenaRanges)
66field unrestricted arenaStateHazard : Nat
67end-family
68
69def arenaResidentOffsetOf =
70  (lambda unrestricted resident : (family ArenaResident) .
71    (eliminate ArenaResident (lambda unrestricted current : (family ArenaResident) . Nat) resident
72      (branch ArenaResidentValue identity offset extent alignment . offset)))
73
74def arenaResidentEndOf =
75  (lambda unrestricted resident : (family ArenaResident) .
76    (eliminate ArenaResident (lambda unrestricted current : (family ArenaResident) . Nat) resident
77      (branch ArenaResidentValue identity offset extent alignment . (naturalAdd offset extent))))
78
79-- offset mod alignment = 0, extent > 0, alignment > 0, offset + extent <= arena
80def arenaResidentValid =
81  (lambda unrestricted arenaExtent : Nat .
82    (lambda unrestricted resident : (family ArenaResident) .
83      (eliminate ArenaResident (lambda unrestricted current : (family ArenaResident) . Nat) resident
84        (branch ArenaResidentValue identity offset extent alignment .
85          (naturalAnd
86            (naturalIsZero (naturalIsZero alignment))
87            (naturalAnd
88              (naturalIsZero (nat-modulo offset alignment))
89              (naturalAnd
90                (naturalIsZero (naturalIsZero extent))
91                (naturalLessOrEqual (naturalAdd offset extent) arenaExtent))))))))
92
93-- [a, a+n) and [b, b+m) are disjoint when one ends before the other begins.
94def arenaDisjoint =
95  (lambda unrestricted left : (family ArenaResident) .
96    (lambda unrestricted right : (family ArenaResident) .
97      (naturalOr
98        (naturalLessOrEqual (arenaResidentEndOf left) (arenaResidentOffsetOf right))
99        (naturalLessOrEqual (arenaResidentEndOf right) (arenaResidentOffsetOf left)))))
100
101def arenaDisjointFromAll =
102  (lambda unrestricted resident : (family ArenaResident) .
103    (lambda unrestricted others : (family ArenaResidents) .
104      (eliminate ArenaResidents (lambda unrestricted current : (family ArenaResidents) . Nat) others
105        (branch ArenaResidentsEnd . 1)
106        (branch ArenaResidentsNext head tail induction .
107          (naturalAnd (arenaDisjoint resident head) induction)))))
108
109-- 1 when the placement is certified, 0 otherwise.
110def arenaCertificate =
111  (lambda unrestricted arenaExtent : Nat .
112    (lambda unrestricted residents : (family ArenaResidents) .
113      (eliminate ArenaResidents (lambda unrestricted current : (family ArenaResidents) . Nat) residents
114        (branch ArenaResidentsEnd . 1)
115        (branch ArenaResidentsNext head tail induction .
116          (naturalAnd (arenaResidentValid arenaExtent head)
117            (naturalAnd (arenaDisjointFromAll head tail) induction))))))
118
119-- ---- the schedule over the arena ----
120-- What the certificate sees of a host's schedule over its host-visible
121-- arena: the host writes a range, reads a range, awaits a submission by its
122-- generation (the submissions issued once it is written; the host goes on
123-- only when that one has completed), or observes an awaited submission (a
124-- timestamp of it).  The device's work is ordered with the host's by those
125-- waits alone, so the certificate decides that the order the host relies on
126-- is the order it has:
127--   * generations strictly increase, so every wait awaits work its own
128--     submit issued -- a completion of an earlier generation cannot satisfy
129--     it -- and the last is the plan's count: every submission awaited;
130--   * a host write is pending until a submission consumes it; a host write
131--     over a pending range would overwrite staging no submission has read,
132--     and none may be pending at the end;
133--   * a host read of a pending range would read back the host's own
134--     staging, not a submission's result;
135--   * an observation names an awaited generation.
136-- Ranges of no bytes touch nothing.
137
138def arenaRangesNone : (family ArenaRanges) = (constructor ArenaRanges ArenaRangesNone)
139
140-- 1 when [start, stop) meets a range of the list
141def arenaRangesMeet =
142  (lambda unrestricted start : Nat .
143    (lambda unrestricted stop : Nat .
144      (lambda unrestricted ranges : (family ArenaRanges) .
145        (eliminate ArenaRanges (lambda unrestricted current : (family ArenaRanges) . Nat) ranges
146          (branch ArenaRangesNone . 0)
147          (branch ArenaRangesNext otherStart otherStop tail induction .
148            (naturalOr (naturalAnd (naturalLess start otherStop) (naturalLess otherStart stop)) induction))))))
149
150def arenaRangesEmpty =
151  (lambda unrestricted ranges : (family ArenaRanges) .
152    (eliminate ArenaRanges (lambda unrestricted current : (family ArenaRanges) . Nat) ranges
153      (branch ArenaRangesNone . 1)
154      (branch ArenaRangesNext start stop tail induction . 0)))
155
156-- The walk as a state: each event moves it (one recursive call an event;
157-- a choice between two continuations would be evaluated on both sides by
158-- the build's evaluator), the first hazard found kept.
159def arenaScheduleStart : (family ArenaScheduleState) =
160  (constructor ArenaScheduleState ArenaScheduleStateValue 1 0 (constructor ArenaRanges ArenaRangesNone) 0)
161def arenaStateIndexOf : (pi unrestricted state : (family ArenaScheduleState) . Nat) =
162  (lambda unrestricted state : (family ArenaScheduleState) . (project ArenaScheduleState arenaStateIndex state))
163def arenaStateLastOf : (pi unrestricted state : (family ArenaScheduleState) . Nat) =
164  (lambda unrestricted state : (family ArenaScheduleState) . (project ArenaScheduleState arenaStateLast state))
165def arenaStatePendingOf : (pi unrestricted state : (family ArenaScheduleState) . (family ArenaRanges)) =
166  (lambda unrestricted state : (family ArenaScheduleState) . (project ArenaScheduleState arenaStatePending state))
167def arenaStateHazardOf : (pi unrestricted state : (family ArenaScheduleState) . Nat) =
168  (lambda unrestricted state : (family ArenaScheduleState) . (project ArenaScheduleState arenaStateHazard state))
169def arenaScheduleRun =
170  (lambda unrestricted state : (family ArenaScheduleState) .
171    (lambda unrestricted events : (family ArenaEvents) .
172      (app
173        (eliminate ArenaEvents
174          (lambda unrestricted current : (family ArenaEvents) .
175            (pi unrestricted at : (family ArenaScheduleState) . (family ArenaScheduleState)))
176          events
177          (branch ArenaEventsEnd . (lambda unrestricted at : (family ArenaScheduleState) . at))
178          (branch ArenaEventsNext event rest induction .
179            (lambda unrestricted at : (family ArenaScheduleState) .
180              (let unrestricted index = (arenaStateIndexOf at) in
181              (let unrestricted last = (arenaStateLastOf at) in
182              (let unrestricted pending = (arenaStatePendingOf at) in
183              (let unrestricted hazard = (arenaStateHazardOf at) in
184              (let unrestricted found = (lambda unrestricted failed : Nat . (naturalSelect hazard hazard (naturalSelect failed index 0))) in
185              (let unrestricted next = (lambda unrestricted newLast : Nat . (lambda unrestricted newPending : (family ArenaRanges) .
186                  (lambda unrestricted newHazard : Nat .
187                    (constructor ArenaScheduleState ArenaScheduleStateValue (succ index) newLast newPending newHazard)))) in
188                (induction
189                  (eliminate ArenaEvent (lambda unrestricted current : (family ArenaEvent) . (family ArenaScheduleState)) event
190                    (branch ArenaHostWrite offset extent .
191                      (let unrestricted meets = (naturalAnd (naturalNonzero extent) (arenaRangesMeet offset (naturalAdd offset extent) pending))
192                        in (next last
193                             (nat-eliminate (lambda unrestricted current : Nat . (family ArenaRanges))
194                               pending
195                               (lambda unrestricted predecessor : Nat . (lambda unrestricted unused : (family ArenaRanges) .
196                                 (constructor ArenaRanges ArenaRangesNext offset (naturalAdd offset extent) pending)))
197                               (naturalAnd (naturalNonzero extent) (naturalIsZero meets)))
198                             (found meets))))
199                    (branch ArenaHostRead offset extent .
200                      (next last pending
201                        (found (naturalAnd (naturalNonzero extent) (arenaRangesMeet offset (naturalAdd offset extent) pending)))))
202                    (branch ArenaAwait generation .
203                      (let unrestricted fresh = (naturalLess last generation)
204                        in (next (naturalSelect fresh generation last)
205                             (nat-eliminate (lambda unrestricted current : Nat . (family ArenaRanges))
206                               pending
207                               (lambda unrestricted predecessor : Nat . (lambda unrestricted unused : (family ArenaRanges) . arenaRangesNone))
208                               fresh)
209                             (found (naturalIsZero fresh)))))
210                    (branch ArenaObserve generation .
211                      (next last pending
212                        (found (naturalIsZero (naturalAnd (naturalNonzero generation) (naturalLessOrEqual generation last)))))))))))))))))
213        state)))
214-- The first event that breaks the order, counted from 1 (one past the last
215-- when the end does: a submission never awaited, or a write never
216-- consumed), or 0 when none does.
217def arenaScheduleEnd =
218  (lambda unrestricted count : Nat .
219    (lambda unrestricted state : (family ArenaScheduleState) .
220      (let unrestricted hazard = (arenaStateHazardOf state) in
221        (naturalSelect hazard hazard
222          (naturalSelect (naturalAnd (naturalEqual (arenaStateLastOf state) count) (arenaRangesEmpty (arenaStatePendingOf state)))
223            0 (arenaStateIndexOf state))))))
224def arenaScheduleHazard =
225  (lambda unrestricted count : Nat .
226    (lambda unrestricted events : (family ArenaEvents) .
227      (arenaScheduleEnd count (arenaScheduleRun arenaScheduleStart events))))
228
229-- a choice of two states (flag nonzero: the first)
230def arenaSelectState =
231  (lambda unrestricted flag : Nat .
232    (lambda unrestricted whenNonzero : (family ArenaScheduleState) . (lambda unrestricted whenZero : (family ArenaScheduleState) .
233      (nat-eliminate (lambda unrestricted current : Nat . (family ArenaScheduleState)) whenZero
234        (lambda unrestricted p : Nat . (lambda unrestricted ignored : (family ArenaScheduleState) . whenNonzero)) flag))))
235
236-- ---- a repeat without its iterations ----
237-- 1 when `later` is `earlier` with every awaited and observed generation
238-- `shift` higher, the host's ranges the same: the next iteration of a
239-- repeat body whose generations advance by `shift` an iteration
240def arenaEventShifted =
241  (lambda unrestricted shift : Nat .
242    (lambda unrestricted a : (family ArenaEvent) . (lambda unrestricted b : (family ArenaEvent) .
243      (eliminate ArenaEvent (lambda unrestricted current : (family ArenaEvent) . Nat) a
244        (branch ArenaHostWrite offset extent .
245          (eliminate ArenaEvent (lambda unrestricted current : (family ArenaEvent) . Nat) b
246            (branch ArenaHostWrite o e . (naturalAnd (naturalEqual offset o) (naturalEqual extent e)))
247            (branch ArenaHostRead o e . 0) (branch ArenaAwait g . 0) (branch ArenaObserve g . 0)))
248        (branch ArenaHostRead offset extent .
249          (eliminate ArenaEvent (lambda unrestricted current : (family ArenaEvent) . Nat) b
250            (branch ArenaHostWrite o e . 0)
251            (branch ArenaHostRead o e . (naturalAnd (naturalEqual offset o) (naturalEqual extent e)))
252            (branch ArenaAwait g . 0) (branch ArenaObserve g . 0)))
253        (branch ArenaAwait generation .
254          (eliminate ArenaEvent (lambda unrestricted current : (family ArenaEvent) . Nat) b
255            (branch ArenaHostWrite o e . 0) (branch ArenaHostRead o e . 0)
256            (branch ArenaAwait g . (naturalEqual g (naturalAdd generation shift))) (branch ArenaObserve g . 0)))
257        (branch ArenaObserve generation .
258          (eliminate ArenaEvent (lambda unrestricted current : (family ArenaEvent) . Nat) b
259            (branch ArenaHostWrite o e . 0) (branch ArenaHostRead o e . 0) (branch ArenaAwait g . 0)
260            (branch ArenaObserve g . (naturalEqual g (naturalAdd generation shift)))))))))
261def arenaEventsShifted =
262  (lambda unrestricted shift : Nat .
263    (lambda unrestricted earlier : (family ArenaEvents) . (lambda unrestricted later : (family ArenaEvents) .
264      (app
265        (eliminate ArenaEvents
266          (lambda unrestricted current : (family ArenaEvents) . (pi unrestricted other : (family ArenaEvents) . Nat))
267          earlier
268          (branch ArenaEventsEnd . (lambda unrestricted other : (family ArenaEvents) .
269            (eliminate ArenaEvents (lambda unrestricted c : (family ArenaEvents) . Nat) other
270              (branch ArenaEventsEnd . 1) (branch ArenaEventsNext h t i . 0))))
271          (branch ArenaEventsNext head rest induction . (lambda unrestricted other : (family ArenaEvents) .
272            (eliminate ArenaEvents (lambda unrestricted c : (family ArenaEvents) . Nat) other
273              (branch ArenaEventsEnd . 0)
274              (branch ArenaEventsNext h t i . (naturalAnd (arenaEventShifted shift head h) (induction t)))))))
275        later))))
276def arenaEventsLength =
277  (lambda unrestricted events : (family ArenaEvents) .
278    (eliminate ArenaEvents (lambda unrestricted c : (family ArenaEvents) . Nat) events
279      (branch ArenaEventsEnd . 0) (branch ArenaEventsNext head rest induction . (succ induction))))
280def arenaRangesEqual =
281  (lambda unrestricted a : (family ArenaRanges) . (lambda unrestricted b : (family ArenaRanges) .
282    (app
283      (eliminate ArenaRanges (lambda unrestricted c : (family ArenaRanges) . (pi unrestricted other : (family ArenaRanges) . Nat)) a
284        (branch ArenaRangesNone . (lambda unrestricted other : (family ArenaRanges) . (arenaRangesEmpty other)))
285        (branch ArenaRangesNext start stop rest induction . (lambda unrestricted other : (family ArenaRanges) .
286          (eliminate ArenaRanges (lambda unrestricted c : (family ArenaRanges) . Nat) other
287            (branch ArenaRangesNone . 0)
288            (branch ArenaRangesNext s2 e2 t2 i2 .
289              (naturalAnd (naturalAnd (naturalEqual start s2) (naturalEqual stop e2)) (induction t2)))))))
290      b)))
291-- A repeat of `count` iterations whose iteration k's events are
292-- `events k`, run from `state` without walking every iteration.
293-- Iterations 0 and 1 run; then iteration 2's events must be iteration 1's
294-- with every generation shifted by what iteration 1 advanced the last
295-- awaited generation (shift), and iteration 1 must leave the pending writes
296-- it found.  Iteration k + 1 then starts from iteration k's state shifted
297-- by `shift`, with the same pending writes, and runs events shifted by
298-- `shift` (the steps are affine in k: their difference from k to k + 1 is
299-- fixed): every comparison the walk makes (a generation against the last,
300-- a range against the pending ones) is the same as iteration 1's, so it
301-- finds what iteration 1 found -- no hazard -- and ends shifted again.  So
302-- the repeat ends `count - 2` shifts past iteration 1.  A body whose next
303-- iteration is not so shifted is a hazard at its index.
304def arenaScheduleRepeat =
305  (lambda unrestricted count : Nat .
306    (lambda unrestricted events : (pi unrestricted iteration : Nat . (family ArenaEvents)) .
307      (lambda unrestricted state : (family ArenaScheduleState) .
308        (let unrestricted one = (arenaScheduleRun state (events 0)) in
309        (let unrestricted two = (arenaScheduleRun one (events 1)) in
310        (let unrestricted shift = (naturalSaturatingSubtract (arenaStateLastOf two) (arenaStateLastOf one)) in
311        (let unrestricted periodic =
312            (naturalAnd (arenaEventsShifted shift (events 1) (events 2))
313              (arenaRangesEqual (arenaStatePendingOf one) (arenaStatePendingOf two))) in
314        (let unrestricted rest = (naturalSaturatingSubtract count 2) in
315        (let unrestricted hazard = (arenaStateHazardOf two) in
316        (let unrestricted many =
317            (constructor ArenaScheduleState ArenaScheduleStateValue
318              (naturalAdd (arenaStateIndexOf two) (naturalMultiply rest (arenaEventsLength (events 1))))
319              (naturalAdd (arenaStateLastOf two) (naturalMultiply rest shift))
320              (arenaStatePendingOf two)
321              (naturalSelect hazard hazard (naturalSelect periodic 0 (arenaStateIndexOf two)))) in
322          (arenaSelectState (naturalIsZero count) state
323            (arenaSelectState (naturalEqual count 1) one
324              (arenaSelectState (naturalEqual count 2) two many)))))))))))))
325
326
327-- 1 when the schedule keeps the order, 0 otherwise.
328def arenaScheduleCertificate =
329  (lambda unrestricted count : Nat .
330    (lambda unrestricted events : (family ArenaEvents) .
331      (naturalIsZero (arenaScheduleHazard count events))))