swung0x48/MobileGL
1
0
Fork 0
mirror of https://github.com/MobileGL-Dev/MobileGL synced 2026-11-07 01:53:24 +09:00
Code Issues Packages Projects Releases Wiki Activity

[Docs] (Disaggregated): P5e ID-120 - contract amendment 8's sticky-forward clause is marked UNLANDED

Browse Source 
- CONTRACT-P5E section 8 item 8 says GetBufferBindingPointCount's sticky forward becomes FATAL
  under split. It is not in the code and must not be put there this phase: FieldOwnership.def:147
  (field row) and :179 (forward row) both say BARRIER_PULLED, and the generator refuses a
  field/forward pair that disagrees - pinned by
  FieldOwnershipTest.TheSevenStickyForwardsAgreeWithTheirFieldRows.
- Landing it as written would either trip the generator or drag the FIELD row to FATAL with it,
  and that second reading moves 23 pairs of the derived admitted set: the row's retiring phase is
  "P7/P13", which is exactly what admits it on every stamped verb under ID-125, and a FATAL row is
  admitted nowhere - so 23 reads this phase never promised to migrate would start aborting.
- MEASURED, NOT INHERITED: ID-120 said 10 pairs; that count predates ID-125's retiring-phase
  disjunct. `--print-admitted | grep -c '^GetBufferBindingPointCount@'` says 23 on this head, and
  the note records the command as well as the number.
- Annotated in place, struck through with the phase that lands it (P7/P13), for ID-105's reason:
  a contract clause that is arithmetically impossible against the code is a clause that changes,
  and the divergence is better stated than discovered from a red gate two phases from now.
This commit is contained in:
swung0x48
2026-09-18 12:33:04 -04:00
parent 664cbf3ef8
commit e5b74028b5
1 changed files with 23 additions and 3 deletions
Download Patch File Download Diff File Expand all files Collapse all files
MobileGL/MG_Remote/CONTRACT-P5E.md
+23 -3
View File
@@ -539,9 +539,29 @@ both backends.
re-derived as `MGPipeBarriered`. 7. **§3.3's state note** is retired by fb (§5.4).
8. **`FieldOwnership.def`**: `GetBoundVertexArray`, `GetTextureUnitObject`, `GetImageTextureBinding`,
`GetFramebufferBindingSlot`, `GetProgramForDraw/Dispatch`, `GetBufferBindingPoint` gain retiring
phase "P5e (Espryt unbarriered), P7 (Magma)"; `GetBufferBindingPointCount`'s forward → FATAL under
split; `GetTransformFeedbackProgram`, `GetProgramObject`, `GetTextureObject`, `ValidateProgramName`,
`HasOpenTransformFeedbackSpan`, `RecordError` keep their rows (barriered-only readers).
phase "P5e (Espryt unbarriered), P7 (Magma)"; ~~`GetBufferBindingPointCount`'s forward → FATAL under
split~~ (**UNLANDED — see below**); `GetTransformFeedbackProgram`, `GetProgramObject`,
`GetTextureObject`, `ValidateProgramName`, `HasOpenTransformFeedbackSpan`, `RecordError` keep
their rows (barriered-only readers).
> **UNLANDED, and deliberately so (P5e gl, ruling ID-120). Lands with P7/P13.** The clause
> "`GetBufferBindingPointCount`'s forward → FATAL under split" is NOT in the code and must not
> be put there this phase. `FieldOwnership.def:147` (the field row) and `:179` (the forward row)
> both say `BARRIER_PULLED`, and the generator refuses a field/forward pair that disagrees —
> pinned by `FieldOwnershipTest.TheSevenStickyForwardsAgreeWithTheirFieldRows`. So landing the
> clause as written would either trip the generator or drag the FIELD row to FATAL with it, and
> that second reading changes **23 pairs** of the derived admitted set (§7, measured with
> `--print-admitted | grep -c '^GetBufferBindingPointCount@'`; ID-120 said 10, which was
> counted before ID-125's retiring-phase disjunct widened the set). The row's retiring phase is
> "P7/P13", which is exactly what admits it on every stamped verb today; a FATAL row is
> admitted nowhere, so those reads would start aborting on a migration this phase never
> promised.
>
> The divergence is STATED HERE rather than discovered from a red gate, for ID-105's reason:
> when a contract clause is arithmetically impossible against the code, the contract is what
> changes. The phase that retires the buffer-binding-point family (P7 for the Magma half, P13
> for the transfer half) lands the field row and its forward TOGETHER, in one commit, and
> deletes this note.
9. **Table 1** gains `set_program_bindings` (80), appended; `set_shader_buffers` (38) gains its
route, sink and emitter (`PipeCatalogueTest.cpp:170-171, 242-243` invert). **Table 0** gains §1's
thirteen rows. **Table 3** gains `IpcTable::RunAhead/PresentCredit`.