Skip to content

Commit bcd8abd

Browse files
db7db7
committed
doc: Improve documentation in verify
Signed-off-by: Diogo Behrens <[email protected]>
1 parent cffe266 commit bcd8abd

File tree

3 files changed

+124
-75
lines changed

3 files changed

+124
-75
lines changed

‎verify/README.md‎

Lines changed: 58 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -1,33 +1,70 @@
11
# Builtin Atomics Verification
22

3-
## Prerequisites
3+
`vatomic` ships a Boogie-based pipeline that checks each atomic primitive
4+
against the VSync Memory Model. This directory contains the scripts and
5+
templates that power the `build_boogie_*` targets exposed by CMake.
46

5-
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
6-
```
7-
gem install parallel
8-
```
7+
## Dependencies
98

10-
## Generating the assembly file
9+
The verification targets are available when configuring the project with
10+
`VATOMIC_DEV=ON` (the default for top-level builds). Locally you will need:
1111

12-
The assembly file with the builtin atomics can be generated by:
12+
- CMake (>= 3.16) and a build backend (Ninja or Make)
13+
- A Rust toolchain (`cargo`) to build the assembly parser/generator in
14+
`verify/src`
15+
- Boogie CLI (`boogie`) and its SMT solver dependency (Z3)
16+
- Cross compilers: `aarch64-linux-gnu-gcc` (ARMv8) and
17+
`riscv64-linux-gnu-gcc` (RISC-V)
1318

14-
```
15-
aarch64-linux-gnu-gcc -DVATOMIC_BUILTINS -O2 -x c include/vsync/atomic.h -Iinclude -fkeep-inline-functions -S -mno-outline-atomics -o atomics.s
16-
```
17-
The `atomics.s` file should be located in the `armv8` subfolder
19+
> Tip: CI uses the container image `ghcr.io/open-s4c/vatomic/boogie-ci:latest`,
20+
> which bundles all of the above. You can pull it locally if you prefer a
21+
> hermetic environment.
1822
19-
## Running the verification
23+
## Running the verification suite
2024

21-
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.
25+
1. Configure the project and enable developer targets:
2226

23-
The verification for a specific `list.txt` can be started by:
27+
```sh
28+
cmake -S . -B build -DVATOMIC_DEV=ON
29+
```
2430

25-
```
26-
ruby verify_all.rb -a armv8 -s list.txt
27-
```
31+
2. Build one (or all) Boogie targets. Available options are `lse`, `llsc`,
32+
`lxe`, and `no_polite_await`.
2833

29-
A specific function `func` can be verified by (git specifying that the boogie files should be generated in `output_folder`):
34+
```sh
35+
cmake --build build --target build_boogie_lse
36+
```
3037

31-
```
32-
ruby verify_all.rb -a armv8 -f func -o output_folder
33-
```
38+
Each target:
39+
40+
- Preprocesses `vsync/atomic.h` with the chosen compiler flags to obtain
41+
`atomic.s` (and optionally sanitises it via `cleaner.sh`).
42+
- Runs the Rust generator (`cargo run` via `generate.sh`) to parse the
43+
assembly and emit Boogie (`.bpl`) files.
44+
- Instantiates the templates under `verify/boogie/templates`.
45+
- Executes Boogie to prove each atomic operation (driven by `verify.sh`).
46+
47+
3. Inspect results via CTest or directly in the generated logs:
48+
49+
```sh
50+
ctest --test-dir build/verify -R lse --output-on-failure
51+
# Logs: build/verify/lse/*.log
52+
```
53+
54+
## Customising the toolchain
55+
56+
- Pass `-DARMV8_CMAKE_C_COMPILER=/path/to/aarch64-linux-gnu-gcc` or
57+
`-DRISCV_CMAKE_C_COMPILER=/path/to/riscv64-linux-gnu-gcc` to override the
58+
default cross compilers.
59+
- Set `BPL`/`Z3_EXE` or adjust `PATH` so Boogie and Z3 are discoverable.
60+
- Export `CARGO` to point at a specific `cargo` binary when multiple toolchains
61+
coexist on the system.
62+
63+
## Maintaining the function list
64+
65+
The list of verified entry points lives in `atomics_list.txt`. When adding new
66+
atomic primitives, make sure to update that file so the verification targets
67+
cover the new functions. See [boogie/templates/README.md][] for details about
68+
the available templates and how they correspond to atomic behaviour.
69+
70+
[boogie/templates/README.md]: boogie/templates/README.md

‎verify/boogie/templates/BoogieTemplate.md‎

Lines changed: 0 additions & 54 deletions
This file was deleted.

‎verify/boogie/templates/README.md‎

Lines changed: 66 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,66 @@
1+
# Boogie Template
2+
3+
## Overview
4+
5+
Each .bpl of the following is a template describing some aspects of correctness
6+
of different atomics. For each atomic, one or more of these templates need
7+
to be used to fully specify the correctness. The templates are:
8+
9+
- `read_only` -- describes atomics that never write, eg, `read`, `await`
10+
(non-RMW)
11+
- `read` -- describes atomics that perform a read, eg, `RMW`, `read`, `await`,
12+
`await-RMW`
13+
- `write` -- describes `write` atomics
14+
- `await` -- describes `await` and `await-RMW` atomics
15+
- `rmw` -- describes atomics performing a read-modify-write operation, eg, `RMW`
16+
and `await-RMW`
17+
18+
## Templating
19+
20+
Each template uses one or more of the following parameters, written as `#NAME`:
21+
22+
- `#registers` -- comma seperated sequence of identifiers specifying all
23+
registers used in the function, eg, `a0, a1, a2, x5, x6`.
24+
- `#address` -- identifier specifiying register that originally holds the
25+
address, eg, `a0`.
26+
- `#input1` -- identifier for register holding first function argument, eg, for
27+
`write(a, v)` the value of `v`, or for `cmpxchg(a, e, v)` the value of `e`.
28+
Could be `a1`.
29+
- `#input2` -- second function argument. Could be `a2`.
30+
- `#output` -- register holding the output value at the end of the function,
31+
eg, `a0`.
32+
- `#implementation` -- body of the function, including: assumes for all
33+
procedure parameters, code, 2 basic loop invariants.
34+
- `#state` -- comma seperated list of identifiers for all additional state
35+
introduced by the architecture, eg, `local_monitor, monitor_exclusive`
36+
37+
## Example
38+
39+
For an example, see `test.bpl` which contains instantiation of two templates
40+
(`read`, `rmw`) for one RMW atomic (`add_set`).
41+
42+
## Templates
43+
44+
List of templates and their functions:
45+
46+
| template | write number | return value | store order | load order |
47+
|--------------|--------------|--------------|-------------|------------|
48+
| `read_only` | 0 | output | - | - |
49+
| `read` | - | ret | - | yes |
50+
| `write` | <=1 | - | yes | - |
51+
| `await` | - | await cond | - | - |
52+
| `must_store` | 1 (+value) | - | yes | - |
53+
| `rmw` | (+op) | - | yes | - |
54+
55+
List of templates used by each atomic:
56+
57+
| template | read | write | RMW | await | await RMW |
58+
|--------------|------|-------|-----|-------|-----------|
59+
| `read_only` | x | | | x | |
60+
| `read` | x | | x | x | x |
61+
| `write` | | x | x | | x |
62+
| `await` | | | | x | x |
63+
| `must_store` | | x | | | |
64+
| `rmw` | | | x | | x |
65+
66+

0 commit comments

Comments
 (0)