Add CMake option to auto-detect and link tcmalloc or jemalloc by tautschnig · Pull Request #8973 · diffblue/cbmc

tautschnig · 2026-04-27T10:24:49Z

Add -Dallocator=auto|tcmalloc|jemalloc|system CMake option. When set to 'auto' (the default), CMake searches for tcmalloc then jemalloc and links the first one found. This gives 18-25% speedup on typical CBMC workloads due to better handling of many small allocations.

tcmalloc and jemalloc both use thread-local caches and size-class segregation that are much faster than glibc's malloc for CBMC's workload pattern (millions of ~64-128 byte irept tree nodes).

Also tested: mimalloc (~1% improvement, not worth the dependency), glibc tuning via MALLOC_ARENA_MAX/MALLOC_TRIM_THRESHOLD (~1-3%).

On macOS, the system allocator (libmalloc) already uses magazine-based allocation similar to tcmalloc, so the improvement is smaller. On Windows, the default allocator is also reasonably fast for small objects. Use -Dallocator=system to disable.

Install: apt-get install libgoogle-perftools-dev (or libjemalloc-dev)

Each commit message has a non-empty body, explaining why the change was made.
n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

Add -Dallocator=auto|tcmalloc|jemalloc|system CMake option. When set to 'auto' (the default), CMake searches for tcmalloc then jemalloc and links the first one found. This gives 18-25% speedup on typical CBMC workloads due to better handling of many small allocations. tcmalloc and jemalloc both use thread-local caches and size-class segregation that are much faster than glibc's malloc for CBMC's workload pattern (millions of ~64-128 byte irept tree nodes). Also tested: mimalloc (~1% improvement, not worth the dependency), glibc tuning via MALLOC_ARENA_MAX/MALLOC_TRIM_THRESHOLD (~1-3%). On macOS, the system allocator (libmalloc) already uses magazine-based allocation similar to tcmalloc, so the improvement is smaller. On Windows, the default allocator is also reasonably fast for small objects. Use -Dallocator=system to disable. Install: apt-get install libgoogle-perftools-dev (or libjemalloc-dev) Co-authored-by: Kiro <[email protected]>

Add libgoogle-perftools-dev to apt-get install in all Linux CI workflows that build CBMC with CMake. The CMake allocator auto- detection will find and link tcmalloc, giving 18-25% speedup on all CBMC runs. Workflows updated: - build-and-test-Linux.yaml - pull-request-checks.yaml (CMake-based jobs) - performance.yaml - coverage.yaml - profiling.yaml Co-authored-by: Kiro <[email protected]>

Copilot

Pull request overview

Note

Copilot was unable to run its full agentic suite in this review.

Adds a CMake-controlled memory allocator selection mechanism (auto/tcmalloc/jemalloc/system) and links it into CBMC-related executables to improve performance on allocation-heavy workloads.

Changes:

Introduces a new allocator CMake cache option with auto-detection and an INTERFACE link target (cprover_allocator).
Links cprover_allocator into several executables (cbmc, goto-*, symtab2gb).
Updates GitHub Actions workflows to install libgoogle-perftools-dev (tcmalloc provider) on Linux CI runners.

Reviewed changes

Copilot reviewed 13 out of 13 changed files in this pull request and generated 5 comments.

Show a summary per file

File	Description
CMakeLists.txt	Adds allocator selection logic + `cprover_allocator` interface target
src/cbmc/CMakeLists.txt	Links `cbmc` with `cprover_allocator`
src/goto-cc/CMakeLists.txt	Links `goto-cc` with `cprover_allocator`
src/goto-analyzer/CMakeLists.txt	Links `goto-analyzer` with `cprover_allocator`
src/goto-diff/CMakeLists.txt	Links `goto-diff` with `cprover_allocator`
src/goto-harness/CMakeLists.txt	Links `goto-harness` with `cprover_allocator`
src/goto-instrument/CMakeLists.txt	Links `goto-instrument` with `cprover_allocator`
src/symtab2gb/CMakeLists.txt	Links `symtab2gb` with `cprover_allocator`
.github/workflows/pull-request-checks.yaml	Installs `libgoogle-perftools-dev` in multiple jobs
.github/workflows/build-and-test-Linux.yaml	Installs `libgoogle-perftools-dev`
.github/workflows/performance.yaml	Installs `libgoogle-perftools-dev`
.github/workflows/coverage.yaml	Installs `libgoogle-perftools-dev`
.github/workflows/profiling.yaml	Adds a note about `perf_event_paranoid`

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

Copilot · 2026-04-27T10:46:52Z

+set(allocator "auto" CACHE STRING "Memory allocator: auto, tcmalloc, jemalloc, or system")
+
+if(NOT allocator STREQUAL "system")
+    if(allocator STREQUAL "auto" OR allocator STREQUAL "tcmalloc")
+        find_library(TCMALLOC_LIB NAMES tcmalloc_minimal tcmalloc)
+    endif()
+    if(allocator STREQUAL "auto" OR allocator STREQUAL "jemalloc")
+        find_library(JEMALLOC_LIB NAMES jemalloc)
+    endif()


The allocator cache option accepts arbitrary strings, but invalid values currently fall through silently (e.g., -Dallocator=jemaloc results in no allocator selection and no diagnostic). Add explicit validation for allowed values (and fail fast with a helpful error) and consider advertising valid values to CMake UIs via set_property(CACHE allocator PROPERTY STRINGS auto tcmalloc jemalloc system).

Copilot · 2026-04-27T10:46:53Z

+set(allocator "auto" CACHE STRING "Memory allocator: auto, tcmalloc, jemalloc, or system")
+
+if(NOT allocator STREQUAL "system")
+    if(allocator STREQUAL "auto" OR allocator STREQUAL "tcmalloc")
+        find_library(TCMALLOC_LIB NAMES tcmalloc_minimal tcmalloc)
+    endif()
+    if(allocator STREQUAL "auto" OR allocator STREQUAL "jemalloc")
+        find_library(JEMALLOC_LIB NAMES jemalloc)
+    endif()
+
+    if(allocator STREQUAL "tcmalloc")
+        if(NOT TCMALLOC_LIB)
+            message(FATAL_ERROR "tcmalloc requested but not found")
+        endif()
+        set(CBMC_ALLOCATOR_LIB ${TCMALLOC_LIB})
+        message(STATUS "Using tcmalloc: ${TCMALLOC_LIB}")
+    elseif(allocator STREQUAL "jemalloc")
+        if(NOT JEMALLOC_LIB)
+            message(FATAL_ERROR "jemalloc requested but not found")
+        endif()
+        set(CBMC_ALLOCATOR_LIB ${JEMALLOC_LIB})
+        message(STATUS "Using jemalloc: ${JEMALLOC_LIB}")
+    elseif(allocator STREQUAL "auto")


The cache variable name allocator is very generic and can collide with parent projects when CBMC is used as a subproject. Prefer a project-prefixed cache variable (e.g., CBMC_ALLOCATOR) and then map it internally as needed.

Suggested change

set(allocator "auto" CACHE STRING "Memory allocator: auto, tcmalloc, jemalloc, or system")

if(NOT allocator STREQUAL "system")

if(allocator STREQUAL "auto" OR allocator STREQUAL "tcmalloc")

find_library(TCMALLOC_LIB NAMES tcmalloc_minimal tcmalloc)

endif()

if(allocator STREQUAL "auto" OR allocator STREQUAL "jemalloc")

find_library(JEMALLOC_LIB NAMES jemalloc)

endif()

if(allocator STREQUAL "tcmalloc")

if(NOT TCMALLOC_LIB)

message(FATAL_ERROR "tcmalloc requested but not found")

endif()

set(CBMC_ALLOCATOR_LIB ${TCMALLOC_LIB})

message(STATUS "Using tcmalloc: ${TCMALLOC_LIB}")

elseif(allocator STREQUAL "jemalloc")

if(NOT JEMALLOC_LIB)

message(FATAL_ERROR "jemalloc requested but not found")

endif()

set(CBMC_ALLOCATOR_LIB ${JEMALLOC_LIB})

message(STATUS "Using jemalloc: ${JEMALLOC_LIB}")

elseif(allocator STREQUAL "auto")

set(CBMC_ALLOCATOR "auto" CACHE STRING "Memory allocator: auto, tcmalloc, jemalloc, or system")

if(NOT CBMC_ALLOCATOR STREQUAL "system")

if(CBMC_ALLOCATOR STREQUAL "auto" OR CBMC_ALLOCATOR STREQUAL "tcmalloc")

find_library(TCMALLOC_LIB NAMES tcmalloc_minimal tcmalloc)

endif()

if(CBMC_ALLOCATOR STREQUAL "auto" OR CBMC_ALLOCATOR STREQUAL "jemalloc")

find_library(JEMALLOC_LIB NAMES jemalloc)

endif()

if(CBMC_ALLOCATOR STREQUAL "tcmalloc")

if(NOT TCMALLOC_LIB)

message(FATAL_ERROR "tcmalloc requested but not found")

endif()

set(CBMC_ALLOCATOR_LIB ${TCMALLOC_LIB})

message(STATUS "Using tcmalloc: ${TCMALLOC_LIB}")

elseif(CBMC_ALLOCATOR STREQUAL "jemalloc")

if(NOT JEMALLOC_LIB)

message(FATAL_ERROR "jemalloc requested but not found")

endif()

set(CBMC_ALLOCATOR_LIB ${JEMALLOC_LIB})

message(STATUS "Using jemalloc: ${JEMALLOC_LIB}")

elseif(CBMC_ALLOCATOR STREQUAL "auto")

Copilot · 2026-04-27T10:46:53Z

+if(CBMC_ALLOCATOR_LIB)
+    add_library(cprover_allocator INTERFACE)
+    target_link_libraries(cprover_allocator INTERFACE ${CBMC_ALLOCATOR_LIB})
+else()
+    add_library(cprover_allocator INTERFACE)


add_library(cprover_allocator INTERFACE) is duplicated in both branches. Create the interface library once, then conditionally add target_link_libraries(...) when CBMC_ALLOCATOR_LIB is set; this reduces branching and makes it harder to accidentally diverge behavior later.

Suggested change

if(CBMC_ALLOCATOR_LIB)

add_library(cprover_allocator INTERFACE)

target_link_libraries(cprover_allocator INTERFACE ${CBMC_ALLOCATOR_LIB})

else()

add_library(cprover_allocator INTERFACE)

add_library(cprover_allocator INTERFACE)

if(CBMC_ALLOCATOR_LIB)

target_link_libraries(cprover_allocator INTERFACE ${CBMC_ALLOCATOR_LIB})

Copilot · 2026-04-27T10:46:53Z

        run: |
          sudo apt-get update
-          sudo apt-get install --no-install-recommends -yq gcc gdb g++ maven jq flex bison libxml2-utils ccache cmake z3
+          sudo apt-get install --no-install-recommends -yq gcc gdb g++ maven jq flex bison libxml2-utils ccache cmake z3 libgoogle-perftools-dev


Installing libgoogle-perftools-dev in CI will likely cause the default allocator=auto to select tcmalloc, changing the allocator used in most CI runs versus developer environments and historical CI baselines. Consider either (a) explicitly configuring CI builds with -Dallocator=system to keep CI consistent, or (b) gating installation/usage to a dedicated performance job that validates allocator linking, rather than affecting all build/test jobs.

Suggested change

sudo apt-get install --no-install-recommends -yq gcc gdb g++ maven jq flex bison libxml2-utils ccache cmake z3 libgoogle-perftools-dev

sudo apt-get install --no-install-recommends -yq gcc gdb g++ maven jq flex bison libxml2-utils ccache cmake z3

Copilot · 2026-04-27T10:46:53Z

+# Alternative memory allocator for improved performance.
+# tcmalloc and jemalloc give 18-25% speedup on typical CBMC workloads
+# due to better handling of many small allocations (irept tree nodes).
+# Set to "auto" to detect, or "tcmalloc", "jemalloc", or "system".
+set(allocator "auto" CACHE STRING "Memory allocator: auto, tcmalloc, jemalloc, or system")


This introduces a user-visible build option (-Dallocator=...) but the PR description indicates the User Guide wasn’t updated. Add a brief section to the manual documenting the option, defaults, platform notes, and the required packages (e.g., libgoogle-perftools-dev / libjemalloc-dev) so users can discover and use it without reading CMake code.

codecov · 2026-04-27T10:57:31Z

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 80.50%. Comparing base (b32074b) to head (c488451).

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #8973      +/-   ##
===========================================
- Coverage    80.50%   80.50%   -0.01%     
===========================================
  Files         1704     1704              
  Lines       188778   188778              
  Branches        73       74       +1     
===========================================
- Hits        151975   151974       -1     
- Misses       36803    36804       +1

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

tautschnig and others added 2 commits April 27, 2026 10:23

tautschnig self-assigned this Apr 27, 2026

Copilot AI review requested due to automatic review settings April 27, 2026 10:24

tautschnig requested review from a team and peterschrammel as code owners April 27, 2026 10:24

Copilot AI reviewed Apr 27, 2026

View reviewed changes

Copilot started reviewing on behalf of tautschnig April 27, 2026 12:33 View session

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add CMake option to auto-detect and link tcmalloc or jemalloc#8973

Add CMake option to auto-detect and link tcmalloc or jemalloc#8973
tautschnig wants to merge 2 commits intodiffblue:developfrom
tautschnig:tcmalloc

tautschnig commented Apr 27, 2026

Uh oh!

Copilot AI left a comment

Uh oh!

Copilot AI Apr 27, 2026

Uh oh!

Copilot AI Apr 27, 2026

Uh oh!

Copilot AI Apr 27, 2026

Uh oh!

Copilot AI Apr 27, 2026

Uh oh!

Copilot AI Apr 27, 2026

Uh oh!

codecov Bot commented Apr 27, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

	sudo apt-get install --no-install-recommends -yq gcc gdb g++ maven jq flex bison libxml2-utils ccache cmake z3 libgoogle-perftools-dev
	sudo apt-get install --no-install-recommends -yq gcc gdb g++ maven jq flex bison libxml2-utils ccache cmake z3

Conversation

tautschnig commented Apr 27, 2026

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Copilot AI Apr 27, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Apr 27, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Apr 27, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Apr 27, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Apr 27, 2026

Choose a reason for hiding this comment

Uh oh!

codecov Bot commented Apr 27, 2026

Codecov Report

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants