GAC

GAC is a C++20 research harness for absorber-gated sparse computations. Its
selector checks algebraic legality, finds a usable rewrite scope, removes exact
post-lowering duplicates, and applies a cost policy to the remaining
candidates.

The main implementation is Boolean sparse matrix-vector multiplication.
The repository includes traversal and selector studies, exact work accounting,
provenance checks, compiler-facing experiments, and a small Lean formalisation of the core absorber semantics.

Project history

Most files were retro-imported after roughly seven to eight months of local
development. They were gathered and cleaned up near the end of that work before
being added here. The early commit dates show the import, not when the files
were first written.

Research papers

Version 1.0 of the papers matches repository release v1.0.0. Read the
focused manuscript first for the Boolean SpMV selection algorithm and its
evaluation. The companion extended technical report contains the complete
audit record. It is also the sole home of the broader semiring mechanism
studies, cross-host evidence, and resource-planning work.

How it works

GAC uses an additive absorber, a value that stays the same once a reduction
reaches it. In a pull kernel, that can let the current row finish early and in a
push kernel, it can avoid another update to an output that is already
saturated.

The Boolean SpMV implementation has four sources:

  csr_pull_ungated
  csr_pull_terminal_break
  csc_push_ungated
  csc_push_saturation_guard

Before picking one, GAC checks that the rewrite is valid and that there is
useful work left to skip. It also checks whether the compiler turned two source
candidates into the same machine code. It then estimates the cost of the
candidates left and keeps a trace showing why one was chosen.

Code map

These files cover the main path through the project:

  include/gac_harness/semirings.h
      semiring definitions and absorber properties

  include/gac_harness/absorber_scope_classifier.h
  src/absorber_scope_classifier*.cpp
      checks which absorber rewrite fits a loop

  include/gac_harness/boolean_spmv_candidates.h
  src/boolean_spmv_candidate_specializations.cpp
      the four Boolean SpMV kernels

  include/gac_harness/boolean_spmv_selector.h
  src/boolean_spmv_selector.cpp
      selection logic and its decision trace

  include/gac_harness/boolean_spmv_work_model.h
  src/boolean_spmv_work_model.cpp
      work estimates for pull and push

  include/gac_harness/post_lowering_candidate_identity.h
  src/post_lowering_candidate_identity.cpp
      checks whether lowered candidates are exact duplicates

  include/gac_harness/h8_memory.h
  src/h8_memory.cpp
      tracks requested bytes through a fixed event sequence

  formal/lean/gac_algebraic_semantics.lean
      small value-preservation proofs for the absorber rewrites

The kernels, selector, and experiment runners are C++. Python under `tools` is
used to run studies, check inputs and results, analyse data, and draw graphs/charts.

Build and test

To build from a checkout, you will need Git, CMake 3.25 or newer, Ninja,
Python 3, and a C++20 compiler.

  cmake -S . -B build -G Ninja -DBUILD_TESTING=ON
  cmake --build build
  ctest --test-dir build --output-on-failure

For a quicker pass, skip the tests labelled `slow`:

  ctest --test-dir build -LE slow --output-on-failure

There is also an unpinned Clang preset that uses the installed version:

  cmake --preset clang_debug
  cmake --build --preset clang_debug
  ctest --preset clang_debug

Clean targets are used for timing. Counted targets tally the work done by the
same kernels.

Extra checks

The Lean project is separate from the CMake build:

  cd formal/lean
  lake build

Run `cmake --list-presets` to see the pinned Linux builds. They expect the
recorded compiler versions and paths.

The SuiteSparse:GraphBLAS and TACO comparisons are optional. Their dependencies
are not stored here. The related presets expect prepared builds under the
ignored `third_party/h7` directory.

Old names and results

Some names in the tree come from earlier experiments. H2 through H8 are study
labels. Names containing `phase3` or `phase5` belong to a later selector
work that was done, so they are separate from H3 and H5. The older file versions are kept
because existing result records still use those formats.

A fresh clone has enough for the regular C++ tests and Lean checks. Re-running
the documented timings also need the recorded compilers, matrices, raw inputs,
and optional libraries.

The `corpus` directory holds study metadata and review records.
`corpus/public_commit_crosswalk.json` connects older reviews to
their corresponding sanitised public commits. A small set of compiler records
are kept under `results/selector`.


Layout

  include/gac_harness  C++ headers
  src                  C++ code and experiment runners
  tools                scripts for running and checking studies
  tests                C++ and Python tests
  corpus               study metadata and revision records
  formal/lean          Lean proofs
  generated            generated source kept for comparison
  results/selector     selected compiler records

Citation details are in `CITATION.cff`.

OpenPGP fingerprint:
  F559 DFA2 0198 401E 8687  F978 EBA6 F37C 3D59 AB7F

Public key:
  gac_paper_PGP.asc

Repository: https://github.com/000x999/GAC
Licence: GNU General Public License, version 2. See LICENSE.