ExMaude Benchmarks

View Source
Run in Livebook 
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)
|> Enum.each(fn {:ok, {:ok, _}} -> :ok end)

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 -> {:ok, _} = 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 and Scheduling Overhead

The pool holds pool_size persistent Maude processes, plus a bounded overflow: extra workers spawned under pressure and torn down afterwards. Starting overflow workers adds process startup costs to the measured workload.

Uncapped concurrency starts 50 tasks. Calls beyond the persistent pool size may start overflow workers or wait for a worker:

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()
    |> Enum.each(fn {:ok, _} -> :ok end)
  end)

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

Capped concurrency limits active tasks to the persistent pool size:

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

{sequential_us, _} =
  :timer.tc(fn ->
    Enum.each(expressions, fn expression -> {:ok, _} = ExMaude.reduce("NAT", expression) end)
  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

Pairwise detection examines each unordered pair once: n * (n - 1) / 2 pairs. Rule complexity, result size, and Maude matching costs also affect elapsed time. Measure representative policies when choosing request deadlines and pool size. Independent rule sets can use separate workers, subject to available CPU and memory.

Pool Health

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

ExMaude.Pool.status()

Interpreting Results

  • Use the measured latency for your workload when setting request deadlines.
  • Compare capped, uncapped, and sequential execution on your deployment hardware.
  • Benchmark heavy searches separately from short reductions.
  • Include rule count and rule complexity in conflict-detection measurements.

Next Steps