diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 9b94202c..671215f6 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -1254,10 +1254,17 @@ jobs: # 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. + # The rule is ID-84 said in tables that already exist (ID-116, refined by ID-125): a + # @ pull is admitted iff the field's ownership row is BARRIER_PULLED, the + # verb has a stamp row, the field is inside the verb class's may-read mask, and EITHER + # the verb's wire op is statically barriered (kMGPipeWaitClasses != kWaitNone, i.e. the + # client really is parked behind the record) OR the field's retiring phase does not + # name P5e. The second disjunct is the honest reading of ID-84: this comparison only + # ever sees pulls on records the server stamped BARRIERED - an unbarriered one aborts + # before any of this - so the pull is legal by construction and the only question left + # is whether THIS phase still owes the migration. Without it the lane would go red on + # GetTransformFeedbackProgram@DrawArrays, a row CONTRACT-P5E §5.7 rules out of P5e + # entirely and no package here is allowed to touch. # `--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 diff --git a/MobileGL/MG_Pipe/generated/PipeFieldOwnership.inc b/MobileGL/MG_Pipe/generated/PipeFieldOwnership.inc index 72df2b01..7d922734 100644 --- a/MobileGL/MG_Pipe/generated/PipeFieldOwnership.inc +++ b/MobileGL/MG_Pipe/generated/PipeFieldOwnership.inc @@ -323,7 +323,7 @@ inline constexpr SizeT kMGPipeVerbBoundaryExemptCount = 3; // 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 + {{0x5808402000000140ull, 0x0000000000000000ull}}, // DrawArrays {{0x0000000000000000ull, 0x0000000000000000ull}}, // DrawElements {{0x0000000000000000ull, 0x0000000000000000ull}}, // DrawElementsBaseVertex {{0x0000000000000000ull, 0x0000000000000000ull}}, // MultiDrawArrays @@ -343,7 +343,7 @@ inline constexpr MGPipeFieldMask kMGPipeAdmittedPullMask[kMGPipeVerbCount] = { {{0x0000000000000000ull, 0x0000000000000000ull}}, // DrawArraysInstanced {{0x0000000000000000ull, 0x0000000000000000ull}}, // DrawElementsIndirect {{0x0000000000000000ull, 0x0000000000000000ull}}, // DrawArraysIndirect - {{0x0000000000000000ull, 0x0000000000000000ull}}, // Clear + {{0x5800402000000100ull, 0x0000000000000000ull}}, // Clear {{0x0000000000000000ull, 0x0000000000000000ull}}, // ClearBufferfi {{0x0000000000000000ull, 0x0000000000000000ull}}, // ClearBufferfv {{0x0000000000000000ull, 0x0000000000000000ull}}, // ClearBufferuiv @@ -352,7 +352,7 @@ inline constexpr MGPipeFieldMask kMGPipeAdmittedPullMask[kMGPipeVerbCount] = { {{0x0000000000000000ull, 0x0000000000000000ull}}, // ClearNamedFramebufferfi {{0x0000000000000000ull, 0x0000000000000000ull}}, // ClearNamedFramebufferiv {{0x0000000000000000ull, 0x0000000000000000ull}}, // ClearNamedFramebufferuiv - {{0x0000000000000000ull, 0x0000000000000000ull}}, // BlitFramebuffer + {{0x5800402000000100ull, 0x0000000000000000ull}}, // BlitFramebuffer {{0x0000000000000000ull, 0x0000000000000000ull}}, // BlitNamedFramebuffer {{0x5800c02000300180ull, 0x0000000000000000ull}}, // CopyTexImage2D {{0x0000000000000000ull, 0x0000000000000000ull}}, // CopyTexSubImage2D @@ -361,17 +361,17 @@ inline constexpr MGPipeFieldMask kMGPipeAdmittedPullMask[kMGPipeVerbCount] = { {{0x5800c02000300140ull, 0x0000000000000000ull}}, // ReadPixels {{0x0000000000000000ull, 0x0000000000000000ull}}, // GetTexImage {{0x5800c02000300140ull, 0x0000000000000000ull}}, // GetTextureImage - {{0x0000000000000000ull, 0x0000000000000000ull}}, // DispatchCompute + {{0x5800402000000140ull, 0x0000000000000000ull}}, // DispatchCompute {{0x0000000000000000ull, 0x0000000000000000ull}}, // DispatchComputeIndirect - {{0x0000000000000000ull, 0x0000000000000000ull}}, // MemoryBarrier + {{0x5800402000000100ull, 0x0000000000000000ull}}, // MemoryBarrier {{0x0000000000000000ull, 0x0000000000000000ull}}, // MemoryBarrierByRegion - {{0x0000000000000000ull, 0x0000000000000000ull}}, // BindImageTexture + {{0x5800402000000100ull, 0x0000000000000000ull}}, // BindImageTexture {{0x0000000000000000ull, 0x0000000000000000ull}}, // GetIntegeri_v {{0x5800c02000300100ull, 0x0000000000000000ull}}, // ShaderStorageBlockBinding - {{0x0000000000000000ull, 0x0000000000000000ull}}, // FenceSync + {{0x5800402000000100ull, 0x0000000000000000ull}}, // FenceSync {{0x5800402000000100ull, 0x0000000000000000ull}}, // ClientWaitSync - {{0x0000000000000000ull, 0x0000000000000000ull}}, // WaitSync - {{0x0000000000000000ull, 0x0000000000000000ull}}, // DeleteSync + {{0x5800402000000100ull, 0x0000000000000000ull}}, // WaitSync + {{0x5800402000000100ull, 0x0000000000000000ull}}, // DeleteSync {{0x5800402000000100ull, 0x0000000000000000ull}}, // GetSyncStatus {{0x0000000000000000ull, 0x0000000000000000ull}}, // IsTimerQuerySupported {{0x0000000000000000ull, 0x0000000000000000ull}}, // BeginTimeElapsedQuery @@ -384,7 +384,7 @@ inline constexpr MGPipeFieldMask kMGPipeAdmittedPullMask[kMGPipeVerbCount] = { {{0x0000000000000000ull, 0x0000000000000000ull}}, // EndOcclusionQuery {{0x0000000000000000ull, 0x0000000000000000ull}}, // BeginXfbPrimitivesQuery {{0x0000000000000000ull, 0x0000000000000000ull}}, // EndXfbPrimitivesQuery - {{0x0000000000000000ull, 0x0000000000000000ull}}, // PatchParameteri + {{0x5800402000000100ull, 0x0000000000000000ull}}, // PatchParameteri {{0x5808402000000180ull, 0x0000000000000000ull}}, // BeginTransformFeedback {{0x5808402000000180ull, 0x0000000000000000ull}}, // EndTransformFeedback {{0x5808402000000180ull, 0x0000000000000000ull}}, // PauseTransformFeedback @@ -394,7 +394,7 @@ inline constexpr MGPipeFieldMask kMGPipeAdmittedPullMask[kMGPipeVerbCount] = { {{0x0000000000000000ull, 0x0000000000000000ull}}, // GetGpuTimestampNs }; -inline constexpr SizeT kMGPipeAdmittedPullPairCount = 111; +inline constexpr SizeT kMGPipeAdmittedPullPairCount = 174; // 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. diff --git a/MobileGL/MG_Test/Pipe/FieldOwnershipTest.cpp b/MobileGL/MG_Test/Pipe/FieldOwnershipTest.cpp index 4b923f74..feb0db9e 100644 --- a/MobileGL/MG_Test/Pipe/FieldOwnershipTest.cpp +++ b/MobileGL/MG_Test/Pipe/FieldOwnershipTest.cpp @@ -28,6 +28,7 @@ #include +#include #include #include #include @@ -388,40 +389,86 @@ 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. +// P5e (gl), ID-116 + ID-125: THE §7 ALLOWLIST IS A DERIVATION, RESTATED HERE 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. +// The generator emits kMGPipeAdmittedPullMask by joining four columns; the header's own +// static_assert can only check two of them, because the wait column and the stamp map live in +// other generated files. This case walks those and asserts the rule end to end. A derivation +// that quietly dropped a term would still produce a plausible table - which is precisely how the +// hand-kept copy in test.yml came to admit GetTextureObject@CopyImageSubData while omitting +// GetFramebufferBindingSlot@ReadPixels. +// +// THE RULE (ID-125). Admitted iff the field is BARRIER-PULLED, the verb has a stamp row, the +// field is inside the verb class's may-read mask, and EITHER the verb's op is statically +// barriered OR the field's retiring phase does not name P5e. The second disjunct is the honest +// statement of ID-84: this table is consulted only on a record the server already stamped +// BARRIERED - CountBarrierPull's unbarriered arm is [[noreturn]] and fires first - so the pull +// is legal by construction and the only open question is whether THIS phase still owes the +// migration. The retiring-phase column is exactly that answer. TEST_F(FieldOwnershipTest, TheAdmittedPullTableIsID84sDerivationAndNotAList) { - // The largest survivor of the lane, and the row the hand-kept copy omitted (21 entries). + // "Does this row's retiring phase name P5e", tokenised rather than substring-matched for + // the generator's reason: a "P5" or a future "P5e2" must not answer for "P5e". + const auto owedByThisPhase = [](const char* retires) { + const std::string phase(retires == nullptr ? "" : retires); + for (std::size_t at = phase.find("P5e"); at != std::string::npos; + at = phase.find("P5e", at + 1)) { + const Bool leftOk = at == 0 || !std::isalnum(static_cast(phase[at - 1])); + const std::size_t after = at + 3; + const Bool rightOk = after >= phase.size() || + !std::isalnum(static_cast(phase[after])); + if (leftOk && rightOk) return true; + } + return false; + }; + + // ---- ID-125's survivors, each named with the disjunct that carries it ---------------- + // Disjunct 1, and the largest survivor in the lane (21 entries) - the row the hand-kept + // copy omitted. The field IS this phase's debt; read_pixels is kWaitReply, so the client + // is parked behind the record and P5C's semantics hold for it. 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. + MGPipeVerb::ReadPixels)); + EXPECT_TRUE(MGPipeBarrierPullAdmitted(MGPipeInputField::GetTextureUnitObject, + MGPipeVerb::CopyTexImage2D)); + // Disjunct 2: a debt a LATER phase owes, on a verb this phase does not barrier. + // CONTRACT-P5E §5.7 rules transform feedback out of P5e entirely and this row retires in + // P3b/P4b, so the static rule alone would have failed the lane on a row no package in this + // phase is allowed to touch. + EXPECT_TRUE(MGPipeBarrierPullAdmitted(MGPipeInputField::GetTransformFeedbackProgram, + MGPipeVerb::DrawArrays)) + << "the lane would be red on a transform-feedback row CONTRACT-P5E §5.7 rules out of " + "this phase; ID-125's second disjunct is what admits it"; + EXPECT_TRUE(MGPipeBarrierPullAdmitted(MGPipeInputField::ValidateProgramName, + MGPipeVerb::ShaderStorageBlockBinding)); + // BOTH DISJUNCTS, ASSERTED SEPARATELY (ID-118 and ID-125 on one pair). GetTextureObject + // retires in P7, so disjunct 2 admits it whatever the wire says - and ID-118 ALSO moved + // resource_copy_region to a barriered class, so disjunct 1 holds independently. Putting + // that op back to kWaitNone must therefore leave the pair admitted and still be wrong, so + // the wait class is asserted here in its own words rather than through the allowlist. + EXPECT_TRUE(MGPipeBarrierPullAdmitted(MGPipeInputField::GetTextureObject, + MGPipeVerb::CopyImageSubData)); + EXPECT_NE(MGPipeWaitClassFor(MGPWireOp::ResourceCopyRegion), kWaitNone) + << "resource_copy_region is unbarriered again (ID-118): after the flip, a copy record " + "reading the client's texture object is an unconditional Fatal - the allowlist still " + "admits the pair on the retiring-phase disjunct, so THIS is the assertion that sees it"; + EXPECT_FALSE(owedByThisPhase( + kMGPipeFieldRetiringPhase[static_cast(MGPipeInputField::GetTextureObject)])); + + // ---- and the two rows THIS phase owes stay rejected --------------------------------- EXPECT_FALSE(MGPipeBarrierPullAdmitted(MGPipeInputField::GetProgramForDraw, MGPipeVerb::DrawArrays)) - << "the draw path's pull became admitted - the allowlist is now forgiving the 61 lane " + << "the draw path's pull became admitted - the allowlist is now forgiving the lane " "entries this phase is being run to fix"; EXPECT_FALSE(MGPipeBarrierPullAdmitted(MGPipeInputField::GetBoundVertexArray, MGPipeVerb::DrawArrays)); - // P5e (gl), ID-118: the pair that made resource_copy_region's wait class move. The field - // retires in P7, so it had to be admitted somewhere - and it is admitted HERE, by the - // derivation and with no exception, only because the op is kWaitApplied. Put that row back - // to kWaitNone in PipeCalls.def and this goes red, which is the whole argument for moving - // the wait class rather than writing the field into a list. - EXPECT_TRUE(MGPipeBarrierPullAdmitted(MGPipeInputField::GetTextureObject, - MGPipeVerb::CopyImageSubData)) - << "resource_copy_region is unbarriered again: after the flip, a copy record reading " - "the client's texture object is an unconditional Fatal and P7 is two phases away"; + EXPECT_FALSE(MGPipeBarrierPullAdmitted(MGPipeInputField::GetProgramForDispatch, + MGPipeVerb::DispatchCompute)); + // Magma's row: GetFramebufferBindingSlot retires in P5e on Espryt and P7 on Magma, and the + // phase column is ONE string for both, so the derivation cannot admit it on the unbarriered + // Clear verb. That is deliberate rather than a gap - the DirectVulkan entries carry their + // own expected-red lane label instead, so the Espryt allowlist stays a statement about + // Espryt (this package's item 7). + EXPECT_FALSE(MGPipeBarrierPullAdmitted(MGPipeInputField::GetFramebufferBindingSlot, + MGPipeVerb::Clear)); // A field that is not a debt at all is never admitted, on any verb. EXPECT_FALSE(MGPipeBarrierPullAdmitted(MGPipeInputField::GetRenderStateParameters, MGPipeVerb::ReadPixels)); @@ -430,30 +477,39 @@ TEST_F(FieldOwnershipTest, TheAdmittedPullTableIsID84sDerivationAndNotAList) { 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. + // ---- 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 verb a pull is reported against. + Bool stamped[kMGPipeVerbCount] = {}; 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; + stamped[static_cast(verb)] = true; if (MGPipeWaitClassFor(static_cast(op)) != kWaitNone) { waitedFor[static_cast(verb)] = true; } } SizeT admitted = 0; + SizeT byWaitClass = 0; + SizeT byRetiringPhase = 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]) + if (waitedFor[v]) ++byWaitClass; + if (!owedByThisPhase(kMGPipeFieldRetiringPhase[f])) ++byRetiringPhase; + EXPECT_TRUE(stamped[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"; + << " is admitted on a verb the server never stamps, so it is a row of the " + "allowlist nothing can exercise and nobody can retire"; + EXPECT_TRUE(waitedFor[v] || !owedByThisPhase(kMGPipeFieldRetiringPhase[f])) + << kMGPipeInputFieldNames[f] << "@" << kMGPipeVerbNames[v] + << " is admitted although this phase owes the row AND no barriered op stamps the " + "verb: 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( @@ -468,6 +524,10 @@ TEST_F(FieldOwnershipTest, TheAdmittedPullTableIsID84sDerivationAndNotAList) { 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"; + // BOTH DISJUNCTS CARRY REAL WEIGHT. If either count were zero the rule would have collapsed + // to the other one and a whole class of rows would be silently mis-classified. + EXPECT_GT(byWaitClass, SizeT{0}) << "no pair is admitted by its verb's wait class"; + EXPECT_GT(byRetiringPhase, SizeT{0}) << "no pair is admitted by its retiring phase"; } // --------------------------------------------------------------------------------------- @@ -838,15 +898,38 @@ TEST_F(FieldOwnershipTest, TheSameReadWithoutStrictErrorsSurvivesAndIsCounted) { EXPECT_EQ(r.Log.find("Fatal{"), std::string::npos) << r.Log; } -TEST_F(FieldOwnershipTest, StrictErrorsAlsoPromotesTheStickyForwards) { +// THE SEVEN STICKY FORWARDS ARE NOT EXEMPT FROM THE DETECTOR, which is what this case has +// always been for - it was written as "strict PROMOTES them to a Fatal" because before ID-125 +// every barrier-pulled read under strict aborted. +// +// P5e (gl), ID-125 CHANGED THE VERDICT AND NOT THE REACH, and the rename says which. All seven +// sticky forwards retire in a LATER phase (P7, P7/P9, P7/P13, P9 - FieldOwnership.def's forward +// list; not one names P5e), so on any stamped verb the second disjunct admits them: the record +// is barriered, the pull is legal by construction, and the phase that owes the migration is not +// this one. The thing that would be a defect is a sticky forward the detector never REACHED - +// a read that answered out of gPipeInputs without being counted or named - and that is what is +// asserted here, by the counter moving and by the marker naming the field and its phase. +// +// The Fatal half of the mechanism keeps its own case beside this one: +// StrictErrorsTurnsABarrierPulledReadIntoANamedAbort uses GetBoundVertexArray, which IS this +// phase's debt on an unbarriered verb and therefore still aborts. +TEST_F(FieldOwnershipTest, StrictErrorsReachTheStickyForwardsAndNameThemByField) { const ChildResult r = RunInChild([] { MG_Config::Ipc.StrictErrors = true; MGPipeServerStampVerbBoundary(MGPipeVerb::DrawArrays); (void)gPipeInputs.ValidateProgramName(1u); + // NOT EXEMPT: the forward went through CountBarrierPull like any field accessor. Without + // this, "it did not abort" would be indistinguishable from "it was never detected", and + // the sticky set is exactly where the gate is structurally blind if it is. + if (MGPipeResidualPullCount() != 1) ::_exit(7); }); - ASSERT_TRUE(DiedOfAbort(r)) << DescribeStatus(r) << "\n" << r.Log; - EXPECT_NE(r.Log.find("Fatal{UnmigratedPipeInput, \"ValidateProgramName@DrawArrays\"}"), + ASSERT_TRUE(ExitedWith(r, 0)) << DescribeStatus(r) << "\n" << r.Log; + EXPECT_EQ(r.Log.find("Fatal{UnmigratedPipeInput"), std::string::npos) << r.Log; + EXPECT_NE(r.Log.find("Admitted{UnmigratedPipeInput, \"ValidateProgramName@DrawArrays\"} " + "[BARRIER-PULLED, ADMITTED, retires in P9]"), std::string::npos) + << "the sticky forward was neither aborted on nor named; a debt nobody prints is a debt " + "nobody retires\n" << r.Log; } diff --git a/scripts/gen_pipe_field_ownership.py b/scripts/gen_pipe_field_ownership.py index 32dbe240..cfe72734 100644 --- a/scripts/gen_pipe_field_ownership.py +++ b/scripts/gen_pipe_field_ownership.py @@ -296,16 +296,47 @@ def parse_verb_classes(text=None): 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]. +THIS_PHASE = "P5e" +PHASE_TOKEN_RE = re.compile(r"\bP\d+[a-z]*\b") - 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. + +def phase_is_owed_by_this_phase(retires): + """Does this row's RetiringPhase column name THIS phase? + + Tokenised rather than substring-matched: the column is prose ("P5e (Espryt unbarriered), + P7 (Magma)", "P3b/P4b (Espryt), P7 (Magma)", "P8 (indirect), P9 (readback), P13 + (transfer)"), and a substring test would let a future "P5e2" or a "P5" answer for "P5e".""" + return THIS_PHASE in PHASE_TOKEN_RE.findall(retires) + + +def build_admitted(accessors, ownership, phase, verbs, verb_ops, waits, verb_class, class_mask): + """ID-84 AS A DERIVATION (ID-116), WITH ID-125's SECOND DISJUNCT. + + A @ pull is ADMITTED iff the field's row is BARRIER_PULLED, the field is inside + kMGPipeClassFieldMask[class of verb] - a field outside the verb's own may-read table was + never filled for it - and EITHER + + 1. the verb's wire op is STATICALLY BARRIERED (MGPipeWaitClassFor(op) != kWaitNone), so the + client is parked in its own wait and P5C's semantics hold for the record; OR + 2. the field's RETIRING PHASE does not name this phase. + + ID-125 ADDED (2) AND IT IS THE HONEST STATEMENT OF ID-84. At runtime this table is only ever + consulted on a record the server already stamped BARRIERED - CountBarrierPull's unbarriered + arm is [[noreturn]] and fires first - so the record's pull is legal by construction and the + only remaining question is whether THIS PHASE still owes the migration. The retiring-phase + column is precisely that answer, and it is already in the table. + + Disjunct (1) survives as its own term because it is a stronger claim about the same pair: it + says the client waits for the record STATICALLY, which is what lets a row whose phase IS this + one (GetFramebufferBindingSlot@ReadPixels, GetTextureUnitObject@CopyTexImage2D) still be + admitted. Without (1) those two would fail the lane; without (2) + GetTransformFeedbackProgram@DrawArrays would fail it, and CONTRACT-P5E §5.7 rules transform + feedback out of this phase entirely - so the lane would be red on a row no package here is + allowed to touch. + + A verb with no stamp row still admits NOTHING under (1): the server stamps only the ops + MGP_VERB_OP_LIST names. Under (2) it admits its non-P5e debts, which is correct for the same + reason - the mask is consulted only where a stamp already happened. Returns (per-verb (word0, word1), the sorted @ pairs).""" field_index = {name: i for i, name in enumerate(accessors)} @@ -319,19 +350,27 @@ def build_admitted(accessors, ownership, verbs, verb_ops, waits, verb_class, cla 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)) + # A VERB WITH NO STAMP ROW ADMITS NOTHING UNDER EITHER DISJUNCT, and that is not an + # omission - it is the precondition both disjuncts are stated under. This table is read + # only from CountBarrierPull, which is reachable only after MGPipeServerStampVerbBoundary, + # and the server stamps only the ops MGP_VERB_OP_LIST names. A bit set for any other verb + # would be a row of the allowlist that nothing can exercise and nobody can retire. + if op is None: + masks.append((0, 0)) + continue + 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 + if not barriered and phase_is_owed_by_this_phase(phase[field]): + continue + words[index // 64] |= 1 << (index % 64) + pairs.append("%s@%s" % (field, verb)) masks.append((words[0], words[1])) return masks, sorted(pairs) @@ -876,13 +915,13 @@ def self_test(): # 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) + own, ph, _, _, _, _ = 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, + return build_admitted(accessors, own, ph, verbs, verb_ops_now, waits_now, verb_class_now, class_mask_now)[1] no_waits = wire_inc.replace("kMGPipeWaitClasses[static_cast(MGPWireOp::kOpCount)] =", @@ -940,13 +979,32 @@ def self_test(): # 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() + waits_real = parse_wait_classes(wire_inc) derivation = [] def expect(name, condition): derivation.append((name, bool(condition))) - expect("GetFramebufferBindingSlot@ReadPixels is admitted (ID-116's named survivor)", + # ---- ID-125's six survivors, each by the disjunct that carries it -------------------- + expect("GetFramebufferBindingSlot@ReadPixels is admitted by disjunct 1 (read_pixels waits)", "GetFramebufferBindingSlot@ReadPixels" in derived) + expect("GetTextureUnitObject@CopyTexImage2D is admitted by disjunct 1", + "GetTextureUnitObject@CopyTexImage2D" in derived) + # Disjunct 2's three. Each is a debt some LATER phase owes, on a verb this phase does not + # barrier - and CONTRACT-P5E §5.7 rules transform feedback out of P5e entirely, so the + # static rule alone would have failed the lane on a row no package here may touch. + expect("GetTransformFeedbackProgram@DrawArrays is admitted by disjunct 2 (retires P3b/P4b)", + "GetTransformFeedbackProgram@DrawArrays" in derived) + expect("GetTextureObject@CopyImageSubData is admitted (retires P7)", + "GetTextureObject@CopyImageSubData" in derived) + expect("ValidateProgramName@ShaderStorageBlockBinding is admitted (retires P9)", + "ValidateProgramName@ShaderStorageBlockBinding" in derived) + # ... and the two rows this phase OWES are still rejected: both are P5e rows on an + # unbarriered verb, which is exactly the debt pa and mv are retiring. + expect("GetProgramForDraw@DrawArrays is REJECTED (a P5e row on an unbarriered verb)", + "GetProgramForDraw@DrawArrays" not in derived) + expect("GetBoundVertexArray@DrawArrays is REJECTED (a P5e row on an unbarriered verb)", + "GetBoundVertexArray@DrawArrays" not 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 @@ -965,17 +1023,32 @@ def self_test(): 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))) + expect("unbarriering ReadPixels' op drops its P5e-owed pair " + "(GetFramebufferBindingSlot@ReadPixels) and keeps the later phases' pairs", + "GetFramebufferBindingSlot@ReadPixels" not in admitted_pairs_for(wire_text=unwaited) + and "GetTextureObject@ReadPixels" 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. + # The same disjunct from the other side. ID-118 moved ResourceCopyRegion to a barriered wait + # class; unbarrier it again and its P5e-owed pairs go, while GetTextureObject stays admitted + # on ID-125's second disjunct because it retires in P7. BOTH disjuncts hold for that pair + # today and this control is what says they are independent rather than one masking the other. uncopied = unbarrier("ResourceCopyRegion") - expect("unbarriering ResourceCopyRegion removes every @CopyImageSubData pair", - not any(p.endswith("@CopyImageSubData") - for p in admitted_pairs_for(wire_text=uncopied))) + expect("unbarriering ResourceCopyRegion drops its P5e-owed @CopyImageSubData pairs", + "GetFramebufferBindingSlot@CopyImageSubData" + not in admitted_pairs_for(wire_text=uncopied)) + expect("GetTextureObject@CopyImageSubData is admitted by BOTH disjuncts (ID-118 and ID-125)", + "GetTextureObject@CopyImageSubData" in admitted_pairs_for(wire_text=uncopied) + and "GetTextureObject@CopyImageSubData" in derived) + + # ID-125's DISJUNCT 2, MOVED: make the transform-feedback row this phase's debt and it must + # leave the allowlist on the unbarriered draw verb. Without this the second disjunct could + # be a constant `true` and every control above would still hold. + owed_now = edit(r"X\(GetTransformFeedbackProgram," + GAP + r"BARRIER_PULLED," + GAP + + r"\"[^\"]*\",", + "X(GetTransformFeedbackProgram, BARRIER_PULLED, \"P5e (moved by the control)\",", + "make GetTransformFeedbackProgram this phase's debt") + expect("a row whose retiring phase becomes P5e leaves the unbarriered verb's allowlist", + "GetTransformFeedbackProgram@DrawArrays" not in admitted_pairs_for(own_text=owed_now)) # 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 @@ -986,11 +1059,19 @@ def self_test(): 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)) + # AND THE RULE OVER THE WHOLE TABLE, not just its six named rows: nothing THIS PHASE owes is + # ever admitted on a verb no barriered op stamps. If this goes false the allowlist has + # started forgiving the debt P5e exists to retire. + op_for_verb = {verb: op for op, verb in parse_ownership(ownership_text)[3]} + ownership_now, phase_now = run()[0], run()[1] + unbarriered_p5e = sorted( + pair for pair in derived + if (lambda f, v: (op_for_verb.get(v) is None + or waits_real.get(op_for_verb[v]) in (None, "kWaitNone")) + and phase_is_owed_by_this_phase(phase_now[f]))(*pair.split("@", 1))) + expect("no pair this phase owes is admitted on an unbarriered verb: " + + (", ".join(unbarriered_p5e) or "none"), + not unbarriered_p5e) failed = [name for name, ok in derivation if not ok] if failed: @@ -1037,7 +1118,7 @@ def main(): 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) + accessors, ownership, phase, 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