From adcd7d2f05e5f5463c861064eeb968dddd5f1550 Mon Sep 17 00:00:00 2001 From: Diogo Behrens Date: Thu, 27 Nov 2025 09:50:04 +0000 Subject: [PATCH 1/2] cicd: Fine tuning of file filtering Signed-off-by: Diogo Behrens --- .github/workflows/actions.yml | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/.github/workflows/actions.yml b/.github/workflows/actions.yml index 887e583..9f42cfb 100644 --- a/.github/workflows/actions.yml +++ b/.github/workflows/actions.yml @@ -16,6 +16,9 @@ jobs: verify: ${{ steps.verify.outputs.changed }} test: ${{ steps.test.outputs.changed }} steps: + - uses: actions/checkout@v4 + with: + fetch-depth: 0 - uses: dorny/paths-filter@v3 id: include with: @@ -33,7 +36,10 @@ jobs: with: filters: | changed: - - 'verify/**' + - 'verify/**.bpl' + - 'verify/**.rs' + - 'verify/**.sh' + - 'verify/**.txt' - uses: dorny/paths-filter@v3 id: test with: From 84c80312e767588d7d0fdf7ba6a9a55bd97928de Mon Sep 17 00:00:00 2001 From: Diogo Behrens Date: Tue, 25 Nov 2025 12:58:45 +0100 Subject: [PATCH 2/2] doc: Improve documentation in verify Signed-off-by: Diogo Behrens --- doc/VERIFICATION.md | 176 ++++++++++++++++++++++ verify/README.md | 34 +---- verify/boogie/atomics_list.txt | 10 -- verify/boogie/templates/BoogieTemplate.md | 54 ------- 4 files changed, 177 insertions(+), 97 deletions(-) create mode 100644 doc/VERIFICATION.md delete mode 100644 verify/boogie/atomics_list.txt delete mode 100644 verify/boogie/templates/BoogieTemplate.md diff --git a/doc/VERIFICATION.md b/doc/VERIFICATION.md new file mode 100644 index 0000000..17a0239 --- /dev/null +++ b/doc/VERIFICATION.md @@ -0,0 +1,176 @@ +# Verification Guide + +`vatomic` ships a Boogie-based pipeline that checks each atomic primitive +against the [VSync Memory Model][]. The verification assets live under `verify/` +and power the `build_boogie_*` targets exposed by CMake. + +[VSync Memory Model]: ../vmm.cat +[VMM]: ../vmm.cat + +## Dependencies + +The verification targets are available when configuring the project with +`-DVATOMIC_TESTS=ON` (the default for top-level builds). Locally you will need: + +- CMake (>= 3.16) and a build backend (Ninja or Make) +- A Rust toolchain (`cargo`) to build the assembly parser/generator in + `verify/src` +- Boogie CLI (`boogie`) and its SMT solver dependency (Z3) +- Cross compilers: `aarch64-linux-gnu-gcc` (ARMv8) and + `riscv64-linux-gnu-gcc` (RISC-V) + +### Details + +- Boogie support for irreducible control flow (needed for several atomics) + only landed in release [**3.5.5**][] (see our [contribution to + upstream][]). Stick to that version or newer when running the pipeline + outside the CI image. +- Z3 results varied wildly with old releases. Use at least the version baked + into `.github/Dockerfile.boogie` (currently **z3-solver 4.13.0.0** from + PyPI) to match CI behaviour. +- The cross-compilers shipped with Ubuntu 24.04 (GCC **13.2** series, as + installed in `.github/Dockerfile.boogie`) are the minimum known-good + versions. Older Ubuntu toolchains could not inline the builtin assembly + that powers the verification flow. + +[contribution to upstream]: https://github.com/boogie-org/boogie/pull/1032 +[**3.5.5**]: https://github.com/boogie-org/boogie/releases/tag/v3.5.5 + +### Using the CICD container + +CI uses the container image `ghcr.io/open-s4c/vatomic/boogie-ci:latest`, +which bundles all of the above. You can pull it locally if you prefer a +hermetic environment. + +```sh +docker pull ghcr.io/open-s4c/vatomic/boogie-ci:latest +``` + +Then you can start the container mounting the vatomic directory as follows: + +```sh +cd vatomic +docker run -it --rm -v $(pwd):$(pwd) -w $(pwd) -u $(id -u):$(id -g) \ + ghcr.io/open-s4c/vatomic/boogie-ci:latest +``` + +You current `vatomic` directory is mounted over the exact same path in the +container (`-v` flag), and you start with the workdir set to that directory +(`-w` flag). Also the user id and user group match the ids in the host (`-u` +flag), so that if you create files they preserve the right ownership after +leaving the container. + +Inside the container, you can follow the instructions in the next section. + +--- + +## Running the verification suite + +1. Configure the project and enable `VATOMIC_TESTS` targets: + + ```sh + cmake -S . -B build -DVATOMIC_TESTS=ON + ``` + +2. Build one (or all) Boogie targets. Available options are `lse`, `llsc`, + `lxe`, and `no_polite_await`. + + ```sh + cmake --build build --target build_boogie_lse + ``` + + Each target: + + - Preprocesses `vsync/atomic.h` with the chosen compiler flags to obtain + `atomic.s` (and optionally sanitises it via `cleaner.sh`). + - Runs the Rust generator (`cargo run` via `generate.sh`) to parse the + assembly and emit Boogie (`.bpl`) files. + - Instantiates the templates under `verify/boogie/templates`. + - Executes Boogie to prove each atomic operation (driven by `verify.sh`). + +3. Inspect results via CTest or directly in the generated logs: + + ```sh + ctest --test-dir build/verify -R lse --output-on-failure + # Logs: build/verify/lse/*.log + ``` + +### Customising the toolchain + +- Pass `-DARMV8_CMAKE_C_COMPILER=/path/to/aarch64-linux-gnu-gcc` or + `-DRISCV_CMAKE_C_COMPILER=/path/to/riscv64-linux-gnu-gcc` to override the + default cross compilers. +- Set `BPL`/`Z3_EXE` or adjust `PATH` so Boogie and Z3 are discoverable. +- Export `CARGO` to point at a specific `cargo` binary when multiple toolchains + coexist on the system. + +--- + +## Maintaining the function list + +The lists of verified entry points lives in `verify/lists`. When adding new +atomic primitives, update that file so the verification targets cover the +new functions. Refer to the [Boogie templates](#boogie-templates) section +for the available templates and how they map to atomic behaviour. + +--- + +## Boogie templates + +Each `.bpl` template describes some aspect of correctness for the supported +atomics. For each atomic, one or more templates are instantiated to fully +specify the proof obligations. The templates are: + +- `read_only` — describes atomics that never write, e.g., `read`, `await` + (non-RMW) +- `read` — describes atomics that perform a read, e.g., `RMW`, `read`, `await`, + `await-RMW` +- `write` — describes `write` atomics +- `await` — describes `await` and `await-RMW` atomics +- `rmw` — describes atomics performing a read-modify-write operation, e.g., + `RMW` and `await-RMW` + +### Template parameters + +Each template uses one or more of the following parameters, written as `#NAME`: + +- `#registers` — comma separated identifiers specifying all registers used in + the function, e.g., `a0, a1, a2, x5, x6`. +- `#address` — identifier specifying the register that originally holds the + address, e.g., `a0`. +- `#input1` — identifier for the register holding the first function argument, + e.g., for `write(a, v)` the value of `v`, or for `cmpxchg(a, e, v)` the value + of `e`. Could be `a1`. +- `#input2` — second function argument. Could be `a2`. +- `#output` — register holding the output value at the end of the function, + e.g., `a0`. +- `#implementation` — body of the function, including assumes for all procedure + parameters, code, and two basic loop invariants. +- `#state` — comma separated list of identifiers for all additional state + introduced by the architecture, e.g., `local_monitor, monitor_exclusive`. + +### Template matrix + +List of templates and their functions: + +| template | write number | return value | store order | load order | +|--------------|--------------|--------------|-------------|------------| +| `read_only` | 0 | output | – | – | +| `read` | – | ret | – | yes | +| `write` | ≤1 | – | yes | – | +| `await` | – | await cond | – | – | +| `must_store` | 1 (+value) | – | yes | – | +| `rmw` | (+op) | – | yes | – | + +List of templates used by each atomic: + +| template | read | write | RMW | await | await RMW | +|--------------|------|-------|-----|-------|-----------| +| `read_only` | x | | | x | | +| `read` | x | | x | x | x | +| `write` | | x | x | | x | +| `await` | | | | x | x | +| `must_store` | | x | | | | +| `rmw` | | | x | | x | + +--- diff --git a/verify/README.md b/verify/README.md index 42a63fe..00c985b 100644 --- a/verify/README.md +++ b/verify/README.md @@ -1,33 +1 @@ -# Builtin Atomics Verification - -## Prerequisites - -To run the verification scripts, one needs to have *Ruby*, *Rust*, *Boogie* and *Z3* installations. To run the verification with parallelism, the `parallel` gem is also needed and can be installed by -``` - gem install parallel -``` - -## Generating the assembly file - -The assembly file with the builtin atomics can be generated by: - -``` - aarch64-linux-gnu-gcc -DVATOMIC_BUILTINS -O2 -x c include/vsync/atomic.h -Iinclude -fkeep-inline-functions -S -mno-outline-atomics -o atomics.s -``` - The `atomics.s` file should be located in the `armv8` subfolder - - ## Running the verification - - To start the verification for the builtin armv8 atomics, you need a list of functions that should be checked. You can find the lists organized by prefixes in the `lists` subfolder. - - The verification for a specific `list.txt` can be started by: - - ``` - ruby verify_all.rb -a armv8 -s list.txt - ``` - -A specific function `func` can be verified by (git specifying that the boogie files should be generated in `output_folder`): - -``` - ruby verify_all.rb -a armv8 -f func -o output_folder -``` +See `../doc/VERIFICATION.md` for details. diff --git a/verify/boogie/atomics_list.txt b/verify/boogie/atomics_list.txt deleted file mode 100644 index ce42e92..0000000 --- a/verify/boogie/atomics_list.txt +++ /dev/null @@ -1,10 +0,0 @@ -read -read_acq -read_rlx -write -write_rel -write_rlx -cmpxchg -cmpxchg_acq -cmpxchg_rel -cmpxchg_rlx diff --git a/verify/boogie/templates/BoogieTemplate.md b/verify/boogie/templates/BoogieTemplate.md deleted file mode 100644 index 6634834..0000000 --- a/verify/boogie/templates/BoogieTemplate.md +++ /dev/null @@ -1,54 +0,0 @@ -# Boogie Template -## Overview - -Each .bpl of the following is a template describing some aspects of correctness of different atomics. -For each atomic, one or more of these templates need to be used to fully specify the correctness. -The templates are: - -- read_only -- describes atomics that never write, such as read, await (non-RMW) -- read -- describes atomics that perform a read, such as RMW, read, await, await-RMW -- write -- describes write atomics -- await -- describes await, await-RMW atomics -- rmw -- describes atomics performing a read-modify-write operation, such as RMW and await-RMW - -## Templating - -Each template uses one or more of the following parameters, written as `#NAME`: - -- #registers -- comma seperated sequence of identifiers specifying all registers used in the function, such as `a0, a1, a2, x5, x6` -- #address -- identifier specifiying register that originally holds the address, such as `a0` -- #input1 -- identifier for register holding first function argument, e.g., for `write(a, v)` the value of `v`, or for `cmpxchg(a, e, v)` the value of `e`. Could be `a1` -- #input2 -- second function argument. Could be `a2`. -- #output -- register holding the output value at the end of the function, e.g., `a0` -- #implementation -- body of the function, including: assumes for all procedure parameters, code, 2 basic loop invariants -- #state -- comma seperated list of identifiers for all additional state introduced by the architecture, e.g., `local_monitor, monitor_exclusive` - -## Example - -For an example, see `test.bpl` which contains instantiation of two templates (read, rmw) for one RMW atomic (add_set). - -## Templates - -List of templates and their functions: - -| template | write number | return value | store order | load order | ------------------------------------------------------------------------ -| read_only | 0 | output | - | - | -| read | - | ret | - | yes | -| write | <=1 | - | yes | - | -| await | - | await cond | - | - | -| must_store | 1 (+value) | - | yes | - | -| rmw | (+op) | - | yes | - | - -List of templates used by each atomic: - -| template | read | write | RMW | await | await RMW | -------------------------------------------------------- -| read_only | x | | | x | | -| read | x | | x | x | x | -| write | | x | x | | x | -| await | | | | x | x | -| must_store | | x | | | | -| rmw | | | x | | x | - -