Schedule Equivalence

Schedule Equivalence: a plan's declared meaning is its dependency graph - which implies a PROMISE nobody usually tests: outputs must not depend on the schedule. Run the same plan at concurrency 1, 2, and 8; if the outputs differ, the plan has an undeclared dependency smuggled through shared state. This prover runs both an honest plan and a smuggler, and shows the exact fix.

source on github

a real captured run

SCHEDULE EQUIVALENCE (outputs must not know the schedule)

  honest plan across concurrency 1/2/8:
    identical outputs under every schedule - EQUIVALENT

  smuggler plan (same graph, plus a shared array on the side):
    concurrency 1  sum => "7 (a won the race)"
    concurrency 2  sum => "7 (b won the race)"
    concurrency 8  sum => "7 (b won the race)"
    DIVERGED: at concurrency 1 the schedule is the insertion order,
    so :a always wins; under parallelism the race decides. the
    output encodes WHO WON A RACE - meaning that travels outside
    every declared edge.

  the fix is always the same and always boring: whatever the shared
  state was whispering, SAY IT WITH AN EDGE - needs: hands the sum
  exactly the values it may know, and the graph becomes the whole
  truth. ruby/spec taught me that 'works on this implementation'
  means nothing until the behavior is pinned across VMs; same
  theorem here with schedules for VMs: a plan isn't correct until
  its outputs are a function of its GRAPH, and this prover is how
  you find the plans that are secretly functions of the clock.

source

# frozen_string_literal: true

# Schedule Equivalence: a plan's declared meaning is its dependency
# graph - which implies a PROMISE nobody usually tests: outputs must
# not depend on the schedule. Run the same plan at concurrency 1, 2,
# and 8; if the outputs differ, the plan has an undeclared dependency
# smuggled through shared state. This prover runs both an honest plan
# and a smuggler, and shows the exact fix.
#
#   bundle exec ruby examples/schedule_equivalence.rb
#
# Runs offline; exits 1 only if the HONEST plan proves schedule-dependent.

require class="s">"bundler/setup"
require class="s">"agentic"

Agentic.logger.level = class="y">:fatal

CONCURRENCIES = [1, 2, 8].freeze

def outputs_under(concurrency, &builder)
  orchestrator = Agentic:class="y">:PlanOrchestrator.new(concurrency_limit: concurrency)
  tasks = builder.call(orchestrator)
  result = orchestrator.execute_plan
  tasks.to_h { |name, task| [name, result.task_result(task.id).output] }
end

def equivalence_verdict(&builder)
  runs = CONCURRENCIES.to_h { |c| [c, outputs_under(c, &builder)] }
  baseline = runs[CONCURRENCIES.first]
  divergent = runs.reject { |_, outputs| outputs == baseline }.keys
  [runs, divergent]
end

# --- the honest plan: all communication travels the declared edges --------------
honest = lambda do |o|
  a = Agentic:class="y">:Task.new(description: class="s">"count_a", agent_spec: {class="s">"name" => class="s">"a", class="s">"instructions" => class="s">"w"})
  b = Agentic:class="y">:Task.new(description: class="s">"count_b", agent_spec: {class="s">"name" => class="s">"b", class="s">"instructions" => class="s">"w"})
  sum = Agentic:class="y">:Task.new(description: class="s">"sum", agent_spec: {class="s">"name" => class="s">"s", class="s">"instructions" => class="s">"w"})
  o.add_task(a, agent: ->(_t) {
    sleep(rand * 0.01)
    3
  })
  o.add_task(b, agent: ->(_t) {
    sleep(rand * 0.01)
    4
  })
  o.add_task(sum, needs: {a: a, b: b}, agent: ->(t) { t.needs[class="y">:a] + t.needs[class="y">:b] })
  {a: a, b: b, sum: sum}
end

# --- the smuggler: same shape, but tasks ALSO talk through a shared array --------
def smuggler_plan
  lambda do |o|
    ledger = [] # the contraband channel: order of arrival becomes meaning (fresh per run)
    a = Agentic:class="y">:Task.new(description: class="s">"count_a", agent_spec: {class="s">"name" => class="s">"a", class="s">"instructions" => class="s">"w"})
    b = Agentic:class="y">:Task.new(description: class="s">"count_b", agent_spec: {class="s">"name" => class="s">"b", class="s">"instructions" => class="s">"w"})
    sum = Agentic:class="y">:Task.new(description: class="s">"sum", agent_spec: {class="s">"name" => class="s">"s", class="s">"instructions" => class="s">"w"})
    o.add_task(a, agent: ->(_t) {
      sleep(rand * 0.01)
      ledger << class="y">:a
      3
    })
    o.add_task(b, agent: ->(_t) {
      sleep(rand * 0.01)
      ledger << class="y">:b
      4
    })
    # The sin: reading who arrived FIRST - information no edge declares
    o.add_task(sum, needs: {a: a, b: b}, agent: ->(t) {
      class="s">"#{t.needs[class="y">:a] + t.needs[class="y">:b]} (#{ledger.first} won the race)"
    })
    {a: a, b: b, sum: sum}
  end
end

puts class="s">"SCHEDULE EQUIVALENCE (outputs must not know the schedule)"
puts

_, honest_divergent = equivalence_verdict(&honest)
puts class="s">"  honest plan across concurrency #{CONCURRENCIES.join("/class="s">")}:"
puts class="s">"    #{honest_divergent.empty? ? "identical outputs under every schedule - EQUIVALENTclass="s">" : "DIVERGED at #{honest_divergent.join(class="s">", ")}class="s">"}"
puts

# The smuggler needs several attempts because races are shy under observation
diverged = false
5.times do
  runs, divergent = equivalence_verdict(&smuggler_plan)
  next if divergent.empty?

  diverged = true
  puts class="s">"  smuggler plan (same graph, plus a shared array on the side):"
  runs.each { |c, outputs| puts format(class="s">"    concurrency %-2d sum => %s", c, outputs[class="y">:sum].inspect) }
  puts class="s">"    DIVERGED: at concurrency 1 the schedule is the insertion order,"
  puts class="s">"    so class="y">:a always wins; under parallelism the race decides. the"
  puts class="s">"    output encodes WHO WON A RACE - meaning that travels outside"
  puts class="s">"    every declared edge."
  break
end
puts class="s">"  (smuggler raced identically this run - rerun to catch it; races are shy)" unless diverged
puts
puts class="s">"  the fix is always the same and always boring: whatever the shared"
puts class="s">"  state was whispering, SAY IT WITH AN EDGE - needs: hands the sum"
puts class="s">"  exactly the values it may know, and the graph becomes the whole"
puts class="s">"  truth. ruby/spec taught me that 'works on this implementation'"
puts class="s">"  means nothing until the behavior is pinned across VMs; same"
puts class="s">"  theorem here with schedules for VMs: a plan isn't correct until"
puts class="s">"  its outputs are a function of its GRAPH, and this prover is how"
puts class="s">"  you find the plans that are secretly functions of the clock."
exit(honest_divergent.empty? ? 0 : 1)