diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 7dbbba56..9b94202c 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -1246,31 +1246,25 @@ jobs: exit 1 fi - # THE ADMITTED MARKERS, `@`, 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 @ 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 \ diff --git a/MobileGL/MG_Pipe/generated/PipeFieldOwnership.inc b/MobileGL/MG_Pipe/generated/PipeFieldOwnership.inc index 1aac550c..c03b22e5 100644 --- a/MobileGL/MG_Pipe/generated/PipeFieldOwnership.inc +++ b/MobileGL/MG_Pipe/generated/PipeFieldOwnership.inc @@ -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 @ 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(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(kMGPipeVerbClass[v])]; + for (SizeT f = 0; f < kMGPipeInputFieldCount; ++f) { + const auto field = static_cast(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; diff --git a/MobileGL/MG_Test/Pipe/FieldOwnershipTest.cpp b/MobileGL/MG_Test/Pipe/FieldOwnershipTest.cpp index 17ea339e..44fd73f9 100644 --- a/MobileGL/MG_Test/Pipe/FieldOwnershipTest.cpp +++ b/MobileGL/MG_Test/Pipe/FieldOwnershipTest.cpp @@ -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(MGPWireOp::kOpCount); ++op) { + const MGPipeVerb verb = MGPipeVerbForWireOp(static_cast(op)); + if (verb == MGPipeVerb::kVerbCount) continue; + if (MGPipeWaitClassFor(static_cast(op)) != kWaitNone) { + waitedFor[static_cast(verb)] = true; + } + } + SizeT admitted = 0; + for (SizeT v = 0; v < kMGPipeVerbCount; ++v) { + const auto verb = static_cast(v); + for (SizeT f = 0; f < kMGPipeInputFieldCount; ++f) { + const auto field = static_cast(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(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. diff --git a/scripts/gen_pipe_field_ownership.py b/scripts/gen_pipe_field_ownership.py index 71d06ab3..32dbe240 100644 --- a/scripts/gen_pipe_field_ownership.py +++ b/scripts/gen_pipe_field_ownership.py @@ -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 `... = {` 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\(\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(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 @ 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 @ 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 @ 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(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(kMGPipeVerbClass[v])]; + for (SizeT f = 0; f < kMGPipeInputFieldCount; ++f) { + const auto field = static_cast(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(MGPWireOp::kOpCount)] =", + "kMGPipeWaitClassesXX[static_cast(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\()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 @ 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 " + "@ 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 @ " + "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 = {}