Skip to content

Commit 22385cc

Browse files
karthikbhargavankarthikbhargavan
authored
Make models closer to upstream core (#3)
* Provided more detailed description for how to model and test intrinsics * Restored static asserts which were in the upstream code * Switched the use of u64 back to u32 to make it closer to upstream * Defined functions like `transpose` to reduce visual diffs
1 parent e6696fc commit 22385cc

File tree

24 files changed

+5394
-2812
lines changed

24 files changed

+5394
-2812
lines changed

‎library/Cargo.lock

Lines changed: 90 additions & 0 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

‎testable-simd-models/README.md

Lines changed: 148 additions & 49 deletions
Original file line numberDiff line numberDiff line change
@@ -6,26 +6,132 @@ The structure of this crate is based on [rust-lang/stdarch/crates/core_arch](htt
66

77
## Code Structure
88
Within the `core_arch` folder in this crate, there is a different
9-
folder for each architecture for which we have wrtten models.
9+
folder for each architecture for which we have written models.
1010
In particular, it contains folders for `x86` and `arm_shared`.
11-
Each such folder has 3 sub-folders, `models`, `tests`, and `specs`.
11+
Each such folder has 2 sub-folders: `models` and `tests`.
1212

13-
The `models` folder contains the models of the intrinsics, with a file
14-
corresponding to different target features, and are written using the
15-
various abstractions implementedin `crate::abstractions`, especially
16-
those in `crate::abstractions::simd`. These models are meant to
17-
closely resemble their implementations within the Rust core itself.
13+
The `models` folder contains the models of the intrinsics, with
14+
different files for different target features (e.g. `sse2`, `avx2`
15+
etc.). The code in this folder is written using the various
16+
abstractions implemented in `abstractions`, especially those in
17+
`abstractions::simd`. These models are meant to closely
18+
resemble their implementations within the Rust core itself.
1819

1920
The `tests` folder contains the tests of these models, and is
20-
structured the same way as `models`. Each file additionally contains
21+
structured the same way as `models`. Each file additionally includes
2122
the definition of a macro that makes writing these tests easier. The
2223
tests work by testing the models against the intrinsics in the Rust
2324
core, trying out random inputs (generally 1000), and comparing their
2425
outputs.
2526

26-
## Modeling Process
27-
The process of adding a specific intrinsic's model goes as follows.
28-
For this example, let us say the intrinsic we are adding is
27+
All tests can be run by executing `cargo test`, and we expect this to be
28+
run as part of CI.
29+
30+
## Modeling a SIMD Intrinsic
31+
32+
There are three kinds of SIMD intrinsics in `core::arch`.
33+
34+
The first kind are builtin Rust compiler intrinsics, some of which are
35+
in the [`intrinsics/simd.rs` file](https://github.com/model-checking/verify-rust-std/blob/main/library/core/src/intrinsics/simd.rs)
36+
in the `core` crate, and others are in the [`simd.rs` file of `core_arch`](https://github.com/model-checking/verify-rust-std/blob/main/library/stdarch/crates/core_arch/src/simd.rs).
37+
These builtin intrinsics define generic SIMD operations that the Rust compiler knows how to implement on each platform.
38+
39+
The second kind are `extern` intrinsics that are links to definitions in LLVM.
40+
See, for example, [this list](https://github.com/rust-lang/stdarch/blob/master/crates/core_arch/src/x86/avx2.rs#L3596C8-L3596C14)
41+
of `extern` intrinsics used in the Intel x86 AVX2 library.
42+
These extern intrinsics are typically platform-specific functions that map to low-level instructions.
43+
44+
The third kind are `defined` intrinsics that are given proper definitions in Rust, and their code may
45+
depend on the builtin intrinsics or the extern intrinsics. These defined intrinsics represent higher-level
46+
operations that are wrappers around one or more assembly instructions.
47+
48+
### Modeling builtin intrinsics manually
49+
50+
We model all three kinds of intrinsics, but in slightly different
51+
ways. For the builtin intrinsics, we can write implementations once
52+
and for all, and to this end, we use a library within the
53+
`abstractions/simd.rs` file, where we copy the signatures of the
54+
intrinsics from Rust but give them our own implementation. In
55+
particular, we model each SIMD vector as an array of scalars, and
56+
define each generic operation as functions over such arrays. This can
57+
be seen as a reference implementation of the builtin intrinsics.
58+
59+
Hence, for example, the SIMD add intrinsic `simd_add` is modeled as follows,
60+
it takes two arrays of machine integers and adds them pointwise using a
61+
`wrapping_add` operation:
62+
63+
```rust
64+
pub fn simd_add<const N: u64, T: MachineInteger + Copy>(
65+
x: FunArray<N, T>,
66+
y: FunArray<N, T>,
67+
) -> FunArray<N, T> {
68+
FunArray::from_fn(|i| (x[i].wrapping_add(y[i])))
69+
}
70+
```
71+
72+
Notably, we model a strongly typed version of `simd_add`, in contrast to the compiler
73+
intrinsic, which is too generic and unimplementable in safe Rust:
74+
75+
```rust
76+
/// Adds two simd vectors elementwise.
77+
///
78+
/// `T` must be a vector of integers or floats.
79+
#[rustc_intrinsic]
80+
#[rustc_nounwind]
81+
pub unsafe fn simd_add<T>(x: T, y: T) -> T;
82+
```
83+
84+
The main rules for writing these models are that they should be simple and self-contained,
85+
relying only on the libraries in `abstractions`, on builtin Rust language features, or
86+
other testable models. In particular, they should not themselves directly call Rust libraries
87+
or external crates, without going through the abstractions API.
88+
89+
90+
### Modeling extern intrinsics manually
91+
92+
For each file in `core::arch`, we split the code into extern
93+
intrinsics that must be modeled by hand and defined intrinsics whose
94+
models can be derived semi-automatically. The extern intrinsics are
95+
placed in a module suffixed with `_handwritten`. Hence, for example,
96+
the extern intrinsics used in `avx2.rs` can be found in `avx2_handwritten.rs`.
97+
98+
Modeling extern intrinsics is similar to modeling the builtin ones,
99+
in that the models are written by hand and treat the SIMD vectors
100+
as arrays of machine integers. The main difference is that these intrinsics
101+
are platform-specific and so their modeling requires looking at the Intel or ARM
102+
documentation for the underlying operation.
103+
104+
For example, the extern intrinsic `phaddw` used in `avx2` corresponds to an
105+
Intel instruction called "Packed Horizontal Add" and is used in AVX2 intrinsics
106+
like `_mm256_hadd_epi16` documented [here](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_hadd_epi16&ig_expand=3667_)
107+
By inspecting the Intel documentation, we can write a Rust model for it
108+
as follows
109+
110+
```rust
111+
pub fn phaddw(a: i16x16, b: i16x16) -> i16x16 {
112+
i16x16::from_fn(|i| {
113+
if i < 4 {
114+
a[2 * i].wrapping_add(a[2 * i + 1])
115+
} else if i < 8 {
116+
b[2 * (i - 4)].wrapping_add(b[2 * (i - 4) + 1])
117+
} else if i < 12 {
118+
a[2 * (i - 4)].wrapping_add(a[2 * (i - 4) + 1])
119+
} else {
120+
b[2 * (i - 8)].wrapping_add(b[2 * (i - 8) + 1])
121+
}
122+
})
123+
}
124+
```
125+
126+
### Modeling defined intrinsics semi-automatically
127+
128+
To model a defined intrinsic, we essentially copy the Rust code of
129+
the intrinsic from `core::arch` and adapt it to use our underlying abstractions. The
130+
changes needed to the code are sometimes scriptable, and indeed most
131+
of our models were generated from a script, but some changes are still
132+
needed by hand.
133+
134+
For example, let us say the intrinsic we are modeling is
29135
`_mm256_bsrli_epi128` from the avx2 feature set.
30136

31137
1. We go to [rust-lang/stdarch/crates/core_arch/src/x86/](https://github.com/rust-lang/stdarch/tree/master/crates/core_arch/src/x86/), and find the implementation of the intrinsic in `avx2.rs`.
@@ -67,56 +173,49 @@ pub fn _mm256_bsrli_epi128<const IMM8: i32>(a: __m256i) -> __m256i {
67173
transmute(r)
68174
}
69175
}
70-
```
71-
Thus, we then go to to `core_arch/x86/models/avx2.rs`, and add the implementation. After some modification, it ends up looking like this.
72-
``` rust
73-
/// Shifts 128-bit lanes in `a` right by `imm8` bytes while shifting in zeros.
74-
///
75-
/// [Intel's documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_bsrli_epi128)
176+
```
76177

77-
pub fn _mm256_bsrli_epi128<const IMM8: i32>(a: __m256i) -> __m256i {
78-
const fn mask(shift: i32, i: u32) -> u64 {
79-
let shift = shift as u32 & 0xff;
80-
if shift > 15 || (15 - (i % 16)) < shift {
81-
0 as u64
82-
} else {
83-
(32 + (i + shift)) as u64
84-
}
85-
}
86-
87-
let a = BitVec::to_i8x32(a);
88-
let r: i8x32 = simd_shuffle(
89-
i8x32::from_fn(|_| 0),
90-
a,
91-
[
92-
mask(IMM8, 0),
93-
mask(IMM8, 1),
94-
mask(IMM8, 2),
95-
mask(IMM8, 3),
96-
...
97-
mask(IMM8, 31),
98-
],
99-
);
100-
r.into()
101-
}
102-
```
178+
Thus, we then go to `core_arch/x86/models/avx2.rs`, and add this implementation.
179+
The only change it requires here is that the `simd_shuffle` macro is a function in our model,
180+
and we discard all the function attributes.
181+
182+
For other intrinsics, we sometimes need to make more changes. Since our model of the builtin intrinsics
183+
is more precise concerning the type of their arguments compared to their Rust counterparts, we
184+
sometimes need to add more type annotations in our defined models. We also remove all `unsafe` guards,
185+
since our models are always in safe Rust. Otherwise, our code for the defined intrinsics looks very
186+
similar to the upstream code in `core::arch`.
103187

104-
3. Next, we add a test for this intrinsic. For this, we navigate to `core_arch/avx2/tests/avx2.rs`. Since the value of
105-
`IMM8` can be up to 8 bits, we want to test constant arguments up to 255. Thus, we write the following macro invocation.
188+
3. Next, we add a test for this intrinsic in `core_arch/avx2/tests/avx2.rs`. For convenience purposes, we have defined a `mk!` macro, which can be used to automatically generate
189+
tests. The test generated by the macro generates a number of random inputs (by default, 1000), and compares the output generated by the model
190+
and that generated by the intrinsic in upstream `core::arch`. A valid test of the intrinsic above looks like this.
106191
```rust
107192
mk!([100]_mm256_bsrli_epi128{<0>,<1>,<2>,<3>,...,<255>}(a: BitVec));
108193
```
109-
Here, the `[100]` means we test 100 random inputs for each constant value. This concludes the necessary steps for implementing an intrinsic.
194+
The macro invocation has four parts.
195+
1. `mk!([100]...`: By default, the macro tests for a thousand randomly generated inputs. If needed, this can be modified, such as here, where the `[100]` is used so that
196+
only 100 inputs are generated.
197+
2. `_mm256_bsrli_epi128`: This is the name of the intrinsic being tested, and is necessary in all cases.
198+
3. `{<0>,<1>,<2>,<3>,...,<255>}`: This part only appears when the intrinsic has a const generic argument, like the `IMM8` in this intrinsic.
199+
As the name indicates, this constant argument is supposed to be at most 8 bits wide.
200+
We can confirm this by looking at the implementation and spotting the `static_assert_uimm_bits!(IMM8, 8);`
201+
line, which asserts that constant argument is positive and fits in 8 bits. Thus, we add `{<0>,<1>,<2>,<3>,...,<255>}` to test for each possible constant
202+
value of the constant argument.
203+
4. `(a: BitVec)`: This part contains all the arguments of the intrinsic and their types.
204+
205+
This summarizes the steps needed to use the `mk!` macro to generate a test. There is a caveat: in the case that the output of an intrinsic is _not_
206+
a bit-vector (and is instead, say, an integer like `i32`), then the macro will not work, and a manual test has to be written. You can see examples in the test files.
207+
110208

111209

112210
## Contributing Models
113211

114212
To contribute new models of intrinsics, we expect the author to follow
115213
the above steps and provide comprehensive tests. It is important that
116-
the model author look carefully at both the Intel/ARM specification
117-
and the Rust `stdarch` implementation, because the Rust implementation
118-
may not necessarily be correct.
214+
the model author looks carefully at both the Intel/ARM specifications
215+
and the Rust `stdarch` implementation, because they may look quite different
216+
from each other.
119217

218+
In some cases, the Rust implementation may not be correct.
120219
Indeed, the previous implementation of `_mm256_bsrli_epi128` (and a
121220
similar intrinsic called `_mm512_bsrli_epi128`) in `stdarch` had a
122221
bug, which we found during the process of modeling and testing this

0 commit comments

Comments
 (0)