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