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
58def arenaResidentOffsetOf =
59  (lambda unrestricted resident : (family ArenaResident) .
60    (eliminate ArenaResident (lambda unrestricted current : (family ArenaResident) . Nat) resident
61      (branch ArenaResidentValue identity offset extent alignment . offset)))
62
63def arenaResidentEndOf =
64  (lambda unrestricted resident : (family ArenaResident) .
65    (eliminate ArenaResident (lambda unrestricted current : (family ArenaResident) . Nat) resident
66      (branch ArenaResidentValue identity offset extent alignment . (naturalAdd offset extent))))
67
68-- offset mod alignment = 0, extent > 0, alignment > 0, offset + extent <= arena
69def arenaResidentValid =
70  (lambda unrestricted arenaExtent : Nat .
71    (lambda unrestricted resident : (family ArenaResident) .
72      (eliminate ArenaResident (lambda unrestricted current : (family ArenaResident) . Nat) resident
73        (branch ArenaResidentValue identity offset extent alignment .
74          (naturalAnd
75            (naturalIsZero (naturalIsZero alignment))
76            (naturalAnd
77              (naturalIsZero (nat-modulo offset alignment))
78              (naturalAnd
79                (naturalIsZero (naturalIsZero extent))
80                (naturalLessOrEqual (naturalAdd offset extent) arenaExtent))))))))
81
82-- [a, a+n) and [b, b+m) are disjoint when one ends before the other begins.
83def arenaDisjoint =
84  (lambda unrestricted left : (family ArenaResident) .
85    (lambda unrestricted right : (family ArenaResident) .
86      (naturalOr
87        (naturalLessOrEqual (arenaResidentEndOf left) (arenaResidentOffsetOf right))
88        (naturalLessOrEqual (arenaResidentEndOf right) (arenaResidentOffsetOf left)))))
89
90def arenaDisjointFromAll =
91  (lambda unrestricted resident : (family ArenaResident) .
92    (lambda unrestricted others : (family ArenaResidents) .
93      (eliminate ArenaResidents (lambda unrestricted current : (family ArenaResidents) . Nat) others
94        (branch ArenaResidentsEnd . 1)
95        (branch ArenaResidentsNext head tail induction .
96          (naturalAnd (arenaDisjoint resident head) induction)))))
97
98-- 1 when the placement is certified, 0 otherwise.
99def arenaCertificate =
100  (lambda unrestricted arenaExtent : Nat .
101    (lambda unrestricted residents : (family ArenaResidents) .
102      (eliminate ArenaResidents (lambda unrestricted current : (family ArenaResidents) . Nat) residents
103        (branch ArenaResidentsEnd . 1)
104        (branch ArenaResidentsNext head tail induction .
105          (naturalAnd (arenaResidentValid arenaExtent head)
106            (naturalAnd (arenaDisjointFromAll head tail) induction))))))
107
108-- ---- the schedule over the arena ----
109-- What the certificate sees of a host's schedule over its host-visible
110-- arena: the host writes a range, reads a range, awaits a submission by its
111-- generation (the submissions issued once it is written; the host goes on
112-- only when that one has completed), or observes an awaited submission (a
113-- timestamp of it).  The device's work is ordered with the host's by those
114-- waits alone, so the certificate decides that the order the host relies on
115-- is the order it has:
116--   * generations strictly increase, so every wait awaits work its own
117--     submit issued -- a completion of an earlier generation cannot satisfy
118--     it -- and the last is the plan's count: every submission awaited;
119--   * a host write is pending until a submission consumes it; a host write
120--     over a pending range would overwrite staging no submission has read,
121--     and none may be pending at the end;
122--   * a host read of a pending range would read back the host's own
123--     staging, not a submission's result;
124--   * an observation names an awaited generation.
125-- Ranges of no bytes touch nothing.
126
127def arenaRangesNone : (family ArenaRanges) = (constructor ArenaRanges ArenaRangesNone)
128
129-- 1 when [start, stop) meets a range of the list
130def arenaRangesMeet =
131  (lambda unrestricted start : Nat .
132    (lambda unrestricted stop : Nat .
133      (lambda unrestricted ranges : (family ArenaRanges) .
134        (eliminate ArenaRanges (lambda unrestricted current : (family ArenaRanges) . Nat) ranges
135          (branch ArenaRangesNone . 0)
136          (branch ArenaRangesNext otherStart otherStop tail induction .
137            (naturalOr (naturalAnd (naturalLess start otherStop) (naturalLess otherStart stop)) induction))))))
138
139def arenaRangesEmpty =
140  (lambda unrestricted ranges : (family ArenaRanges) .
141    (eliminate ArenaRanges (lambda unrestricted current : (family ArenaRanges) . Nat) ranges
142      (branch ArenaRangesNone . 1)
143      (branch ArenaRangesNext start stop tail induction . 0)))
144
145-- The first event that breaks the order, counted from 1 (one past the last
146-- when the end does: a submission never awaited, or a write never
147-- consumed), or 0 when none does.  The walk carries the first hazard found
148-- and makes one recursive call per event (a choice between two
149-- continuations would be evaluated on both sides by the build's evaluator).
150def arenaScheduleHazard =
151  (lambda unrestricted count : Nat .
152    (lambda unrestricted events : (family ArenaEvents) .
153      (app (app (app (app
154        (eliminate ArenaEvents
155          (lambda unrestricted current : (family ArenaEvents) .
156            (pi unrestricted index : Nat . (pi unrestricted last : Nat . (pi unrestricted pending : (family ArenaRanges) . (pi unrestricted hazard : Nat . Nat)))))
157          events
158          (branch ArenaEventsEnd .
159            (lambda unrestricted index : Nat . (lambda unrestricted last : Nat . (lambda unrestricted pending : (family ArenaRanges) . (lambda unrestricted hazard : Nat .
160              (naturalSelect hazard hazard
161                (naturalSelect (naturalAnd (naturalEqual last count) (arenaRangesEmpty pending)) 0 index)))))))
162          (branch ArenaEventsNext event rest induction .
163            (lambda unrestricted index : Nat . (lambda unrestricted last : Nat . (lambda unrestricted pending : (family ArenaRanges) . (lambda unrestricted hazard : Nat .
164              (let unrestricted found = (lambda unrestricted failed : Nat . (naturalSelect hazard hazard (naturalSelect failed index 0)))
165                in (eliminate ArenaEvent (lambda unrestricted current : (family ArenaEvent) . Nat) event
166                  (branch ArenaHostWrite offset extent .
167                    (let unrestricted meets = (naturalAnd (naturalNonzero extent) (arenaRangesMeet offset (naturalAdd offset extent) pending))
168                      in (induction (succ index) last
169                           (nat-eliminate (lambda unrestricted current : Nat . (family ArenaRanges))
170                             pending
171                             (lambda unrestricted predecessor : Nat . (lambda unrestricted unused : (family ArenaRanges) .
172                               (constructor ArenaRanges ArenaRangesNext offset (naturalAdd offset extent) pending)))
173                             (naturalAnd (naturalNonzero extent) (naturalIsZero meets)))
174                           (found meets))))
175                  (branch ArenaHostRead offset extent .
176                    (induction (succ index) last pending
177                      (found (naturalAnd (naturalNonzero extent) (arenaRangesMeet offset (naturalAdd offset extent) pending)))))
178                  (branch ArenaAwait generation .
179                    (let unrestricted fresh = (naturalLess last generation)
180                      in (induction (succ index) (naturalSelect fresh generation last)
181                           (nat-eliminate (lambda unrestricted current : Nat . (family ArenaRanges))
182                             pending
183                             (lambda unrestricted predecessor : Nat . (lambda unrestricted unused : (family ArenaRanges) . arenaRangesNone))
184                             fresh)
185                           (found (naturalIsZero fresh)))))
186                  (branch ArenaObserve generation .
187                    (induction (succ index) last pending
188                      (found (naturalIsZero (naturalAnd (naturalNonzero generation) (naturalLessOrEqual generation last))))))))))))))
189        1) 0) arenaRangesNone) 0)))
190
191-- 1 when the schedule keeps the order, 0 otherwise.
192def arenaScheduleCertificate =
193  (lambda unrestricted count : Nat .
194    (lambda unrestricted events : (family ArenaEvents) .
195      (naturalIsZero (arenaScheduleHazard count events))))