package memprof-limits

Memprof-limits — Memory limits, allocation limits, and thread cancellation for OCaml

Memprof-limits is an implementation of (per-thread) global memory limits, (per-thread) allocation limits, and cancellation of CPU-bound threads, for OCaml. Memprof-limits interrupts a computation by raising an exception asynchronously and offers features to recover from them such as interrupt-safe resources.

The implementation uses OCaml's Memprof engine with a low sampling rate that does not affect performance. A reimplementation of the Gc.Memprof module is also provided for the purpose of profiling without interfering with interrupts.

To help the programmer implement the recovery from a memprof-limits interrupts, resource-management facilities and a detailed explanation are provided with this software. This documentation summarises the experience acquired in the Rocq prover, as well as in other programming languages.

Memprof-limits supports OCaml 5 (starting from 5.3) but full support for profiling with the Memprof_limits.Memprof reimplementation of Gc.Memprof requires OCaml ≥ 5.5.

• Home page: https://gitlab.com/gadmm/memprof-limits/
• Documentation: https://guillaume.munch.name/software/ocaml/memprof-limits/
• Changes: https://gitlab.com/gadmm/memprof-limits/-/blob/master/CHANGES.md

Memprof-limits is distributed under the LGPL license version 3 with linking exception, see LICENSE.

Installation

Memprof-limits can be installed with Opam: opam install memprof-limits. It requires OCaml 4.12 or newer for OCaml 4, and OCaml 5.3 or newer for OCaml 5.

Compilation from sources is done with make. Testing is done with make test.

Building the documentation

• Building the documentation with graphs requires odoc and odoc-driver and involves the following steps:

  • Compile and install memprof-limits in the current opam switch: opam install --working-dir .
  • Compile the documentation with odoc-driver: odoc_driver --remap memprof-limits
  • The documentation is then available in the _html/ subdir.
• Building the documentation with make doc uses odoc via dune and does not support graphs. The documentation is then available at _build/default/_doc/_html.

Documentation

• Guide with use cases and examples.
• Reference manual.
• A statistical analysis of the limits.
• A guide to recover from interrupts.
• Changes.
• FAQ.