Runtime.DeviceArenaCertificate

THE DEVICE SIDE OF AN ARENA: which ranges a whole program's launches read and write, decided on the launch schedule itself. A plan names every tensor it places. Some live for the whole program (the globals: parameter banks, the residual stream); the rest belong to phases. Each launch carries its phase in its source identity (the backend never reads that field), and each phase declares its planes: fresh ones (written in the phase before they are read) and carried ones (holding a value an earlier phase left). Planes of different phases may share bytes -- that is how a workspace is reused -- and the certificate decides that the sharing is sound: (A) the globals are aligned, non-empty and pairwise disjoint; (B) each phase's planes are aligned, non-empty, pairwise disjoint and disjoint from the globals: two tensors live in one phase never share a byte; (C) every parameter word of every launch that lies in one of the plan's address windows lies in a plane of the launch's phase or in a global: no launch reaches memory its phase did not name. A repeat is not unrolled: each launch of its body stands for all its iterations, each word with intervals covering its values over them (the iteration's deltas, or its table frames, applied to the ordinals the launch stands for: an interval per iteration while they are few and one delta names the word, their hull otherwise); a word each of whose intervals lies in one named range lies in a named range at every iteration; (D) in the order the launches run -- the submission schedule's references, in order, each a range of the launch table -- a carried plane was declared, in the same place, by an earlier phase instance (a maximal run of executed launches of one phase), and no instance since declared a different plane over any of its bytes: no value is overwritten while a later phase still needs it. What it trusts is each phase's fresh/carried split; everything else is derived from the schedule. The verdict is 0 when certified; 1 when (A) or (B) fails; 2 + i when the i-th launch as written (counted from 0, a repeat's body once) breaks (C) -- a word in no named range, or a launch of no declared phase; 2 + n + k (n the launches as written) when the k-th executed instance breaks (D).

52field unrestricted deviceArenaPhaseFresh : (family ArenaResidents)