diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 671215f6..60b790e7 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -1214,35 +1214,66 @@ 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 @@ -1269,27 +1300,46 @@ jobs: # from, so this shell and the C++ cannot drift: retiring a verb's wait class narrows # the lane with no edit here, and a new BARRIER_PULLED row widens it only on verbs # that wait. - python3 "${GITHUB_WORKSPACE}/scripts/gen_pipe_field_ownership.py" --print-admitted \ - > "${RUNNER_TEMP}/allowed.txt" - echo "§7 allowlist (derived): $(wc -l < "${RUNNER_TEMP}/allowed.txt") admitted pair(s)" + # 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 - - # `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" - fi - echo "integration-split under strict is GREEN with only the §7 allowlist admitted ($(wc -l < "${RUNNER_TEMP}/markers.txt") distinct marker(s))" + echo "integration-split under strict is GREEN, two-sided, with the arming control present" - name: Upload strict lane logs if: always() diff --git a/MobileGL/MG_Backend/MGPipe/PipeInputs.cpp b/MobileGL/MG_Backend/MGPipe/PipeInputs.cpp index 5405546f..40d37938 100644 --- a/MobileGL/MG_Backend/MGPipe/PipeInputs.cpp +++ b/MobileGL/MG_Backend/MGPipe/PipeInputs.cpp @@ -264,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_IntegrationTest/CMakeLists.txt b/MobileGL/MG_IntegrationTest/CMakeLists.txt index f72d467a..58cfbb1b 100644 --- a/MobileGL/MG_IntegrationTest/CMakeLists.txt +++ b/MobileGL/MG_IntegrationTest/CMakeLists.txt @@ -2275,3 +2275,51 @@ if (MOBILEGL_BUILD_DISAGGREGATED) 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_Remote/CONTRACT-P5E.md b/MobileGL/MG_Remote/CONTRACT-P5E.md index a33de58e..925c8d65 100644 --- a/MobileGL/MG_Remote/CONTRACT-P5E.md +++ b/MobileGL/MG_Remote/CONTRACT-P5E.md @@ -474,16 +474,50 @@ 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. + --- 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 };