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

[MG_Pipe, MG_Test, CI] (Disaggregated): P5e ID-116 - the section 7 allowlist is generated, not hand-kept

Browse Source 
- ra landed a hand-kept 13-row copy of CONTRACT-P5E section 7 in .github/workflows/test.yml, and
  it was wrong in BOTH directions at once: it omitted GetFramebufferBindingSlot@ReadPixels (21
  entries, the lane's largest survivor) and carried GetTextureObject@CopyImageSubData, which
  resource_copy_region's kWaitNone makes a genuine unbarriered read of client memory. Neither
  error is visible by reading the list. Both are obvious once the list is derived.
- gen_pipe_field_ownership.py now joins the three tables ID-84 already states the rule in -
  kMGPipeFieldOwnership, kMGPipeWaitClasses (generated/PipeWire.inc) and kMGPipeClassFieldMask /
  kMGPipeVerbClass (generated/PipeFillPoints.inc) - and emits kMGPipeAdmittedPullMask plus
  MGPipeBarrierPullAdmitted(field, verb): 101 admitted pairs across 12 barriered verbs.
- The three inputs are READ, never restated, so the allowlist moves with the code: retiring a
  verb's wait class narrows it with no edit anywhere, and a new BARRIER_PULLED row widens it only
  on verbs that wait. A verb with no stamp row admits nothing - only MGP_VERB_OP_LIST's ops can
  ever be the record a pull is reported against.
- --print-admitted gives the CI shell the SAME table the C++ answers from, which is what makes
  the hand copy unnecessary rather than merely corrected.
- 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 five derivation
  controls that move an input and read the allowlist back.
- Red-once: dropping the wait-class conjunct from build_admitted fails the self-test by name -
  "3 admission-derivation control(s) did not hold: unbarriering ReadPixels' op removes every
  @ReadPixels pair; unbarriering ResourceCopyRegion removes every @CopyImageSubData pair; no pair
  is admitted on an unbarriered verb (DrawArrays)" - and the new unit case fails with
  "GetBoundVertexArray@DrawArrays is admitted on a verb no barriered op stamps".
This commit is contained in:
swung0x48
2026-09-18 11:54:28 -04:00
parent f94752c01b
commit a211756aec
4 changed files with 531 additions and 26 deletions
Download Patch File Download Diff File Expand all files Collapse all files
.github/workflows/test.yml
+18 -24
View File
@@ -1246,31 +1246,25 @@ jobs:
exit 1
fi
# THE ADMITTED MARKERS, `<field>@<verb>`, AND NOTHING ELSE. These are the barriered
# rows of §2.2 - the ones whose apply still pulls a row, and whose legality is the
# client's own wait (ruling 4). Each line names the package that retires it; a row
# that leaves this list leaves it by deletion, never by widening.
# readbacks / the pack PBO ......... P8/P9 (read_pixels, get_texture_image)
# CopyTex endpoint ................. tx2's trailing item
# GenerateMipmap ................... tx2, until the VerbMipRes arm lands
# set_storage_block_binding ........ pg's trailing item (by MGPStorageBlockBinding::ShaderCso)
# XFB ............................... P3b/P4b/P9 (escalation (i) keeps the span lockstep)
# resource_copy_region's names ..... the declared P5b debt
printf '%s\n' \
'GetTextureUnitObject@ReadPixels' \
'GetTextureUnitObject@GetTextureImage' \
'GetTextureUnitObject@CopyTexImage2D' \
'GetTextureUnitObject@GenerateMipmap' \
'GetBufferBindingSlot@ReadPixels' \
'GetBufferBindingSlot@GetTextureImage' \
'GetProgramObject@ShaderStorageBlockBinding' \
'ValidateProgramName@ShaderStorageBlockBinding' \
'GetTextureObject@CopyImageSubData' \
'GetTransformFeedbackProgram@BeginTransformFeedback' \
'GetTransformFeedbackProgram@EndTransformFeedback' \
'GetBufferBindingPoint@BeginTransformFeedback' \
'GetBufferBindingPoint@EndTransformFeedback' \
# THE ADMITTED MARKERS COME FROM THE GENERATOR, NOT FROM THIS FILE (ID-116).
#
# A hand-kept copy of §7 lived here for one round and was wrong in BOTH directions at
# once: it omitted GetFramebufferBindingSlot@ReadPixels - 21 entries, the largest
# survivor in the lane - and it carried GetTextureObject@CopyImageSubData, which
# nothing made safe, because resource_copy_region is kWaitNone. Neither error is
# visible by reading the list; both are obvious the moment the list is DERIVED.
#
# The rule is ID-84 said in tables that already exist: a <field>@<verb> pull is
# admitted iff the field's ownership row is BARRIER_PULLED, the verb's wire op is
# statically barriered (kMGPipeWaitClasses != kWaitNone, i.e. the client really is
# parked behind the record) and the field is inside the verb class's may-read mask.
# `--print-admitted` prints exactly the table MGPipeBarrierPullAdmitted() answers
# from, so this shell and the C++ cannot drift: retiring a verb's wait class narrows
# the lane with no edit here, and a new BARRIER_PULLED row widens it only on verbs
# that wait.
python3 "${GITHUB_WORKSPACE}/scripts/gen_pipe_field_ownership.py" --print-admitted \
> "${RUNNER_TEMP}/allowed.txt"
echo "§7 allowlist (derived): $(wc -l < "${RUNNER_TEMP}/allowed.txt") admitted pair(s)"
grep -rhoE '\[BARRIER-PULLED[^]]*\]' MobileGL/MG_IntegrationTest/split-logs/ 2>/dev/null > "${RUNNER_TEMP}/markers-raw.txt" || true
grep -rhoE 'Fatal\{UnmigratedPipeInput, "[^"]*"\}' MobileGL/MG_IntegrationTest/split-logs/ 2>/dev/null \
MobileGL/MG_Pipe/generated/PipeFieldOwnership.inc
+126
View File
@@ -300,6 +300,132 @@ constexpr MGPipeVerb MGPipeVerbForWireOp(MGPWireOp op) {
inline constexpr SizeT kMGPipeVerbBoundaryOpCount = 23;
inline constexpr SizeT kMGPipeVerbBoundaryExemptCount = 3;
// ---- THE §7 ALLOWLIST, DERIVED RATHER THAN WRITTEN (ID-116) --------------------------
//
// CONTRACT-P5E §7 lists the barrier-pulled reads the phase ADMITS: debts that are real, ordered
// and fresh because the client is parked behind the record, and that a LATER phase retires. It
// was also kept by hand in .github/workflows/test.yml, and that copy was wrong in both
// directions at once - it omitted GetFramebufferBindingSlot@ReadPixels, the largest survivor,
// and carried GetTextureObject@CopyImageSubData, which nothing made safe.
//
// THE RULE IS ID-84 SAID IN TABLES THAT ALREADY EXIST. A <field>@<verb> pull is admitted iff
//
// 1. the field's ownership row is BARRIER-PULLED - it is a debt and not a defect;
// 2. the verb's wire op is STATICALLY BARRIERED (kMGPipeWaitClasses[op] != kWaitNone), which
// is exactly "the client is parked in its own wait for this record", so P5C's semantics
// survive the flip for it; and
// 3. the field is inside kMGPipeClassFieldMask[class of the verb] - a field outside the
// verb's own may-read table was never filled for it, so a read there is stale by
// construction whatever its ownership row says.
//
// Which makes the allowlist move with the code instead of beside it: retiring a verb's wait
// class NARROWS it with no edit, and a new BARRIER_PULLED row widens it only on verbs that
// wait. A verb with no stamp row admits nothing - the server stamps only MGP_VERB_OP_LIST's
// ops, so no other verb can be the one a residual pull is reported against.
inline constexpr MGPipeFieldMask kMGPipeAdmittedPullMask[kMGPipeVerbCount] = {
{{0x0000000000000000ull, 0x0000000000000000ull}}, // DrawArrays
{{0x0000000000000000ull, 0x0000000000000000ull}}, // DrawElements
{{0x0000000000000000ull, 0x0000000000000000ull}}, // DrawElementsBaseVertex
{{0x0000000000000000ull, 0x0000000000000000ull}}, // MultiDrawArrays
{{0x0000000000000000ull, 0x0000000000000000ull}}, // MultiDrawElements
{{0x0000000000000000ull, 0x0000000000000000ull}}, // MultiDrawElementsBaseVertex
{{0x0000000000000000ull, 0x0000000000000000ull}}, // MultiDrawElementsIndirect
{{0x0000000000000000ull, 0x0000000000000000ull}}, // MultiDrawArraysIndirect
{{0x0000000000000000ull, 0x0000000000000000ull}}, // MultiDrawElementsIndirectCount
{{0x0000000000000000ull, 0x0000000000000000ull}}, // MultiDrawArraysIndirectCount
{{0x0000000000000000ull, 0x0000000000000000ull}}, // DrawRangeElementsBaseVertex
{{0x0000000000000000ull, 0x0000000000000000ull}}, // DrawRangeElements
{{0x0000000000000000ull, 0x0000000000000000ull}}, // DrawElementsInstancedBaseVertexBaseInstance
{{0x0000000000000000ull, 0x0000000000000000ull}}, // DrawElementsInstancedBaseVertex
{{0x0000000000000000ull, 0x0000000000000000ull}}, // DrawElementsInstancedBaseInstance
{{0x0000000000000000ull, 0x0000000000000000ull}}, // DrawElementsInstanced
{{0x0000000000000000ull, 0x0000000000000000ull}}, // DrawArraysInstancedBaseInstance
{{0x0000000000000000ull, 0x0000000000000000ull}}, // DrawArraysInstanced
{{0x0000000000000000ull, 0x0000000000000000ull}}, // DrawElementsIndirect
{{0x0000000000000000ull, 0x0000000000000000ull}}, // DrawArraysIndirect
{{0x0000000000000000ull, 0x0000000000000000ull}}, // Clear
{{0x0000000000000000ull, 0x0000000000000000ull}}, // ClearBufferfi
{{0x0000000000000000ull, 0x0000000000000000ull}}, // ClearBufferfv
{{0x0000000000000000ull, 0x0000000000000000ull}}, // ClearBufferuiv
{{0x0000000000000000ull, 0x0000000000000000ull}}, // ClearBufferiv
{{0x0000000000000000ull, 0x0000000000000000ull}}, // ClearNamedFramebufferfv
{{0x0000000000000000ull, 0x0000000000000000ull}}, // ClearNamedFramebufferfi
{{0x0000000000000000ull, 0x0000000000000000ull}}, // ClearNamedFramebufferiv
{{0x0000000000000000ull, 0x0000000000000000ull}}, // ClearNamedFramebufferuiv
{{0x0000000000000000ull, 0x0000000000000000ull}}, // BlitFramebuffer
{{0x0000000000000000ull, 0x0000000000000000ull}}, // BlitNamedFramebuffer
{{0x5800c02000300180ull, 0x0000000000000000ull}}, // CopyTexImage2D
{{0x0000000000000000ull, 0x0000000000000000ull}}, // CopyTexSubImage2D
{{0x0000000000000000ull, 0x0000000000000000ull}}, // CopyImageSubData
{{0x5800c02000300180ull, 0x0000000000000000ull}}, // GenerateMipmap
{{0x5800c02000300140ull, 0x0000000000000000ull}}, // ReadPixels
{{0x0000000000000000ull, 0x0000000000000000ull}}, // GetTexImage
{{0x5800c02000300140ull, 0x0000000000000000ull}}, // GetTextureImage
{{0x0000000000000000ull, 0x0000000000000000ull}}, // DispatchCompute
{{0x0000000000000000ull, 0x0000000000000000ull}}, // DispatchComputeIndirect
{{0x0000000000000000ull, 0x0000000000000000ull}}, // MemoryBarrier
{{0x0000000000000000ull, 0x0000000000000000ull}}, // MemoryBarrierByRegion
{{0x0000000000000000ull, 0x0000000000000000ull}}, // BindImageTexture
{{0x0000000000000000ull, 0x0000000000000000ull}}, // GetIntegeri_v
{{0x5800c02000300100ull, 0x0000000000000000ull}}, // ShaderStorageBlockBinding
{{0x0000000000000000ull, 0x0000000000000000ull}}, // FenceSync
{{0x5800402000000100ull, 0x0000000000000000ull}}, // ClientWaitSync
{{0x0000000000000000ull, 0x0000000000000000ull}}, // WaitSync
{{0x0000000000000000ull, 0x0000000000000000ull}}, // DeleteSync
{{0x5800402000000100ull, 0x0000000000000000ull}}, // GetSyncStatus
{{0x0000000000000000ull, 0x0000000000000000ull}}, // IsTimerQuerySupported
{{0x0000000000000000ull, 0x0000000000000000ull}}, // BeginTimeElapsedQuery
{{0x0000000000000000ull, 0x0000000000000000ull}}, // EndTimeElapsedQuery
{{0x0000000000000000ull, 0x0000000000000000ull}}, // QueryCounterTimestamp
{{0x0000000000000000ull, 0x0000000000000000ull}}, // IsQueryResultAvailable
{{0x0000000000000000ull, 0x0000000000000000ull}}, // GetQueryResult64
{{0x0000000000000000ull, 0x0000000000000000ull}}, // DeleteBackendQuery
{{0x0000000000000000ull, 0x0000000000000000ull}}, // BeginOcclusionQuery
{{0x0000000000000000ull, 0x0000000000000000ull}}, // EndOcclusionQuery
{{0x0000000000000000ull, 0x0000000000000000ull}}, // BeginXfbPrimitivesQuery
{{0x0000000000000000ull, 0x0000000000000000ull}}, // EndXfbPrimitivesQuery
{{0x0000000000000000ull, 0x0000000000000000ull}}, // PatchParameteri
{{0x5808402000000180ull, 0x0000000000000000ull}}, // BeginTransformFeedback
{{0x5808402000000180ull, 0x0000000000000000ull}}, // EndTransformFeedback
{{0x5808402000000180ull, 0x0000000000000000ull}}, // PauseTransformFeedback
{{0x5808402000000180ull, 0x0000000000000000ull}}, // ResumeTransformFeedback
{{0x5808402000000180ull, 0x0000000000000000ull}}, // BindTransformFeedback
{{0x0000000000000000ull, 0x0000000000000000ull}}, // DeleteTransformFeedback
{{0x0000000000000000ull, 0x0000000000000000ull}}, // GetGpuTimestampNs
};
inline constexpr SizeT kMGPipeAdmittedPullPairCount = 101;
// THE PREDICATE THE STRICT KNOB ASKS (ID-117). A 69 x 128-bit table, so this costs a shift and
// a test on the apply thread - the same shape MGPipeFieldMaskHas already has.
constexpr Bool MGPipeBarrierPullAdmitted(MGPipeInputField field, MGPipeVerb verb) {
const SizeT index = static_cast<SizeT>(verb);
return index < kMGPipeVerbCount && MGPipeFieldMaskHas(kMGPipeAdmittedPullMask[index], field);
}
// THE HAND-EDIT CONTROL, MGPipeEveryFieldIsClassified's shape and for its reason: the generator
// cannot emit a bit that fails this, so it can only fire on an edited header - which is exactly
// the edit the DO NOT EDIT banner cannot prevent on its own. An admitted bit that was not a
// BARRIER-PULLED field of its verb's class would be the allowlist quietly forgiving a read that
// is torn rather than merely unmigrated.
constexpr Bool MGPipeEveryAdmittedPullIsADebtOfItsVerbsClass() {
for (SizeT v = 0; v < kMGPipeVerbCount; ++v) {
const MGPipeFieldMask& admitted = kMGPipeAdmittedPullMask[v];
const MGPipeFieldMask& mayRead =
kMGPipeClassFieldMask[static_cast<SizeT>(kMGPipeVerbClass[v])];
for (SizeT f = 0; f < kMGPipeInputFieldCount; ++f) {
const auto field = static_cast<MGPipeInputField>(f);
if (!MGPipeFieldMaskHas(admitted, field)) continue;
if (kMGPipeFieldOwnership[f] != MGPipeFieldOwnership::kBarrierPulled) return false;
if (!MGPipeFieldMaskHas(mayRead, field)) return false;
}
}
return true;
}
static_assert(MGPipeEveryAdmittedPullIsADebtOfItsVerbsClass(),
"an admitted barrier pull is not a BARRIER-PULLED field of its verb's class "
"(CONTRACT-P5E section 7, ID-84 / ID-116)");
// The class sizes, as constants a test can pin without recounting the table.
inline constexpr SizeT kMGPipeRecordSuppliedFieldCount = 41;
inline constexpr SizeT kMGPipeApplierDerivedFieldCount = 4;
MobileGL/MG_Test/Pipe/FieldOwnershipTest.cpp
+76
View File
@@ -166,6 +166,9 @@ TEST(FieldOwnershipTest, TheSevenStickyForwardsAgreeWithTheirFieldRows) {
TEST(FieldOwnershipTest, VerbBoundaryOpsCoverEveryVerbShapedCall) {
GTEST_SKIP() << "push not compiled in (MOBILEGL_PIPE_PUSH=OFF)";
}
TEST(FieldOwnershipTest, TheAdmittedPullTableIsID84sDerivationAndNotAList) {
GTEST_SKIP() << "push not compiled in (MOBILEGL_PIPE_PUSH=OFF)";
}
TEST(FieldOwnershipTest, TheResidualFillsSuppliedMemoReKeysOnEveryInputThatMovesAnAnswer) {
GTEST_SKIP() << "push not compiled in (MOBILEGL_PIPE_PUSH=OFF)";
}
@@ -385,6 +388,79 @@ TEST_F(FieldOwnershipTest, VerbBoundaryOpsCoverEveryVerbShapedCall) {
EXPECT_EQ(MGPipeVerbForWireOp(MGPWireOp::GetCaps), MGPipeVerb::kVerbCount);
}
// P5e (gl), ID-116: THE §7 ALLOWLIST IS A DERIVATION, AND THIS RESTATES ITS RULE INDEPENDENTLY.
//
// The generator emits kMGPipeAdmittedPullMask by joining three tables; the header carries a
// static_assert that every admitted bit is a BARRIER-PULLED field of its verb's class. What no
// static_assert in that header can check is the SECOND conjunct, because the wait column lives
// in another generated file: this case walks the stamp map itself and asserts that a verb with
// an admitted bit has an op the client actually waits behind. A derivation that dropped that
// term would still produce a plausible table - which is precisely how the hand-kept copy in
// test.yml came to admit GetTextureObject@CopyImageSubData, a read of client memory on a record
// nothing parks behind.
TEST_F(FieldOwnershipTest, TheAdmittedPullTableIsID84sDerivationAndNotAList) {
// The largest survivor of the lane, and the row the hand-kept copy omitted (21 entries).
EXPECT_TRUE(MGPipeBarrierPullAdmitted(MGPipeInputField::GetFramebufferBindingSlot,
MGPipeVerb::ReadPixels))
<< "read_pixels is kWaitReply and GetFramebufferBindingSlot is BARRIER-PULLED in the "
"kReadback mask, so ID-84 admits it; a lane that calls this red is red on a debt "
"that P7 owes, not on anything P5e broke";
// ... and the debt P5e exists to RETIRE is not forgiven: draw_vbo is kWaitNone, so the
// client is not parked behind the record and there is nothing for an allowlist to admit.
EXPECT_FALSE(MGPipeBarrierPullAdmitted(MGPipeInputField::GetProgramForDraw,
MGPipeVerb::DrawArrays))
<< "the draw path's pull became admitted - the allowlist is now forgiving the 61 lane "
"entries this phase is being run to fix";
EXPECT_FALSE(MGPipeBarrierPullAdmitted(MGPipeInputField::GetBoundVertexArray,
MGPipeVerb::DrawArrays));
// A field that is not a debt at all is never admitted, on any verb.
EXPECT_FALSE(MGPipeBarrierPullAdmitted(MGPipeInputField::GetRenderStateParameters,
MGPipeVerb::ReadPixels));
// An out-of-range verb answers false rather than reading off the end: CountBarrierPull is
// reached from a stamp, and a stamp is only as good as the op that produced it.
EXPECT_FALSE(MGPipeBarrierPullAdmitted(MGPipeInputField::GetFramebufferBindingSlot,
MGPipeVerb::kVerbCount));
// THE RULE, RESTATED OVER THE WHOLE TABLE. The stamp map is inverted here rather than
// assumed: only an op MGPipeVerbForWireOp names can ever be the record a pull is reported
// against, so a verb with no op admits nothing, and a verb whose every op is kWaitNone
// admits nothing either.
Bool waitedFor[kMGPipeVerbCount] = {};
for (SizeT op = 0; op < static_cast<SizeT>(MGPWireOp::kOpCount); ++op) {
const MGPipeVerb verb = MGPipeVerbForWireOp(static_cast<MGPWireOp>(op));
if (verb == MGPipeVerb::kVerbCount) continue;
if (MGPipeWaitClassFor(static_cast<MGPWireOp>(op)) != kWaitNone) {
waitedFor[static_cast<SizeT>(verb)] = true;
}
}
SizeT admitted = 0;
for (SizeT v = 0; v < kMGPipeVerbCount; ++v) {
const auto verb = static_cast<MGPipeVerb>(v);
for (SizeT f = 0; f < kMGPipeInputFieldCount; ++f) {
const auto field = static_cast<MGPipeInputField>(f);
if (!MGPipeBarrierPullAdmitted(field, verb)) continue;
++admitted;
EXPECT_TRUE(waitedFor[v])
<< kMGPipeInputFieldNames[f] << "@" << kMGPipeVerbNames[v]
<< " is admitted on a verb no barriered op stamps: after the flip that record's "
"read is torn by construction, and admitting it turns an unconditional Fatal "
"into a warning line";
EXPECT_EQ(kMGPipeFieldOwnership[f], MGPipeFieldOwnership::kBarrierPulled)
<< kMGPipeInputFieldNames[f] << " is admitted but is not a BARRIER-PULLED row";
EXPECT_TRUE(MGPipeFieldMaskHas(
kMGPipeClassFieldMask[static_cast<SizeT>(kMGPipeVerbClass[v])], field))
<< kMGPipeInputFieldNames[f] << "@" << kMGPipeVerbNames[v]
<< " is admitted but is outside the verb class's may-read mask, so the residual "
"fill never copied it for this verb";
}
}
EXPECT_EQ(admitted, kMGPipeAdmittedPullPairCount)
<< "the walk and the generator disagree about how many pairs are admitted";
EXPECT_GT(admitted, SizeT{0})
<< "the admitted set is EMPTY, which reads in the lane as rigour and is blindness: "
"every barriered readback row would be reported as a fresh defect";
}
// ---------------------------------------------------------------------------------------
// The behaviour: the table is load-bearing. Split builds only - it is the server verb stamp
// that arms all of it, and nothing in a monolith lane stamps.
scripts/gen_pipe_field_ownership.py
+311 -2
View File
@@ -42,6 +42,12 @@ OWNERSHIP_DEF = os.path.join(PIPE_DIR, "FieldOwnership.def")
PIPE_FILL = os.path.join(REPO_ROOT, "MobileGL", "MG_Impl", "Pipe", "PipeFill.cpp")
PIPE_CALLS = os.path.join(PIPE_DIR, "PipeCalls.def")
FILL_POINTS = os.path.join(PIPE_DIR, "FillPoints.def")
# P5e (gl, ID-116): the two generated tables the admission derivation joins. They are READ, not
# restated - the whole point of ID-116 is that the allowlist is derived from the tables that
# already exist, so that retiring a verb's wait class narrows it and adding a BARRIER_PULLED row
# widens it only on barriered verbs, with no third place to keep in step.
PIPE_WIRE_INC = os.path.join(GENERATED_DIR, "PipeWire.inc")
FILL_POINTS_INC = os.path.join(GENERATED_DIR, "PipeFillPoints.inc")
OUT_NAME = "PipeFieldOwnership.inc"
CLASSES = ("RECORD_SUPPLIED", "APPLIER_DERIVED", "BARRIER_PULLED", "FATAL")
@@ -206,6 +212,130 @@ def parse_ops_and_verbs(calls_text=None, fill_points_text=None):
return calls, [v for v, _ in verbs]
def array_block(text, declaration):
"""The braced initialiser of a generated `... <declaration> = {` table, comments KEPT.
The generated tables carry the row's name in a trailing comment (`// DrawArrays`) and in a
leading one (`/* 58 ReadPixels */`), and those comments are the only place the row's NAME
appears - the values themselves are enumerators and hex words. So this masker's opposite is
what is wanted here: the comments are the data."""
start = text.find(declaration)
if start < 0:
sys.exit("gen_pipe_field_ownership: %r is not in the generated table it should be in - "
"the admission derivation (ID-116) reads it rather than restating it, so a "
"renamed or moved table has to stop this script rather than produce an empty "
"allowlist" % declaration)
open_at = text.find("{", start)
depth = 0
i = open_at
while i < len(text):
if text[i] == "{":
depth += 1
elif text[i] == "}":
depth -= 1
if depth == 0:
return text[open_at + 1:i]
i += 1
sys.exit("gen_pipe_field_ownership: %r never closes its initialiser" % declaration)
WAIT_ROW_RE = re.compile(r"/\*\s*\d+\s+(\w+)\s*\*/\s*static_cast<Uint8>\(\s*(k\w+)\s*\)")
def parse_wait_classes(text=None):
"""{op name: wait class enumerator} out of generated/PipeWire.inc's kMGPipeWaitClasses.
This is the STATIC half of MGPipeBarriered - the same column the emit table and the sink
both compute from - and it is what decides whether a record is one the client is parked
behind. A pair may only be admitted on a verb whose op is in it and is not kWaitNone."""
text = read(PIPE_WIRE_INC) if text is None else text
block = array_block(text, "kMGPipeWaitClasses[static_cast<SizeT>(MGPWireOp::kOpCount)] =")
rows = WAIT_ROW_RE.findall(block)
if not rows:
sys.exit("gen_pipe_field_ownership: kMGPipeWaitClasses did not parse - with no wait "
"column every op would look unbarriered and the admitted set would be silently "
"empty, which reads as 'the lane is clean' (ID-116)")
waits = {}
for op, wait in rows:
waits[op] = wait
return waits
VERB_CLASS_ROW_RE = re.compile(r"MGPipeVerbClass::(\w+)\s*,\s*//\s*(\w+)")
CLASS_MASK_ROW_RE = re.compile(r"//\s*(k\w+):[^\n]*\n\s*\{\{\s*(0x[0-9a-fA-F]+)ull\s*,\s*"
r"(0x[0-9a-fA-F]+)ull\s*\}\}")
def parse_verb_classes(text=None):
"""({verb: class}, {class: (word0, word1)}) out of generated/PipeFillPoints.inc.
kMGPipeClassFieldMask is the verb's OWN may-read table: a field outside it is one the
client's residual fill never copied for that verb, so it can never be a legitimate read
there whatever its ownership row says. Intersecting with it is ID-84's third term."""
text = read(FILL_POINTS_INC) if text is None else text
verb_rows = VERB_CLASS_ROW_RE.findall(
array_block(text, "kMGPipeVerbClass[kMGPipeVerbCount] ="))
mask_rows = CLASS_MASK_ROW_RE.findall(
array_block(text, "kMGPipeClassFieldMask[kMGPipeVerbClassCount] ="))
if not verb_rows:
sys.exit("gen_pipe_field_ownership: kMGPipeVerbClass did not parse - the admitted set "
"would lose its class intersection (ID-116)")
if not mask_rows:
sys.exit("gen_pipe_field_ownership: kMGPipeClassFieldMask did not parse - the admitted "
"set would lose its class intersection (ID-116)")
verb_class = {}
for cls, verb in verb_rows:
verb_class[verb] = cls
class_mask = {}
for cls, low, high in mask_rows:
class_mask[cls] = (int(low, 16), int(high, 16))
for verb, cls in verb_class.items():
if cls not in class_mask:
sys.exit("gen_pipe_field_ownership: verb %s is in class %s, which has no field mask"
% (verb, cls))
return verb_class, class_mask
def build_admitted(accessors, ownership, verbs, verb_ops, waits, verb_class, class_mask):
"""ID-84 AS A DERIVATION, which is the whole of ID-116: a <field>@<verb> pull is ADMITTED
iff (1) the field's row is BARRIER_PULLED, (2) the verb's wire op is STATICALLY BARRIERED
(MGPipeWaitClassFor(op) != kWaitNone, so the client really is parked behind the record and
P5C's semantics hold), and (3) the field is inside kMGPipeClassFieldMask[class of verb].
A verb with no stamp row admits NOTHING, and that is not an omission: the server stamps only
the ops MGP_VERB_OP_LIST names, so no other verb can ever be the one CountBarrierPull is
told about. Answering "admitted" for a verb that cannot arrive would widen the allowlist
by a row nothing can exercise.
Returns (per-verb (word0, word1), the sorted <field>@<verb> pairs)."""
field_index = {name: i for i, name in enumerate(accessors)}
op_for_verb = {}
for op, verb in verb_ops:
op_for_verb[verb] = op
masks = []
pairs = []
for verb in verbs:
words = [0, 0]
op = op_for_verb.get(verb)
barriered = op is not None and waits.get(op) not in (None, "kWaitNone")
if barriered:
cls = verb_class.get(verb)
if cls is None:
sys.exit("gen_pipe_field_ownership: verb %s has a stamp row but no verb class"
% verb)
allowed = class_mask[cls]
for field, index in field_index.items():
if ownership[field] != "BARRIER_PULLED":
continue
if not ((allowed[index // 64] >> (index % 64)) & 1):
continue
words[index // 64] |= 1 << (index % 64)
pairs.append("%s@%s" % (field, verb))
masks.append((words[0], words[1]))
return masks, sorted(pairs)
def verb_shaped_calls(calls, verbs):
"""The calls that MUST have a stamp row or an exemption, by two derived tests: the
catalogue's own kind (kCtxVerb) and a name that is also a verb's. Neither can see a call
@@ -343,7 +473,7 @@ def build(accessors, sticky, emitted, refused, rows, forwards, args):
def emit(accessors, sticky, ownership, phase, why, forward_map, arg_rows, counts, verb_ops,
exemptMap):
exemptMap, verbs, admitted_masks, admitted_pairs):
out = [BANNER.format(name=OUT_NAME)]
add = out.append
add("""
@@ -472,6 +602,64 @@ static_assert(MGPipeEveryFieldIsClassified(),
add("inline constexpr SizeT kMGPipeVerbBoundaryOpCount = %d;" % len(verb_ops))
add("inline constexpr SizeT kMGPipeVerbBoundaryExemptCount = %d;" % len(exemptMap))
add("")
add("""// ---- THE §7 ALLOWLIST, DERIVED RATHER THAN WRITTEN (ID-116) --------------------------
//
// CONTRACT-P5E §7 lists the barrier-pulled reads the phase ADMITS: debts that are real, ordered
// and fresh because the client is parked behind the record, and that a LATER phase retires. It
// was also kept by hand in .github/workflows/test.yml, and that copy was wrong in both
// directions at once - it omitted GetFramebufferBindingSlot@ReadPixels, the largest survivor,
// and carried GetTextureObject@CopyImageSubData, which nothing made safe.
//
// THE RULE IS ID-84 SAID IN TABLES THAT ALREADY EXIST. A <field>@<verb> pull is admitted iff
//
// 1. the field's ownership row is BARRIER-PULLED - it is a debt and not a defect;
// 2. the verb's wire op is STATICALLY BARRIERED (kMGPipeWaitClasses[op] != kWaitNone), which
// is exactly "the client is parked in its own wait for this record", so P5C's semantics
// survive the flip for it; and
// 3. the field is inside kMGPipeClassFieldMask[class of the verb] - a field outside the
// verb's own may-read table was never filled for it, so a read there is stale by
// construction whatever its ownership row says.
//
// Which makes the allowlist move with the code instead of beside it: retiring a verb's wait
// class NARROWS it with no edit, and a new BARRIER_PULLED row widens it only on verbs that
// wait. A verb with no stamp row admits nothing - the server stamps only MGP_VERB_OP_LIST's
// ops, so no other verb can be the one a residual pull is reported against.""")
add("inline constexpr MGPipeFieldMask kMGPipeAdmittedPullMask[kMGPipeVerbCount] = {")
for verb, (low, high) in zip(verbs, admitted_masks):
add(" {{0x%016xull, 0x%016xull}}, // %s" % (low, high, verb))
add("};\n")
add("inline constexpr SizeT kMGPipeAdmittedPullPairCount = %d;" % len(admitted_pairs))
add("""
// THE PREDICATE THE STRICT KNOB ASKS (ID-117). A 69 x 128-bit table, so this costs a shift and
// a test on the apply thread - the same shape MGPipeFieldMaskHas already has.
constexpr Bool MGPipeBarrierPullAdmitted(MGPipeInputField field, MGPipeVerb verb) {
const SizeT index = static_cast<SizeT>(verb);
return index < kMGPipeVerbCount && MGPipeFieldMaskHas(kMGPipeAdmittedPullMask[index], field);
}
// THE HAND-EDIT CONTROL, MGPipeEveryFieldIsClassified's shape and for its reason: the generator
// cannot emit a bit that fails this, so it can only fire on an edited header - which is exactly
// the edit the DO NOT EDIT banner cannot prevent on its own. An admitted bit that was not a
// BARRIER-PULLED field of its verb's class would be the allowlist quietly forgiving a read that
// is torn rather than merely unmigrated.
constexpr Bool MGPipeEveryAdmittedPullIsADebtOfItsVerbsClass() {
for (SizeT v = 0; v < kMGPipeVerbCount; ++v) {
const MGPipeFieldMask& admitted = kMGPipeAdmittedPullMask[v];
const MGPipeFieldMask& mayRead =
kMGPipeClassFieldMask[static_cast<SizeT>(kMGPipeVerbClass[v])];
for (SizeT f = 0; f < kMGPipeInputFieldCount; ++f) {
const auto field = static_cast<MGPipeInputField>(f);
if (!MGPipeFieldMaskHas(admitted, field)) continue;
if (kMGPipeFieldOwnership[f] != MGPipeFieldOwnership::kBarrierPulled) return false;
if (!MGPipeFieldMaskHas(mayRead, field)) return false;
}
}
return true;
}
static_assert(MGPipeEveryAdmittedPullIsADebtOfItsVerbsClass(),
"an admitted barrier pull is not a BARRIER-PULLED field of its verb's class "
"(CONTRACT-P5E section 7, ID-84 / ID-116)");
""")
add("// The class sizes, as constants a test can pin without recounting the table.")
for cls in CLASSES:
add("inline constexpr SizeT kMGPipe%sFieldCount = %d;"
@@ -531,6 +719,8 @@ def self_test():
refused = parse_supplies_whole_field(fill)
calls, verbs = parse_ops_and_verbs()
wire_inc = read(PIPE_WIRE_INC)
points_inc = read(FILL_POINTS_INC)
def run(own_text=None, cov=None, fill_text=None, calls_text=None):
acc, stk, emt = parse_coverage(cov if cov is not None else coverage)
@@ -679,6 +869,38 @@ def self_test():
"is exempted from the stamp map but is not verb-shaped",
lambda: run(calls_text=kindless)))
# ---- 16-18: THE ADMISSION DERIVATION'S OWN SOURCES (P5e gl, ID-116) -------------------
#
# The allowlist is DERIVED from three generated tables. Each of them is read rather than
# restated, so each of them can go missing - and a missing one does not produce a visibly
# broken allowlist, it produces a SILENTLY EMPTY or SILENTLY WIDER one. An empty admitted
# set reads in the lane as "nothing is admitted", which looks like rigour and is blindness.
def admitted_pairs_for(own_text=None, wire_text=None, points_text=None):
own, _, _, _, _, _ = run(own_text=own_text)
_, _, _, verb_ops_now, _ = parse_ownership(
own_text if own_text is not None else ownership_text)
waits_now = parse_wait_classes(wire_text if wire_text is not None else wire_inc)
verb_class_now, class_mask_now = parse_verb_classes(
points_text if points_text is not None else points_inc)
return build_admitted(accessors, own, verbs, verb_ops_now, waits_now, verb_class_now,
class_mask_now)[1]
no_waits = wire_inc.replace("kMGPipeWaitClasses[static_cast<SizeT>(MGPWireOp::kOpCount)] =",
"kMGPipeWaitClassesXX[static_cast<SizeT>(MGPWireOp::kOpCount)] =", 1)
controls.append(("the wait-class column renamed away",
"kMGPipeWaitClasses",
lambda: admitted_pairs_for(wire_text=no_waits)))
no_verb_class = points_inc.replace("kMGPipeVerbClass[kMGPipeVerbCount] =",
"kMGPipeVerbClassXX[kMGPipeVerbCount] =", 1)
controls.append(("the verb-class column renamed away",
"kMGPipeVerbClass[kMGPipeVerbCount]",
lambda: admitted_pairs_for(points_text=no_verb_class)))
no_class_mask = points_inc.replace("kMGPipeClassFieldMask[kMGPipeVerbClassCount] =",
"kMGPipeClassFieldMaskXX[kMGPipeVerbClassCount] =", 1)
controls.append(("the class field mask renamed away",
"kMGPipeClassFieldMask[kMGPipeVerbClassCount]",
lambda: admitted_pairs_for(points_text=no_class_mask)))
# THE HARNESS'S OWN CONTROL, and it is the durable form of how M-1 was found. The defect was
# not the escaping in control #4; it was that expect_trip asked "did something exit" rather
# than "did THIS exit", so a control could silently become a duplicate of another. Prove the
@@ -711,6 +933,70 @@ def self_test():
if len(refused) != 8:
sys.exit("gen_pipe_field_ownership: self-test: EmittedCallSuppliesTheWholeField refuses %d "
"fields, not the eight the contract's derivation is written against" % len(refused))
# ---- THE ADMISSION DERIVATION, MOVED AND READ BACK (P5e gl, ID-116) ------------------
#
# Controls 16-18 prove the three sources are READ. These prove the three CONJUNCTS are
# USED: move each input and watch the derived allowlist move with it. A derivation that
# quietly ignored one of them would still produce a plausible table - which is exactly how
# the hand-kept copy in test.yml came to be wrong in BOTH directions at once.
derived = admitted_pairs_for()
derivation = []
def expect(name, condition):
derivation.append((name, bool(condition)))
expect("GetFramebufferBindingSlot@ReadPixels is admitted (ID-116's named survivor)",
"GetFramebufferBindingSlot@ReadPixels" in derived)
# Conjunct 2, the wait class. ReadPixels is kWaitReply so its pairs are admitted; make the
# op kWaitNone and every @ReadPixels pair must leave, because an unbarriered record's read
# is torn BY CONSTRUCTION and no ownership row can make it legal.
# THE EDIT IS COUNTED, NOT DIFFED. ResourceCopyRegion below is ALREADY kWaitNone today, so a
# "did the text change" guard would call its own control broken while it was working
# perfectly - and once item 5 moves that op, the same guard would start passing for a
# different reason. What has to hold is that the row was FOUND.
def unbarrier(op):
edited, count = re.subn(
r"(/\*\s*\d+\s+" + op + r"\s*\*/\s*static_cast<Uint8>\()kWait\w+(\))",
r"\1kWaitNone\2", wire_inc, count=1)
if count != 1:
sys.exit("gen_pipe_field_ownership: self-test: could not unbarrier %s - the control's "
"own edit no longer matches generated/PipeWire.inc" % op)
return edited
unwaited = unbarrier("ReadPixels")
expect("unbarriering ReadPixels' op removes every @ReadPixels pair",
not any(p.endswith("@ReadPixels") for p in admitted_pairs_for(wire_text=unwaited)))
# The same conjunct from the other side, and it is ID-118's whole argument: an op that is
# kWaitNone admits NOTHING on its verb, so GetTextureObject cannot be forgiven on
# CopyImageSubData by a field row alone. Written as a MOVEMENT rather than as a fixed
# expectation, so that it keeps its meaning once ResourceCopyRegion's wait class moves.
uncopied = unbarrier("ResourceCopyRegion")
expect("unbarriering ResourceCopyRegion removes every @CopyImageSubData pair",
not any(p.endswith("@CopyImageSubData")
for p in admitted_pairs_for(wire_text=uncopied)))
# Conjunct 1, the ownership row: a field that stops being a debt stops being admitted.
not_a_debt = edit(r"X\(GetFramebufferBindingSlot," + GAP + r"BARRIER_PULLED," + GAP
+ r"\"[^\"]*\"," + GAP,
"X(GetFramebufferBindingSlot, FATAL, \"-\", ",
"make GetFramebufferBindingSlot FATAL")
expect("a field that stops being BARRIER_PULLED leaves the allowlist",
not any(p.startswith("GetFramebufferBindingSlot@")
for p in admitted_pairs_for(own_text=not_a_debt)))
# And the pairs this phase is actually paying off are NOT admitted: draw_vbo is kWaitNone,
# which is why 61 lane entries abort on GetProgramForDraw@DrawArrays today. If this ever
# goes false the allowlist has started forgiving the debt P5e exists to retire.
expect("no pair is admitted on an unbarriered verb (DrawArrays)",
not any(p.endswith("@DrawArrays") for p in derived))
failed = [name for name, ok in derivation if not ok]
if failed:
sys.exit("gen_pipe_field_ownership: self-test: %d admission-derivation control(s) did "
"not hold: %s" % (len(failed), "; ".join(failed)))
if trips == 0:
sys.exit("gen_pipe_field_ownership: self-test: no negative control tripped - the gates are "
"not checking anything")
@@ -720,6 +1006,9 @@ def self_test():
print("gen_pipe_field_ownership: self-test: %d negative-control trip(s), each asserted against "
"its OWN message; harness control OK; positive control OK "
"(%d fields partitioned, 7 sticky forwards, 8 refusals)" % (trips, total))
print("gen_pipe_field_ownership: self-test: %d admission-derivation control(s) held; the "
"derived section 7 allowlist is %d <field>@<verb> pair(s)"
% (len(derivation), len(derived)))
return 0
@@ -729,6 +1018,10 @@ def main():
help="do not write; exit 1 if regenerating would change anything")
parser.add_argument("--self-test", action="store_true",
help="run the negative controls (each gate must trip) and exit")
parser.add_argument("--print-admitted", action="store_true",
help="print the derived CONTRACT-P5E section 7 allowlist, one "
"<field>@<verb> per line, and exit - so the CI shell and the C++ "
"read the SAME table (ID-116)")
args = parser.parse_args()
if args.self_test:
@@ -741,13 +1034,25 @@ def main():
_, exemptMap, required = check_verb_ops(verb_ops, exempt, calls, verbs)
ownership, phase, why, forward_map, arg_list, counts = build(
accessors, sticky, emitted, refused, rows, forwards, arg_rows)
waits = parse_wait_classes()
verb_class, class_mask = parse_verb_classes()
admitted_masks, admitted_pairs = build_admitted(
accessors, ownership, verbs, verb_ops, waits, verb_class, class_mask)
if args.print_admitted:
# STDOUT IS THE INTERFACE. One pair per line, sorted, nothing else - the lane's marker
# ratchet reads this and compares it against what the run actually logged, so a
# decorated line here is a false red there.
for pair in admitted_pairs:
print(pair)
return 0
if not os.path.isdir(GENERATED_DIR):
os.makedirs(GENERATED_DIR)
changed = []
write(os.path.join(GENERATED_DIR, OUT_NAME),
emit(accessors, sticky, ownership, phase, why, forward_map, arg_list, counts, verb_ops,
exemptMap),
exemptMap, verbs, admitted_masks, admitted_pairs),
args.check, changed)
print("gen_pipe_field_ownership: %d fields + %d sticky forwards = %d rows; "
@@ -759,6 +1064,10 @@ def main():
print("gen_pipe_field_ownership: stamp map: %d verb-shaped call(s) = %d row(s) + %d "
"exemption(s), 0 unanswered"
% (len(required), len(verb_ops), len(exemptMap)))
admitted_verbs = sorted({pair.split("@", 1)[1] for pair in admitted_pairs})
print("gen_pipe_field_ownership: section 7 allowlist (derived): %d admitted <field>@<verb> "
"pair(s) across %d barriered verb(s): %s"
% (len(admitted_pairs), len(admitted_verbs), ", ".join(admitted_verbs) or "-"))
pulled = [(f, phase[f]) for f in accessors if ownership[f] == "BARRIER_PULLED"]
print("gen_pipe_field_ownership: the debt, by retiring phase:")
by_phase = {}