Manuscript En05-B@1 · En05-B.tex · theorem · 8b626460

Theorem: Routing from every starting tick

A legal partition schedule under one clock · lines 726–791 · proof included or linked

En05-B@1#thm:routing, En05-B@1#eq:hubtime, En05-B@1#eq:alltime

Back to manuscript

For any starting tick and hubs at physical separation , a logical register can be delivered to the target hub in elapsed physical time at most

For arbitrary sites at physical separation , one may use

All waiting, junction transitions, initialization into a lane, and terminal delivery are included.

In particular, on journeys with ,

and the excess tends to zero uniformly.

Proof. For hubs, wait less than one frame, hence at most , for a phase-zero firing. Use the hub route of Lemma lem:hubroute. At the initial phase-zero firing, move the register from hub memory into the first outgoing port. Lemma lem:frame traverses the lane. At each intermediate phase-zero firing, move directly from the incoming port into the next outgoing port, inside the one junction block. Each complete lane consumes one frame of duration . After the last lane, the next phase-zero firing moves the register into target hub memory in one further tick. Thus

If the hubs coincide, waiting or local storage satisfies the same bound.

For an arbitrary starting site on a lane, wait until a transport frame starts. If its index is even, start forward movement at the first transport phase; if odd, start at the second. Advance to the last port, retain the register there, and move it into that hub at the next phase-zero firing. This costs at most . A register at a hub can similarly reach any specified site on one of its outgoing lanes in at most .

Choose these initial and final hubs. Each is within physical distance of its respective site. The hub-to-hub separation is at most . Applying (eq:hubtime) and adding the two endpoint costs gives

Storage is achieved by leaving the relevant memory factor unchanged, not by changing the partition schedule.

Displayed formulas in this passage

  • En05-B@1#eq:hubtime · line 731

  • En05-B@1#eq:alltime · line 737

  • unlabeled · line 748

  • unlabeled · line 767

  • unlabeled · line 786

Nearby in this section