#!/usr/bin/env python3 # MobileGL - scripts/gen_pipe_field_ownership.py # Copyright (c) 2025-2026 MobileGL-Dev # Licensed under the GNU Lesser General Public License v3.0: # https://www.gnu.org/licenses/gpl-3.0.txt # https://www.gnu.org/licenses/lgpl-3.0.txt # SPDX-License-Identifier: LGPL-3.0-only # End of Source File Header """TABLE 2 - where every PipeInputs field's value comes from once the backend is a server. CONTRACT-P5.md section 3 / BRIEF-P5 R-7. Reads MobileGL/MG_Pipe/Coverage.def the 63 accessors, the 7 sticky, the 40 emitted MobileGL/MG_Impl/Pipe/PipeFill.cpp EmittedCallSuppliesTheWholeField's refusals MobileGL/MG_Pipe/FieldOwnership.def the hand-maintained half and writes MobileGL/MG_Pipe/generated/PipeFieldOwnership.inc. The output is COMMITTED; CI regenerates it and fails on a diff, exactly as gen_pipe.py's seven outputs do. ONE CLASS PER ROW, AND THE BUILD FAILS OTHERWISE. 63 field rows + the 7 sticky forwards = 70, each in exactly one of RECORD_SUPPLIED / APPLIER_DERIVED / BARRIER_PULLED / FATAL. A field in none of them stops this script, so the committed header can never contain an unclassified row and --check is what catches a stale one. RECORD_SUPPLIED is DERIVED rather than listed - it is Coverage.def's emitted list minus PipeFill.cpp's refusals - so the mapping file cannot drift away from the emitters it describes without a red gate. python3 scripts/gen_pipe_field_ownership.py # write it, print the summary python3 scripts/gen_pipe_field_ownership.py --check # THE GATE: rc 1 on any hole python3 scripts/gen_pipe_field_ownership.py --self-test # the gate's own negative controls """ import argparse import os import re import sys REPO_ROOT = os.path.dirname(os.path.dirname(os.path.abspath(__file__))) PIPE_DIR = os.path.join(REPO_ROOT, "MobileGL", "MG_Pipe") GENERATED_DIR = os.path.join(PIPE_DIR, "generated") COVERAGE_DEF = os.path.join(PIPE_DIR, "Coverage.def") 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") ENUMERATOR = { "RECORD_SUPPLIED": "kRecordSupplied", "APPLIER_DERIVED": "kApplierDerived", "BARRIER_PULLED": "kBarrierPulled", "FATAL": "kFatal", } BANNER = """// MobileGL - MobileGL/MG_Pipe/generated/{name} // Copyright (c) 2025-2026 MobileGL-Dev // Licensed under the GNU Lesser General Public License v3.0: // https://www.gnu.org/licenses/gpl-3.0.txt // https://www.gnu.org/licenses/lgpl-3.0.txt // SPDX-License-Identifier: LGPL-3.0-only // End of Source File Header // TABLE 2: PipeInputs field ownership (CONTRACT-P5.md section 3, R-7). // // GENERATED by scripts/gen_pipe_field_ownership.py from Coverage.def, FieldOwnership.def and // MG_Impl/Pipe/PipeFill.cpp - DO NOT EDIT. Regenerate with // `python3 scripts/gen_pipe_field_ownership.py`; CI runs it and diffs the result. // // Included from MG_Backend/MGPipe/PipeInputs.h inside namespace MobileGL::MG_Pipe, which is // the one header that both the poison check and the server's verb stamp already see. It is // NOT included from MG_Pipe/MGPipe.h with the other seven generated files, on purpose: that // header is in the PULL build's include closure and G1 admits no symbol motion there. """ def read(path): with open(path, "r", encoding="utf-8") as handle: return handle.read() def mask_comments(text): """Blank comment bodies, keeping every offset and newline. String literals are LEFT ALONE - unlike gen_pipe_dirty_surface.py's masker - because this file's rows carry their retiring phase and their reason as quoted arguments.""" out = list(text) i = 0 n = len(text) while i < n: if text[i] == "/" and i + 1 < n and text[i + 1] == "/": while i < n and text[i] != "\n": out[i] = " " i += 1 elif text[i] == "/" and i + 1 < n and text[i + 1] == "*": out[i] = out[i + 1] = " " i += 2 while i < n and not (text[i] == "*" and i + 1 < n and text[i + 1] == "/"): if text[i] != "\n": out[i] = " " i += 1 if i < n: out[i] = out[i + 1] = " " i += 2 else: i += 1 return "".join(out) def macro_block(text, name): """The body of a `#define (X) ...` continued-line macro, comments blanked.""" masked = mask_comments(text) start = masked.find("#define %s(X)" % name) if start < 0: sys.exit("gen_pipe_field_ownership: %s is not in the file" % name) end = start while True: line_end = masked.find("\n", end) if line_end < 0: body = masked[start:] break if not masked[end:line_end].rstrip().endswith("\\"): body = masked[start:line_end] break end = line_end + 1 # The rows wrap, so the continuation backslashes have to go before a row regex can see a # row as one thing. Offsets do not matter here; only the token sequence does. return body.replace("\\\n", "\n") def parse_coverage(text=None): """The ordered 63 accessors, the 7 sticky and the 40 emitted, out of Coverage.def.""" text = read(COVERAGE_DEF) if text is None else text accessors = re.findall(r"X\(\s*(\w+)\s*,\s*\w+\s*\)", macro_block(text, "MGP_COVERAGE_ACCESSOR_LIST")) sticky = re.findall(r"X\(\s*(\w+)\s*,", macro_block(text, "MGP_COVERAGE_STICKY_LIST")) emitted = re.findall(r"X\(\s*(\w+)\s*,\s*\w+\s*\)", macro_block(text, "MGP_COVERAGE_EMITTED_LIST")) if not accessors: sys.exit("gen_pipe_field_ownership: Coverage.def's accessor list did not parse") seen = set() for name in accessors: if name in seen: sys.exit("gen_pipe_field_ownership: %s appears twice in the accessor list" % name) seen.add(name) for name in sticky + emitted: if name not in seen: sys.exit("gen_pipe_field_ownership: %s is not an accessor in MGP_COVERAGE_ACCESSOR_LIST" % name) return accessors, sticky, emitted def parse_supplies_whole_field(text=None): """The fields EmittedCallSuppliesTheWholeField REFUSES, read out of PipeFill.cpp rather than restated here - the derivation that keeps RECORD_SUPPLIED honest is only as good as its source, so the source is the function itself.""" text = read(PIPE_FILL) if text is None else text masked = mask_comments(text) start = masked.find("Bool EmittedCallSuppliesTheWholeField(MGPipeInputField field)") if start < 0: sys.exit("gen_pipe_field_ownership: EmittedCallSuppliesTheWholeField is not in %s" % os.path.basename(PIPE_FILL)) false_at = masked.find("return false;", start) if false_at < 0: sys.exit("gen_pipe_field_ownership: EmittedCallSuppliesTheWholeField has no `return false` arm") refused = re.findall(r"case\s+MGPipeInputField::(\w+)\s*:", masked[start:false_at]) if not refused: sys.exit("gen_pipe_field_ownership: EmittedCallSuppliesTheWholeField refuses nothing - " "either the function moved or the parse broke; a silently empty refusal set " "would make every emitted field RECORD_SUPPLIED") return refused ROW_RE = re.compile(r"X\(\s*(\w+)\s*,\s*(\w+)\s*,\s*\"([^\"]*)\"\s*,\s*\"([^\"]*)\"\s*\)") ARG_ROW_RE = re.compile(r"X\(\s*(\w+)\s*,\s*(\d+)\s*,\s*(\w+)\s*,\s*\"([^\"]*)\"\s*\)") PAIR_RE = re.compile(r"X\(\s*(\w+)\s*,\s*(\w+)\s*\)") # An exemption's reason may be one string or several adjacent ones, the way a long C literal is # written; the row regex takes the first and the check only cares that there is one. EXEMPT_RE = re.compile(r"X\(\s*(\w+)\s*,\s*\"([^\"]*)\"") def parse_ownership(text=None): text = read(OWNERSHIP_DEF) if text is None else text fields = ROW_RE.findall(macro_block(text, "MGP_FIELD_OWNERSHIP_LIST")) forwards = ROW_RE.findall(macro_block(text, "MGP_FIELD_OWNERSHIP_FORWARD_LIST")) args = ARG_ROW_RE.findall(macro_block(text, "MGP_FIELD_OWNERSHIP_ARG_LIST")) verb_ops = PAIR_RE.findall(macro_block(text, "MGP_VERB_OP_LIST")) exempt = EXEMPT_RE.findall(macro_block(text, "MGP_VERB_OP_EXEMPT_LIST")) if not fields: sys.exit("gen_pipe_field_ownership: FieldOwnership.def's field list did not parse") return fields, forwards, args, verb_ops, exempt def parse_ops_and_verbs(calls_text=None, fill_points_text=None): """The two name spaces the stamp map joins, read from the files that define them: the catalog's calls (PipeCalls.def, which IS the MGPWireOp enum, with each call's KIND) and the verb set (FillPoints.def, which IS MG_Backend::GLFunctionsTable's member list).""" calls_text = read(PIPE_CALLS) if calls_text is None else calls_text fill_points_text = read(FILL_POINTS) if fill_points_text is None else fill_points_text calls = re.findall(r"X\(\s*(\w+)\s*,\s*\w+\s*,\s*(k\w+)\s*,", macro_block(calls_text, "MGP_CALL_LIST")) verbs = re.findall(r"X\(\s*(\w+)\s*,\s*(k\w+)\s*\)", macro_block(fill_points_text, "MGP_FILL_VERB_LIST")) if not calls: sys.exit("gen_pipe_field_ownership: PipeCalls.def's call list did not parse") if not verbs: sys.exit("gen_pipe_field_ownership: FillPoints.def's verb list did not parse") return calls, [v for v, _ in verbs] def array_block(text, declaration): """The braced initializer of a generated `... = {` table, comments KEPT. The generated tables carry the row's name in a trailing comment (`// DrawArrays`) and in a leading one (`/* 58 ReadPixels */`), and those comments are the only place the row's NAME appears - the values themselves are enumerators and hex words. So this masker's opposite is what is wanted here: the comments are the data.""" start = text.find(declaration) if start < 0: sys.exit("gen_pipe_field_ownership: %r is not in the generated table it should be in - " "the admission derivation (ID-116) reads it rather than restating it, so a " "renamed or moved table has to stop this script rather than produce an empty " "allowlist" % declaration) open_at = text.find("{", start) depth = 0 i = open_at while i < len(text): if text[i] == "{": depth += 1 elif text[i] == "}": depth -= 1 if depth == 0: return text[open_at + 1:i] i += 1 sys.exit("gen_pipe_field_ownership: %r never closes its initializer" % declaration) WAIT_ROW_RE = re.compile(r"/\*\s*\d+\s+(\w+)\s*\*/\s*static_cast\(\s*(k\w+)\s*\)") def parse_wait_classes(text=None): """{op name: wait class enumerator} out of generated/PipeWire.inc's kMGPipeWaitClasses. This is the STATIC half of MGPipeBarriered - the same column the emit table and the sink both compute from - and it is what decides whether a record is one the client is parked behind. A pair may only be admitted on a verb whose op is in it and is not kWaitNone.""" text = read(PIPE_WIRE_INC) if text is None else text block = array_block(text, "kMGPipeWaitClasses[static_cast(MGPWireOp::kOpCount)] =") rows = WAIT_ROW_RE.findall(block) if not rows: sys.exit("gen_pipe_field_ownership: kMGPipeWaitClasses did not parse - with no wait " "column every op would look unbarriered and the admitted set would be silently " "empty, which reads as 'the lane is clean' (ID-116)") waits = {} for op, wait in rows: waits[op] = wait return waits VERB_CLASS_ROW_RE = re.compile(r"MGPipeVerbClass::(\w+)\s*,\s*//\s*(\w+)") CLASS_MASK_ROW_RE = re.compile(r"//\s*(k\w+):[^\n]*\n\s*\{\{\s*(0x[0-9a-fA-F]+)ull\s*,\s*" r"(0x[0-9a-fA-F]+)ull\s*\}\}") def parse_verb_classes(text=None): """({verb: class}, {class: (word0, word1)}) out of generated/PipeFillPoints.inc. kMGPipeClassFieldMask is the verb's OWN may-read table: a field outside it is one the client's residual fill never copied for that verb, so it can never be a legitimate read there whatever its ownership row says. Intersecting with it is ID-84's third term.""" text = read(FILL_POINTS_INC) if text is None else text verb_rows = VERB_CLASS_ROW_RE.findall( array_block(text, "kMGPipeVerbClass[kMGPipeVerbCount] =")) mask_rows = CLASS_MASK_ROW_RE.findall( array_block(text, "kMGPipeClassFieldMask[kMGPipeVerbClassCount] =")) if not verb_rows: sys.exit("gen_pipe_field_ownership: kMGPipeVerbClass did not parse - the admitted set " "would lose its class intersection (ID-116)") if not mask_rows: sys.exit("gen_pipe_field_ownership: kMGPipeClassFieldMask did not parse - the admitted " "set would lose its class intersection (ID-116)") verb_class = {} for cls, verb in verb_rows: verb_class[verb] = cls class_mask = {} for cls, low, high in mask_rows: class_mask[cls] = (int(low, 16), int(high, 16)) for verb, cls in verb_class.items(): if cls not in class_mask: sys.exit("gen_pipe_field_ownership: verb %s is in class %s, which has no field mask" % (verb, cls)) return verb_class, class_mask THIS_PHASE = "P5e" PHASE_TOKEN_RE = re.compile(r"\bP\d+[a-z]*\b") def phase_is_owed_by_this_phase(retires): """Does this row's RetiringPhase column name THIS phase? Tokenised rather than substring-matched: the column is prose ("P5e (Espryt unbarriered), P7 (Magma)", "P3b/P4b (Espryt), P7 (Magma)", "P8 (indirect), P9 (readback), P13 (transfer)"), and a substring test would let a future "P5e2" or a "P5" answer for "P5e".""" return THIS_PHASE in PHASE_TOKEN_RE.findall(retires) def build_admitted(accessors, ownership, phase, verbs, verb_ops, waits, verb_class, class_mask): """ID-84 AS A DERIVATION (ID-116), WITH ID-125's SECOND DISJUNCT. A @ pull is ADMITTED iff the field's row is BARRIER_PULLED, the field is inside kMGPipeClassFieldMask[class of verb] - a field outside the verb's own may-read table was never filled for it - and EITHER 1. the verb's wire op is STATICALLY BARRIERED (MGPipeWaitClassFor(op) != kWaitNone), so the client is parked in its own wait and P5C's semantics hold for the record; OR 2. the field's RETIRING PHASE does not name this phase. ID-125 ADDED (2) AND IT IS THE HONEST STATEMENT OF ID-84. At runtime this table is only ever consulted on a record the server already stamped BARRIERED - CountBarrierPull's unbarriered arm is [[noreturn]] and fires first - so the record's pull is legal by construction and the only remaining question is whether THIS PHASE still owes the migration. The retiring-phase column is precisely that answer, and it is already in the table. Disjunct (1) survives as its own term because it is a stronger claim about the same pair: it says the client waits for the record STATICALLY, which is what lets a row whose phase IS this one still be admitted (GetTextureUnitObject@CopyTexImage2D was, until P15 made copy_framebuffer_to_texture fire-and-forget; the self-test barriers that op again to show it). Without (1) such a row 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. (1) IS A STATEMENT ABOUT EVERY OP THAT STAMPS THE VERB (P9, CONTRACT-P9.md §1). The mask is per verb and the server stamps the same verb for each op in MGP_VERB_OP_LIST that names it, so one op that publishes without a wait makes the verb's pull torn for THAT op's records. read_pixels_to_buffer stamps ReadPixels and waits for nothing, which is why GetFramebufferBindingSlot@ReadPixels - admitted by (1) until P9 - no longer is. The first version of this function kept the LAST op per verb, so the answer depended on the order of the stamp list. A verb with no stamp row still admits NOTHING under (1): the server stamps only the ops MGP_VERB_OP_LIST names. Under (2) it admits its non-P5e debts, which is correct for the same reason - the mask is consulted only where a stamp already happened. Returns (per-verb (word0, word1), the sorted @ pairs).""" field_index = {name: i for i, name in enumerate(accessors)} ops_for_verb = {} for op, verb in verb_ops: ops_for_verb.setdefault(verb, []).append(op) masks = [] pairs = [] for verb in verbs: words = [0, 0] ops = ops_for_verb.get(verb) op = ops[0] if ops else None barriered = bool(ops) and all(waits.get(o) not in (None, "kWaitNone") for o in ops) # 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 catalog's own kind (kCtxVerb) and a name that is also a verb's. Neither can see a call that is a verb boundary, is not kCtxVerb and is renamed - FieldOwnership.def names the one such call in the tree and says the phase that emits it writes its row.""" verbSet = set(verbs) return [name for name, kind in calls if kind == "kCtxVerb" or name in verbSet] def check_verb_ops(verb_ops, exempt, calls, verbs): """The stamp map, in BOTH directions. A row whose op or verb does not exist would become a switch arm that fails to compile. An OMITTED row is worse and is what this check exists for: the applier would run the record under the PREVIOUS verb's serial, mask and name, so a field inside that mask reads FRESH while holding the previous verb's value - the one failure in this package that is silent.""" opNames = [name for name, _ in calls] if not verb_ops: sys.exit("gen_pipe_field_ownership: MGP_VERB_OP_LIST is empty - the server would have " "no verb boundary to stamp at and every field would read @") seen = set() for op, verb in verb_ops: if op not in opNames: sys.exit("gen_pipe_field_ownership: the stamp map names op %s, which is not a call " "in PipeCalls.def" % op) if verb not in verbs: sys.exit("gen_pipe_field_ownership: the stamp map names verb %s, which is not a " "verb in FillPoints.def" % verb) if op in seen: sys.exit("gen_pipe_field_ownership: op %s has two stamp rows" % op) seen.add(op) required = verb_shaped_calls(calls, verbs) exemptMap = {} for op, why in exempt: if op not in opNames: sys.exit("gen_pipe_field_ownership: the stamp map exempts op %s, which is not a call " "in PipeCalls.def" % op) if op not in required: sys.exit("gen_pipe_field_ownership: op %s is exempted from the stamp map but is not " "verb-shaped, so it was never required - an exemption that exempts nothing " "reads as a decision that was made" % op) if op in seen: sys.exit("gen_pipe_field_ownership: op %s has both a stamp row and an exemption" % op) if not why.strip(): sys.exit("gen_pipe_field_ownership: op %s is exempted with no reason" % op) exemptMap[op] = why missing = [op for op in required if op not in seen and op not in exemptMap] if missing: sys.exit("gen_pipe_field_ownership: %d verb-shaped call(s) have no stamp row and no " "exemption: %s - an omitted stamp point is SILENT (the record would apply under " "the previous verb's serial, mask and name), so it is a build failure here" % (len(missing), ", ".join(missing))) return verb_ops, exemptMap, required def build(accessors, sticky, emitted, refused, rows, forwards, args): """The join, and every gate it is allowed to fail on. Returns (ownership, phase, why, forward rows, argument rows, counts).""" supplied = [f for f in emitted if f not in set(refused)] ownership = {} phase = {} why = {} for field in supplied: ownership[field] = "RECORD_SUPPLIED" phase[field] = "-" why[field] = "derived: Coverage.def's emitted list, and PipeFill.cpp does not refuse it" for field, cls, retires, reason in rows: if field not in accessors: sys.exit("gen_pipe_field_ownership: FieldOwnership.def names %s, which is not a " "PipeInputs field" % field) if cls not in CLASSES: sys.exit("gen_pipe_field_ownership: %s is in class %s, which is not one of %s" % (field, cls, "/".join(CLASSES))) if cls == "RECORD_SUPPLIED": sys.exit("gen_pipe_field_ownership: %s claims RECORD_SUPPLIED, which is DERIVED and " "may not be asserted by hand" % field) if field in ownership: sys.exit("gen_pipe_field_ownership: %s is in TWO classes - the derivation says " "RECORD_SUPPLIED and FieldOwnership.def says %s" % (field, cls)) if cls == "BARRIER_PULLED" and retires.strip() in ("", "-"): sys.exit("gen_pipe_field_ownership: %s is BARRIER_PULLED and names no retiring " "phase - P5's debt is only sized if every row says who pays it" % field) if cls != "BARRIER_PULLED" and retires.strip() != "-": sys.exit("gen_pipe_field_ownership: %s is %s and names a retiring phase; only " "BARRIER_PULLED rows have one" % (field, cls)) ownership[field] = cls phase[field] = retires why[field] = reason missing = [f for f in accessors if f not in ownership] if missing: sys.exit("gen_pipe_field_ownership: %d field(s) in NO class, which is a build failure " "(R-7.1): %s" % (len(missing), ", ".join(missing))) # The seven sticky forwards' own rows. They are the seven that hand the server a frontend # object or write into the frontend, so the gate is structurally blind on them without a # row of their own - and the row has to agree with the field row, or the two halves of the # same accessor would be documented as different things. forward_map = {} for field, cls, retires, mechanism in forwards: if field not in sticky: sys.exit("gen_pipe_field_ownership: %s has a FORWARD row but is not sticky in " "Coverage.def" % field) if field in forward_map: sys.exit("gen_pipe_field_ownership: %s has two FORWARD rows" % field) if cls not in CLASSES: sys.exit("gen_pipe_field_ownership: forward %s is in class %s, which is not one of " "%s" % (field, cls, "/".join(CLASSES))) if ownership[field] != cls: sys.exit("gen_pipe_field_ownership: %s's field row says %s and its forward row says " "%s; a read of a sticky field IS a call of its forward" % (field, ownership[field], cls)) forward_map[field] = (cls, retires, mechanism) absent = [f for f in sticky if f not in forward_map] if absent: sys.exit("gen_pipe_field_ownership: sticky forward(s) with no row: %s" % ", ".join(absent)) arg_rows = [] for field, arg0, cls, reason in args: if field not in accessors: sys.exit("gen_pipe_field_ownership: argument exception names %s, which is not a " "PipeInputs field" % field) if cls not in CLASSES: sys.exit("gen_pipe_field_ownership: argument exception %s(%s) is in class %s" % (field, arg0, cls)) if cls == ownership[field]: sys.exit("gen_pipe_field_ownership: argument exception %s(%s) repeats the field's " "own class (%s) and narrows nothing" % (field, arg0, cls)) arg_rows.append((field, int(arg0), cls, reason)) counts = {cls: sum(1 for f in accessors if ownership[f] == cls) for cls in CLASSES} return ownership, phase, why, forward_map, arg_rows, counts def emit(accessors, sticky, ownership, phase, why, forward_map, arg_rows, counts, verb_ops, exemptMap, verbs, admitted_masks, admitted_pairs): out = [BANNER.format(name=OUT_NAME)] add = out.append add(""" // The four classes. kUnclassified exists so the static_assert below has something to refuse; // the generator never emits it, which is what makes "a field in no class fails the build" // true at two independent points rather than one. enum class MGPipeFieldOwnership : Uint8 { kUnclassified = 0, kRecordSupplied, // a pushed record supplies the WHOLE field kApplierDerived, // the applier writes it out of records it already applies kBarrierPulled, // P5's debt: read out of the client's residual fill under the verb barrier kFatal, // no carrier and the reduced path never reads it }; inline constexpr const char* kMGPipeFieldOwnershipNames[] = { "UNCLASSIFIED", "RECORD-SUPPLIED", "APPLIER-DERIVED", "BARRIER-PULLED", "FATAL", }; """) add("inline constexpr MGPipeFieldOwnership kMGPipeFieldOwnership[kMGPipeInputFieldCount] = {") for field in accessors: add(" MGPipeFieldOwnership::%s, // %s" % (ENUMERATOR[ownership[field]], field)) add("};\n") add("// The ROADMAP phase whose row retires the pull. \"-\" for every class but BARRIER-PULLED.") add("inline constexpr const char* kMGPipeFieldRetiringPhase[kMGPipeInputFieldCount] = {") for field in accessors: add(" \"%s\", // %s" % (phase[field], field)) add("};\n") add("// The seven sticky forwards, which are among the 63 above and need a row of their own:") add("// they are the ones that hand the server a raw frontend object or write into the") add("// frontend, so the exit gate is structurally blind on them without one.") add("inline constexpr SizeT kMGPipeFieldOwnershipForwardCount = %d;" % len(sticky)) add("static_assert(kMGPipeFieldOwnershipForwardCount == kMGPipeInputStickyFieldCount,") add(" \"the forward rows and Coverage.def's sticky set are the same seven\");") add("inline constexpr MGPipeInputField kMGPipeFieldOwnershipForwardField[kMGPipeFieldOwnershipForwardCount] = {") for field in sticky: add(" MGPipeInputField::%s," % field) add("};") add("inline constexpr MGPipeFieldOwnership kMGPipeFieldOwnershipForward[kMGPipeFieldOwnershipForwardCount] = {") for field in sticky: add(" MGPipeFieldOwnership::%s, // %s" % (ENUMERATOR[forward_map[field][0]], field)) add("};") add("inline constexpr const char* kMGPipeFieldOwnershipForwardMechanism[kMGPipeFieldOwnershipForwardCount] = {") for field in sticky: add(" \"%s\", // %s, retires in %s" % (forward_map[field][2], field, forward_map[field][1])) add("};\n") add("// CONTRACT-P5.md section 3: \"70 rows, each in exactly one class\".") add("inline constexpr SizeT kMGPipeFieldOwnershipRowCount =") add(" kMGPipeInputFieldCount + kMGPipeFieldOwnershipForwardCount;") add("static_assert(kMGPipeFieldOwnershipRowCount == 70, \"table 2's row count moved\");\n") add("""// An ARGUMENT-KEYED narrowing of one field. The field keeps its single row above; this // says that one argument value of it belongs to a different class. Coverage.def's comment on the // GetBufferBindingSlot row already rules the shape - "The field is one array, so it stays one // row" - and m_pixelStore[2] is the same shape indexed by its own isUnpack argument. struct MGPipeFieldArgumentOwnership { MGPipeInputField Field; Uint32 Arg0; MGPipeFieldOwnership Class; };""") add("inline constexpr SizeT kMGPipeFieldArgumentOwnershipCount = %d;" % len(arg_rows)) add("inline constexpr MGPipeFieldArgumentOwnership") add(" kMGPipeFieldArgumentOwnership[kMGPipeFieldArgumentOwnershipCount] = {") for field, arg0, cls, reason in arg_rows: add(" {MGPipeInputField::%s, %du, MGPipeFieldOwnership::%s}, // %s" % (field, arg0, ENUMERATOR[cls], reason)) add("};\n") add("""constexpr MGPipeFieldOwnership MGPipeFieldOwnershipOf(MGPipeInputField field) { return kMGPipeFieldOwnership[static_cast(field)]; } // The same answer, narrowed by the accessor's first argument. Every accessor that takes one // may call this; only the fields with a row above answer differently from the field's class. constexpr MGPipeFieldOwnership MGPipeFieldOwnershipOf(MGPipeInputField field, Uint32 arg0) { for (SizeT i = 0; i < kMGPipeFieldArgumentOwnershipCount; ++i) { if (kMGPipeFieldArgumentOwnership[i].Field == field && kMGPipeFieldArgumentOwnership[i].Arg0 == arg0) { return kMGPipeFieldArgumentOwnership[i].Class; } } return MGPipeFieldOwnershipOf(field); } constexpr const char* MGPipeFieldOwnershipName(MGPipeFieldOwnership ownership) { return kMGPipeFieldOwnershipNames[static_cast(ownership)]; } // THE BUILD FAILURE R-7.1 ASKS FOR. The generator refuses to emit an unclassified row, so // this can only fire on a hand-edited header - which is exactly the edit the DO NOT EDIT // banner cannot prevent on its own. constexpr Bool MGPipeEveryFieldIsClassified() { for (SizeT i = 0; i < kMGPipeInputFieldCount; ++i) { if (kMGPipeFieldOwnership[i] == MGPipeFieldOwnership::kUnclassified) return false; } for (SizeT i = 0; i < kMGPipeFieldOwnershipForwardCount; ++i) { if (kMGPipeFieldOwnershipForward[i] == MGPipeFieldOwnership::kUnclassified) return false; } return true; } static_assert(MGPipeEveryFieldIsClassified(), "a PipeInputs field is in none of the four ownership classes (CONTRACT-P5 table 2, R-7.1)"); """) add("""// WHERE THE SERVER STAMPS. The wire's op and the fill's verb are different name spaces // and do not line up by name (draw_vbo is DrawArrays, blit is BlitFramebuffer), so this is the // join. An op with no row is NOT a verb boundary and the applier must not stamp on it. // // EVERY VERB-SHAPED CALL IS ANSWERED HERE OR EXEMPTED BY NAME, and the generator refuses an // omission: a verb-shaped record with no row would apply under the PREVIOUS verb's serial, // mask and name, so a field inside that mask would read FRESH while holding the previous // verb's value - the one silent failure this table has. The exemptions:""") for op in sorted(exemptMap): add("// %-16s %s" % (op, exemptMap[op])) add("""constexpr MGPipeVerb MGPipeVerbForWireOp(MGPWireOp op) { switch (op) {""") for op, verb in verb_ops: add(" case MGPWireOp::%s: return MGPipeVerb::%s;" % (op, verb)) add(""" default: return MGPipeVerb::kVerbCount; } } """) add("inline constexpr SizeT kMGPipeVerbBoundaryOpCount = %d;" % len(verb_ops)) add("inline constexpr SizeT kMGPipeVerbBoundaryExemptCount = %d;" % len(exemptMap)) add("") add("""// ---- THE §7 ALLOWLIST, DERIVED RATHER THAN WRITTEN (ID-116) -------------------------- // // CONTRACT-P5E §7 lists the barrier-pulled reads the phase ADMITS: debts that are real, ordered // and fresh because the client is parked behind the record, and that a LATER phase retires. It // was also kept by hand in .github/workflows/test.yml, and that copy was wrong in both // directions at once - it omitted GetFramebufferBindingSlot@ReadPixels, the largest survivor, // and carried GetTextureObject@CopyImageSubData, which nothing made safe. // // THE RULE IS ID-84 SAID IN TABLES THAT ALREADY EXIST. A @ pull is admitted iff // // 1. the field's ownership row is BARRIER-PULLED - it is a debt and not a defect; // 2. the verb's wire op is STATICALLY BARRIERED (kMGPipeWaitClasses[op] != kWaitNone), which // is exactly "the client is parked in its own wait for this record", so P5C's semantics // survive the flip for it; and // 3. the field is inside kMGPipeClassFieldMask[class of the verb] - a field outside the // verb's own may-read table was never filled for it, so a read there is stale by // construction whatever its ownership row says. // // Which makes the allowlist move with the code instead of beside it: retiring a verb's wait // class NARROWS it with no edit, and a new BARRIER_PULLED row widens it only on verbs that // wait. A verb with no stamp row admits nothing - the server stamps only MGP_VERB_OP_LIST's // ops, so no other verb can be the one a residual pull is reported against.""") add("inline constexpr MGPipeFieldMask kMGPipeAdmittedPullMask[kMGPipeVerbCount] = {") for verb, (low, high) in zip(verbs, admitted_masks): add(" {{0x%016xull, 0x%016xull}}, // %s" % (low, high, verb)) add("};\n") add("inline constexpr SizeT kMGPipeAdmittedPullPairCount = %d;" % len(admitted_pairs)) add(""" // THE PREDICATE THE STRICT KNOB ASKS (ID-117). A 69 x 128-bit table, so this costs a shift and // a test on the apply thread - the same shape MGPipeFieldMaskHas already has. constexpr Bool MGPipeBarrierPullAdmitted(MGPipeInputField field, MGPipeVerb verb) { const SizeT index = static_cast(verb); return index < kMGPipeVerbCount && MGPipeFieldMaskHas(kMGPipeAdmittedPullMask[index], field); } // THE HAND-EDIT CONTROL, MGPipeEveryFieldIsClassified's shape and for its reason: the generator // cannot emit a bit that fails this, so it can only fire on an edited header - which is exactly // the edit the DO NOT EDIT banner cannot prevent on its own. An admitted bit that was not a // BARRIER-PULLED field of its verb's class would be the allowlist quietly forgiving a read that // is torn rather than merely unmigrated. constexpr Bool MGPipeEveryAdmittedPullIsADebtOfItsVerbsClass() { for (SizeT v = 0; v < kMGPipeVerbCount; ++v) { const MGPipeFieldMask& admitted = kMGPipeAdmittedPullMask[v]; const MGPipeFieldMask& mayRead = kMGPipeClassFieldMask[static_cast(kMGPipeVerbClass[v])]; for (SizeT f = 0; f < kMGPipeInputFieldCount; ++f) { const auto field = static_cast(f); if (!MGPipeFieldMaskHas(admitted, field)) continue; if (kMGPipeFieldOwnership[f] != MGPipeFieldOwnership::kBarrierPulled) return false; if (!MGPipeFieldMaskHas(mayRead, field)) return false; } } return true; } static_assert(MGPipeEveryAdmittedPullIsADebtOfItsVerbsClass(), "an admitted barrier pull is not a BARRIER-PULLED field of its verb's class " "(CONTRACT-P5E section 7, ID-84 / ID-116)"); """) add("// The class sizes, as constants a test can pin without recounting the table.") for cls in CLASSES: add("inline constexpr SizeT kMGPipe%sFieldCount = %d;" % ("".join(p.capitalize() for p in cls.split("_")), counts[cls])) add("static_assert(%s == kMGPipeInputFieldCount, \"the four class sizes do not partition the field set\");" % " + ".join("kMGPipe%sFieldCount" % "".join(p.capitalize() for p in cls.split("_")) for cls in CLASSES)) return "\n".join(out) + "\n" def write(path, text, check_only, changed): existing = read(path) if os.path.exists(path) else None if existing == text: return changed.append(os.path.basename(path)) if not check_only: with open(path, "w", encoding="utf-8", newline="\n") as handle: handle.write(text) def expect_trip(name, because, fn, quiet=False): """A control that must exit FOR ITS OWN REASON. The first version of this function caught any SystemExit and asked nothing about which one, and that is exactly how control #4 came to be a silent duplicate of control #1: its replacement string was raw, so it mangled the row instead of blanking the phase, the row stopped parsing, and the generator exited with "a field in NO class" while the report counted a trip for "a BARRIER_PULLED row with no retiring phase". The guard that every debt row names its retiring phase therefore had no control at all. `because` is a substring the control's own message must contain. This is the discipline gen_pipe_dirty_surface.py's self_test already uses (it asserts each control's problem string) and it is the half that was dropped.""" try: fn() except SystemExit as exit: message = str(exit.code) if exit.code is not None else "" if because in message: return 1 if not quiet: print("gen_pipe_field_ownership: self-test: control %r tripped for SOMEONE ELSE'S " "reason:\n expected to contain: %s\n actually said: %s" % (name, because, message), file=sys.stderr) return 0 if not quiet: print("gen_pipe_field_ownership: self-test: control did NOT trip: %s" % name, file=sys.stderr) return 0 def require_no_barrier_pulls(ownership): pulled = sorted(field for field, cls in ownership.items() if cls == "BARRIER_PULLED") if pulled: sys.exit("gen_pipe_field_ownership: P5f forbids production BARRIER_PULLED rows: " + ", ".join(pulled)) def self_test(): """The negative controls (gen_pipe.py --self-test's shape): each gate must go red for its own reason, and zero trips is itself an error.""" coverage = read(COVERAGE_DEF) production_ownership_text = read(OWNERSHIP_DEF) # P5f has no live debt. Exercise admission's historical branches on an explicit # synthetic fixture, rather than requiring real client reads to keep tests alive. ownership_text = production_ownership_text fixture_phases = { "GetBoundVertexArray": "P5e (Espryt unbarriered), P7 (Magma)", "GetBufferBindingSlot": "P8/P9/P13", "GetBufferBindingPoint": "P5e (Espryt unbarriered), P7 (Magma)", "GetFramebufferBindingSlot": "P5e (Espryt unbarriered), P7 (Magma)", "GetImageTextureBinding": "P5e (Espryt unbarriered), P7 (Magma)", "GetTextureUnitObject": "P5e (Espryt unbarriered), P7 (Magma)", "GetProgramForDraw": "P5e (Espryt unbarriered), P7 (Magma)", "GetProgramForDispatch": "P5e (Espryt unbarriered), P7 (Magma)", "GetTransformFeedbackProgram": "P3b/P4b (Espryt), P7 (Magma)", "GetProgramObject": "P9", "GetTextureObject": "P7", "ValidateProgramName": "P9", "RecordError": "P9", } for field, phase in fixture_phases.items(): pattern = r'(X\(\s*' + field + r'\s*,)\s*FATAL,\s*"-",' ownership_text, count = re.subn(pattern, lambda m: m[1] + ' BARRIER_PULLED, "' + phase + '",', ownership_text) if count not in (1, 2): sys.exit("gen_pipe_field_ownership: fixture field is not retired: " + field) prefix, forward = ownership_text.split("#define MGP_FIELD_OWNERSHIP_FORWARD_LIST(X)", 1) forward = re.sub(r'(X\(RecordError,\s*BARRIER_PULLED,\s*"P9",\s*)"[^\"]*"', r'\1"OnGlError, synthetic legacy error forward"', forward, count=1) forward = re.sub(r'(X\(GetTextureObject,\s*BARRIER_PULLED,\s*"P7",\s*)"[^\"]*"', r'\1"a server-side texture handle table"', forward, count=1) ownership_text = prefix + "#define MGP_FIELD_OWNERSHIP_FORWARD_LIST(X)" + forward fill = read(PIPE_FILL) accessors, sticky, emitted = parse_coverage(coverage) 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) ref = parse_supplies_whole_field(fill_text if fill_text is not None else fill) rows, fwd, args, verb_ops, exempt = parse_ownership( own_text if own_text is not None else ownership_text) c, v = parse_ops_and_verbs(calls_text) if calls_text is not None else (calls, verbs) check_verb_ops(verb_ops, exempt, c, v) return build(acc, stk, emt, ref, rows, fwd, args) # The rows wrap over two lines with a trailing backslash, so every control below edits # them through a regex whose gaps tolerate that rather than through a literal that would # silently stop matching the day someone re-aligns the file. GAP = r"[\s\\]*" def edit(pattern, replacement, what, text=None): text = ownership_text if text is None else text edited, count = re.subn(pattern, replacement, text, count=1) if count != 1: sys.exit("gen_pipe_field_ownership: self-test: could not %s - the control's own " "edit no longer matches the file it is supposed to break" % what) return edited # Every control below is (name, the substring its own message must contain, the edit). The # substring is not decoration: see expect_trip. # 1. THE HEADLINE CONTROL (exit gate E4): take one field out of the table. It is in no # class, and that is a build failure rather than a silent default. GetBoundVertexArray is # the control's field since P5c rv (it keeps a hand-written BARRIER_PULLED row; the value # rows the first version used are RECORD_SUPPLIED-derived now, so they have no row to # edit). dropped = edit(r"X\(GetBoundVertexArray," + GAP + r"BARRIER_PULLED," + GAP + r"\"[^\"]*\"," + GAP + r"\"[^\"]*\"\)", "", "remove GetBoundVertexArray's row") controls = [("a field in NO class (GetBoundVertexArray's row removed)", "field(s) in NO class", lambda: run(own_text=dropped))] # 2. The other direction: a field the derivation already placed in RECORD_SUPPLIED, also # claimed by hand. E4's negative control is "move a field from supplied to FATAL". doubled = ownership_text.replace( "#define MGP_FIELD_OWNERSHIP_LIST(X)", "#define MGP_FIELD_OWNERSHIP_LIST(X) X(GetClearColor, FATAL, \"-\", \"moved by hand\") \\\n", 1) controls.append(("a RECORD_SUPPLIED field claimed by hand (supplied -> FATAL)", "GetClearColor is in TWO classes", lambda: run(own_text=doubled))) # 3. A row naming something that is not a field at all. typo = edit(r"X\(GetBoundVertexArray,", "X(GetBoundVertexArrayy,", "misspell a field name") controls.append(("a row naming a non-field", "GetBoundVertexArrayy, which is not a PipeInputs field", lambda: run(own_text=typo))) # 4. A BARRIER_PULLED row with no retiring phase: the debt is only sized if every row # says who pays it, which is the whole of R-7.2's "rsp IS the size of the debt". # THE REPLACEMENT IS NOT A RAW STRING. It was, and the backslashes survived into the # substitution, mangled the row past ROW_RE's reach and made this control a silent # duplicate of #1 for a whole round. unphased = edit(r"(X\(GetBoundVertexArray," + GAP + r"BARRIER_PULLED,)" + GAP + r"\"[^\"]*\",", "\\1 \"-\",", "blank a BARRIER_PULLED row's retiring phase") controls.append(("a BARRIER_PULLED row with no retiring phase", "GetBoundVertexArray is BARRIER_PULLED and names no retiring phase", lambda: run(own_text=unphased))) # 5. A class that is not one of the four. bogus = edit(r"(X\(GetBoundVertexArray,)" + GAP + r"BARRIER_PULLED,", "\\1 SOMEHOW_FINE,", "introduce a fifth class") controls.append(("a fifth class", "GetBoundVertexArray is in class SOMEHOW_FINE", lambda: run(own_text=bogus))) # 6. A sticky forward that lost its own row - the seven most dangerous fields are exactly # the ones a table without forward rows is blind to. no_forward = edit(r"X\(RecordError," + GAP + r"BARRIER_PULLED," + GAP + r"\"P9\"," + GAP + r"\"OnGlError[^\"]*\"\)", "", "remove RecordError's forward row") controls.append(("a sticky forward with no row", "sticky forward(s) with no row: RecordError", lambda: run(own_text=no_forward))) # 7. A forward row that disagrees with its field row. disagree = edit(r"X\(GetTextureObject," + GAP + r"BARRIER_PULLED," + GAP + r"\"P7\"," + GAP + r"\"a server-side texture handle table\"\)", "X(GetTextureObject, FATAL, \"-\", \"a server-side texture handle table\")", "contradict GetTextureObject's field row") controls.append(("a forward row that contradicts its field row", "field row says BARRIER_PULLED and its forward row says FATAL", lambda: run(own_text=disagree))) # 8. An argument exception that narrows nothing. same = edit(r"X\(GetPixelStoreParameters, 1, FATAL,", "X(GetPixelStoreParameters, 1, APPLIER_DERIVED,", "make the argument exception repeat the field's class") controls.append(("an argument exception that repeats the field's class", "narrows nothing", lambda: run(own_text=same))) # 9. THE DERIVATION'S OWN SOURCE. If EmittedCallSuppliesTheWholeField's refusals stop # parsing, every emitted field silently becomes RECORD_SUPPLIED and eight rows of this # table quietly contradict themselves - so an empty refusal set has to stop the script # rather than produce a plausible table. blinded = fill.replace("Bool EmittedCallSuppliesTheWholeField(MGPipeInputField field)", "Bool EmittedCallSuppliesTheWholeFieldXX(MGPipeInputField field)", 1) controls.append(("the derivation's source function renamed away", "EmittedCallSuppliesTheWholeField is not in PipeFill.cpp", lambda: run(fill_text=blinded))) # 10-11. THE STAMP MAP against both name spaces. bad_op = edit(r"X\(Clear,\s*Clear\)", "X(Klear, Clear)", "misspell a stamp map op") controls.append(("a stamp row naming an op that does not exist", "names op Klear, which is not a call in PipeCalls.def", lambda: run(own_text=bad_op))) bad_verb = edit(r"X\(DrawVbo,\s*DrawArrays\)", "X(DrawVbo, DrawArrayz)", "misspell a stamp map verb") controls.append(("a stamp row naming a verb that does not exist", "names verb DrawArrayz, which is not a verb in FillPoints.def", lambda: run(own_text=bad_verb))) # 12. THE OMISSION, which the first version of this gate could not see at all. A # verb-shaped call with neither a row nor an exemption is the one silent failure in # this package: the record applies under the PREVIOUS verb's serial, mask and name. no_row = edit(r"X\(GenerateMipmap,\s*GenerateMipmap\)", "", "remove GenerateMipmap's stamp row") controls.append(("a verb-shaped call with no stamp row and no exemption", "have no stamp row and no exemption: GenerateMipmap", lambda: run(own_text=no_row))) # 13. An exemption is a decision, so it may not be written for a call that was never # required - that would read as a ruling where there was none. idle = edit(r"#define MGP_VERB_OP_EXEMPT_LIST\(X\)", "#define MGP_VERB_OP_EXEMPT_LIST(X) X(SetDynamicState, \"not verb-shaped\") \\\n", "exempt a call that was never required") controls.append(("an exemption for a call that is not verb-shaped", "SetDynamicState is exempted from the stamp map but is not verb-shaped", lambda: run(own_text=idle))) # 14. An exemption with no reason is an absence with extra steps. mute = edit(r"X\(Flush," + GAP + r"\"", "X(Flush, \"\" \"", "blank an exemption's reason") controls.append(("an exemption with no reason", "Flush is exempted with no reason", lambda: run(own_text=mute))) # 15. THE REQUIRED SET'S OWN SOURCE. verb_shaped_calls reads PipeCalls.def's KIND column; if # that column stops parsing as kCtxVerb the required set collapses to the name matches # alone and control 12 would pass for the wrong reason. Renaming the kind is the cheapest # way to prove the kind is actually being read. kindless = read(PIPE_CALLS).replace("kCtxVerb", "kCtxVerbb") controls.append(("the catalog's kCtxVerb kind renamed away", "is exempted from the stamp map but is not verb-shaped", lambda: run(calls_text=kindless))) # ---- 16-18: THE ADMISSION DERIVATION'S OWN SOURCES (P5e gl, ID-116) ------------------- # # The allowlist is DERIVED from three generated tables. Each of them is read rather than # restated, so each of them can go missing - and a missing one does not produce a visibly # broken allowlist, it produces a SILENTLY EMPTY or SILENTLY WIDER one. An empty admitted # set reads in the lane as "nothing is admitted", which looks like rigour and is blindness. def admitted_pairs_for(own_text=None, wire_text=None, points_text=None): own, ph, _, _, _, _ = run(own_text=own_text) _, _, _, verb_ops_now, _ = parse_ownership( own_text if own_text is not None else ownership_text) waits_now = parse_wait_classes(wire_text if wire_text is not None else wire_inc) verb_class_now, class_mask_now = parse_verb_classes( points_text if points_text is not None else points_inc) return build_admitted(accessors, own, ph, verbs, verb_ops_now, waits_now, verb_class_now, class_mask_now)[1] no_waits = wire_inc.replace("kMGPipeWaitClasses[static_cast(MGPWireOp::kOpCount)] =", "kMGPipeWaitClassesXX[static_cast(MGPWireOp::kOpCount)] =", 1) controls.append(("the wait-class column renamed away", "kMGPipeWaitClasses", lambda: admitted_pairs_for(wire_text=no_waits))) no_verb_class = points_inc.replace("kMGPipeVerbClass[kMGPipeVerbCount] =", "kMGPipeVerbClassXX[kMGPipeVerbCount] =", 1) controls.append(("the verb-class column renamed away", "kMGPipeVerbClass[kMGPipeVerbCount]", lambda: admitted_pairs_for(points_text=no_verb_class))) no_class_mask = points_inc.replace("kMGPipeClassFieldMask[kMGPipeVerbClassCount] =", "kMGPipeClassFieldMaskXX[kMGPipeVerbClassCount] =", 1) controls.append(("the class field mask renamed away", "kMGPipeClassFieldMask[kMGPipeVerbClassCount]", lambda: admitted_pairs_for(points_text=no_class_mask))) # THE HARNESS'S OWN CONTROL, and it is the durable form of how M-1 was found. The defect was # not the escaping in control #4; it was that expect_trip asked "did something exit" rather # than "did THIS exit", so a control could silently become a duplicate of another. Prove the # harness can tell them apart: control #1's edit, asserted against control #4's reason, must # be REJECTED. Without this line the stricter harness could itself rot back. if expect_trip("(harness control) control #1's edit under control #4's reason", "names no retiring phase", lambda: run(own_text=dropped), quiet=True) != 0: sys.exit("gen_pipe_field_ownership: self-test: expect_trip accepted an exit that belongs " "to another control - the harness cannot tell one control from another, which is " "exactly the defect that let control #4 be a silent duplicate of control #1") controls.append(("a retired field is reintroduced as production debt", "P5f forbids production BARRIER_PULLED rows", lambda: require_no_barrier_pulls(run()[0]))) trips = 0 for name, because, fn in controls: trips += expect_trip(name, because, fn) # The positive control: the real tables pass, and they partition the real field set. production = run(own_text=production_ownership_text) require_no_barrier_pulls(production[0]) counts = production[-1] total = sum(counts.values()) if total != len(accessors): sys.exit("gen_pipe_field_ownership: self-test: the positive control does not partition " "the field set (%d of %d)" % (total, len(accessors))) if len(sticky) != 7: sys.exit("gen_pipe_field_ownership: self-test: Coverage.def no longer has seven sticky fields") # EIGHT SINCE P5e (5.6): GetBufferBindingPoint joined the seven # when set_shader_buffers got its Coverage.def emitted row. The number is pinned rather # than merely derived because it is the SIZE OF THE SHAPE-ONLY SET - the rows where an # emitted call exists and still does not supply the field - and a row that quietly left # that set would flip to RECORD_SUPPLIED and let the residual fill skip a pull nothing # replaces. Every addition to it is a phase's deliberate act, so it is spelled here. 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 -------------------- # P9 moved the first of them: read_pixels_to_buffer stamps ReadPixels and waits for nothing, # so ReadPixels is no longer statically barriered and its P5e-owed pair leaves (the P9 # controls below put it back by barriering that op, and take it away again from the other op). expect("GetFramebufferBindingSlot@ReadPixels is REJECTED since P9 (read_pixels_to_buffer " "stamps ReadPixels without a wait)", "GetFramebufferBindingSlot@ReadPixels" not in derived) # P15 moved the second: copy_framebuffer_to_texture is fire-and-forget (kWaitNone), so # CopyTexImage2D is no longer statically barriered and its P5e-owed pair leaves too. The # control below barriers that op again and the pair must come back by disjunct 1. expect("GetTextureUnitObject@CopyTexImage2D is REJECTED since P15 (copy_framebuffer_to_texture " "waits for nothing)", "GetTextureUnitObject@CopyTexImage2D" not 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 set_wait(op, wait_class, text=None): edited, count = re.subn( r"(/\*\s*\d+\s+" + op + r"\s*\*/\s*static_cast\()kWait\w+(\))", r"\g<1>" + wait_class + r"\2", wire_inc if text is None else text, count=1) if count != 1: sys.exit("gen_pipe_field_ownership: self-test: could not set %s's wait class - the " "control's own edit no longer matches generated/PipeWire.inc" % op) return edited def unbarrier(op, text=None): return set_wait(op, "kWaitNone", text) # P9: EVERY OP THAT STAMPS THE VERB. Barrier read_pixels_to_buffer as well and ReadPixels is # statically barriered again, so its P5e-owed pair comes back by disjunct 1 - which proves the # pair left above because of THAT op and not for some other reason. rewaited = set_wait("ReadPixelsToBuffer", "kWaitApplied") expect("barriering read_pixels_to_buffer too brings GetFramebufferBindingSlot@ReadPixels back " "(disjunct 1 needs every op that stamps the verb to wait)", "GetFramebufferBindingSlot@ReadPixels" in admitted_pairs_for(wire_text=rewaited)) unwaited = unbarrier("ReadPixels", rewaited) expect("unbarriering ReadPixels' own op drops the pair again " "(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)) recopied = set_wait("CopyFramebufferToTexture", "kWaitApplied") expect("barriering copy_framebuffer_to_texture brings GetTextureUnitObject@CopyTexImage2D back " "(disjunct 1)", "GetTextureUnitObject@CopyTexImage2D" in admitted_pairs_for(wire_text=recopied)) # 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. # A verb is unbarriered when ANY op that stamps it publishes without a wait (P9) - the same # rule build_admitted states, restated here so that the two cannot drift together. ops_for_verb = {} for op, verb in parse_ownership(ownership_text)[3]: ops_for_verb.setdefault(verb, []).append(op) ownership_now, phase_now = run()[0], run()[1] unbarriered_p5e = sorted( pair for pair in derived if (lambda f, v: (not ops_for_verb.get(v) or any(waits_real.get(o) in (None, "kWaitNone") for o in ops_for_verb[v])) 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") if trips != len(controls): sys.exit("gen_pipe_field_ownership: self-test: %d of %d negative controls did not trip" % (len(controls) - trips, len(controls))) 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 " "synthetic legacy allowlist is %d pair(s); production has zero debt" % (len(derivation), len(derived))) return 0 def main(): parser = argparse.ArgumentParser(description=__doc__) parser.add_argument("--check", action="store_true", help="do not write; exit 1 if regenerating would change anything") parser.add_argument("--self-test", action="store_true", help="run the negative controls (each gate must trip) and exit") parser.add_argument("--print-admitted", action="store_true", help="print the derived CONTRACT-P5E section 7 allowlist, one " "@ per line, and exit - so the CI shell and the C++ " "read the SAME table (ID-116)") args = parser.parse_args() if args.self_test: return self_test() accessors, sticky, emitted = parse_coverage() refused = parse_supplies_whole_field() rows, forwards, arg_rows, verb_ops, exempt = parse_ownership() calls, verbs = parse_ops_and_verbs() _, 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) require_no_barrier_pulls(ownership) 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, verbs, admitted_masks, admitted_pairs), args.check, changed) print("gen_pipe_field_ownership: %d fields + %d sticky forwards = %d rows; " "%d record-supplied (derived), %d applier-derived, %d barrier-pulled, %d fatal, " "%d argument exception(s)" % (len(accessors), len(sticky), len(accessors) + len(sticky), counts["RECORD_SUPPLIED"], counts["APPLIER_DERIVED"], counts["BARRIER_PULLED"], counts["FATAL"], len(arg_list))) print("gen_pipe_field_ownership: stamp map: %d verb-shaped call(s) = %d row(s) + %d " "exemption(s), 0 unanswered" % (len(required), len(verb_ops), len(exemptMap))) admitted_verbs = sorted({pair.split("@", 1)[1] for pair in admitted_pairs}) print("gen_pipe_field_ownership: section 7 allowlist (derived): %d admitted @ " "pair(s) across %d barriered verb(s): %s" % (len(admitted_pairs), len(admitted_verbs), ", ".join(admitted_verbs) or "-")) pulled = [(f, phase[f]) for f in accessors if ownership[f] == "BARRIER_PULLED"] print("gen_pipe_field_ownership: the debt, by retiring phase:") by_phase = {} for field, retires in pulled: by_phase.setdefault(retires, []).append(field) for retires in sorted(by_phase): print("gen_pipe_field_ownership: %-42s %d" % (retires, len(by_phase[retires]))) if changed: if args.check: print("gen_pipe_field_ownership: OUT OF DATE: %s" % ", ".join(changed), file=sys.stderr) return 1 print("gen_pipe_field_ownership: wrote %s" % ", ".join(changed)) else: print("gen_pipe_field_ownership: generated file is up to date") return 0 if __name__ == "__main__": sys.exit(main())