mirror of https://github.com/MobileGL-Dev/MobileGL synced 2026-11-07 18:13:23 +09:00

Files

T

swung0x48 aba329cc53 [Docs] (Disaggregated): P6's plan and contract draft; the working notes move from a local directory into the repository

Two things land together: the plan and contract draft P6 needs before it starts, and the
working notes that until now existed on exactly one machine.

1. P6's plan and contract draft (neither started; not one line of code)

docs/Disaggregated/P6-SPAWN-PLAN.md the package plan
docs/Disaggregated/P6-CONTRACT-DRAFT.md the contract draft (moves to
MG_Remote/CONTRACT-P6.md when c6 lands)

The three findings that mattered, all written into the documents:

a. P6 is SMALLER than its roadmap cell suggests. The transport primitives are already in
the tree and already tested: SocketDoorbell including hangup detection and the two
lost-wakeup fences (Doorbell.cpp:211-360, four cases in FdPassingTest), SCM_RIGHTS fd
passing, ShmSegment::Adopt, and the SurfaceOp / WindowKind schema already defined in
protocol.fbs. inproc uses a real second shm mapping rather than an alias, and
SessionRings.h:22-28 says that was done so today is not the first time it runs. P6 is
assembly plus a control plane plus a process, not "write a socket transport".

b. The evidence for "P6 is only a transport swap" has EXPIRED. It was bought by P5c, whose
audit found 59 direct memory accesses in a tree that already looked clean. P5e changed
the tree again. So the first package, a6, is a read-only audit that writes no code, and
every contract row that depends on it is marked PENDING a6 rather than decided in
advance.

c. P6 does not get a game running on the phone. ANativeWindow* is meaningless in the child,
and protocol.fbs:186-196's own comment says Android transfers the window out of band -
that band is P12. P6 lands pbuffer / surfaceless / offscreen, which is what HeadlessGL,
the split-equivalent lane and trace replay need, and which is exactly what P6's own exit
gate measures. A real window reaching the server is a named refusal. This gets its own
section because "P6 is done" would otherwise read as "the game runs now".

The contract adds rule G: a role may not name a process-local handle. It extends P5c's
rule E (a role may not name the other role's memory) from memory to identity - EGLDisplay /
EGLSurface / EGLContext / ANativeWindow* / fd number / pid / mapped address either cross as
a token this contract defines or they do not cross, and a descriptor crosses only through
SCM_RIGHTS, where the kernel renumbers it.

What P5e left for P6 gets its own section. The latch semantics are already designed
(ARCHITECTURE.md:504) and are copied unchanged. What is new is that after run-ahead the
client no longer waits while the peer process can DIE: the client holds records that were
published and will never be applied, and Android's freezer suspends the child without
closing anything. So slow and dead must be distinguishable WITHOUT a timeout threshold.
That is P6's only new design; everything else is carriage. It shares a predicate with E1's
outstanding re-specification (ID-122), and the two should be designed together.

Two gates carried over from P5e's lessons: G2 requires integration-spawn's test-name set to
match integration-split's name for name, because a differing set means the lane is quietly
running less; and the arm-proof gate requires every entry to record the child pid and
transport=spawn in its OWN private log - ID-124 established that this kind of false green
really happens, and a spawn lane that actually ran monolith would pass every other gate.
S2's shape must be settled before it is written, and the document says why: E1 is the
cautionary case.

2. The working notes move into the repository (docs/Disaggregated/notes/, 415 .md files)

ROADMAP / CURRENT_STAGE_PROGRESS / MEASUREMENTS cite ruling numbers, audit line numbers and
the provenance of gate figures from ~/w7/notes/, a directory that exists on one machine and
is under no version control. A record cited hundreds of times that lives only locally is not
a record, so it moves in whole, with its directory structure intact.

Only .md moves. Scripts, run logs, census and gate result JSON, patches, APKs and nm dumps
stay where they are: they are evidence DATA rather than documents - large, regenerated per
run, and mostly carrying absolute paths and device serials that mean something only on the
machine that produced them. The mapping and this split are written in
docs/Disaggregated/notes/README.md.

Two exceptions are recorded there too: P6's BRIEF has been promoted to a first-class
document and keeps no copy under notes/, so the two cannot drift apart; and recovered/ holds
material salvaged from failed workflow runs, which may duplicate the like-named phase
directories and is kept because a few of those were the only complete version at the time.

CI's citation lint takes docs/Disaggregated/*.md only (non-recursive), and notes/ is
deliberately outside it: those notes' file:line citations were written against their own
code heads, and resolving them against today's HEAD would fail wholesale - which is not an
error, it is their correct state as a historical record. To check one, use the revision it
declares (--rev).

3. Inconsistencies fixed in passing

- README.md's status line still said P5e was in progress while the stage table already said
closed.
- CURRENT_STAGE_PROGRESS's next-step item 1 still listed the exit gate as pending, though
(a) and (b) were run in the previous commit; rewritten to closed plus the one item that
actually remains (E1).
- ROADMAP's P6 row still had the pre-phase plan in three of its cells; it now carries the
package order, the scope boundary and the two new gates.

Checked with check_doc_citations.py: 125 citations across docs/Disaggregated/*.md, 0 problems.

2026-09-18 23:31:39 -04:00

20 KiB

Raw Blame History

gl-v1 — the gate mechanism, and two latent crashes

Branch p5e/gl, base 7c6f6886, head e5b74028. Ten commits; all eight brief items landed, plus ID-125 and ID-128 which arrived mid-task.

#	item	commit
1	barriered stamp asks the server's capability (ID-111)	`8df7861f`
2	compile-time trip wire on the residual fill (ID-112)	`f94752c0`
3	admission predicate, generated (ID-116)	`a211756a`
—	retiring-phase disjunct (ID-125)	`faf19a6a`
—	escalation disjunct (ID-128)	`a0836568`
4	strict knob becomes admission-aware (ID-117)	`4f492edb`
5	`ResourceCopyRegion` becomes barriered (ID-118)	`a6ddeb08`
6	lane reads every log, counts, positive control (ID-119/115)	`bc6e24ff`
7	Magma's entries get their own lane	`664cbf3e`
8	amendment 8 marked UNLANDED (ID-120)	`e5b74028`

Gate

step	result	delta and why
`build`	rc=0
`unit`	2254/2254	+4 split-only cases (one per red-once: ID-111, ID-116, ID-117, ID-128). One rename, no deletions.
`isplit`	117/117	+3 for the new `TriangleScenario` case (plain split, `SmallRing`, and its own `StrictArming` block); −2 for the DirectVulkan `NamedBlit` pair moving to `integration-magma-split`.
`gpu`	1299/1299	+5: the same case is discovered by five gpu-labelled blocks and skips loudly in four.
`strict`	49/117, 68 abort	was 7/116. The 68 are exactly `pa`'s and `mv`'s rows — table below.
`integration-magma-split`	0/2 under strict, 2/2 without	the expected-red step, asserted red and asserted on its marker.
`gens`	all rc=0	incl. `--check` and `--self-test` (18 negative + 13 derivation controls). The one `check_doc_citations` line (`CONTRACT-P5.md:524`) is pre-existing in a file I did not touch.
`flavours`	rc=1, not mine	breaks in `DirectGLES/DirectGLES.cpp:5575,6716` and `Managers.cpp:9081,9344` on `keysMatch`, `ComputeShaderStorageBlockBindingSignatureOf`, `StagedTextureTargetForPipeTarget`. My diff contains no DirectGLES file; `git log -S` puts those symbols in `49aab57f` / `72e79020`, both ancestors of my base. ID-124's finding, unchanged.

The marker table (this head — base `7c6f6886`, so before `pa` and `mv`)

Two independent instruments agreeing exactly: my in-lane split_log_paths.py markers (reads the entries' own private logs) and the integrator's strict_census3.py (re-runs each entry under its own command and environment). 113 of 113 log-declaring entries read; 117 lane entries.

Fatal{ — must be only what pa and mv owe. It is: GetProgramForDraw@DrawArrays 52 (pa), GetBoundVertexArray@DrawArrays 9 (mv), GetProgramForDispatch@DispatchCompute 7 (pa). Nothing else. GetFramebufferBindingSlot@Clear (Magma, 2) has left this table — item 7.

Admitted{, by the generated table:

pair	entries	admitted by
`GetBufferBindingSlot@ReadPixels`	29	disjunct 2 (P8/P9/P13)
`GetFramebufferBindingSlot@ReadPixels`	29	disjunct 1 (`read_pixels` is `kWaitReply`)
`GetTransformFeedbackProgram@DrawArrays`	11	disjunct 2 (P3b/P4b), also 3
`GetTextureObject@CopyImageSubData`	6	disjuncts 1 and 2, independently
`GetProgramObject@ShaderStorageBlockBinding`	2	disjunct 2 (P9)
`GetTextureUnitObject@CopyTexImage2D`	2	disjunct 1 (`kWaitApplied`)
`ValidateProgramName@ShaderStorageBlockBinding`	2	disjuncts 1 and 2

ADMITTED-ESCALATED (disjunct 3 only): GetProgramForDraw@DrawArrays 13, GetBufferBindingPoint@DrawArrays 11, GetBoundVertexArray@DrawArrays 2.

The first is not a contradiction with the Fatal table: the same pair is Fatal in 52 entries and admitted in 13. The 13 are draws the client is parked behind because the payload escalated them (open XFB span, or client arrays); the 52 are ordinary draws. That is exactly the distinction ID-128 exists to draw, and no table indexed by (field, verb) could have drawn it.

Reconciling with ID-128's census of the merged tree

ID-128 measured 180 entries at 3c13fa4b; I measure 117 at 7c6f6886. Differences, all accounted for, none of them a rule I bent:

pa/mv are not in my base, so their three Fatal rows are still here.
GetFramebufferBindingSlot@Clear is absent from my Espryt table by item 7, not by admission (0/2 red in integration-magma-split with its marker asserted).
GetBufferBindingSlot@ReadPixels, GetProgramObject@ShaderStorageBlockBinding and GetBufferBindingPoint@DrawArrays appear in mine and not in ID-128's table. I believe this is instrument, not disagreement — both of mine record every marker per entry, a first-fault census records one — but I cannot check that from here. Flagging rather than assuming.

Item by item

1 · ID-111 (PipeApplier.h/.cpp). The stamp is now MGPipeApplierStampsBarriered(waitRuleLanded, serverPublishesRunAhead, wireSaysBarriered), a pure function; both predicates still computed unconditionally, as arguments rather than short-circuit arms (ID-103 extended to the capability probe). ServerPublishesRunAhead promoted out of the anonymous namespace, body unchanged, so the red-once can say "this session lacks bit 10" in its own words (ID-102). It is a pure function because the brief's red-once needs it to be: kMGPipeP5eClientWaitRuleLanded is false today, so a case that only drove ApplyOne would pass with or without the conjunct — and keep passing until the integration commit, at which point Magma SIGSEGVs with the lane green. So the case drives a real DrawVbo through ApplyOne on a SetCapabilityBits(0) session and asserts the stamp at the post-flip value of the constant. Red-once, deleting serverPublishesRunAhead &&: ../MobileGL/MG_Test/Wire/RemoteClientControls.inc:143: Failure / Expected: true / exited 124.

2 · ID-112 (PipeFill.cpp, +45 lines after the existing assertion; I did not touch EmittedCallSuppliesTheWholeField itself). The old assertion is keyed on the emitter's subsystem, so it covered five of seven; GetBoundVertexArray and GetBufferBindingPoint are outside kMGPipeP4aFamilySubsystems. All seven are now named in one list with their own assertion, a size assertion, and a comment saying where a fired assertion sends you (P7/P8, not this table). Red-once, deleting the GetBoundVertexArray case: PipeFill.cpp:2720:23: error: static assertion failed due to requirement 'NoPointerBackedRowIsWhollySupplied()': a pointer-backed residual row stopped being pulled (ID-112). The pre-existing NoP4aFamilyFieldIsWhollySupplied stayed silent on that same edit — the gap ID-112 names, now measured.

3 · ID-116 (generator +394, .inc +126, test.yml hand-kept 13 rows deleted, one unit case + skip twin). The generator reads kMGPipeWaitClasses, kMGPipeVerbClass and kMGPipeClassFieldMask and emits kMGPipeAdmittedPullMask + MGPipeBarrierPullAdmitted, with a static_assert that every admitted bit is a BARRIER-PULLED field of its verb's class; --print-admitted hands CI the same table. Final rule after ID-125/128: BARRIER_PULLED ∧ the verb has a stamp row ∧ in the class mask ∧ (statically barriered ∨ retiring phase ≠ P5e ∨ escalated at runtime). Static part: 174 pairs across 23 stamped verbs. Three new negative controls (each source renamed away must stop the script — a missing source yields a silently empty allowlist, which reads as rigour and is blindness) and nine derivation controls. Red-once, dropping the wait-class conjunct: self-test: 3 admission-derivation control(s) did not hold: unbarriering ReadPixels' op removes every @ReadPixels pair; … plus the unit case's GetBoundVertexArray@DrawArrays is admitted on a verb no barriered op stamps.

ID-125. Implemented as ruled; the phase column is matched as a token (\bP\d+[a-z]*\b), not a substring, so a P5 or a future P5e2 cannot answer for P5e. 111 → 174 pairs. All six survivors and all three rejections verified (§Rulings for the sixth). One consequence you should know: not one of the seven sticky forwards names P5e (P7, P7/P9, P7/P13, P9), so after ID-125 no sticky forward can produce a Fatal{ on a stamped verb — they are all admitted. StrictErrorsAlsoPromotesTheStickyForwards therefore stopped going red. That is the "check, do not assume" instruction in item 4 paying off. I renamed it StrictErrorsReachTheStickyForwardsAndNameThemByField and restated it around the claim that still has teeth — the detector reaches them (asserted by rsp moving and by the marker naming field and phase), so "did not abort" cannot pass for "never detected". The Fatal half keeps its own case next door on GetBoundVertexArray, a P5e row; StrictErrorsTurnsABarrierPulledReadIntoANamedAbort still goes red, unchanged.

ID-128. PipeApply.h/.cpp gain MGPipeApplierCurrentRecordIsBarrieredByEscalation() and its setter — a second thread_local defaulting false, the answer that admits nothing; ApplyOne stamps it as wireSaysBarriered && MGPipeWaitClassFor(op) == kWaitNone; the strict arm reads it as disjunct 3. The marker says which disjunct (ADMITTED vs ADMITTED-ESCALATED), in the slot the grammar already had for the reason, so Fatal{UnmigratedPipeInput filters are untouched. That is what keeps the lane exact: an ADMITTED pair is checked against --print-admitted, an escalated one is not — it is a runtime fact about the payload, and widening the static list to hold it would forgive the ordinary draw path too. Red-once, dropping && !escalated: FieldOwnershipTest.cpp:938: Failure / Actual: false / signal 6 with Fatal{UnmigratedPipeInput, "GetBoundVertexArray@DrawArrays"} [BARRIER-PULLED, MOBILEGL_IPC_STRICT_ERRORS=1, retires in P5e (Espryt unbarriered), P7 (Magma)]. Its control is StrictErrorsTurnsABarrierPulledReadIntoANamedAbort, the identical pull with the flag at default.

4 · ID-117 (PipeInputs.cpp). Third state exactly as sketched, both existing arms untouched; AdmittedBarrierPullOnce deduped per (field, verb) in a static bitset — plain, not atomic, for the file's existing reason (reachable only on the apply thread; g_residualPulls beside it is a plain Uint64). Red-once, making the strict arm unconditional again: FieldOwnershipTest.cpp:867: Failure / Actual: false / signal 6.

5 · ID-118. PipeCalls.def: kWaitNone → kWaitApplied. Chosen because the row posts no reply slot (so there is nothing to wait for but the apply, and gen_pipe.py refuses a kWaitReply row without a slot); because copy_framebuffer_to_texture — same kBlitOrCopy class — already carries that wait; and because glCopyImageSubData is zero per frame in the measured scene. PipeCatalogueTest's census moves in the same commit (9 → 10 applied, offset 24 → 25). Red-once, reverting the row: the allowlist loses @CopyImageSubData and PipeCatalogueTest goes red on three counts. After ID-125 the pair is admitted by disjunct 2 as well, so the allowlist alone no longer sees the revert — I restated the unit assertion to check the wait class itself beside the admission. Both disjuncts hold independently, as ID-128 asked me to confirm.

6 · ID-119 / ID-115. (a) split_log_paths.py gains marker_log_paths() and a markers mode driven from ctest's own map: 113 of 113 log-declaring entries read, against 90 for the old split-logs/ grep — the missing 26 were the F1. block, both NamedBlit pairs, the four Ct. entries and PersistentMapArm, i.e. the readback population the allowlist is about. The CI step resets those logs first (a stale file reads as this run's evidence) and runs the census in both arms. The two-sided ratchet is markers + Harness/strict-expected-markers.txt: unadmitted marker fails; ADMITTED outside --print-admitted fails; a pair not in the expected set fails; and an expected pair that no longer appears fails, so the lane cannot rot green. (b) The old rsp check grepped for a counter no entry in that directory emits, testing a sentence true of every possible implementation (the unbarriered arm is [[noreturn]] and runs before ++g_residualPulls). Replaced by an assertion where the counter is: DirectGLES.Split.StrictArming. (MOBILEGL_PIPE_STATS=1, PERIOD=1, own log path, RESOURCE_LOCK), asserting rsp == 0 || rsp >= draws — the device evidence's shape. Measured window: draws=1 … rsp=3 vbs=3. (c) New push-only counter vbs (ServerVerbBoundaries) at MGPipeServerStampVerbBoundary behind Enabled(); the same entry asserts vbs > 0. Deliberately not rsp: rsp reaches zero when the phase succeeds, so a control built on it would fail on the day the debt is paid. The entry skips loudly in the monolith arms and in any lane that is not the counting one (MGITEST_STRICT_ARMING_LANE=1); without that second guard it is discovered by TriangleScenario.* in three other blocks and asserts on a summary line nobody enabled. The CI step also fails if the arming entry did not run — a positive control that can be skipped away is not one.

7 · Magma's lane. Why the split and not admitting the row: FieldOwnership.def carries one retiring-phase string for both backends, so any rule admitting GetFramebufferBindingSlot@Clear for Magma admits it for Espryt, where it is this phase's debt — turning exactly the regression fb's handle arm prevents into a warning line. The split costs two entries; the admission costs the gate. A per-backend phase column is a FieldOwnership.def schema change, far outside this package. Finding: ctest -L takes a regex, so -L integration-split matches a label spelled integration-split-magma. I built the briefed spelling first and measured it — ctest -N -L integration-split still listed both DirectVulkan entries, i.e. the split looked done in every listing and had not happened. The label is integration-magma-split, which no existing -L matches. The step asserts red and the named marker, so "expected red" cannot decay into "did not run".

8 · ID-120. Struck through in place with a blockquote naming P7/P13 and the argument; code untouched. Measured, not inherited: ID-120 says 10 pairs would change; on this head it is 23 (--print-admitted | grep -c '^GetBufferBindingPointCount@'). The 10 predates ID-125's widening; the note records the command as well as the number.

G1 / monolith impact

vbs and its line are inside #if MOBILEGL_PIPE_PUSH; PipeInputs.cpp and PipeApply.cpp are compiled only under MOBILEGL_PIPE_PUSH (the header gains declarations only, which emit no symbol); PipeFieldOwnership.inc is included only from PipeInputs.h, which its banner keeps out of the pull build's include closure, and nothing there odr-uses the new table; PipeFill.cpp's trip wire is constexpr + static_assert. The one shared-code delta is PipeCalls.def's wait class, and that column is read only on a server publishing kCapRunAheadApply — inert until the integration commit. The flavours step could not serve as the empirical G1 check because it is already red at my base (above), so this argument is by construction rather than by build.

G2/G14: the one new non-fork unit case has its skip twin beside the other seven; the new integration case skips loudly in the monolith arms with its reason recorded; the Wire/ suite is registered only under MOBILEGL_BUILD_DISAGGREGATED, so its case needs none.

Kimi audit rows: not applicable — I migrate no field family and retired no apply-thread read of client memory. Every row I touched is left barriered; that is the whole of items 3-5.

Seams, assumptions, rulings I need

The expected-marker file must be refreshed by the wave-3 integration commit. It carries three ADMITTED-ESCALATED rows that pa/mv may retire; the ratchet will name them. That failure is the ratchet working, not breaking.
MG_IntegrationTest/CMakeLists.txt merge (per your note): my new block is at the very end of the file, after the NamedBlit loop, and is the only thing there; my other change in that file is inside the NamedBlit loop (the LABELS variable). pa's StrictProgramArm and mv's tiers are in the big disaggregated section above, so the three should not overlap.
test.yml: I rewrote the strict step's whole body from ready= down, and added one step before "Upload strict lane logs".
RULING WANTED — "a verb with no stamp row admits nothing". That restriction is mine, not ID-125's, and it is the difference between 174 and 491 pairs. The table is read only from CountBarrierPull, reachable only after MGPipeServerStampVerbBoundary, and the server stamps only MGP_VERB_OP_LIST's ops — so a bit for any other verb is an allowlist row nothing can exercise and nobody can retire. I believe it is right; please confirm.
RULING WANTED — the lane count. ID-128 defines done as 180/180. With item 7 the Espryt lane cannot hold the two Magma entries, so the merged number is 180 − 2 + 1 = 179 on integration-split plus 2 on integration-magma-split. I did not adjust the admission rule to reach 180; wanting 180 on one label means admitting GetFramebufferBindingSlot@Clear globally, which I have argued against in item 7.
I assumed pa does not touch EmittedCallSuppliesTheWholeField (ID-112 forbids it); if it did, item 2's assertion is what says so.
Housekeeping: the flavours step left a gitignored build-push/ in my tree. git status is clean. I ran the census to ~/w7/p5e-logs/strict-census-gl/ and strict-census3-gl/; the shared strict-census/ is untouched.

Is "the strict lane is hard green" now a statement a script can evaluate?

Yes — the mechanism is complete, and every part of it is exercised on this branch. One step now decides all five things the phrase has to mean: (1) every entry completed (ctest rc); (2) no Fatal{ marker anywhere in the lane — over the log set ctest itself declares, so the 26 entries the old check could not see are in it; (3) every Admitted{ marker is one the tables admit, compared against the same table the C++ answers from, so shell and runtime cannot drift; (4) no admitted pair appeared and none silently vanished — the two-sided ratchet; (5) strict was actually armed on something that draws — vbs > 0 on an inproc drawing entry, and the step fails if that entry did not run.

What is missing is not mechanism. It is two rows of debt and one flip:

On my head the script evaluates to RED, correctly, naming three rows in three lines: GetProgramForDraw@DrawArrays (52), GetBoundVertexArray@DrawArrays (9), GetProgramForDispatch@DispatchCompute (7) — pa's and mv's, both now merged upstream.
The post-flip arm has never executed. It is gated on kMGPipeP5eRunAheadReady, still false, so the no-fatal call is code no CI run has taken. I exercised it by hand; CI has not.
The expected-marker set is a measurement, and it is mine, not the merged tree's. The first integration run will fail the ratchet on the rows the merge retires. That is the design — but it means "hard green" is not evaluable by a fresh clone until that refresh lands.
One place I read a ruling as intent rather than text. ID-119 says rsp "must equal the admitted-marker tally". It cannot: markers are deduped per (field, verb) per process and rsp counts every pull, so count-equality is not a true statement about either number. I implemented the set equality (which pairs rsp counts — that is what the ratchet checks) and the shape (rsp == 0 || rsp >= draws). If you meant literal count equality, the dedupe has to go, and an 852-draw frame writes 852 lines.

20 KiB Raw Blame History Unescape Escape