ResNet-50's data-parallel forward at SYNCHRONISED BatchNorm — replica r IS shard r #

ResNet50FullB says the typed batch-BN graph denotes resnet50ForwardBFull N q w on one device (resnet50FwdGraphBFull_faithful). At replicas > 1 the data-parallel render makes every BatchNorm site bnFwdSite's sync-BN composition — this replica's mean all-reduced, then Chan's σ²_r + (μ_r − μ)² all-reduced, packed, then bnSyncF — so the statistics each replica normalises by are the GLOBAL batch's. This file is that theorem's data-parallel twin: that forward graph, stated as a family over the R replicas, denotes on replica r exactly batchShard r of the single-device forward at the global batch R·N.

den (resnet50FwdGraphSyncFull R hR N q epsStr w bf16 e r)
  = batchShard R N nCls (resnet50ForwardBFull (R * N) q w X) r

given that each replica's input is its shard of one global batch X. The spec does not move: the right-hand side is the committed resnet50ForwardBFull, at N := R·N. The resolution stays a binder: one statement covers q = 7 (224 px) and q = 5 (160 px), the ladder written as the single-device graph writes it, 2 * (…) nests throughout.

How it is proved #

By induction on the chain, one block at a time, exactly as resnet50FwdGraphBFull_faithful is — with the shard hypothesis ∀ r, den (e r) = batchShard R N _ X r as the invariant carried from block to block. Every piece that is not about the bottleneck is ResNet34SyncB's, imported:

• every conv, relu, pool, GAP and dense node is a per-example lift, and sharding commutes with it (den_batchOp_shard, den_relu_shard);
• every BatchNorm site is bnSyncSiteLA, whose shard lemma den_bnSyncSiteLA is DataParallelSync.den_bnSyncF_allReduce (P1 on the graph) read at the network's index;
• the stem and the head are ResNet-34's sync graphs verbatim (r34StemGraphSync, r34HeadGraphSync) — R50's stem and head ARE those functions at other widths, and they emit the same names (%sW, %sg, %sbt, %Wd, %bd).

What is new is the three bottleneck forms at variable shapes (N ic mid oc h w all variables), each with three sync sites (four with the projection). The two projection forms add in the RENDER's order, addVB(body, projection), where residualProj proj body adds proj + body; that costs one commutation, den_addVB_shard_comm, exactly the add_comm the single-device graph carries.

The index seam #

The conv/relu chain runs at the left-assoc index N·(c·h·w); bnSyncF and its statistics nodes at N·(c·(h·w)). The sync site carries the relabelling as castIdx on the AST value (ResNet-34's bnSyncSiteLA), which changes no emitted text.

What is NOT claimed here #

No stochastic depth: the graph is the drop-path-free forward, as the single-device graph is. The nodes at either precision — bf16 selects the conv kinds at every site, as ResNet34SyncB, true being the bf16 DP artifacts' graph (resnet50in160_lambaccdp4x128wxclipbcebf16, …), read at the identity rounding (Bf16Erasure). The DP artifacts run with no conv biases; the bias operand is biasName false "" c, the render's own function, and the bias fields stay ∀-quantified as in ResNet50FullB. The backward and the parameter collectives are ResNet50SyncTieB.r50_net_syncTiedB's. That the R replicas' inputs ARE the shards of one batch is the driver's, as in DataParallel.Sync. The lowerer's all_reduce is trusted as every other op's lowering is.