[MG_Remote, MG_Pipe, MG_Impl, MG_Backend] (Disaggregated): P5e ra - the wait rule, the present credit and server-owned gPipeInputs

- CONTRACT-P5E §2.3. EmitAndWaitTails now switches on the generated WaitClass column
  when RunAheadArmed(): kWaitNone and kWaitPresent return at the publish, kWaitApplied
  waits and then releases the fill pins, and a reply row is unchanged. It REPLACES the
  BatchWaits skip rather than layering on it - the batch rule reads the call CLASS and
  this one reads what an apply READS, and the server's MGPipeBarriered reads the second,
  so two rules layered is two halves of the wire disagreeing about whether the client is
  parked.
- §1: RunAheadArmed() = barrierArmed && Ipc.RunAhead && Caps().HasCap(kCapRunAheadApply),
  latched at the first caps adoption after Start and demotable but never promotable - a
  record already published without a wait cannot be un-published. A knob set against a
  server that does not publish the bit logs once and runs lockstep.
- §2.4: MGPPresent::FrameSerial is minted client-side, 1-based, by AcquirePresentCredit,
  which pays the credit BEFORE the encode (a client that encoded first would hold a
  SEG_CMD reservation across the park). ServerVerbSink::OnPresent returns one credit per
  swap through ServerSession::ReturnPresentCredit, which has had no production caller
  since v1 wrote it; serial 0 on a run-ahead server is Fatal{ProtocolCorruption,
  "Present.FrameSerial"}. The stats line and the wire ledger gain credit-waits.
- §2.5, the drains and the forced waits: every wait exit drains SEG_EVENT (the applied
  wait, the present-ack wait, the cmd-space wait and - through a hook the session lends
  the encoder - the stage bell); glFinish becomes WaitForApplyToCatchUp, since "the
  commands issued so far have completed" is a promise a queue nobody waits on can break;
  every Server* EGL forwarder waits first, because the control mailbox is pumped BETWEEN
  drain batches and a make-current landing between two run-ahead records is not a wrong
  pixel but a wrong everything. ServerSwapEGLBuffers is not on that list: present is the
  swap.
- §2.5 / ruling 15 (ID-93): resource_subdata's BUFFER half stops waiting. The row keeps
  kReplySlot, the server still posts, and the slot is never read - which is what makes
  the 64 KB persistent-map push fire-and-forget instead of a hidden round trip per block.
  MGPipeSubDataWantsItsReply is the one predicate, read by the route and by the emit
  table, so the two cannot disagree about whether a wait is owed. The texture half keeps
  its reply: DrainTextureSubData clears a level's dirty flag on the accepted answer.
- §3: gPipeInputs becomes server-role memory for unbarriered records. The tracker walk
  and the emitters still run - they produce records - but the serial bump, the verb
  stamp, the server-stamp withdrawal and the whole of step 4 do not, and
  MGPipeNoteFrontendMutation / MGPipeLeaveVerb return instead of writing. `fillOwed` is
  a separate name from `barriered` on purpose: the red-once is that one line.
- §3.3: MGPipeInputUnfreshRead's counter becomes an UNCONDITIONAL abort under an
  unbarriered record, knob or no knob, because the value is torn or stale by
  construction and there is nothing for a counter to count. The marker gains its reason
  so the lane's allowlist can tell the two apart.
- §3.5: RefusePipeInputsTouchWhileApplierOwnsIt is re-derived - under run-ahead the rule
  is "not at all unless you are the barriered fill", and the BatchWaits early return
  goes with the argument that justified it.
- §2.3's ReleaseFillPins drops the four O-class SharedPtr rows once a barriered apply
  returns: under lockstep the next fill overwrote them within a verb, under run-ahead a
  pinned VAO can make the apply thread its last owner a frame later.
- §2.7 / ruling 13 (ID-91): the deferred-destroy queue stays live, and an enqueue from
  an UNBARRIERED apply is now a named finding - loud once, Fatal under strict.
- NAMED DEVIATION from §3.1: the identity/liveness pair is still written on every verb.
  It is not a field of the residual model - no ownership row owns it, no record carries
  it, no server stamp can answer it - it is "does this process still have a GL context",
  which only this thread knows and every null-context guard reads.
- Inert until the integration commit: RunAheadArmed() is false while
  kMGPipeP5eRunAheadReady is, so every branch above answers as it did before.
This commit is contained in:
2026-09-18 07:58:06 -04:00
parent a3466e6f4c
commit 6e6b86e592
13 changed files with 867 additions and 58 deletions
+14 -4
View File
@@ -1034,10 +1034,20 @@ namespace MobileGL::MG_Remote::Client {
}
MG_Pipe::MGPPresent record{};
// FrameSerial 0 = "the server stamps its own". P5 has no client-side present credit
// (MOBILEGL_IPC_PRESENT_CREDIT is P6's), so a client-minted serial would be a second
// id space with no consumer.
record.FrameSerial = 0;
// P5e (ra, CONTRACT-P5E §1, §2.4). FrameSerial USED TO BE 0 - "the server stamps
// its own" - and that was honest while nothing paced on it. It is now minted here,
// 1-based, by AcquirePresentCredit, which also PAYS the credit: if this client
// already has MOBILEGL_IPC_PRESENT_CREDIT presents in flight it parks until the
// server's OnPresent returns one, and only then does it mint.
//
// THE CREDIT WAIT IS BEFORE THE ENCODE, WHICH IS NOT A DETAIL: EmitAndWait
// reserves SEG_CMD bytes as its first act, so a client that encoded and then
// parked would hold a ring reservation across a whole frame of server time. It
// also drains SEG_EVENT on its way out, like every other wait (§2.6).
//
// With run-ahead disarmed this is a counter and nothing else, and the record below
// travels exactly as it did - the present row's own barrier is the pacing there.
record.FrameSerial = session.AcquirePresentCredit();
session.EmitAndWait(MG_Pipe::MGPWireOp::Present, &record, sizeof(record), nullptr, 0,
nullptr, 0, nullptr);