swung0x48/MobileGL
1
0
Fork 0
mirror of https://github.com/MobileGL-Dev/MobileGL synced 2026-11-07 01:53:24 +09:00
Code Issues Packages Projects Releases Wiki Activity

[MG_IntegrationTest, MG_Util, MG_Backend, CI, Docs] (Disaggregated): P5e ID-119/ID-115 - the lane reads every log, counts, and has a positive control

Browse Source 
Three measured defects in the strict lane, one commit each in spirit and one in fact because
they are the same step.

1. THE LOG SET CAME FROM A DIRECTORY. The CI step grepped MG_IntegrationTest/split-logs/, which
   holds 90 of the lane's entries. The ones it could not see were the F1. readback block, both
   NamedBlit pairs, the four Ct. entries and PersistentMapArm - precisely the readback population
   the allowlist is ABOUT, plus the only DirectVulkan entries in the lane. split_log_paths.py
   gains a `markers` mode that walks ctest's own {entry: MOBILEGL_LOG_FILE_PATH} map and
   classifies every Fatal{ and Admitted{ line. Measured on this head: 113 of 113 entries read.
   The lane is now a TWO-SIDED RATCHET - an unadmitted marker fails, an admitted pair not in
   Harness/strict-expected-markers.txt fails, AND an expected pair that no longer appears fails,
   so the lane cannot rot green by outliving its own debts.

2. THE `rsp` CHECK GREPPED FOR A COUNTER NO SPLIT ENTRY EMITS, and the pin behind it was vacuous:
   CountBarrierPull's unbarriered arm is [[noreturn]] and runs BEFORE ++g_residualPulls, so
   "rsp = 0 on unbarriered records" was true of every possible implementation. Replaced by an
   assertion where the counter actually is - one entry, DirectGLES.Split.StrictArming., 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: the library opens that path "w"). It asserts
   rsp == 0 || rsp >= draws, which is the device evidence's shape - rsp ~= the draw count under
   inproc, 0 under monolith - so the draw path's retirement is visible as rsp ceasing to scale.

3. THE LANE HAD NO POSITIVE CONTROL (ID-115). Of the seven entries that passed strict, three were
   monolith transport - where nothing stamps a verb boundary, so 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, so "green" and "strict was never armed" were
   the same observation. New push-only counter `vbs` (PipeStats::ServerVerbBoundaries), counted
   at MGPipeServerStampVerbBoundary behind Enabled(), and the same entry asserts vbs > 0 on a
   frame that drew. It is deliberately NOT rsp: rsp reaches zero when the phase SUCCEEDS, so a
   control built on it would start failing on the day the debt is paid.

- Measured on this head (base 7c6f6886, before pa and mv): isplit 119/119; under strict the
  census is Fatal{ GetProgramForDraw@DrawArrays 52, GetBoundVertexArray@DrawArrays 9,
  GetProgramForDispatch@DispatchCompute 7 - exactly what pa and mv owe - and Admitted{ on ten
  pairs, three of them ADMITTED-ESCALATED. The expected-marker file carries all ten and says in
  its header that the wave-3 merge retires three of them.
- CONTRACT-P5E §7 rewritten around what is now checkable: the derived allowlist and its three
  disjuncts, the two-sided ratchet, the restated rsp pin, and the positive control.
This commit is contained in:
swung0x48
2026-09-18 12:30:10 -04:00
parent a0836568ac
commit bc6e24ff30
9 changed files with 507 additions and 43 deletions
Download Patch File Download Diff File Expand all files Collapse all files
.github/workflows/test.yml
+82 -32
View File
@@ -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()
MobileGL/MG_Backend/MGPipe/PipeInputs.cpp
+11
View File
@@ -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
MobileGL/MG_IntegrationTest/CMakeLists.txt
+48
View File
@@ -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()
MobileGL/MG_IntegrationTest/Harness/split_log_paths.py
+148
View File
@@ -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, "<F>@<V>"} [BARRIER-PULLED, <why>, retires in <phase>]
# MGPipe: Admitted{UnmigratedPipeInput, "<F>@<V>"} [BARRIER-PULLED, ADMITTED[-ESCALATED], retires in <phase>]
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 `<field>@<verb>` 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:
MobileGL/MG_IntegrationTest/Harness/strict-expected-markers.txt
+45
View File
@@ -0,0 +1,45 @@
# The admitted barrier-pull markers the integration-split lane ACTUALLY WRITES under
# MOBILEGL_IPC_STRICT_ERRORS=1, one `<field>@<verb>` 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
MobileGL/MG_IntegrationTest/Scenarios/TriangleScenario.cpp
+104
View File
@@ -47,6 +47,7 @@
#include <vector>
#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
MobileGL/MG_Remote/CONTRACT-P5E.md
+44 -10
View File
@@ -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 `<field>@<verb>`) 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
`<field>@<verb>` 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,
"<F>@<V>"} [BARRIER-PULLED, ADMITTED|ADMITTED-ESCALATED, retires in <phase>]` 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.
---
MobileGL/MG_Util/Metrics/PipeStats.cpp
+9 -1
View File
@@ -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<Uint32>(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<Uint32>(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
MobileGL/MG_Util/Metrics/PipeStats.h
+16
View File
@@ -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
};