ExMaude. Pool
(ExMaude v0.2.0)
View Source
Poolboy-based pool of Maude server processes.
This module manages a pool of backend workers (Port, C-Node, or NIF), providing:
- Automatic worker checkout/checkin
- Connection pooling for concurrent operations
- Worker supervision and restart
Configuration
config :ex_maude,
backend: :port, # :port | :cnode | :nif
pool_size: 4, # Number of Maude processes
pool_max_overflow: 2 # Extra workers under loadUsage
The pool is typically accessed via ExMaude.Maude rather than directly:
# Checkout, execute, and checkin automatically
ExMaude.Pool.transaction(fn worker ->
ExMaude.Server.execute(worker, "reduce in NAT : 1 + 2 .")
end)Architecture
ExMaude.Pool (Poolboy)
│
├── Worker 1 (Backend.impl()) ─── Maude Process 1
├── Worker 2 (Backend.impl()) ─── Maude Process 2
├── Worker 3 (Backend.impl()) ─── Maude Process 3
└── Worker 4 (Backend.impl()) ─── Maude Process 4Telemetry
This module emits the following telemetry events:
[:ex_maude, :pool, :checkout, :start]- Emitted when checkout begins[:ex_maude, :pool, :checkout, :stop]- Emitted when checkout completes
Measurements include :duration in native time units.
Metadata includes :result (:ok or :error) and :backend.
See ExMaude.Telemetry for full event documentation and integration examples.
Summary
Functions
Broadcasts a function to all workers in the pool.
Returns a worker to the pool.
Checks out a worker from the pool.
Returns the child spec for the pool supervisor.
Returns the current pool status.
Executes a function with a checked-out worker.
Functions
@spec broadcast(fun()) :: [:ok | {:error, ExMaude.Error.t() | term()}]
Broadcasts a function to all workers in the pool.
Useful for operations that need to affect all Maude sessions, such as loading a module.
Examples
ExMaude.Pool.broadcast(fn worker ->
ExMaude.Server.load_file(worker, "/path/to/module.maude")
end)
@spec checkin(pid()) :: :ok
Returns a worker to the pool.
@spec checkout(keyword()) :: pid() | :full | {:error, ExMaude.Error.t()}
Checks out a worker from the pool.
Remember to check the worker back in with checkin/1.
Prefer transaction/2 for automatic resource management.
@spec child_spec(keyword()) :: {atom(), {:poolboy, :start_link, [any()]}, :permanent, 5000, :worker, [:poolboy]}
Returns the child spec for the pool supervisor.
Options
:worker_module- Override the backend module (default:Backend.impl()):pool_size- Number of workers (default: from config):pool_max_overflow- Extra workers under load (default: from config)
@spec status() :: %{ size: non_neg_integer(), overflow: non_neg_integer(), available: non_neg_integer(), in_use: integer(), state: atom() }
Returns the current pool status.
Examples
ExMaude.Pool.status()
#=> %{size: 4, overflow: 0, available: 3, in_use: 1}
@spec transaction( (pid() -> result), keyword() ) :: result | {:error, ExMaude.Error.t()} when result: any()
Executes a function with a checked-out worker.
The worker is automatically returned to the pool after the function completes.
Examples
ExMaude.Pool.transaction(fn worker ->
ExMaude.Server.execute(worker, "reduce in NAT : 1 + 2 .")
end)Options
:timeout- Checkout timeout in ms (default: 5000)