ExMaude Benchmarks

app_root = Path.expand("..", __DIR__)

if File.exists?(Path.join(app_root, "mix.exs")) do
  # Running from a clone of the repository: use the local checkout,
  # which bundles the Maude interpreter under priv/.
  Mix.install(
    [{:ex_maude, path: app_root, env: :dev}],
    config_path: :ex_maude,
    lockfile: :ex_maude,
    config: [ex_maude: [use_pty: false]]
  )
else
  # Running standalone (e.g. via the "Run in Livebook" badge): use the
  # released package. This needs a `maude` binary on your PATH, or the
  # MAUDE_PATH env var set — see https://github.com/futhr/ex_maude#installation
  Mix.install(
    [{:ex_maude, "~> 0.4"}],
    config: [ex_maude: [use_pty: false]]
  )
end

{:ok, _pool_supervisor} =
  Supervisor.start_link([ExMaude.Pool.child_spec()], strategy: :one_for_one)

What We're Measuring

Three questions matter in practice:

1. Latency — how long does one round trip to Maude take?
2. Concurrency — when does the worker pool help, and when does it hurt?
3. Verification cost — how does conflict detection scale with rule-set size?

All numbers below are indicative and depend on your machine — run the cells and see your own. First, warm the pool so every worker's Maude process is up before we time anything:

pool_size = ExMaude.Pool.status().size

1..pool_size
|> Task.async_stream(fn _ -> ExMaude.reduce("NAT", "1 + 1") end)
|> Stream.run()

ExMaude.Pool.status()

Single-Operation Latency

One reduce is one round trip: check out a worker, write the command down a pipe, Maude evaluates, parse the reply:

{time_us, {:ok, result}} =
  :timer.tc(fn ->
    ExMaude.reduce("NAT", "100 * 100")
  end)

IO.puts("reduce: #{time_us} µs -> #{result}")

Typically well under a millisecond. The computation itself is nearly free — the round trip dominates, which is the key fact for interpreting everything below.

{time_us, {:ok, result}} =
  :timer.tc(fn ->
    ExMaude.reduce("NAT", "2 ^ 100")
  end)

IO.puts("2 ^ 100: #{time_us} µs -> #{result}")

Throughput

Back-to-back operations on a single caller:

duration_ms = 1000
start_time = System.monotonic_time(:millisecond)
end_time = start_time + duration_ms

count =
  Stream.repeatedly(fn -> ExMaude.reduce("NAT", "1 + 1") end)
  |> Stream.take_while(fn _ -> System.monotonic_time(:millisecond) < end_time end)
  |> Enum.count()

IO.puts("Throughput (single caller): #{count} operations/second")

Concurrency: the Right Way and the Wrong Way

The pool holds pool_size persistent Maude processes, plus a bounded overflow: extra workers spawned under pressure and torn down afterwards. Spawning a Maude OS process costs milliseconds — orders of magnitude more than the microsecond operations above. That leads to a perhaps surprising result.

Wrong way — fire 50 unbounded tasks at once. Every task beyond the pool size forces an overflow spawn or queues up, and the spawn cost swamps the work:

expressions = for i <- 1..50, do: "#{i} + #{i}"

{uncapped_us, _} =
  :timer.tc(fn ->
    expressions
    |> Enum.map(&Task.async(fn -> ExMaude.reduce("NAT", &1) end))
    |> Task.await_many()
  end)

IO.puts("50 ops, uncapped Task.async: #{div(uncapped_us, 1000)} ms")

Right way — cap concurrency at the pool size, so every operation lands on an already-warm worker:

{capped_us, _} =
  :timer.tc(fn ->
    expressions
    |> Task.async_stream(&ExMaude.reduce("NAT", &1), max_concurrency: pool_size)
    |> Stream.run()
  end)

{sequential_us, _} =
  :timer.tc(fn ->
    Enum.each(expressions, &ExMaude.reduce("NAT", &1))
  end)

IO.puts("50 ops, capped at pool size: #{div(capped_us, 1000)} ms")
IO.puts("50 ops, sequential:          #{div(sequential_us, 1000)} ms")

Two honest lessons in those numbers:

• Uncapped fan-out is dramatically slower than doing nothing clever at all.
• For microsecond operations, even well-capped parallelism barely beats sequential — the per-call round trip dominates either way. The pool pays off for expensive operations (deep searches, conflict detection) and for serving many independent callers, not for accelerating a burst of trivial reduces.

Search Cost vs Depth

Search explores the state space breadth-first, so cost grows with the frontier it must visit:

traffic_light = """
mod TRAFFIC-LIGHT is
  sort Light .
  ops red yellow green : -> Light [ctor] .

  rl [to-green]  : red => green .
  rl [to-yellow] : green => yellow .
  rl [to-red]    : yellow => red .
endm
"""

ExMaude.load_module(traffic_light)

for depth <- [1, 3, 5, 10] do
  {time_us, {:ok, solutions}} =
    :timer.tc(fn ->
      ExMaude.search("TRAFFIC-LIGHT", "red", "L:Light",
        max_solutions: 100,
        max_depth: depth
      )
    end)

  IO.puts("depth #{String.pad_leading(to_string(depth), 2)}: #{time_us} µs, #{length(solutions)} solutions")
end

:ok

A three-state cycle saturates quickly — after depth 2 there is nothing new to find, so the cost plateaus. Systems with genuinely growing state spaces behave differently, as the next section shows.

The Real Workload: Conflict Detection

Conflict detection is where ExMaude earns its keep, and its cost scales with the rule set: more rules mean more pairs to check and a bigger state space per check. Generate rule sets of increasing size over a small fleet of devices and time the verification:

ExMaude.load_file(ExMaude.iot_rules_path())

make_rules = fn n ->
  for i <- 1..n do
    %{
      id: "rule-#{i}",
      thing_id: "device-#{rem(i, 5)}",
      trigger: {:prop_gt, "temperature", 20 + i},
      actions: [
        {:set_prop, "device-#{rem(i, 5)}", "state", if(rem(i, 2) == 0, do: "on", else: "off")}
      ],
      priority: rem(i, 3)
    }
  end
end

for n <- [2, 4, 8, 12, 16] do
  {time_us, {:ok, conflicts}} =
    :timer.tc(fn ->
      ExMaude.IoT.detect_conflicts(make_rules.(n), timeout: 60_000)
    end)

  IO.puts(
    "#{String.pad_leading(to_string(n), 2)} rules: " <>
      "#{String.pad_leading(to_string(div(time_us, 1000)), 5)} ms, " <>
      "#{length(conflicts)} conflicts"
  )
end

:ok

Note the growth is superlinear — verification explores interactions, not rules in isolation. This is the number to watch when sizing a deployment: small rule sets verify in milliseconds (fine for a synchronous API call), while large ones may belong in a background job. Since checks for independent rule sets parallelize across the pool, total throughput scales with pool_size for these heavier calls — this is exactly the workload the pool exists for.

Pool Health

After all of the above, the pool should be back at rest — all workers available, overflow drained:

ExMaude.Pool.status()

Summary

• Latency: a Maude round trip runs in the tens-to-hundreds of microseconds; the pipe round trip, not the computation, dominates for small terms.
• Concurrency: cap fan-out at the pool size (Task.async_stream + max_concurrency). Uncapped fan-out triggers overflow-worker churn and is slower than sequential execution.
• Parallelism pays for heavy calls: deep searches and conflict detection scale across pool workers; microsecond reduces do not.
• Verification cost grows superlinearly with rule count — verify early, verify incrementally, and budget accordingly.

Next Steps

• Advanced Usage — the conflict-detection workflow these numbers describe
• Term Rewriting — what search is actually doing
• Quick Start — the basics