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.

for over agreement sequences

for is sugar for a lockstep loop: the iterable must be an agreement sequence (every role sees the same items — it may read only universal values), so the roles iterate in step; the loop variable is agreement.

@choreography
def along(n) -> A:
    total = A(0)
    for i in range(n):
        r0 = move(total, A, B)
        b = B(r0 + 1)
        total = move(b, B, A)
    return total

break/continue work exactly as in a lockstep while (under agreement guards). for over a value located at a subset of roles is rejected — the roles would see different items and desync. for ... else is not supported.

Recursion

A choreography may call itself by name (defchor-style). Each role calls its own endpoint, with the parameters that are located at it; roles stay in step because the recursion is driven by the same agreement guard at every role.

@choreography
def sum_to(n) -> A:
    base = n <= 0
    if base:
        r = A(0)
    else:
        below = sum_to(n - 1)   # recursive call: located at the return location
        r = A(below + n)
    return r

simulate_chor(sum_to, {"n": 4})    # => {'A': 10, 'B': NOOP}

Rules (checked at definition time):

  • A recursive choreography must declare its return location in the -> annotation (def sum_to(n) -> A:) — that is what gives the recursive call its location.
  • The -> location must agree with the non-recursive (base) return's location; the type checker catches a base case that returns elsewhere.
  • Self-recursion only: mutual recursion / forward declarations are not implemented yet.
  • Termination is the same story as while: the recursion must reach a base case, otherwise it recurses forever.

The base case can even involve real communication between the roles at every level (the recursion test relay_recursive moves a value A → B → A on each unwind).