diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 7dbbba56..b9bbd91f 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -1214,81 +1214,171 @@ jobs: ulimit -c unlimited ready=$(grep -oE 'kMGPipeP5eRunAheadReady = (true|false)' "${GITHUB_WORKSPACE}/MobileGL/MG_Backend/Init.cpp" | head -1 | awk '{print $3}') echo "kMGPipeP5eRunAheadReady = ${ready}" + helper="${GITHUB_WORKSPACE}/MobileGL/MG_IntegrationTest/Harness/split_log_paths.py" + expected="${GITHUB_WORKSPACE}/MobileGL/MG_IntegrationTest/Harness/strict-expected-markers.txt" + + # THE LOG SET COMES FROM ctest, NOT FROM A DIRECTORY (P5e gl, ID-119). This step used to + # grep MobileGL/MG_IntegrationTest/split-logs/, which holds 90 of the lane's entries. + # The 26 it could not see were the F1. readback block, both NamedBlit pairs, the four + # Ct. entries and PersistentMapArm - i.e. PRECISELY the readback population the + # allowlist is about, plus the only DirectVulkan entries in the lane. A directory is a + # guess about where the lane put its logs; `--show-only=json-v1` is the lane saying so. + ctest -L integration-split --show-only=json-v1 > "${RUNNER_TEMP}/lane.json" + + # Stale logs from an earlier job would be read as this run's evidence: an entry that + # never starts leaves the previous file in place, and "no marker" is exactly what a + # lane that never ran looks like. + python3 - "${RUNNER_TEMP}/lane.json" "${helper}" <<'PY' + import importlib.util, json, os, sys + spec = importlib.util.spec_from_file_location("slp", sys.argv[2]) + slp = importlib.util.module_from_spec(spec); spec.loader.exec_module(slp) + logs = slp.marker_log_paths(json.load(open(sys.argv[1]))) + for path in set(logs.values()): + try: + os.unlink(path) + except OSError: + pass + print(f"reset {len(set(logs.values()))} private log(s) across {len(logs)} entries") + PY + rc=0 ctest -L integration-split --no-tests=error -j 4 > "${RUNNER_TEMP}/strict-split.txt" 2>&1 || rc=$? tail -5 "${RUNNER_TEMP}/strict-split.txt" echo "strict run: rc=${rc}" + 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)" + if [ "${ready}" != "true" ]; then - # ---- the pre-flip arm, unchanged from P5c ---- + # ---- the pre-flip arm ---- if [ "${rc}" -eq 0 ]; then echo "::error::integration-split under MOBILEGL_IPC_STRICT_ERRORS=1 went GREEN while kMGPipeP5eRunAheadReady is false - the object-class residual pulls (P3b/P4b/P7) are still pinned, so strict must abort every drawing scenario. If P5e has just landed, flip that constant in the same commit." exit 1 fi - marker='BARRIER-PULLED, MOBILEGL_IPC_STRICT_ERRORS=1' - hits=$(grep -rl "${marker}" MobileGL/MG_IntegrationTest/split-logs/ 2>/dev/null | wc -l) - if [ "${hits}" -lt 1 ]; then - echo "::error::no split entry's private log carries the strict marker '${marker}' - the lane went red without the strict Fatal firing, which is a defect, not the control" - exit 1 - fi - echo "integration-split under strict is red by design; ${hits} private log(s) carry the strict marker" + # The census, and the ADMITTED half of the ratchet, run in this arm too: the Fatal + # half is expected here (it is what "red by design" MEANS), but a debt that appeared + # or vanished on the admitted side is news whichever arm the tree is in. + python3 "${helper}" markers "${RUNNER_TEMP}/lane.json" '.' \ + "${RUNNER_TEMP}/allowed.txt" "${expected}" + echo "integration-split under strict is red by design, and its marker census above is the evidence" exit 0 fi - # ---- the post-flip arm: HARD GREEN, with §7's allowlist ---- + # ---- the post-flip arm: HARD GREEN, two-sided ---- # - # EVERY ENTRY MUST COMPLETE. An abort here is either an unbarriered pull (§3.3's - # unconditional Fatal, which is a missed migration) or a barriered row that is not on - # the list below, and both are the lane's job to catch. + # EVERY ENTRY MUST COMPLETE, and the census is what says why when one does not: an abort + # is either an unbarriered pull (§3.3's unconditional Fatal, a missed migration) or a + # barriered pull nothing admits, and both come out of the census by field and verb. if [ "${rc}" -ne 0 ]; then - echo "::error::integration-split under MOBILEGL_IPC_STRICT_ERRORS=1 is RED on a run-ahead server. CONTRACT-P5E §7 makes this lane a hard green gate: an unbarriered record's pull aborts whatever the knob says, so a red here names a field and a verb in the failing entry's private log." - grep -hoE 'Fatal\{UnmigratedPipeInput, "[^"]*"\}' MobileGL/MG_IntegrationTest/split-logs/*.log 2>/dev/null | sort | uniq -c | sort -rn | head -20 + echo "::error::integration-split under MOBILEGL_IPC_STRICT_ERRORS=1 is RED on a run-ahead server. CONTRACT-P5E §7 makes this lane a hard green gate; the census below names the field and the verb of every entry that aborted." + python3 "${helper}" markers "${RUNNER_TEMP}/lane.json" '.' \ + "${RUNNER_TEMP}/allowed.txt" "${expected}" || true 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' \ - > "${RUNNER_TEMP}/allowed.txt" + # 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 (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 + # that wait. + # THE RATCHET, BOTH SIDES (ID-119). `no-fatal` is what makes this arm the hard gate: + # - any Fatal marker fails; + # - an ADMITTED marker outside the generated allowlist fails, which can only mean the + # committed PipeFieldOwnership.inc and the generator disagree; + # - a pair that appears and is not in strict-expected-markers.txt fails: it is a debt + # somebody now owes and it gets written down with the phase that retires it; + # - AND a pair in that file that no longer appears fails, so the lane CANNOT ROT + # GREEN. Without that half, a retired debt leaves its row behind as a permanent + # licence and the next regression to re-introduce the read reads as "expected". + # ADMITTED-ESCALATED markers are checked against the expected set but NOT against the + # allowlist: they are a runtime fact about the record's payload (an open XFB span, a + # draw carrying client vertex arrays) that no table indexed by (field, verb) can carry, + # and widening the static list to hold them would forgive the ordinary draw path too. + python3 "${helper}" markers "${RUNNER_TEMP}/lane.json" '.' \ + "${RUNNER_TEMP}/allowed.txt" "${expected}" no-fatal - 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 \ - | sed -E 's/.*"([^"]*)".*/\1/' | sort -u > "${RUNNER_TEMP}/markers.txt" || true - bad=$(comm -23 "${RUNNER_TEMP}/markers.txt" <(sort -u "${RUNNER_TEMP}/allowed.txt") || true) - if [ -n "${bad}" ]; then - echo "::error::a BARRIER-PULLED marker outside CONTRACT-P5E §7's allowlist appeared on a run-ahead server. Each one is a field an apply still reads out of client memory:" - echo "${bad}" + # `rsp`, AND THE PIN THAT REPLACED A VACUOUS ONE (ID-119). What stood here was a grep + # for `rsp=` over split-logs/ - a counter no entry in that directory emits, because + # PipeStats is off unless a lane asks for it - testing a sentence that was true of every + # possible implementation: CountBarrierPull's unbarriered arm is [[noreturn]] and runs + # BEFORE ++g_residualPulls, so an unbarriered pull can never reach the counter whatever + # the code does. It has been replaced by an assertion inside a lane entry that actually + # counts: DirectGLES.Split.StrictArming., which runs with MOBILEGL_PIPE_STATS=1, + # MOBILEGL_PIPE_STATS_PERIOD=1 and a private log path of its own (a whole-lane env flip + # races under -j, since the library opens that path "w"), and asserts + # vbs > 0 - the server stamped a verb boundary on a DRAWING inproc entry, which is + # ID-115's positive control: everything strict checks is downstream of + # that stamp, and before it existed "the lane is green" and "strict was + # never armed" were the same observation; + # rsp == 0 or rsp >= draws - the checkable shape of the debt. While the draw path's + # pull is unretired every draw pulls, so rsp scales with draws; the + # retirement is visible as rsp ceasing to scale. That is what the device + # measured (rsp ~= the draw count under inproc, 0 under monolith). + # So the assertion lives where the counter is, and this step only has to insist the + # entry RAN - a positive control that can be skipped away is not one. + if ! grep -q 'DirectGLES\.Split\.StrictArming\.' "${RUNNER_TEMP}/strict-split.txt"; then + echo "::error::the strict lane did not run DirectGLES.Split.StrictArming., so nothing in this run proves the server ever stamped a verb boundary. A green lane without it is indistinguishable from a lane where strict was never armed (ID-115)." exit 1 fi + echo "integration-split under strict is GREEN, two-sided, with the arming control present" - # `rsp` = 0 ON UNBARRIERED RECORDS, in every summary that printed it. A non-zero count - # would be an abort that did not fire, which is the one failure §3.3's unconditional - # arm cannot report by itself. - if grep -rhoE 'rsp=[0-9]+' MobileGL/MG_IntegrationTest/split-logs/ 2>/dev/null | grep -qvE 'rsp=0$'; then - echo "::warning::a scenario summary reports a non-zero rsp; under P5e every remaining pull is a BARRIERED row on the allowlist above, and the count belongs in the trailing inventory rather than in this lane" + # ---- P5e (gl), CONTRACT-P5E §7: MAGMA'S OWN LANE, EXPECTED RED ----------------------- + # + # The two DirectVulkan.Split.NamedBlit entries abort on GetFramebufferBindingSlot@Clear + # (VulkanRenderer.cpp:7648). That field retires in P5e ON ESPRYT and in P7 ON MAGMA, and + # FieldOwnership.def carries ONE retiring-phase string for both - so admitting the pair to + # keep them in the Espryt lane would forgive an Espryt Clear reading the frontend's binding + # slot again, which is exactly the regression fb's handle arm exists to prevent. Splitting + # the lane costs two entries; admitting the row would cost the gate. + # + # THE LABEL IS `integration-magma-split` AND THE SPELLING MATTERS: `ctest -L` is a REGEX, so + # a label named `integration-split-magma` is still matched by `-L integration-split` and the + # entries would never have left. Measured before the rename. + # + # IT IS ASSERTED RED, WITH ITS MARKER. "Magma is red" must not be allowed to decay into + # "Magma did not run": the step fails both when the run goes green (P7 landed early, or the + # entries stopped drawing) and when it goes red without the named abort in a private log. + - name: Integration-magma-split under strict - expected red until P7 (CONTRACT-P5E section 7) + working-directory: build-split + env: + MOBILEGL_ITEST_REQUIRE_GPU: "1" + MOBILEGL_IPC_STRICT_ERRORS: "1" + MOBILEGL_TRANSPORT: "inproc" + run: | + ulimit -c unlimited + rc=0 + ctest -L integration-magma-split --no-tests=error -j 2 > "${RUNNER_TEMP}/strict-magma.txt" 2>&1 || rc=$? + tail -5 "${RUNNER_TEMP}/strict-magma.txt" + if [ "${rc}" -eq 0 ]; then + echo "::error::integration-magma-split went GREEN under strict. Magma is in lockstep for the whole of P5e (ID-90) and GetFramebufferBindingSlot retires there in P7, so these entries are expected to abort. If P7 has landed, delete this step and fold the entries back into integration-split." + exit 1 fi - echo "integration-split under strict is GREEN with only the §7 allowlist admitted ($(wc -l < "${RUNNER_TEMP}/markers.txt") distinct marker(s))" + marker='Fatal{UnmigratedPipeInput, "GetFramebufferBindingSlot@Clear"}' + if ! grep -rqF "${marker}" MobileGL/MG_IntegrationTest/p5b-DirectVulkan-*.log 2>/dev/null; then + echo "::error::integration-magma-split is red but no private log carries ${marker} - the lane failed for some OTHER reason, which is a defect rather than the expected-red control" + grep -rhoE '(Fatal|Admitted)\{[A-Za-z]*, "[^"]*"\}' MobileGL/MG_IntegrationTest/p5b-DirectVulkan-*.log 2>/dev/null | sort | uniq -c | sort -rn | head + exit 1 + fi + echo "integration-magma-split is red by design on ${marker}" - name: Upload strict lane logs if: always() diff --git a/MobileGL/MG_Backend/MGPipe/PipeInputs.cpp b/MobileGL/MG_Backend/MGPipe/PipeInputs.cpp index bc8f9741..40d37938 100644 --- a/MobileGL/MG_Backend/MGPipe/PipeInputs.cpp +++ b/MobileGL/MG_Backend/MGPipe/PipeInputs.cpp @@ -74,6 +74,48 @@ namespace MobileGL::MG_Pipe { std::abort(); } + // P5e (gl), ID-117: THE ADMITTED MARKER, AND WHY IT IS ONLY THE TAG THAT CHANGED. + // + // `@` and the `[BARRIER-PULLED, …, retires in ]` tail are IDENTICAL + // to the Fatal above; the leading tag is `Admitted{` instead of `Fatal{`. Every filter + // written since P5c matches `Fatal{UnmigratedPipeInput`, so all of them keep meaning + // exactly "red" and none of them has to learn a new grammar to keep meaning it. A reader + // grepping for the pair still finds it, and the lane can ratchet on both sets with one + // regex per tag (ID-119's two-sided ratchet). + // + // THE DEDUPE IS NOT TIDINESS. An 852-draw Minecraft frame reaches an admitted readback + // row once per draw; without this, one frame writes 852 identical lines, the log file is + // the size of the run and the marker census cannot be read at all. So it is once per + // (field, verb) per process, which is the granularity the allowlist is written in. + // + // A PLAIN ARRAY, NOT AN ATOMIC, and that is the file's existing rule rather than a + // shortcut: CountBarrierPull is reachable only after the server stamped a verb boundary, + // which happens on the apply thread inside PipeApplier::ApplyOne, and g_residualPulls + // beside it is a plain Uint64 for the same reason. A racing writer here would at worst + // log a duplicate line, never lose one. + void AdmittedBarrierPullOnce(MGPipeInputField field, MGPipeVerb verb, Bool escalated) { + const SizeT fieldIndex = static_cast(field); + const SizeT verbIndex = static_cast(verb); + if (fieldIndex >= kMGPipeInputFieldCount || verbIndex >= kMGPipeVerbCount) return; + static Uint64 seen[(kMGPipeVerbCount * kMGPipeInputFieldCount + 63) / 64] = {}; + const SizeT bit = verbIndex * kMGPipeInputFieldCount + fieldIndex; + const Uint64 mask = Uint64{1} << (bit % 64); + if ((seen[bit / 64] & mask) != 0) return; + seen[bit / 64] |= mask; + // P5e (gl), ID-128: WHICH DISJUNCT ADMITTED IT, in the slot the grammar already has + // for the reason. `ADMITTED` means the generated table said so, and the lane can + // check that against `--print-admitted`. `ADMITTED-ESCALATED` means the table did + // NOT and the record was barriered by an escalation the table cannot see, which is a + // RUNTIME fact about that record's payload - so the lane must not look for it in a + // static list. Saying which is what keeps the lane's comparison exact instead of + // widening the list with every pair that could ever escalate. + MGLOG_W("MGPipe: Admitted{UnmigratedPipeInput, \"%s@%s\"} [BARRIER-PULLED, %s, " + "retires in %s]", + kMGPipeInputFieldNames[fieldIndex], MGPipeVerbName(verb), + escalated ? "ADMITTED-ESCALATED" : "ADMITTED", + kMGPipeFieldRetiringPhase[fieldIndex]); + } + // One place decides what a BARRIER-PULLED read does, so the field accessors and the // seven sticky forwards cannot drift apart on it. // @@ -89,8 +131,34 @@ namespace MobileGL::MG_Pipe { // torn or stale BY CONSTRUCTION and there is nothing for a counter to count. A // "count it" arm here would be a wrong picture with a number beside it. // - // rsp is therefore 0 on unbarriered records in every scenario summary (§7's pin): a - // non-zero count would be an abort that did not fire. + // P5e (gl), ID-119: THE OLD PIN HERE - "rsp is 0 on unbarriered records" - WAS VACUOUS + // AND HAS BEEN WITHDRAWN. The unbarriered arm below is [[noreturn]] and runs BEFORE + // ++g_residualPulls, so an unbarriered pull can never reach the counter whatever this + // function is written to do; the sentence was true of every possible implementation and + // therefore checked nothing. What rsp actually counts is BARRIERED pulls, and under the + // strict knob it counts exactly the ADMITTED ones, because every other barriered pull + // aborts two lines down. That is the form CONTRACT-P5E §7 now states and the lane checks. + // + // ---- P5e (gl), ID-117: AN ADMITTED PULL IS LOUD, NOT FATAL --------------------------- + // + // Before this, strict aborted on EVERY barrier-pulled read, admitted or not - which made + // the CI's allowlist comparison unreachable code (the run's rc != 0 exits first) and made + // "hard green" impossible with the knob as written. So there is a third state, and the + // two existing ones are untouched: + // + // unbarriered -> Fatal, no knob. The value is torn by construction. + // barriered, unadmitted -> Fatal under strict. A debt no phase has taken. + // barriered, admitted -> ONE MGLOG_W per (field, verb), and the entry completes. + // + // "Admitted" has three disjuncts and the third is a runtime one (ID-128): the generated + // table answers the first two, and the record's own escalation flag answers the third. + // + // An admitted pull is a debt this phase deliberately leaves standing: the field's row is + // BARRIER_PULLED, the verb's op is statically barriered so the client really is parked + // behind the record, and the field is inside the verb's own may-read mask - so the value + // is real, ordered and fresh, exactly ruling 4's "barriered records keep P5C semantics". + // MGPipeBarrierPullAdmitted is generated from those three tables (ID-116); there is no + // list here to drift. void CountBarrierPull(MGPipeInputField field, MGPipeVerb verb) { if (!MGPipeApplierCurrentRecordIsBarriered()) { StrictBarrierPullFatal(field, verb, "UNBARRIERED, the client did not fill it"); @@ -100,7 +168,21 @@ namespace MobileGL::MG_Pipe { MG_Util::PipeStats::AddCalls(MG_Util::PipeStats::CallClass::ResidualPulls, 1); } if (MG_Config::Ipc.StrictErrors) { - StrictBarrierPullFatal(field, verb, "MOBILEGL_IPC_STRICT_ERRORS=1"); + // THE THIRD DISJUNCT (P5e gl, ID-128), and it has to be asked at RUNTIME because + // it is a fact about this record's payload rather than about its opcode. The + // static table admits a pair when the verb's op waits (disjunct 1) or when the + // field's retiring phase is not this phase (disjunct 2); an escalated record is + // one the client parks behind for a reason only the payload knows - an open + // transform-feedback span, or a draw carrying client vertex arrays. Both are + // outside this phase by ruling (§5.7, ID-82), and the client-array read site + // aborts by its own name if it is ever applied unbarriered, so the pull is legal + // and P5e is not the phase that owes it. + const Bool statically = MGPipeBarrierPullAdmitted(field, verb); + const Bool escalated = MGPipeApplierCurrentRecordIsBarrieredByEscalation(); + if (!statically && !escalated) { + StrictBarrierPullFatal(field, verb, "MOBILEGL_IPC_STRICT_ERRORS=1"); + } + AdmittedBarrierPullOnce(field, verb, !statically); } } @@ -182,6 +264,17 @@ namespace MobileGL::MG_Pipe { void MGPipeServerStampVerbBoundary(MGPipeVerb verb) { PipeInputs& inputs = gPipeInputs; + // P5e (gl), ID-115: THE POSITIVE CONTROL'S ONLY HONEST SIGNAL, and it belongs HERE + // because this is the line the whole strict mechanism hangs off. The poison, rsp and + // the BARRIER-PULLED verdict are all reachable only after this stamp, and the monolith + // arm never stamps at all - so "the strict lane is green" and "strict was never armed" + // were observationally identical, which is how a lane whose seven passing entries + // included no record-carrying split GL scenario read as rigour. Behind Enabled(), which + // is the file's rule for counters (`rsp` beside it does the same) and keeps the stamp a + // table lookup and a branch-free fill when stats are off. + if (MG_Util::PipeStats::Enabled()) { + MG_Util::PipeStats::AddCalls(MG_Util::PipeStats::CallClass::ServerVerbBoundaries, 1); + } MGPipeFilledState& filled = MGPipeStampAccess::Filled(inputs); MGPipeStampAccess::SetVerb(inputs, verb); // Starts at 1 for MGPipeValidateForVerb's reason: FilledGen == 0 is "never filled" on diff --git a/MobileGL/MG_Impl/Pipe/PipeFill.cpp b/MobileGL/MG_Impl/Pipe/PipeFill.cpp index 983ffe5e..8e05a588 100644 --- a/MobileGL/MG_Impl/Pipe/PipeFill.cpp +++ b/MobileGL/MG_Impl/Pipe/PipeFill.cpp @@ -2680,6 +2680,51 @@ namespace MobileGL::MG_Pipe { "memo can now answer differently for the consumer signal, so that key input " "needs the unit case the paragraph above names"); + // ---- P5e (gl), ID-112: THE SAME TRIP WIRE FOR THE TWO ROWS THAT ONE CANNOT SEE ------ + // + // The assertion above is keyed on the EMITTER'S SUBSYSTEM, so it covers exactly the five + // P4a-family rows. GetBoundVertexArray (P3a's, emitted by BindVertexElements) and + // GetBufferBindingPoint (P5e sb's, emitted by SetShaderBuffers) sit outside + // kMGPipeP4aFamilySubsystems and had therefore no compile-time protection at all. + // + // WHY THAT IS A DEVICE CRASH AND NOT A STYLE POINT. This residual fill is MAGMA'S ONLY + // SOURCE for all seven pointer-backed rows, and Magma dereferences them on its first + // draw: it is in lockstep for the whole of P5e (ID-90) and reads them through + // MagmaP7AllocatorDebtScope. A package retiring a DirectGLES consumer that "tidied up" + // by deleting one of these two rows from EmittedCallSuppliesTheWholeField would not + // break the build - it would SIGSEGV Magma on a phone, which is the exact shape that + // cost this phase 38 scenarios once already (ID-107). So the seven are NAMED, and the + // naming is the deliverable: it converts the most likely mistake of every remaining + // package from a device crash into a build break. + // + // IF THIS ASSERTION FIRED ON YOU: the answer for each row is argued above + // EmittedCallSuppliesTheWholeField and it is the same argument every time - the field's + // storage is a frontend heap reference and no payload may carry a pointer. What retires + // a row is the phase where the BACKEND stops reading a frontend object (P7 for the + // texture/framebuffer/program mirrors, P8 for the VAO), never a consumer-side cleanup + // in the package you are writing. + constexpr MGPipeInputField kMGPipePointerBackedResidualRows[] = { + MGPipeInputField::GetBoundVertexArray, MGPipeInputField::GetBufferBindingPoint, + MGPipeInputField::GetFramebufferBindingSlot, MGPipeInputField::GetImageTextureBinding, + MGPipeInputField::GetTextureUnitObject, MGPipeInputField::GetProgramForDraw, + MGPipeInputField::GetProgramForDispatch, + }; + static_assert(sizeof(kMGPipePointerBackedResidualRows) / sizeof(MGPipeInputField) == 7, + "ID-112 names SEVEN pointer-backed residual rows; this list is the whole of " + "them and a row removed from it is a row with no trip wire"); + constexpr Bool NoPointerBackedRowIsWhollySupplied() { + for (const MGPipeInputField field : kMGPipePointerBackedResidualRows) { + if (EmittedCallSuppliesTheWholeField(field)) return false; + } + return true; + } + static_assert(NoPointerBackedRowIsWhollySupplied(), + "a pointer-backed residual row stopped being pulled (ID-112). This fill is " + "Magma's ONLY source for GetBoundVertexArray, GetBufferBindingPoint and the " + "five P4a-family mirrors, and Magma dereferences them on its first draw - so " + "this is a build break standing in for a device SIGSEGV. Retire the row in " + "the phase that stops the backend reading a frontend object (P7/P8)"); + struct ResidualFillPlan { Bool Valid = false; Uint64 PushMask = 0; diff --git a/MobileGL/MG_IntegrationTest/CMakeLists.txt b/MobileGL/MG_IntegrationTest/CMakeLists.txt index a2af3879..4d57f2de 100644 --- a/MobileGL/MG_IntegrationTest/CMakeLists.txt +++ b/MobileGL/MG_IntegrationTest/CMakeLists.txt @@ -2383,21 +2383,95 @@ if (MOBILEGL_BUILD_DISAGGREGATED) endif() # P5b measured named-blit blockers, exercising both backend bound-form lowerings. +# +# P5e (gl), CONTRACT-P5E §7: THE TWO BACKENDS GET DIFFERENT LABELS, because under strict they are +# answering different questions. +# +# Both DirectVulkan entries abort on GetFramebufferBindingSlot@Clear (VulkanRenderer.cpp:7648). +# That field's row retires in P5e ON ESPRYT and in P7 ON MAGMA, and FieldOwnership.def carries ONE +# retiring-phase string for both - so the derived allowlist cannot admit the pair without admitting +# it for Espryt too, where it would forgive exactly the regression fb's handle arm exists to +# prevent (an Espryt Clear reading the frontend's binding slot again would become a warning line). +# The alternative to a label is therefore not "admit one row"; it is "stop the Espryt lane from +# being able to see that row at all", which is a real loss of gate strength. +# +# So the lane is SPLIT rather than the allowlist WIDENED: `integration-split` stays a statement +# about Espryt and goes hard green, and the Magma entries get the expected-red step the contract +# already promises them for the backend it keeps in lockstep all phase (ID-90). if (MOBILEGL_BUILD_DISAGGREGATED) foreach(namedBlitBackend DirectGLES DirectVulkan) mgl_itest_join_environment(MGL_ITEST_NAMED_BLIT_ENVIRONMENT "MOBILEGL_BACKEND_TYPE=${namedBlitBackend}" "MOBILEGL_TRANSPORT=inproc" "MOBILEGL_ITEST_REQUIRE_GPU=1" "MGITEST_SPLIT_LANE=1" ${MGL_ITEST_CAPABILITY_ENV} ${MGL_ITEST_COMMON_ENV}) + # THE LABEL IS `integration-magma-split` AND NOT `integration-split-magma`, and that is not + # a preference: `ctest -L` takes a REGEX, not an exact name, so `-L integration-split` + # MATCHES a label spelled `integration-split-magma` as a substring. The obvious name would + # have left both entries in the Espryt lane while every listing showed them relabelled - a + # split that looks done and is not. Measured: with that spelling + # `ctest -N -L integration-split` still listed both DirectVulkan entries. + if (namedBlitBackend STREQUAL "DirectVulkan") + set(MGL_ITEST_NAMED_BLIT_LABELS "integration-magma-split") + else() + set(MGL_ITEST_NAMED_BLIT_LABELS "integration-split") + endif() foreach(namedBlitCase NamedBlitPreservesBindingsAndRestoresNextVerbsPixels NamedBlitDefaultEndpointPixels) gtest_discover_tests(MobileGLIntegrationTest TEST_PREFIX "${namedBlitBackend}.Split.NamedBlit." TEST_FILTER "F1WireScenario.${namedBlitCase}" DISCOVERY_TIMEOUT 30 PROPERTIES - LABELS "integration-split" + LABELS "${MGL_ITEST_NAMED_BLIT_LABELS}" TIMEOUT ${MGL_ITEST_TIMEOUT} ENVIRONMENT "${MGL_ITEST_NAMED_BLIT_ENVIRONMENT}\;MOBILEGL_LOG_FILE_PATH=${CMAKE_CURRENT_BINARY_DIR}/p5b-${namedBlitBackend}-${namedBlitCase}.log") endforeach() endforeach() endif() + +# ===================================================================================== +# P5e (gl), ID-115 / ID-119: THE STRICT LANE'S POSITIVE CONTROL, AND THE ONE COUNTING ENTRY +# ===================================================================================== +# +# ONE ENTRY, TWO JOBS, AND BOTH NEED THE SAME THING - a drawing split scenario that can read its +# own PipeStats window. +# +# ID-115: prove strict was ARMED. Of the seven entries that passed the strict lane before this +# phase, three were monolith transport (where nothing stamps a verb boundary and the whole +# mechanism is structurally unreachable), two self-skipped, one was a death test and one was a +# Python check - so "116/116" and "strict never ran on anything that draws" were the same +# observation. `vbs` on the summary line is the arming proof and this entry is where it is read. +# +# ID-119: the `rsp` pin. The old wording ("rsp = 0 on unbarriered records") was true of every +# possible implementation, because CountBarrierPull's unbarriered arm is [[noreturn]] and runs +# BEFORE the counter. The checkable statement is the relation to `draws`, which is what the +# device measured (rsp ~= the draw count under inproc, 0 under monolith). +# +# IT IS ITS OWN ENTRY WITH ITS OWN LOG PATH, NOT A WHOLE-LANE ENV FLIP. The library opens +# MOBILEGL_LOG_FILE_PATH with "w", so every process in a lane TRUNCATES it; two entries sharing +# one path under `ctest -j` race into an empty read that looks exactly like "the counter was +# never emitted" (Harness/PipeStatsWindow.h:19-24 has the long version). RESOURCE_LOCK is the +# same belt as the PersistentMapArm entry's. +# +# BLOCK PLACED AT THE END OF THE FILE ON PURPOSE (wave-3 integration): `pa`'s +# DirectGLES.Split.StrictProgramArm. block and `mv`'s multi-draw tiers are added inside the big +# disaggregated section above, so keeping this one textually apart lets all three merge cleanly. +if (MOBILEGL_BUILD_DISAGGREGATED) + mgl_itest_join_environment(MGL_ITEST_GLES_SPLIT_STRICT_ARMING_ENVIRONMENT + "MOBILEGL_BACKEND_TYPE=DirectGLES" "MOBILEGL_TRANSPORT=inproc" + "MOBILEGL_IPC_SERVER_PATH=${MGL_ITEST_SPLIT_SERVER_PATH}" "MGITEST_SPLIT_LANE=1" + "MGITEST_STRICT_ARMING_LANE=1" + "MOBILEGL_PIPE_STATS=1" "MOBILEGL_PIPE_STATS_PERIOD=1" + "MOBILEGL_LOG_FILE_PATH=${CMAKE_CURRENT_BINARY_DIR}/p5e-strict-arming-DirectGLES.log" + ${MGL_ITEST_CAPABILITY_ENV} ${MGL_ITEST_COMMON_ENV}) + + gtest_discover_tests(MobileGLIntegrationTest + TEST_PREFIX "DirectGLES.Split.StrictArming." + TEST_FILTER "TriangleScenario.TheServerStampedAVerbBoundaryOnThisDrawingFrame" + DISCOVERY_TIMEOUT 30 + PROPERTIES + LABELS "integration-gpu\;integration-split" + TIMEOUT ${MGL_ITEST_TIMEOUT} + RESOURCE_LOCK p5e-strict-arming-DirectGLES.log + ENVIRONMENT "${MGL_ITEST_GLES_SPLIT_STRICT_ARMING_ENVIRONMENT}" + ) +endif() diff --git a/MobileGL/MG_IntegrationTest/Harness/split_log_paths.py b/MobileGL/MG_IntegrationTest/Harness/split_log_paths.py index c082f73d..c6a38e70 100644 --- a/MobileGL/MG_IntegrationTest/Harness/split_log_paths.py +++ b/MobileGL/MG_IntegrationTest/Harness/split_log_paths.py @@ -33,6 +33,150 @@ def paths(document): return split +# P5e (gl), ID-119: THE MARKER GRAMMAR, PARSED WHERE IT IS WRITTEN. +# +# MG_Backend/MGPipe/PipeInputs.cpp writes exactly two shapes and they differ only in the leading +# tag and the reason, which is what lets every filter written since P5c keep meaning "red": +# +# MGPipe: Fatal{UnmigratedPipeInput, "@"} [BARRIER-PULLED, , retires in ] +# MGPipe: Admitted{UnmigratedPipeInput, "@"} [BARRIER-PULLED, ADMITTED[-ESCALATED], retires in ] +MARKER_RE = re.compile( + r"(Fatal|Admitted)\{UnmigratedPipeInput,\s*\"([^\"@]+)@([^\"]+)\"\}" + r"(?:\s*\[BARRIER-PULLED,\s*([^,\]]+))?") + + +def marker_log_paths(document): + """{entry: absolute MOBILEGL_LOG_FILE_PATH} for EVERY entry that declares one. + + P5e (gl), ID-119: THE LOG SET COMES FROM ctest, NOT FROM A DIRECTORY. The CI step used to + grep MobileGL/MG_IntegrationTest/split-logs/, which holds 90 of the lane's entries. The ones + it missed were the F1. readback block, both NamedBlit pairs, the four Ct. entries and + PersistentMapArm - i.e. precisely the readback population the allowlist is ABOUT, plus the + only DirectVulkan entries in the lane. A directory is a guess about where the lane put its + logs; `ctest --show-only=json-v1` is the lane saying where it put them. + + Unlike paths() above this does not restrict itself to DirectGLES.Split. entries and does not + validate ownership - that is paths()' job and SplitLogPaths.PrivateAndDistinct runs it. This + one answers "which files might carry a marker", for every backend prefix the lane has.""" + logs = {} + for test in document["tests"]: + props = {p["name"]: p["value"] for p in test.get("properties", [])} + values = [v.split("=", 1)[1] for v in props.get("ENVIRONMENT", []) + if v.startswith("MOBILEGL_LOG_FILE_PATH=")] + if len(values) != 1 or not values[0]: + continue + logs[test["name"]] = str(Path(values[0]).resolve()) + return logs + + +def read_pair_set(path): + """A committed `@` set, one per line; blank lines and # comments ignored.""" + pairs = set() + for line in Path(path).read_text().splitlines(): + line = line.split("#", 1)[0].strip() + if line: + pairs.add(line) + return pairs + + +def classify_markers(logs): + """(fatal, admitted, escalated, scanned) - each a {pair: sorted entry names}. + + Counted BY ENTRY and not by line: the runtime dedupes each (field, verb) once per process, + so a line count would only ever say how many processes ran.""" + fatal, admitted, escalated = {}, {}, {} + scanned = [] + for name in sorted(logs): + path = logs[name] + if not Path(path).is_file(): + continue + scanned.append(name) + text = Path(path).read_text(errors="replace") + for tag, field, verb, why in MARKER_RE.findall(text): + pair = f"{field}@{verb}" + if tag == "Fatal": + fatal.setdefault(pair, set()).add(name) + elif (why or "").strip() == "ADMITTED-ESCALATED": + escalated.setdefault(pair, set()).add(name) + else: + admitted.setdefault(pair, set()).add(name) + return ({p: sorted(e) for p, e in fatal.items()}, + {p: sorted(e) for p, e in admitted.items()}, + {p: sorted(e) for p, e in escalated.items()}, + scanned) + + +def print_marker_table(title, table): + print(f" {title}: {len(table)} distinct pair(s)") + for pair in sorted(table, key=lambda p: (-len(table[p]), p)): + print(f" {len(table[pair]):4d} {pair}") + + +def markers(document, selector, allowed_path, expected_path, require_no_fatal): + """THE TWO-SIDED RATCHET (ID-119). + + One side: a marker that is not admitted fails the lane. That half existed in spirit but was + unreachable code, because strict aborted on every barrier-pulled read and the run's rc took + the step out before the comparison (ID-117 fixed the knob; this reads the result). + + The other side, which is the new half: an admitted pair that NO LONGER APPEARS must be + removed from the expected set. Without it the lane rots green - a debt retires, its marker + stops being written, and the expected list quietly becomes a list of things that used to + happen, so the next regression to re-introduce one of them reads as "expected".""" + logs = {name: path for name, path in marker_log_paths(document).items() + if re.search(selector, name)} + if not logs: + raise ValueError(f"no lane entry matching /{selector}/ declares a " + "MOBILEGL_LOG_FILE_PATH, so there is nothing to read markers out of") + fatal, admitted, escalated, scanned = classify_markers(logs) + print(f"SplitLogPaths markers: {len(scanned)} of {len(logs)} selected entries wrote a log") + print_marker_table("Fatal{UnmigratedPipeInput", fatal) + print_marker_table("Admitted{UnmigratedPipeInput", admitted) + print_marker_table("Admitted{UnmigratedPipeInput (ESCALATED)", escalated) + if not scanned: + raise ValueError("not one selected entry wrote its private log: the marker census is " + "EMPTY because nothing was read, which is not the same statement as " + "'no marker fired' and must never be reported as one") + + problems = [] + if require_no_fatal and fatal: + problems.append("%d Fatal marker(s) - each is a field an apply still reads out of client " + "memory with nothing admitting it: %s" + % (len(fatal), "; ".join(f"{p} ({len(e)} entries, e.g. {e[0]})" + for p, e in sorted(fatal.items())))) + + # An ADMITTED (non-escalated) marker claims the GENERATED table admitted it, so it must be in + # that table. An ADMITTED-ESCALATED one does not: it is a runtime fact about the record's + # payload (an open XFB span, a draw with client arrays) that no table indexed by + # (field, verb) can carry, so looking for it in a static list would mean widening that list + # with every pair that could ever escalate - which would forgive the ordinary draw path too. + allowed = read_pair_set(allowed_path) + outside = sorted(set(admitted) - allowed) + if outside: + problems.append("%d marker(s) tagged ADMITTED are not in the generated allowlist, so the " + "committed PipeFieldOwnership.inc and the generator disagree: %s" + % (len(outside), ", ".join(outside))) + + expected = read_pair_set(expected_path) + observed = set(admitted) | set(escalated) + appeared = sorted(observed - expected) + vanished = sorted(expected - observed) + if appeared: + problems.append("%d admitted pair(s) the lane has not seen before: %s. Each is a debt " + "somebody now owes - add it to %s with the phase that retires it, or " + "retire it." + % (len(appeared), ", ".join(appeared), Path(expected_path).name)) + if vanished: + problems.append("%d expected pair(s) no longer appear: %s. Remove them from %s in the " + "commit that retired them - an expected set that keeps rows nothing " + "writes any more is how this lane rots green." + % (len(vanished), ", ".join(vanished), Path(expected_path).name)) + if problems: + raise ValueError("the strict lane's marker ratchet: " + " | ".join(problems)) + print(f"SplitLogPaths markers: ratchet OK - {len(observed)} admitted pair(s), " + f"{len(fatal)} fatal pair(s)") + + def main(): mode = sys.argv[1] if mode == "check": @@ -41,6 +185,10 @@ def main(): selected = paths(json.loads(data)) print(f"SplitLogPaths: {len(selected)} entries, {len(set(selected.values()))} distinct private paths") return + if mode == "markers": + markers(json.loads(Path(sys.argv[2]).read_text()), sys.argv[3], sys.argv[4], sys.argv[5], + len(sys.argv) > 6 and sys.argv[6] == "no-fatal") + return selected = paths(json.loads(Path(sys.argv[2]).read_text())) selected = {name: path for name, path in selected.items() if re.search(sys.argv[3], name)} if not selected: diff --git a/MobileGL/MG_IntegrationTest/Harness/strict-expected-markers.txt b/MobileGL/MG_IntegrationTest/Harness/strict-expected-markers.txt new file mode 100644 index 00000000..b96fa532 --- /dev/null +++ b/MobileGL/MG_IntegrationTest/Harness/strict-expected-markers.txt @@ -0,0 +1,45 @@ +# The admitted barrier-pull markers the integration-split lane ACTUALLY WRITES under +# MOBILEGL_IPC_STRICT_ERRORS=1, one `@` per line. +# +# P5e (gl), ruling ID-119. THIS IS THE OTHER SIDE OF THE RATCHET, and it is the side that was +# missing. The generated allowlist (scripts/gen_pipe_field_ownership.py --print-admitted) says +# which pairs MAY be admitted - it is a statement about the tables. This file says which ones the +# lane DOES produce - a statement about the run. A lane checked only against the first kind +# ROTS GREEN: a debt retires, its marker stops being written, and nothing notices, so the day a +# regression re-introduces that read the lane calls it "expected". +# +# So Harness/split_log_paths.py's `markers` mode fails BOTH ways: +# - a pair here that no longer appears -> delete it, in the commit that retired it; +# - a pair that appears and is not here -> add it with the phase that owes it, or retire it. +# +# HOW TO REFRESH (never by hand from a guess): +# ctest -L integration-split --show-only=json-v1 > lane.json +# MOBILEGL_IPC_STRICT_ERRORS=1 ctest -L integration-split -j 4 +# python3 MobileGL/MG_IntegrationTest/Harness/split_log_paths.py markers lane.json . \ +# <(python3 scripts/gen_pipe_field_ownership.py --print-admitted) this-file +# and put the census it prints here. +# +# --------------------------------------------------------------------------------------------- +# MEASURED AT p5e/gl's BASE, 7c6f6886, WHICH IS BEFORE pa AND mv LANDED. That is stated rather +# than hidden: the wave-3 integration commit retires GetProgramForDraw@DrawArrays, +# GetProgramForDispatch@DispatchCompute and the ordinary GetBoundVertexArray@DrawArrays, so the +# three escalated rows below WILL stop appearing and the ratchet will say so by name. Removing +# them is part of that merge, not a failure of it. +# --------------------------------------------------------------------------------------------- +# +# Admitted by the generated table (disjuncts 1 and 2 of ID-116 / ID-125): +GetBufferBindingSlot@ReadPixels +GetFramebufferBindingSlot@ReadPixels +GetProgramObject@ShaderStorageBlockBinding +GetTextureObject@CopyImageSubData +GetTextureUnitObject@CopyTexImage2D +GetTransformFeedbackProgram@DrawArrays +ValidateProgramName@ShaderStorageBlockBinding +# +# Admitted by ESCALATION only (disjunct 3, ID-128): the record was barriered because its payload +# said so - an open transform-feedback span, or a draw carrying client vertex arrays - which no +# table indexed by (field, verb) can see. All three are pulls on the draw verb by entries that +# are NOT the ordinary draw path. +GetBoundVertexArray@DrawArrays +GetBufferBindingPoint@DrawArrays +GetProgramForDraw@DrawArrays diff --git a/MobileGL/MG_IntegrationTest/Scenarios/TriangleScenario.cpp b/MobileGL/MG_IntegrationTest/Scenarios/TriangleScenario.cpp index 490822b4..a50e0c50 100644 --- a/MobileGL/MG_IntegrationTest/Scenarios/TriangleScenario.cpp +++ b/MobileGL/MG_IntegrationTest/Scenarios/TriangleScenario.cpp @@ -47,6 +47,7 @@ #include #include "../Harness/HeadlessGL.h" +#include "../Harness/PipeStatsWindow.h" #include "../Harness/ScenarioFixture.h" #include "../Harness/SplitLane.h" #include "../Harness/WireLedgerChecks.h" @@ -285,4 +286,107 @@ void main() { oColor = vec4(vColor, 1.0); } } } + // =================================================================================== + // P5e (gl), ID-115 / ID-119: THE STRICT LANE'S POSITIVE CONTROL + // =================================================================================== + // + // WHY THE LANE NEEDS ONE AT ALL. Of the seven entries that passed `integration-split` under + // MOBILEGL_IPC_STRICT_ERRORS=1 before this phase, three were MOBILEGL_TRANSPORT=monolith - + // where the server never stamps a verb boundary, so the entire strict mechanism is + // structurally unreachable - two self-skipped, one was a death test and one was a Python + // check. Not one was a record-carrying split GL scenario. So "116/116 under strict" and + // "strict was never armed on anything that draws" were indistinguishable from outside, and + // a gate that cannot tell those apart is not a gate (ID-115). + // + // WHAT IT ASSERTS, AND WHY EACH PART IS NECESSARY. + // `vbs` > 0 - the server stamped at least one verb boundary IN THIS ENTRY. Everything + // strict checks is downstream of that stamp. This is the arming proof and + // it is deliberately not rsp: rsp goes to ZERO exactly when the phase + // SUCCEEDS, so a control built on it would start failing on the day the + // debt is paid. + // `draws` > 0 - and the entry really drew, so "armed" is not "armed on a clear". + // rsp vs draws (ID-119) - the old pin, "rsp = 0 on unbarriered records", was VACUOUS: the + // unbarriered arm of CountBarrierPull is [[noreturn]] and runs before the + // counter, so no implementation could ever have made it false. What is + // checkable is the SHAPE: while the draw path's debt is unretired every draw + // pulls, so rsp scales with draws; when it retires, rsp goes to 0. The + // measured device numbers are the same statement - rsp was ~852 (the draw + // count) under inproc and 0 under monolith. So the assertion is "rsp is 0 or + // it scales with draws", and the retirement is visible as the transition. + // + // THE WINDOW IS READ, NOT INFERRED. `found == false` means the stats channel never reached + // this process, which is a DIFFERENT failure from "the counter read zero" and is reported as + // one - otherwise a lane that lost MOBILEGL_PIPE_STATS would report the arming proof as a + // clean zero. The lane entry that runs this case owns its own MOBILEGL_LOG_FILE_PATH for + // PipeStatsWindow.h's reason: the library opens it "w", so two entries sharing a path under + // `ctest -j` race into an empty read that looks exactly like "never emitted". + TEST_F(TriangleScenario, TheServerStampedAVerbBoundaryOnThisDrawingFrame) { + if (!Ready() || IsSkipped()) return; + + const std::string skip = SplitLane::SkipReasonForSplitOnlyAssertions(); + if (!skip.empty()) { + // The monolith arms' skip twin (G2/G14), and it is LOUD rather than silent because + // this case's whole subject is a counter that is zero there BY CONSTRUCTION - + // nothing stamps a verb boundary in a monolith build, and a case that "passed" + // by reading that zero would be the exact confusion it exists to prevent. + RecordProperty("strict_arming_skip_reason", skip); + GTEST_SKIP() << "the server verb stamp exists only under split: " << skip; + return; + } + // ONE LANE OWNS THIS CASE, and it declares itself by name the way MGITEST_PMAP_LANE does. + // TriangleScenario.* is discovered by several blocks (the plain split lane, the small-ring + // lane, the monolith lanes), and every one of them gives its entries a private + // MOBILEGL_LOG_FILE_PATH - so "is there a log path" cannot distinguish the lane that + // asked for counters from the lanes that merely have somewhere to log. Reading the window + // in those would assert on a summary line nobody enabled. + if (!SplitLane::MarkerIsOne("MGITEST_STRICT_ARMING_LANE")) { + GTEST_SKIP() << "not the strict-arming lane: this case reads a PipeStats window and " + "only DirectGLES.Split.StrictArming. sets MOBILEGL_PIPE_STATS=1, " + "MOBILEGL_PIPE_STATS_PERIOD=1 and a log path of its own"; + return; + } + if (PipeStatsWindow::LibraryLogPath().empty()) { + GTEST_SKIP() << "the lane configured no MOBILEGL_LOG_FILE_PATH, and the library's " + "summary line is the only channel this module has for PipeStats"; + return; + } + + // Close the setup window, run the workload, close it again: the LAST line then covers + // the draw and nothing else (PipeStatsWindow.h's "since the previous line"). + Gl().EndFrame(); + const Image image = ClearThenDrawThenRead(0.0f, 0.0f, 1.0f); + EXPECT_EQ(FirstGLError(), 0u); + ExpectTriangleInterior(image, "green", "the drawing frame the counters are taken over"); + Gl().EndFrame(); + + const PipeStatsWindow::Window window = PipeStatsWindow::LastFromLaneLog(); + ASSERT_TRUE(window.found) + << "the library emitted no `MGPipe stats:` line, so this lane's arming proof is " + "MISSING rather than zero - check MOBILEGL_PIPE_STATS=1, " + "MOBILEGL_PIPE_STATS_PERIOD=1 and this entry's private MOBILEGL_LOG_FILE_PATH"; + + const long long draws = PipeStatsWindow::CounterOrAbsent(window, "draws"); + const long long stamps = PipeStatsWindow::CounterOrAbsent(window, "vbs"); + const long long residual = PipeStatsWindow::CounterOrAbsent(window, "rsp"); + RecordProperty("pipe_stats_window", window.line); + RecordProperty("server_verb_boundaries", std::to_string(stamps)); + RecordProperty("residual_pulls", std::to_string(residual)); + + EXPECT_GT(draws, 0) << "no draw reached the instrumented entry point in the window this " + "case took, so there is nothing for the arming proof to be about: " + << window.line; + EXPECT_GT(stamps, 0) + << "the server stamped NO verb boundary on a drawing split entry. Every strict check " + "- the poison, rsp, the BARRIER-PULLED verdict - is downstream of that stamp, so " + "a green strict lane containing only entries like this one would mean the knob " + "was never armed rather than that the debt was paid (ID-115): " + << window.line; + EXPECT_TRUE(residual == 0 || residual >= draws) + << "rsp neither scales with draws nor is zero (" << residual << " vs " << draws + << "). ID-119: while this phase's draw-path debt is unretired every draw pulls at " + "least one BARRIER-PULLED row, and the retirement is visible as rsp ceasing to " + "scale with draws - a value strictly between is neither state: " + << window.line; + } + } // namespace MGITest diff --git a/MobileGL/MG_Pipe/PipeApply.cpp b/MobileGL/MG_Pipe/PipeApply.cpp index fb42b14f..2fca9c03 100644 --- a/MobileGL/MG_Pipe/PipeApply.cpp +++ b/MobileGL/MG_Pipe/PipeApply.cpp @@ -3031,6 +3031,11 @@ namespace MobileGL::MG_Pipe { // MGPipeBarriered in the sink's ApplyOne. namespace { thread_local Bool g_currentRecordBarriered = true; + // P5e (gl), ID-128. FALSE IS THE DEFAULT AND IT IS THE STRICT ANSWER: "this record was + // barriered by escalation" admits a pull that neither the wait class nor the retiring + // phase admits, so a reader that runs before any writer must say no. The stamp above + // defaults the other way because ITS safe answer is "the client is parked". + thread_local Bool g_currentRecordBarrieredByEscalation = false; } // namespace Bool MGPipeApplierCurrentRecordIsBarriered() { return g_currentRecordBarriered; } @@ -3039,6 +3044,14 @@ namespace MobileGL::MG_Pipe { g_currentRecordBarriered = barriered; } + Bool MGPipeApplierCurrentRecordIsBarrieredByEscalation() { + return g_currentRecordBarrieredByEscalation; + } + + void MGPipeApplierSetCurrentRecordBarrieredByEscalation(Bool escalated) { + g_currentRecordBarrieredByEscalation = escalated; + } + // ================================================================================ // w3: the shader CSO, the two program bindings and the default uniform block // diff --git a/MobileGL/MG_Pipe/PipeApply.h b/MobileGL/MG_Pipe/PipeApply.h index 8e47e222..a791c97b 100644 --- a/MobileGL/MG_Pipe/PipeApply.h +++ b/MobileGL/MG_Pipe/PipeApply.h @@ -948,6 +948,32 @@ namespace MobileGL::MG_Pipe { // the call site (it is the line ra rebases onto); c0e owns the storage so both compile. void MGPipeApplierSetCurrentRecordBarriered(Bool barriered); + // ---- P5e (gl), ID-128: WAS THIS RECORD BARRIERED BY ESCALATION? ---------------------- + // + // MGPipeBarriered is the static wait class PLUS two payload-derived escalations (ID-83): an + // open transform-feedback span makes every context verb inside it barriered, and a draw + // carrying client vertex arrays makes that draw barriered. "Escalated" is therefore exactly + // + // MGPipeBarriered(op, payload, st) && MGPipeWaitClassFor(op) == kWaitNone + // + // and BOTH HALVES ARE ALREADY COMPUTED on every record - ApplyOne computes the predicate + // unconditionally for ID-103's reason and the static class is a table - so this is a bit + // carried beside the existing stamp rather than new plumbing. + // + // IT IS A SEPARATE FLAG AND NOT A REFINEMENT OF THE ONE ABOVE, because the two answer + // different questions. The stamp above answers "is the client parked behind this record", + // which the allocator guard and the frontend-keyed registry guard ask. This one answers "and + // was it parked for a reason the STATIC table cannot see", which only the strict knob asks - + // and it asks because the escalations happen exactly for XFB-active and client-array draws, + // both of which CONTRACT-P5E puts outside this phase (§5.7 and ID-82). A pull on such a + // record is a debt some later phase owes, not a migration P5e skipped. + // + // FALSE IS THE DEFAULT, which is the opposite of the stamp's default and deliberately so: + // "not escalated" is the answer that admits nothing, so a reader that runs before any writer + // is strict rather than lax. + Bool MGPipeApplierCurrentRecordIsBarrieredByEscalation(); + void MGPipeApplierSetCurrentRecordBarrieredByEscalation(Bool escalated); + // THE CLIENT'S HALF OF THE WAIT RULE IS NOT LANDED YET, AND THIS CONSTANT IS THAT FACT. // MGPipeBarriered above describes what the client WILL do; until package ra changes // EmitAndWaitTails the client still blocks after every record, so the answer the server diff --git a/MobileGL/MG_Pipe/PipeCalls.def b/MobileGL/MG_Pipe/PipeCalls.def index db4083cf..c8b1b808 100644 --- a/MobileGL/MG_Pipe/PipeCalls.def +++ b/MobileGL/MG_Pipe/PipeCalls.def @@ -236,7 +236,22 @@ /* only way bytes reach it - a blobref here would be a SECOND way to say the same thing. */ \ X(ResourceFlushRange, MGPFlushRange, kCtxObject, kNone, kWaitNone) \ X(ResourceReadback, MGPReadback, kCtxObject, kReplySlot, kWaitReply) \ - X(ResourceCopyRegion, MGPCopyRegion, kCtxObject, kNone, kWaitNone) \ + /* P5e (gl), ID-118: kWaitNone -> kWaitApplied, AND IT IS THE FIELD'S RETIRING PHASE THAT */ \ + /* forces it. This row's verb is CopyImageSubData, whose apply reads GetTextureObject - */ \ + /* a BARRIER_PULLED row whose retiring phase is P7, not P5e. Left kWaitNone, the flip */ \ + /* would make a genuinely UNBARRIERED record read client memory: an unconditional Fatal */ \ + /* (PipeInputs.cpp), no knob, for two whole phases. The alternative was to special-case */ \ + /* the field into section 7's allowlist, which ID-118 refused: the allowlist is DERIVED */ \ + /* (ID-116), and an exception written into it would be a real defect kept quiet rather */ \ + /* than a debt stated. With the wait class moved, the derivation admits the pair with no */ \ + /* exception at all and P7 retires the field on its own schedule. */ \ + /* kWaitApplied AND NOT kWaitReply: the call posts no reply slot and needs no answer - the */ \ + /* client parks until the record applies, which is exactly what CopyFramebufferToTexture */ \ + /* below already does for the two framebuffer-sourced copies. Same verb class */ \ + /* (kBlitOrCopy), same shape, a wait that is already carried in this lane. THE COST IS */ \ + /* MEASURED, NOT ASSUMED: glCopyImageSubData is zero per frame in the Minecraft 26.3-rc-3 */ \ + /* scene (~849 draws/frame), so the wait is not on any per-frame path. */ \ + X(ResourceCopyRegion, MGPCopyRegion, kCtxObject, kNone, kWaitApplied) \ X(GenerateMipmap, MGPMipPlan, kCtxObject, kNone, kWaitApplied) \ X(GetTextureImage, MGPReadbackInfo, kCtxObject, kReplySlot, kWaitReply) \ /* ---- context: transfer calls that read whole-context state, and the commands ---- */ \ diff --git a/MobileGL/MG_Pipe/generated/PipeFieldOwnership.inc b/MobileGL/MG_Pipe/generated/PipeFieldOwnership.inc index 1aac550c..7d922734 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] = { + {{0x5808402000000140ull, 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 + {{0x5800402000000100ull, 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 + {{0x5800402000000100ull, 0x0000000000000000ull}}, // BlitFramebuffer + {{0x0000000000000000ull, 0x0000000000000000ull}}, // BlitNamedFramebuffer + {{0x5800c02000300180ull, 0x0000000000000000ull}}, // CopyTexImage2D + {{0x0000000000000000ull, 0x0000000000000000ull}}, // CopyTexSubImage2D + {{0x5800c02000300180ull, 0x0000000000000000ull}}, // CopyImageSubData + {{0x5800c02000300180ull, 0x0000000000000000ull}}, // GenerateMipmap + {{0x5800c02000300140ull, 0x0000000000000000ull}}, // ReadPixels + {{0x0000000000000000ull, 0x0000000000000000ull}}, // GetTexImage + {{0x5800c02000300140ull, 0x0000000000000000ull}}, // GetTextureImage + {{0x5800402000000140ull, 0x0000000000000000ull}}, // DispatchCompute + {{0x0000000000000000ull, 0x0000000000000000ull}}, // DispatchComputeIndirect + {{0x5800402000000100ull, 0x0000000000000000ull}}, // MemoryBarrier + {{0x0000000000000000ull, 0x0000000000000000ull}}, // MemoryBarrierByRegion + {{0x5800402000000100ull, 0x0000000000000000ull}}, // BindImageTexture + {{0x0000000000000000ull, 0x0000000000000000ull}}, // GetIntegeri_v + {{0x5800c02000300100ull, 0x0000000000000000ull}}, // ShaderStorageBlockBinding + {{0x5800402000000100ull, 0x0000000000000000ull}}, // FenceSync + {{0x5800402000000100ull, 0x0000000000000000ull}}, // ClientWaitSync + {{0x5800402000000100ull, 0x0000000000000000ull}}, // WaitSync + {{0x5800402000000100ull, 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 + {{0x5800402000000100ull, 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 = 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. +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_Pipe/generated/PipeWire.inc b/MobileGL/MG_Pipe/generated/PipeWire.inc index d1bb7246..906e7f59 100644 --- a/MobileGL/MG_Pipe/generated/PipeWire.inc +++ b/MobileGL/MG_Pipe/generated/PipeWire.inc @@ -428,7 +428,7 @@ inline constexpr Uint8 kMGPipeWaitClasses[static_cast(MGPWireOp::kOpCount /* 50 ResourceSubDataComplete */ static_cast(kWaitNone), /* 51 ResourceFlushRange */ static_cast(kWaitNone), /* 52 ResourceReadback */ static_cast(kWaitReply), - /* 53 ResourceCopyRegion */ static_cast(kWaitNone), + /* 53 ResourceCopyRegion */ static_cast(kWaitApplied), /* 54 GenerateMipmap */ static_cast(kWaitApplied), /* 55 GetTextureImage */ static_cast(kWaitReply), /* 56 Blit */ static_cast(kWaitNone), diff --git a/MobileGL/MG_Remote/CONTRACT-P5E.md b/MobileGL/MG_Remote/CONTRACT-P5E.md index a33de58e..36a3dac0 100644 --- a/MobileGL/MG_Remote/CONTRACT-P5E.md +++ b/MobileGL/MG_Remote/CONTRACT-P5E.md @@ -474,16 +474,56 @@ BRIEF-P5E per package. `MOBILEGL_PIPE_VERIFY` forces lockstep (`ConfigLoader.cpp ## §7 The strict gate -`integration-split-strict` (`.github/workflows/test.yml:1140-1206`) becomes a HARD GREEN lane for -the Espryt run-ahead server: with `MOBILEGL_IPC_STRICT_ERRORS=1` and the caps bit published, every -scenario must complete and every `[BARRIER-PULLED, ...]` marker in a private log is red. Because -§3.3 aborts on an unbarriered pull regardless of the knob, strict adds only the barriered rows' -pulls (readbacks, GenerateMipmap until tx2, XFB, CopyTex, set_storage_block_binding) — the lane's -step lists those rows as the ONLY admitted markers (an allowlist by `@`) and fails on -any other. A revert of any handle arm in vi/sb/pg/tx2/fb goes red HERE, by field and verb, not in -a picture. Magma keeps the expected-red step. `rsp` on unbarriered records is 0 in every scenario -summary (pinned: a non-zero count would be a Fatal that did not fire). The `PipeSlotPeek` harness -asserts zero scope entries per frame on the draw path. +`integration-split-strict` (`.github/workflows/test.yml`) becomes a HARD GREEN lane for the Espryt +run-ahead server: with `MOBILEGL_IPC_STRICT_ERRORS=1` and the caps bit published, every scenario +must complete. Because §3.3 aborts on an unbarriered pull regardless of the knob, strict adds only +the barriered rows' pulls, and a revert of any handle arm in vi/sb/pg/tx2/fb goes red HERE, by +field and verb, not in a picture. The `PipeSlotPeek` harness asserts zero scope entries per frame +on the draw path. + +**The allowlist is DERIVED, not written** (ID-116, refined by ID-125 and ID-128). A +`@` pull is ADMITTED iff the field's ownership row is `BARRIER_PULLED`, the verb has a +stamp row, the field is inside `kMGPipeClassFieldMask[class of verb]`, and any one of: + +1. the verb's wire op is statically barriered (`MGPipeWaitClassFor(op) != kWaitNone`); +2. the field's retiring phase does not name P5e — a debt some later phase owes; +3. the record was barriered BY ESCALATION (`MGPipeBarriered(op, payload, st)` true while the op is + `kWaitNone`): an open transform-feedback span or a draw carrying client vertex arrays, both of + which this contract puts outside P5e (§5.7, ID-82). + +Disjuncts 1 and 2 are static and generated by `scripts/gen_pipe_field_ownership.py` into +`MGPipeBarrierPullAdmitted(field, verb)`; `--print-admitted` gives CI the same table. Disjunct 3 is +a fact about the record and is stamped beside the barriered stamp in `PipeApplier::ApplyOne`. An +admitted pull is **loud, not fatal** (ID-117): one deduped `Admitted{UnmigratedPipeInput, +"@"} [BARRIER-PULLED, ADMITTED|ADMITTED-ESCALATED, retires in ]` per process, keeping +the `Fatal{UnmigratedPipeInput` grammar so every filter written since P5c still means "red". + +**The lane is a two-sided ratchet** (ID-119). Its log set comes from +`ctest --show-only=json-v1`, not from a directory — the directory form missed 26 of the entries, +exactly the readback population the allowlist is about. An unadmitted marker fails; so does an +admitted pair the expected set (`MG_IntegrationTest/Harness/strict-expected-markers.txt`) does not +carry, AND an expected pair that no longer appears, so the lane cannot rot green. + +**The `rsp` pin, restated** (ID-119). The former pin — "`rsp` is 0 on unbarriered records" — was +VACUOUS: `CountBarrierPull`'s unbarriered arm is `[[noreturn]]` and runs before `++g_residualPulls`, +so it was true of every possible implementation. What is checkable: `rsp` counts barriered pulls +only, and under the strict knob every one it counts is an ADMITTED pull, because the rest abort. +Its shape is asserted against `draws` rather than against 0 — `rsp == 0 || rsp >= draws` — since +the draw path's retirement is observable as `rsp` ceasing to scale with `draws` (measured on the +device: `rsp` ~= the draw count under inproc, 0 under monolith). + +**The lane has a positive control** (ID-115). `DirectGLES.Split.StrictArming.` runs one drawing +inproc entry with `MOBILEGL_PIPE_STATS=1`, `MOBILEGL_PIPE_STATS_PERIOD=1` and a private log path, +and asserts `vbs > 0` — the server stamped a verb boundary. Everything strict checks is downstream +of that stamp and the monolith arm never stamps, so without it "the lane is green" and "strict was +never armed" are the same observation. + +**Magma keeps the expected-red step, in a lane of its own.** The two `DirectVulkan.Split.NamedBlit` +entries carry `integration-magma-split` (so spelled: `ctest -L` is a regex and +`-L integration-split` matches `integration-split-magma`) and are asserted RED on +`Fatal{UnmigratedPipeInput, "GetFramebufferBindingSlot@Clear"}`. Admitting that pair instead would +forgive the same read on Espryt, where it is this phase's debt — one retiring-phase string serves +both backends. --- @@ -499,9 +539,29 @@ asserts zero scope entries per frame on the draw path. re-derived as `MGPipeBarriered`. 7. **§3.3's state note** is retired by fb (§5.4). 8. **`FieldOwnership.def`**: `GetBoundVertexArray`, `GetTextureUnitObject`, `GetImageTextureBinding`, `GetFramebufferBindingSlot`, `GetProgramForDraw/Dispatch`, `GetBufferBindingPoint` gain retiring - phase "P5e (Espryt unbarriered), P7 (Magma)"; `GetBufferBindingPointCount`'s forward → FATAL under - split; `GetTransformFeedbackProgram`, `GetProgramObject`, `GetTextureObject`, `ValidateProgramName`, - `HasOpenTransformFeedbackSpan`, `RecordError` keep their rows (barriered-only readers). + phase "P5e (Espryt unbarriered), P7 (Magma)"; ~~`GetBufferBindingPointCount`'s forward → FATAL under + split~~ (**UNLANDED — see below**); `GetTransformFeedbackProgram`, `GetProgramObject`, + `GetTextureObject`, `ValidateProgramName`, `HasOpenTransformFeedbackSpan`, `RecordError` keep + their rows (barriered-only readers). + + > **UNLANDED, and deliberately so (P5e gl, ruling ID-120). Lands with P7/P13.** The clause + > "`GetBufferBindingPointCount`'s forward → FATAL under split" is NOT in the code and must not + > be put there this phase. `FieldOwnership.def:147` (the field row) and `:179` (the forward row) + > both say `BARRIER_PULLED`, and the generator refuses a field/forward pair that disagrees — + > pinned by `FieldOwnershipTest.TheSevenStickyForwardsAgreeWithTheirFieldRows`. So landing the + > clause as written would either trip the generator or drag the FIELD row to FATAL with it, and + > that second reading changes **23 pairs** of the derived admitted set (§7, measured with + > `--print-admitted | grep -c '^GetBufferBindingPointCount@'`; ID-120 said 10, which was + > counted before ID-125's retiring-phase disjunct widened the set). The row's retiring phase is + > "P7/P13", which is exactly what admits it on every stamped verb today; a FATAL row is + > admitted nowhere, so those reads would start aborting on a migration this phase never + > promised. + > + > The divergence is STATED HERE rather than discovered from a red gate, for ID-105's reason: + > when a contract clause is arithmetically impossible against the code, the contract is what + > changes. The phase that retires the buffer-binding-point family (P7 for the Magma half, P13 + > for the transfer half) lands the field row and its forward TOGETHER, in one commit, and + > deletes this note. 9. **Table 1** gains `set_program_bindings` (80), appended; `set_shader_buffers` (38) gains its route, sink and emitter (`PipeCatalogueTest.cpp:170-171, 242-243` invert). **Table 0** gains §1's thirteen rows. **Table 3** gains `IpcTable::RunAhead/PresentCredit`. diff --git a/MobileGL/MG_Remote/Server/PipeApplier.cpp b/MobileGL/MG_Remote/Server/PipeApplier.cpp index e1a15363..f9c4fa22 100644 --- a/MobileGL/MG_Remote/Server/PipeApplier.cpp +++ b/MobileGL/MG_Remote/Server/PipeApplier.cpp @@ -30,19 +30,21 @@ namespace MobileGL::MG_Remote::Server { - namespace { - // P5e (ra, CONTRACT-P5E §1 / §6): DOES THIS SERVER PUBLISH kCapRunAheadApply? The - // question is asked of the server's OWN CallMask and not of a build constant, because - // "the client may run ahead" is exactly what that bit says and Magma never sets it. - // A session with no CallMask yet (the bring-up window, a fixture that never called - // SetCapabilityBits) answers false: no client can have latched run-ahead against a - // snapshot that was never published. - Bool ServerPublishesRunAhead() { - const ServerSession* session = ServerSession::Active(); - if (session == nullptr || !session->CallMaskIsSet()) return false; - return (session->CallMask() & static_cast(MG_Pipe::kCapRunAheadApply)) != 0; - } - } // namespace + // P5e (ra, CONTRACT-P5E §1 / §6): DOES THIS SERVER PUBLISH kCapRunAheadApply? The + // question is asked of the server's OWN CallMask and not of a build constant, because + // "the client may run ahead" is exactly what that bit says and Magma never sets it. + // A session with no CallMask yet (the bring-up window, a fixture that never called + // SetCapabilityBits) answers false: no client can have latched run-ahead against a + // snapshot that was never published. + // + // P5e (gl, ID-111): PROMOTED OUT OF THE ANONYMOUS NAMESPACE, unchanged in body. It is now + // the second conjunct of the barriered stamp as well as Present's frame-serial gate, and + // the red-once has to be able to assert what it answers for the session it built. + Bool MGPipeServerPublishesRunAhead() { + const ServerSession* session = ServerSession::Active(); + if (session == nullptr || !session->CallMaskIsSet()) return false; + return (session->CallMask() & static_cast(MG_Pipe::kCapRunAheadApply)) != 0; + } ReplyPool::ReplyPool(void* base, Uint64 sizeBytes, Uint32 slotCount, Uint32 slotBytes) : m_base(static_cast(base)), m_size(sizeBytes), m_slots(slotCount), m_slotBytes(slotBytes) {} @@ -311,7 +313,7 @@ namespace MobileGL::MG_Remote::Server { // peer that has not been re-built - and on a server that PUBLISHES the run-ahead cap it // is a protocol fault, because such a client is pacing on this answer and a 0 would // acknowledge a frame nobody asked about. - if (present.FrameSerial == 0 && ServerPublishesRunAhead()) { + if (present.FrameSerial == 0 && MGPipeServerPublishesRunAhead()) { MGLOG_F("MGPipe: Fatal{ProtocolCorruption, \"Present.FrameSerial\"} - a run-ahead " "server was handed present serial 0. The client mints this 1-based and " "waits on it for its credit (CONTRACT-P5E §2.4); returning a credit for " @@ -1183,10 +1185,38 @@ namespace MobileGL::MG_Remote::Server { // §4.4 exemptions from a probe the client's own wait still makes safe - a refusal with // no defect behind it. The predicate is computed on every record all the same, so it is // exercised for the whole phase rather than first run on the day it starts deciding. + // + // AND THE SERVER'S OWN CAPABILITY IS THE SECOND CONJUNCT (P5e gl, ID-111). The constant + // above says what the CLIENT will do once ra's wait rule is live; it says nothing about + // which server this is. kCapRunAheadApply is never published on DirectVulkan (ID-90, + // MGPipeRunAheadCapBitsFor), yet draw_vbo / blit / clear / launch_grid are all + // kWaitNone - so a stamp that read the build constant alone would, on the day it flips, + // have a MAGMA server mark every draw record UNBARRIERED while its client is still + // lockstep. CountBarrierPull (PipeInputs.cpp) is an unconditional Fatal on an + // unbarriered pull, no knob involved, and Magma's residual fill is its ONLY source for + // the seven pointer-backed fields: Magma would die on its first draw and take + // MagmaP7AllocatorDebtScope's exemption with it. + // + // BOTH PREDICATES ARE COMPUTED UNCONDITIONALLY, as arguments rather than as the arms of + // a short-circuit, which is ID-103's reason extended to the capability probe: they are + // exercised on every record for the whole phase rather than first running on the day + // they start deciding. const Bool wireSaysBarriered = MG_Pipe::MGPipeBarriered( static_cast(record.kind), record.payload, MG_Pipe::MGPipeApplier()); MG_Pipe::MGPipeApplierSetCurrentRecordBarriered( - MG_Pipe::kMGPipeP5eClientWaitRuleLanded ? wireSaysBarriered : true); + MGPipeApplierStampsBarriered(MG_Pipe::kMGPipeP5eClientWaitRuleLanded, + MGPipeServerPublishesRunAhead(), wireSaysBarriered)); + // P5e (gl), ID-128: AND WHETHER IT WAS BARRIERED BY ESCALATION RATHER THAN BY ITS CLASS. + // The predicate above is the static wait class plus two payload-derived escalations + // (ID-83: an open transform-feedback span, a draw carrying client vertex arrays), so the + // difference between it and the table IS the escalation - both halves are already + // computed here, and the second flag costs one compare. The strict knob is the only + // reader: a pull on an escalated record is a debt the phase that owns XFB (§5.7) or + // client arrays (ID-82) owes, neither of which is this one. + MG_Pipe::MGPipeApplierSetCurrentRecordBarrieredByEscalation( + wireSaysBarriered && + MG_Pipe::MGPipeWaitClassFor(static_cast(record.kind)) == + MG_Pipe::kWaitNone); // ORDER IS THE CONTRACT'S: stamp, then apply. The stamp is what makes any server-side // read of gPipeInputs legal at all (PipeApplier.h's block 1), so a record applied // before it aborts on the FIRST field inside SyncRenderState. diff --git a/MobileGL/MG_Remote/Server/PipeApplier.h b/MobileGL/MG_Remote/Server/PipeApplier.h index e8c3d3e1..a9c5e178 100644 --- a/MobileGL/MG_Remote/Server/PipeApplier.h +++ b/MobileGL/MG_Remote/Server/PipeApplier.h @@ -48,6 +48,39 @@ namespace MobileGL::MG_Remote::Server { + // P5e (gl, ID-111): DOES THIS SERVER PUBLISH kCapRunAheadApply? Asked of the server's OWN + // CallMask and not of a build constant - that bit IS the sentence "the client may run ahead + // of this apply", and Magma never sets it (MGPipeRunAheadCapBitsFor returns kCapNone for + // every backend but DirectGLES, ID-90). A session with no CallMask yet answers false: no + // client can have latched run-ahead against a snapshot that was never published. + // + // PUBLIC because the red-once has to be able to say "the session I built lacks bit 10" in + // its own words rather than inferring it from the stamp it is testing (ID-102's rule: the + // action under test is the probe itself). + Bool MGPipeServerPublishesRunAhead(); + + // ---- the barriered stamp, AS A PURE FUNCTION (ID-111) --------------------------------- + // + // ApplyOne stamps "is the client parked behind this record" before anything can ask + // (CONTRACT-P5E §2.1 / §4.4). Until the P5e integration commit the answer is `true` for + // every record whatever the wire says, because the client still blocks after each one + // (ID-103) - but the day the constant flips, the answer must ALSO ask whether this server + // published the run-ahead bit at all. It is `wireSaysBarriered` only when BOTH halves of + // the run-ahead arm are true; Magma publishes no bit 10, so a Magma server keeps stamping + // `true` and its lockstep client keeps being safe. Without the second conjunct a Magma + // server would stamp every draw_vbo / blit / clear / launch_grid UNBARRIERED (they are all + // kWaitNone) while its client is still parked, and CountBarrierPull aborts unconditionally + // on an unbarriered pull - Magma dies on its first draw, no knob involved. + // + // IT IS A PURE FUNCTION for MGPipeRunAheadCapBitsFor's reason: "Magma never runs ahead" is + // then something a unit case can hold AT THE POST-FLIP VALUE of the constant, rather than a + // claim that first becomes testable on the day the integration commit throws the switch. + constexpr Bool MGPipeApplierStampsBarriered(Bool clientWaitRuleLanded, + Bool serverPublishesRunAhead, + Bool wireSaysBarriered) { + return (clientWaitRuleLanded && serverPublishesRunAhead) ? wireSaysBarriered : true; + } + // Writes answers into SEG_REPLY at seq % slots, stamping the seq back into the slot header // so a wrong-slot read is detectable rather than plausible (table 0's slot header row: // {Uint64 Seq; Int32 Status; Uint32 Size;}). diff --git a/MobileGL/MG_Test/Pipe/FieldOwnershipTest.cpp b/MobileGL/MG_Test/Pipe/FieldOwnershipTest.cpp index 17ea339e..1dc143e2 100644 --- a/MobileGL/MG_Test/Pipe/FieldOwnershipTest.cpp +++ b/MobileGL/MG_Test/Pipe/FieldOwnershipTest.cpp @@ -28,6 +28,7 @@ #include +#include #include #include #include @@ -93,11 +94,16 @@ namespace { MG_Config::Ipc.StrictErrors = false; MGPipeServerClearVerbBoundary(); MGPipeResetResidualPullCountForTesting(); + // P5e (gl), ID-128: the escalation flag is per-thread state PipeApplier::ApplyOne + // stamps on every record, so a case that set it would otherwise hand its answer to + // the next one - and the arm it selects is "admitted", so the leak is silent. + MGPipeApplierSetCurrentRecordBarrieredByEscalation(false); #endif } void TearDown() override { #if MOBILEGL_BUILD_DISAGGREGATED MGPipeServerClearVerbBoundary(); + MGPipeApplierSetCurrentRecordBarrieredByEscalation(false); MG_Config::Ipc.StrictErrors = false; #endif MG_State::pGLContext = Move(m_previous); @@ -166,6 +172,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 +394,147 @@ TEST_F(FieldOwnershipTest, VerbBoundaryOpsCoverEveryVerbShapedCall) { EXPECT_EQ(MGPipeVerbForWireOp(MGPWireOp::GetCaps), MGPipeVerb::kVerbCount); } +// P5e (gl), ID-116 + ID-125: THE §7 ALLOWLIST IS A DERIVATION, RESTATED HERE INDEPENDENTLY. +// +// 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) { + // "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)); + 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 lane " + "entries this phase is being run to fix"; + EXPECT_FALSE(MGPipeBarrierPullAdmitted(MGPipeInputField::GetBoundVertexArray, + MGPipeVerb::DrawArrays)); + 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)); + // 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 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; + if (waitedFor[v]) ++byWaitClass; + if (!owedByThisPhase(kMGPipeFieldRetiringPhase[f])) ++byRetiringPhase; + EXPECT_TRUE(stamped[v]) + << kMGPipeInputFieldNames[f] << "@" << kMGPipeVerbNames[v] + << " 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( + 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"; + // 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"; +} + // --------------------------------------------------------------------------------------- // 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. @@ -753,15 +903,128 @@ TEST_F(FieldOwnershipTest, TheSameReadWithoutStrictErrorsSurvivesAndIsCounted) { EXPECT_EQ(r.Log.find("Fatal{"), std::string::npos) << r.Log; } -TEST_F(FieldOwnershipTest, StrictErrorsAlsoPromotesTheStickyForwards) { +// P5e (gl) RED-ONCE, ID-128: THE THIRD DISJUNCT, AND IT IS A RUNTIME FACT ABOUT THE RECORD. +// +// GetBoundVertexArray@DrawArrays is this phase's debt on an unbarriered verb, so the static +// table rejects it and strict aborts - that is the case two blocks up, and it must keep doing +// that for the ORDINARY draw path vi and mv retired. But the two +// DirectGLES.Split.ClientVertexArrayScenario entries pull the same pair on a record the client +// IS parked behind: MGPipeBarriered escalates a draw carrying client vertex arrays (ID-83), and +// ID-82 puts client arrays outside P5e entirely - under run-ahead the client refuses them by +// name and staging is P8's. The read site (SyncClientSideVertexArraysForDrawArrays) aborts with +// Fatal{RoleViolation, "MGPipeSlots"} if it is ever applied unbarriered, so the pull is legal. +// +// ONE PAIR, TWO VERDICTS, DECIDED BY THE RECORD AND NOT BY THE TABLE. That is why the flag is +// stamped in ApplyOne beside the barriered stamp rather than folded into the generated table: +// no table indexed by (field, verb) can tell these two entries apart. +// +// THE RED: drop `&& !escalated` from CountBarrierPull's strict arm and this case dies of +// SIGABRT on Fatal{UnmigratedPipeInput, "GetBoundVertexArray@DrawArrays"}. +// +// THE CONTROL IS THE CASE TWO BLOCKS UP, NOT A SECOND CHILD HERE. +// StrictErrorsTurnsABarrierPulledReadIntoANamedAbort drives the IDENTICAL pull - same field, +// same verb, same knob - with the escalation flag at its `false` default, and asserts the abort. +// Reading the log delta of two forks in one case is what a shared log file cannot support. +TEST_F(FieldOwnershipTest, AnEscalatedRecordsPullIsAdmittedAndSaysWhy) { + const ChildResult escalated = RunInChild([] { + MG_Config::Ipc.StrictErrors = true; + // What PipeApplier::ApplyOne stamps for a draw whose payload carries kDrawClientArrays: + // MGPipeBarriered says barriered, the static wait class of draw_vbo says kWaitNone. + MGPipeApplierSetCurrentRecordBarrieredByEscalation(true); + MGPipeServerStampVerbBoundary(MGPipeVerb::DrawArrays); + (void)gPipeInputs.GetBoundVertexArray(); + if (MGPipeResidualPullCount() != 1) ::_exit(7); + }); + ASSERT_TRUE(ExitedWith(escalated, 0)) << DescribeStatus(escalated) << "\n" << escalated.Log; + EXPECT_EQ(escalated.Log.find("Fatal{UnmigratedPipeInput"), std::string::npos) << escalated.Log; + // THE MARKER SAYS WHICH DISJUNCT, and that is what keeps the lane's comparison exact: a pair + // admitted by the table is checkable against `--print-admitted`, one admitted by escalation + // is not in any static list and must not widen one. + EXPECT_NE(escalated.Log.find("Admitted{UnmigratedPipeInput, \"GetBoundVertexArray@DrawArrays\"}" + " [BARRIER-PULLED, ADMITTED-ESCALATED, retires in "), + std::string::npos) + << escalated.Log; +} + +// 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; +} + +// P5e (gl) RED-ONCE, ID-117: THE THIRD STATE, AND IT IS THE SAME FIELD AS THE CASE ABOVE. +// +// ValidateProgramName@DrawArrays aborts (draw_vbo is kWaitNone: the client will not be parked +// behind that record and the read is torn by construction). ValidateProgramName@ReadPixels is +// the same sticky forward under a verb whose op IS statically barriered, so the client is +// parked, the value is real and ordered, and the debt is P9's rather than this phase's - it +// says so and the entry COMPLETES. One field, two verbs, opposite verdicts: that is the whole +// of ID-84 in two cases, and before this change the lane could not tell them apart because +// strict aborted on both, which made CI's allowlist comparison unreachable code. +// +// THE RED: delete the `if (!MGPipeBarrierPullAdmitted(...))` guard in CountBarrierPull so the +// strict arm is unconditional again, and this case dies of SIGABRT instead of exiting 0. +TEST_F(FieldOwnershipTest, AnAdmittedBarrierPullIsLoudOnceAndNotFatal) { + const ChildResult r = RunInChild([] { + MG_Config::Ipc.StrictErrors = true; + MGPipeServerStampVerbBoundary(MGPipeVerb::ReadPixels); + (void)gPipeInputs.ValidateProgramName(1u); + (void)gPipeInputs.ValidateProgramName(1u); + (void)gPipeInputs.ValidateProgramName(2u); + // rsp counts every barriered pull, and under strict every surviving barriered pull is an + // admitted one - ID-119's reworded pin, from the counter's side. + if (MGPipeResidualPullCount() != 3) ::_exit(7); + }); + ASSERT_TRUE(ExitedWith(r, 0)) << DescribeStatus(r) << "\n" << r.Log; + EXPECT_EQ(r.Log.find("Fatal{UnmigratedPipeInput"), std::string::npos) + << "an admitted pull aborted: the lane can never be green while a debt this phase " + "deliberately leaves standing is fatal\n" + << r.Log; + // THE GRAMMAR, VERBATIM. `@` and the bracketed tail are the Fatal's, character + // for character; only the leading tag differs, so every filter written since P5c that + // matches `Fatal{UnmigratedPipeInput` still means exactly "red". + EXPECT_NE(r.Log.find("MGPipe: Admitted{UnmigratedPipeInput, \"ValidateProgramName@ReadPixels\"}" + " [BARRIER-PULLED, ADMITTED, retires in P9]"), + std::string::npos) + << r.Log; + // DEDUPED PER (field, verb): three pulls, one line. An 852-draw frame must not write 852. + SizeT lines = 0; + for (std::size_t at = r.Log.find("Admitted{UnmigratedPipeInput"); at != std::string::npos; + at = r.Log.find("Admitted{UnmigratedPipeInput", at + 1)) { + ++lines; + } + EXPECT_EQ(lines, SizeT{1}) + << "the admitted marker is not deduped per (field, verb); a frame of draws would write " + "one line per pull and the marker census could not be read\n" << r.Log; } diff --git a/MobileGL/MG_Test/Pipe/PipeCatalogueTest.cpp b/MobileGL/MG_Test/Pipe/PipeCatalogueTest.cpp index b44f265f..f9a571ad 100644 --- a/MobileGL/MG_Test/Pipe/PipeCatalogueTest.cpp +++ b/MobileGL/MG_Test/Pipe/PipeCatalogueTest.cpp @@ -763,6 +763,15 @@ TEST(PipeCatalogue, EveryRowCarriesTheWaitClassTheContractGivesIt) { MGPWireOp::EndStreamOutput, MGPWireOp::PauseStreamOutput, MGPWireOp::ResumeStreamOutput, MGPWireOp::BindStreamOutput, MGPWireOp::CopyFramebufferToTexture, + // P5e (gl), ID-118. resource_copy_region JOINED THIS SET, and it is the retiring phase + // of a field that put it here: its verb is CopyImageSubData, whose apply reads + // GetTextureObject, and that row retires in P7. An unbarriered record reading client + // memory is an unconditional Fatal, so leaving it kWaitNone would have meant a real + // defect standing for two phases - or an exception hand-written into a DERIVED + // allowlist, which is the same thing with a comment on it. It sits beside + // copy_framebuffer_to_texture here for the reason it took that class: same verb class, + // no reply slot, and zero calls per frame in the measured scene. + MGPWireOp::ResourceCopyRegion, }; for (const MGPWireOp op : appliedRows) { EXPECT_EQ(MGPipeWaitClassFor(op), kWaitApplied) << WireOpNameForDiag(op); @@ -787,8 +796,10 @@ TEST(PipeCatalogue, EveryRowCarriesTheWaitClassTheContractGivesIt) { EXPECT_EQ(MGPipeWaitClassFor(op), kWaitNone) << WireOpNameForDiag(op); } - // The partition, by count. 14 + 1 + 9 = 24 rows wait; every other row of the catalogue does - // not. A row that changed class moves two of these numbers at once. + // The partition, by count. 14 + 1 + 10 = 25 rows wait; every other row of the catalogue does + // not. A row that changed class moves two of these numbers at once - which is why the + // kWaitApplied count went 9 -> 10 and the kWaitNone offset 24 -> 25 in the SAME commit that + // moved resource_copy_region (P5e gl, ID-118). SizeT reply = 0, applied = 0, present = 0, none = 0, other = 0; for (SizeT i = 1; i < static_cast(MGPWireOp::kOpCount); ++i) { switch (MGPipeWaitClassFor(static_cast(i))) { @@ -800,9 +811,9 @@ TEST(PipeCatalogue, EveryRowCarriesTheWaitClassTheContractGivesIt) { } } EXPECT_EQ(reply, 14u); - EXPECT_EQ(applied, 9u); + EXPECT_EQ(applied, 10u); EXPECT_EQ(present, 1u); - EXPECT_EQ(none, static_cast(kMGPipeCallCount) - 24u); + EXPECT_EQ(none, static_cast(kMGPipeCallCount) - 25u); EXPECT_EQ(other, 0u) << "a row carries the kWaitClassCount terminator as its class"; // And the reply half of the partition BOTH WAYS, over the whole catalogue: exactly the rows diff --git a/MobileGL/MG_Test/Wire/RemoteClientControls.inc b/MobileGL/MG_Test/Wire/RemoteClientControls.inc index b04edfbd..d5158b32 100644 --- a/MobileGL/MG_Test/Wire/RemoteClientControls.inc +++ b/MobileGL/MG_Test/Wire/RemoteClientControls.inc @@ -659,4 +659,61 @@ TEST(RemoteClientControls, StagingWaitsForRetirementAfterThePriorRecordApplied) }); ExpectChildSuccess(child); } + +// P5e (gl) RED-ONCE, ID-111. THE SERVER-SIDE MIRROR OF THE CLIENT LATCH - the line that makes +// ID-90 ("Magma keeps the lockstep for the whole of P5e") true in code rather than in prose. +// +// The control session calls SetCapabilityBits(0), so its CallMask IS set and does NOT carry +// bit 10. That is a Magma server's answer for ever (MGPipeRunAheadCapBitsFor returns kCapNone +// off DirectGLES) and an Espryt server's answer for the whole bring-up window. A DrawVbo then +// crosses for real, so what is under test is the stamp PipeApplier::ApplyOne writes and not a +// test-only branch beside it. +// +// FOUR ASSERTIONS, because each one alone can be true for the wrong reason: +// 1. the session really lacks the bit, said in its own words rather than inferred from the +// stamp being tested (ID-102: the action under test is the probe itself); +// 2. the wire really answers UNBARRIERED for this record - draw_vbo is kWaitNone - so the +// `wireSaysBarriered` arm is the one a flipped constant would take; +// 3. the record that actually crossed was stamped barriered; +// 4. and the stamp is STILL barriered at the POST-FLIP value of the wait-rule constant. +// +// (4) IS THE ONE THAT MATTERS AND IT IS STATED AT `true` RATHER THAN READ FROM THE CONSTANT. +// kMGPipeP5eClientWaitRuleLanded is false today, so (3) alone would pass for a server that had +// no capability conjunct at all - and would keep passing until the integration commit, at which +// point Magma SIGSEGVs on its first draw with the lane still green. Asking the pure function +// for the post-flip answer is how the claim gets tested before the day it starts deciding. +// +// THE RED: delete `serverPublishesRunAhead &&` from MGPipeApplierStampsBarriered +// (MG_Remote/Server/PipeApplier.h) and (4) flips to false - the child exits 124. +TEST(RemoteClientControls, ADrawOnASessionWithoutTheRunAheadBitStaysStampedBarriered) { + const auto child = RunInChild([] { + StartControlSession(); + DrawPeer peer; + peer.Install(); + MGPDrawInfo info{}; + info.NumDraws = 1; + MGPDrawRange range{}; + if (ClientSessionInstance().EmitAndWait(MGPWireOp::DrawVbo, &info, sizeof(info), &range, + sizeof(range), nullptr, 0, nullptr) == 0) + ::_exit(120); + // Read the stamp on the thread that owns it: it is a thread_local describing "which + // record is the apply thread inside right now", and ApplyOne leaves it standing. + if (Srv::ServerLoopInstance().RunOnApplyThread([](void*) { + if (Srv::MGPipeServerPublishesRunAhead()) ::_exit(121); + MGPDrawInfo probe{}; + probe.NumDraws = 1; + if (MGPipeBarriered(MGPWireOp::DrawVbo, &probe, MGPipeApplier())) ::_exit(122); + if (!MGPipeApplierCurrentRecordIsBarriered()) ::_exit(123); + if (!Srv::MGPipeApplierStampsBarriered(/*clientWaitRuleLanded=*/true, + Srv::MGPipeServerPublishesRunAhead(), + /*wireSaysBarriered=*/false)) + ::_exit(124); + return MOBILEGL_OK; + }, + nullptr) != MOBILEGL_OK) + ::_exit(125); + ClientSessionInstance().Stop(); + }); + ExpectChildSuccess(child); +} #endif diff --git a/MobileGL/MG_Util/Metrics/PipeStats.cpp b/MobileGL/MG_Util/Metrics/PipeStats.cpp index 5590da31..fccd0a0b 100644 --- a/MobileGL/MG_Util/Metrics/PipeStats.cpp +++ b/MobileGL/MG_Util/Metrics/PipeStats.cpp @@ -211,7 +211,7 @@ namespace MobileGL::MG_Util::PipeStats { "render-state-cso-mints", "render-state-cso-binds", "map-persistent-roundtrips", "framebuffer-emissions", "sampler-view-emissions", "sampler-state-emissions", "shader-image-emissions", "client-tex-upload-emissions", "tex-remint-pulls", - "residual-pulls", + "residual-pulls", "server-verb-boundaries", #endif }; const char* const kGateNames[kGateCount] = { @@ -514,6 +514,14 @@ namespace MobileGL::MG_Util::PipeStats { // tracks the draw count is a pull inside a loop, and one that tracks the frame count is // a pull per verb. Zero in every monolith lane by construction. line += " rsp=" + std::to_string(calls[static_cast(CallClass::ResidualPulls)]); + // P5e (gl), ID-115: `vbs` is the server's verb-boundary stamp count, and it is on this + // line so that "strict was armed on this entry" is a number a lane can read rather than + // an inference from an absence. Everything strict checks is downstream of that stamp and + // the monolith arm never stamps, so a green lane with vbs=0 says only that the mechanism + // never ran. It is deliberately NOT rsp: rsp reaches zero when the phase SUCCEEDS, so a + // positive control built on it would fail on the day the debt is paid. + line += " vbs=" + + std::to_string(calls[static_cast(CallClass::ServerVerbBoundaries)]); // P5's three wire gauges, and THEY ARE RUN TOTALS on a line whose every other field is // a window - see the Gauge enum for the argument. `maxrec` is R-10's proof obligation // (BRIEF 8 item 3): the largest single record this run wrote, in BYTES, beside the cap diff --git a/MobileGL/MG_Util/Metrics/PipeStats.h b/MobileGL/MG_Util/Metrics/PipeStats.h index 7b679375..9c333eee 100644 --- a/MobileGL/MG_Util/Metrics/PipeStats.h +++ b/MobileGL/MG_Util/Metrics/PipeStats.h @@ -179,6 +179,22 @@ namespace MobileGL::MG_Util::PipeStats { // forwards cannot drift apart on it. It is zero in every monolith lane by // construction: nothing arms it but a server verb-boundary stamp. ResidualPulls, + // P5e (gl), ID-115: `vbs` - SERVER VERB BOUNDARIES STAMPED. One per record that IS a + // verb boundary, counted at MGPipeServerStampVerbBoundary itself. + // + // IT EXISTS BECAUSE "THE STRICT LANE IS GREEN" AND "STRICT WAS NEVER ARMED" WERE + // OBSERVATIONALLY IDENTICAL. Every strict check downstream - the poison, rsp, the + // BARRIER-PULLED verdict - is reachable ONLY after this stamp, and the monolith arm + // never stamps at all. So of the entries that passed strict before this counter existed, + // three were monolith transport (where the whole mechanism is structurally unreachable), + // two self-skipped, one was a death test and one was a Python check: not one was a + // record-carrying split GL scenario, and the lane could not tell that from rigour. + // + // rsp CANNOT PLAY THIS PART, which is the reason for a counter rather than a reused one: + // rsp goes to zero exactly when the phase SUCCEEDS, so a positive control built on it + // would start failing on the day the debt is paid. `vbs` is non-zero whenever the + // server applied a verb at all, before and after retirement alike. + ServerVerbBoundaries, #endif Count }; diff --git a/scripts/gen_pipe_field_ownership.py b/scripts/gen_pipe_field_ownership.py index 71d06ab3..cfe72734 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,169 @@ 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 + + +THIS_PHASE = "P5e" +PHASE_TOKEN_RE = re.compile(r"\bP\d+[a-z]*\b") + + +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)} + 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") + # 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) + + 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 +512,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 +641,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 +758,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 +908,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, 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, ph, 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 +972,112 @@ 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() + waits_real = parse_wait_classes(wire_inc) + derivation = [] + + def expect(name, condition): + derivation.append((name, bool(condition))) + + # ---- 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 + # 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 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 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 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 + + 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 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: + 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 +1087,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 +1099,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 +1115,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, 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 + # 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 +1145,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 = {}