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 load

Usage

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 4

Telemetry

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

broadcast(fun)

@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)

checkin(worker)

@spec checkin(pid()) :: :ok

Returns a worker to the pool.

checkout(opts \\ [])

@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.

child_spec(opts \\ [])

@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)

status()

@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}

transaction(fun, opts \\ [])

@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)