Skip to content

Commit 5159323

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

File tree

4 files changed

+184
-87
lines changed

4 files changed

+184
-87
lines changed

‎doc/VERIFICATION.md‎

Lines changed: 181 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,181 @@
1+
# Verification Guide
2+
3+
`vatomic` ships a Boogie-based pipeline that checks each atomic primitive
4+
against the [VSync Memory Model][]. The verification assets live under `verify/`
5+
and power the `build_boogie_*` targets exposed by CMake.
6+
7+
[VSync Memory Model]: ../vmm.cat
8+
[VMM]: ../vmm.cat
9+
10+
## Dependencies
11+
12+
The verification targets are available when configuring the project with
13+
`-DVATOMIC_DEV=ON` (the default for top-level builds). Locally you will need:
14+
15+
- CMake (>= 3.16) and a build backend (Ninja or Make)
16+
- A Rust toolchain (`cargo`) to build the assembly parser/generator in
17+
`verify/src`
18+
- Boogie CLI (`boogie`) and its SMT solver dependency (Z3)
19+
- Cross compilers: `aarch64-linux-gnu-gcc` (ARMv8) and
20+
`riscv64-linux-gnu-gcc` (RISC-V)
21+
22+
### Details
23+
24+
- Boogie support for irreducible control flow (needed for several atomics)
25+
only landed in release [**3.5.5**][] (see our [contribution to
26+
upstream][]). Stick to that version or newer when running the pipeline
27+
outside the CI image.
28+
- Z3 results varied wildly with old releases. Use at least the version baked
29+
into `.github/Dockerfile.boogie` (currently **z3-solver 4.13.0.0** from
30+
PyPI) to match CI behaviour.
31+
- The cross-compilers shipped with Ubuntu 24.04 (GCC **13.2** series, as
32+
installed in `.github/Dockerfile.boogie`) are the minimum known-good
33+
versions. Older Ubuntu toolchains could not inline the builtin assembly
34+
that powers the verification flow.
35+
36+
[contribution to upstream]: https://github.com/boogie-org/boogie/pull/1032
37+
[**3.5.5**]: https://github.com/boogie-org/boogie/releases/tag/v3.5.5
38+
39+
### Using the CICD container
40+
41+
CI uses the container image `ghcr.io/open-s4c/vatomic/boogie-ci:latest`,
42+
which bundles all of the above. You can pull it locally if you prefer a
43+
hermetic environment.
44+
45+
```sh
46+
docker pull ghcr.io/open-s4c/vatomic/boogie-ci:latest
47+
```
48+
49+
Then you can start the container mounting the vatomic directory as follows:
50+
51+
```sh
52+
cd vatomic
53+
docker run -it --rm -v $(pwd):$(pwd) -w $(pwd) -u $(id -u):$(id -g) \
54+
ghcr.io/open-s4c/vatomic/boogie-ci:latest
55+
```
56+
57+
You current `vatomic` directory is mounted over the exact same path in the
58+
container (`-v` flag), and you start with the workdir set to that directory
59+
(`-w` flag). Also the user id and user group match the ids in the host (`-u`
60+
flag), so that if you create files they preserve the right ownership after
61+
leaving the container.
62+
63+
Inside the container, you can follow the instructions in the next section.
64+
65+
---
66+
67+
## Running the verification suite
68+
69+
1. Configure the project and enable developer targets:
70+
71+
```sh
72+
cmake -S . -B build -DVATOMIC_TESTS=ON
73+
```
74+
75+
2. Build one (or all) Boogie targets. Available options are `lse`, `llsc`,
76+
`lxe`, and `no_polite_await`.
77+
78+
```sh
79+
cmake --build build --target build_boogie_lse
80+
```
81+
82+
Each target:
83+
84+
- Preprocesses `vsync/atomic.h` with the chosen compiler flags to obtain
85+
`atomic.s` (and optionally sanitises it via `cleaner.sh`).
86+
- Runs the Rust generator (`cargo run` via `generate.sh`) to parse the
87+
assembly and emit Boogie (`.bpl`) files.
88+
- Instantiates the templates under `verify/boogie/templates`.
89+
- Executes Boogie to prove each atomic operation (driven by `verify.sh`).
90+
91+
3. Inspect results via CTest or directly in the generated logs:
92+
93+
```sh
94+
ctest --test-dir build/verify -R lse --output-on-failure
95+
# Logs: build/verify/lse/*.log
96+
```
97+
98+
### Customising the toolchain
99+
100+
- Pass `-DARMV8_CMAKE_C_COMPILER=/path/to/aarch64-linux-gnu-gcc` or
101+
`-DRISCV_CMAKE_C_COMPILER=/path/to/riscv64-linux-gnu-gcc` to override the
102+
default cross compilers.
103+
- Set `BPL`/`Z3_EXE` or adjust `PATH` so Boogie and Z3 are discoverable.
104+
- Export `CARGO` to point at a specific `cargo` binary when multiple toolchains
105+
coexist on the system.
106+
107+
---
108+
109+
## Maintaining the function list
110+
111+
The list of verified entry points lives in `verify/atomics_list.txt`. When
112+
adding new atomic primitives, update that file so the verification targets cover
113+
the new functions. Refer to the [Boogie templates](#boogie-templates) section
114+
for the available templates and how they map to atomic behaviour.
115+
116+
---
117+
118+
## Boogie templates
119+
120+
Each `.bpl` template describes some aspect of correctness for the supported
121+
atomics. For each atomic, one or more templates are instantiated to fully
122+
specify the proof obligations. The templates are:
123+
124+
- `read_only` — describes atomics that never write, e.g., `read`, `await`
125+
(non-RMW)
126+
- `read` — describes atomics that perform a read, e.g., `RMW`, `read`, `await`,
127+
`await-RMW`
128+
- `write` — describes `write` atomics
129+
- `await` — describes `await` and `await-RMW` atomics
130+
- `rmw` — describes atomics performing a read-modify-write operation, e.g.,
131+
`RMW` and `await-RMW`
132+
133+
### Template parameters
134+
135+
Each template uses one or more of the following parameters, written as `#NAME`:
136+
137+
- `#registers` — comma separated identifiers specifying all registers used in
138+
the function, e.g., `a0, a1, a2, x5, x6`.
139+
- `#address` — identifier specifying the register that originally holds the
140+
address, e.g., `a0`.
141+
- `#input1` — identifier for the register holding the first function argument,
142+
e.g., for `write(a, v)` the value of `v`, or for `cmpxchg(a, e, v)` the value
143+
of `e`. Could be `a1`.
144+
- `#input2` — second function argument. Could be `a2`.
145+
- `#output` — register holding the output value at the end of the function,
146+
e.g., `a0`.
147+
- `#implementation` — body of the function, including assumes for all procedure
148+
parameters, code, and two basic loop invariants.
149+
- `#state` — comma separated list of identifiers for all additional state
150+
introduced by the architecture, e.g., `local_monitor, monitor_exclusive`.
151+
152+
### Example
153+
154+
For an example, see `verify/boogie/templates/test.bpl`, which instantiates two
155+
templates (`read`, `rmw`) for one RMW atomic (`add_set`).
156+
157+
### Template matrix
158+
159+
List of templates and their functions:
160+
161+
| template | write number | return value | store order | load order |
162+
|--------------|--------------|--------------|-------------|------------|
163+
| `read_only` | 0 | output | – | – |
164+
| `read` | – | ret | – | yes |
165+
| `write` | ≤1 | – | yes | – |
166+
| `await` | – | await cond | – | – |
167+
| `must_store` | 1 (+value) | – | yes | – |
168+
| `rmw` | (+op) | – | yes | – |
169+
170+
List of templates used by each atomic:
171+
172+
| template | read | write | RMW | await | await RMW |
173+
|--------------|------|-------|-----|-------|-----------|
174+
| `read_only` | x | | | x | |
175+
| `read` | x | | x | x | x |
176+
| `write` | | x | x | | x |
177+
| `await` | | | | x | x |
178+
| `must_store` | | x | | | |
179+
| `rmw` | | | x | | x |
180+
181+
---

‎verify/README.md‎

Lines changed: 1 addition & 33 deletions
Original file line numberDiff line numberDiff line change
@@ -1,33 +1 @@
1-
# Builtin Atomics Verification
2-
3-
## Prerequisites
4-
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-
```
9-
10-
## Generating the assembly file
11-
12-
The assembly file with the builtin atomics can be generated by:
13-
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
18-
19-
## Running the verification
20-
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.
22-
23-
The verification for a specific `list.txt` can be started by:
24-
25-
```
26-
ruby verify_all.rb -a armv8 -s list.txt
27-
```
28-
29-
A specific function `func` can be verified by (git specifying that the boogie files should be generated in `output_folder`):
30-
31-
```
32-
ruby verify_all.rb -a armv8 -f func -o output_folder
33-
```
1+
See `../doc/VERIFICATION.md` for details.

‎verify/boogie/templates/BoogieTemplate.md‎

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

‎verify/boogie/templates/README.md‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
See `../../../doc/VERIFICATION.md` for details.
2+

0 commit comments

Comments
 (0)