Skip to content

Loops

Loops are how distributed algorithms are expressed. KlorPy supports one loop construct, while, with two regimes depending on where the condition's value lives.

Lockstep while (agreement condition)

If the condition reads only universal agreement values, every role evaluates the same boolean each iteration, so all roles loop in lockstep — no broadcast, no extra communication. Loop-carried variables updated identically at every role make the loop terminate together.

@choreography
def ring_rounds(rounds, init) -> A:
    acc = A(init)
    i = 0
    while i < rounds:            # i is agreement -> lockstep
        i = i + 1
        m1 = move(acc, A, B)
        bval = B(m1 + 1)
        m2 = move(bval, B, C)
        cval = C(m2 + 1)
        acc = move(cval, C, A)
    return acc

The body may still do real communication every pass (a token circles the ring above). What keeps the roles in step is the agreement condition, not the body.

Broadcast while (subset condition)

If the condition is located at a subset of roles (say only A owns the counter), one role decides and broadcasts a continue/stop token to every other role at each iteration, so the non-deciding roles run their bodies and exit together with the decider.

c = A(n)                 # the counter lives at A
result = A(0)
while c > 0:             # condition located at {A} -> A decides, B is kept in step
    b = move(result, A, B)
    bb = B(b + 1)
    result = move(bb, B, A)
    c2 = A(c - 1)
    c = c2

A condition no one can evaluate

A condition whose operands live at disjoint roles (e.g. x > y with x at A and y at B) is rejected: no single role can decide it.

break and continue

Both are supported inside lockstep loops only, and must appear under an agreement guard so every role breaks/skips together:

too_far = i > limit    # agreement guard
if too_far:
    break

is_even = i % 2 == 0
if is_even:
    continue

Anything else is rejected at definition time:

  • break/continue inside a broadcast loop (the token protocol can't absorb unpredictable early exits);
  • break outside a loop (Python itself already rejects this).

Type stability

The static type checker requires loop-carried variables to keep a stable location across the loop: n = B(i) inside a while after n = A(0) is a type error. This prevents a variable from "relocating" mid-loop in a way the per-role programs couldn't track. See Types & parameters.