ResNet-34's data-parallel step at SYNCHRONISED BatchNorm IS the single-device step at R·N #

ResNet34StepTieB.lean threads the label-smoothed loss cotangent down the batch-BN backward chain on ONE device and ties every parameter gradient node to the certified per-op gradient at the cotangent that chain delivers. This is its data-parallel twin, for the render ResNet34RenderB emits at replicas > 1: R replicas at batch N, every BatchNorm synchronised (bnFwdSite / bnBackSite / bnGammaSite), every parameter gradient all-reduced by its mean. The capstone r34_net_syncTiedB says that, for every parameter,

mean over the R replicas of replica r's gradient node, loss divided by B
  = the single-device gradient node at the global batch R·N, loss divided by R·B

— the gradient node r34_net_tiedB at N := R·N ties to the certified per-op gradient. So the sentence the DP render header carries ("this step IS the single-device step at the global batch") is a theorem, and the spec it is stated against has not moved: the right-hand side is the existing single-device chain at N := R·N.

Four steps #

The per-op facts behind each step are in DataParallel.SyncKit; this file states ResNet-34's block chains and ties over them.

1. Sharding — each replica's backward chain, handed its shard of a global cotangent, computes the shard of the global chain. Every non-BN link (relu mask, conv and strided-conv input-VJP, the 3×3/s2 pool's scatter, the head) is a per-example map and commutes with sharding by definition; the BN link is bnSyncInB, whose shard lemma bnSyncInB_shard is P2 on the graph (DataParallel.Sync.den_bnSyncBack_allReduce) carried across the mul_assoc seam.
2. The collectives — the mean over replicas of each replica's gradient node is 1/R of the global node at the global cotangent (the P4 lemmas of DataParallel.Sync and DataParallel.SyncKit). The γ node is the sync one, bnSyncGammaGradB, reading the forward's all-reduced statistics — the one parameter gradient sync-BN changes.
3. Homogeneity — the single-device chain and its gradient nodes are linear in the loss cotangent (*_smul): R × the cotangent gives R × every node.
4. The divisor — replica r divides its loss by B and the global step by R·B, so replica r's loss cotangent is R × its shard of the global one (replicaLossCot_eq). Steps 1–3 carry that R down the chain and it cancels the collective's 1/R.

What is NOT claimed #

The replicas' saved forward activations enter as the shards of the single-device forward's (batchShard r (r34Pre_k (R*N) w X)); that the sync forward graph computes exactly those is ResNet34SyncB.resnet34FwdGraphSyncFull_shard, the forward half. That the replicas' inputs are the shards of one batch is the driver's. The emitted artifacts run convBias := false, so the conv-bias nodes are not emitted and are not tied here (r34_net_tiedB keeps them for the flag). The lowerer's all_reduce is trusted as every other op's lowering is.

Precision is a flag on the statement. The ImageNet run the book reports trains from resnet34in_momdp64bf16, whose conv weight gradients are the bf16 kinds. Every conv weight collective below is stated on the renderers' switch — ConvWSyncAt bf16 / ConvStridedWSyncAt bf16 (Foundation.GradNodesBAt): the replicas' nodes and the batch-R·N node are the f32 kind at false and the bf16 kind at true — and the capstone takes bf16, so it covers that run's step read over ℝ at the identity rounding (Bf16Erasure), where each bf16 collective is 1/R of the batch-R·N bf16 node exactly as at f32 (DataParallel.SyncBf16's …_shard_id). At a real rounding the bf16 weight-gradient collective differs from the single-device node by the per-replica rounding of each partial sum, which SyncBf16 states and this file does not model, as the f32 tie does not model f32 rounding.

The block cotangents, each one line from the previous link's.

The gradient nodes.