Merge branch p5e/gl into feat/disaggregated (P5e gl)

This commit is contained in:
2026-09-18 12:42:54 -04:00
21 changed files with 1743 additions and 96 deletions
+142 -52
View File
@@ -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, `<field>@<verb>`, 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
# <field>@<verb> 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()
+96 -3
View File
@@ -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.
//
// `<field>@<verb>` and the `[BARRIER-PULLED, …, retires in <phase>]` 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<SizeT>(field);
const SizeT verbIndex = static_cast<SizeT>(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
+45
View File
@@ -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;
+75 -1
View File
@@ -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()
@@ -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:
@@ -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
@@ -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
+13
View File
@@ -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
//
+26
View File
@@ -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
+16 -1
View File
@@ -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 ---- */ \
@@ -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 <field>@<verb> 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<SizeT>(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<SizeT>(kMGPipeVerbClass[v])];
for (SizeT f = 0; f < kMGPipeInputFieldCount; ++f) {
const auto field = static_cast<MGPipeInputField>(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;
+1 -1
View File
@@ -428,7 +428,7 @@ inline constexpr Uint8 kMGPipeWaitClasses[static_cast<SizeT>(MGPWireOp::kOpCount
/* 50 ResourceSubDataComplete */ static_cast<Uint8>(kWaitNone),
/* 51 ResourceFlushRange */ static_cast<Uint8>(kWaitNone),
/* 52 ResourceReadback */ static_cast<Uint8>(kWaitReply),
/* 53 ResourceCopyRegion */ static_cast<Uint8>(kWaitNone),
/* 53 ResourceCopyRegion */ static_cast<Uint8>(kWaitApplied),
/* 54 GenerateMipmap */ static_cast<Uint8>(kWaitApplied),
/* 55 GetTextureImage */ static_cast<Uint8>(kWaitReply),
/* 56 Blit */ static_cast<Uint8>(kWaitNone),
+73 -13
View File
@@ -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 `<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.
**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`.
+45 -15
View File
@@ -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<Uint64>(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<Uint64>(MG_Pipe::kCapRunAheadApply)) != 0;
}
ReplyPool::ReplyPool(void* base, Uint64 sizeBytes, Uint32 slotCount, Uint32 slotBytes)
: m_base(static_cast<Uint8*>(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<MG_Pipe::MGPWireOp>(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<MG_Pipe::MGPWireOp>(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.
+33
View File
@@ -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;}).
+266 -3
View File
@@ -28,6 +28,7 @@
#include <gtest/gtest.h>
#include <cctype>
#include <cstdio>
#include <cstdlib>
#include <filesystem>
@@ -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<unsigned char>(phase[at - 1]));
const std::size_t after = at + 3;
const Bool rightOk = after >= phase.size() ||
!std::isalnum(static_cast<unsigned char>(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<SizeT>(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<SizeT>(MGPWireOp::kOpCount); ++op) {
const MGPipeVerb verb = MGPipeVerbForWireOp(static_cast<MGPWireOp>(op));
if (verb == MGPipeVerb::kVerbCount) continue;
stamped[static_cast<SizeT>(verb)] = true;
if (MGPipeWaitClassFor(static_cast<MGPWireOp>(op)) != kWaitNone) {
waitedFor[static_cast<SizeT>(verb)] = true;
}
}
SizeT admitted = 0;
SizeT byWaitClass = 0;
SizeT byRetiringPhase = 0;
for (SizeT v = 0; v < kMGPipeVerbCount; ++v) {
const auto verb = static_cast<MGPipeVerb>(v);
for (SizeT f = 0; f < kMGPipeInputFieldCount; ++f) {
const auto field = static_cast<MGPipeInputField>(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<SizeT>(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. `<field>@<verb>` 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;
}
+15 -4
View File
@@ -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<SizeT>(MGPWireOp::kOpCount); ++i) {
switch (MGPipeWaitClassFor(static_cast<MGPWireOp>(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<SizeT>(kMGPipeCallCount) - 24u);
EXPECT_EQ(none, static_cast<SizeT>(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
@@ -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
+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
+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
};
+392 -2
View File
@@ -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 `... <declaration> = {` 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<Uint8>\(\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<SizeT>(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 <field>@<verb> 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 <field>@<verb> 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 <field>@<verb> 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<SizeT>(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<SizeT>(kMGPipeVerbClass[v])];
for (SizeT f = 0; f < kMGPipeInputFieldCount; ++f) {
const auto field = static_cast<MGPipeInputField>(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<SizeT>(MGPWireOp::kOpCount)] =",
"kMGPipeWaitClassesXX[static_cast<SizeT>(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<Uint8>\()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 <field>@<verb> 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 "
"<field>@<verb> 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 <field>@<verb> "
"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 = {}