docs(unsafe): audit all 49 unsafe impl — one proof was wrong, four were missing
windows / build (aarch64-pc-windows-msvc) (push) Canceled after 0s
windows / build (x86_64-pc-windows-msvc) (push) Canceled after 0s
windows-msix / package (arm64, C:\Users\Public\ffmpeg-arm64, --no-default-features, aarch64-pc-windows-msvc, C:\t-a64) (push) Canceled after 0s
windows-msix / package (x64, C:\Users\Public\ffmpeg, , x86_64-pc-windows-msvc, C:\t) (push) Canceled after 0s
windows-host / package (push) Canceled after 0s
windows-host / winget-source (push) Canceled after 0s
windows-drivers / probe-and-proto (push) Canceled after 0s
windows-drivers / driver-build (push) Canceled after 0s
rpm / build-publish (43, bazzite, punktfunk-fedora-rpm) (push) Canceled after 0s
rpm / build-publish (44, fedora-44, punktfunk-fedora44-rpm) (push) Canceled after 0s
flatpak / build-publish (push) Canceled after 0s
docker / build-push (--build-arg FEDORA_VERSION=44, ci, ci/fedora-rpm.Dockerfile, punktfunk-fedora44-rpm) (push) Canceled after 0s
docker / build-push (., web/Dockerfile, punktfunk-web) (push) Canceled after 0s
docker / build-push (ci, ci/fedora-rpm.Dockerfile, punktfunk-fedora-rpm) (push) Canceled after 0s
docker / build-push (ci, ci/rust-ci-noble.Dockerfile, punktfunk-rust-ci-noble) (push) Canceled after 0s
docker / build-push (ci, ci/rust-ci.Dockerfile, punktfunk-rust-ci) (push) Canceled after 0s
docker / build-push (docs-site, docs-site/Dockerfile, punktfunk-docs) (push) Canceled after 0s
docker / build-push-arm64cross (push) Canceled after 0s
docker / deploy-docs (push) Canceled after 0s
decky / build-publish (push) Canceled after 0s
deb / build-publish (push) Canceled after 0s
deb / build-publish-host (push) Canceled after 0s
deb / build-publish-client-arm64 (push) Canceled after 0s
ci / rust (push) Canceled after 0s
ci / rust-arm64 (push) Canceled after 0s
ci / web (push) Canceled after 0s
ci / docs-site (push) Canceled after 0s
ci / bench (push) Canceled after 0s
arch / build-publish (push) Canceled after 0s
apple / swift (push) Canceled after 0s
apple / screenshots (push) Canceled after 0s
android / android (push) Canceled after 0s
windows / build (aarch64-pc-windows-msvc) (push) Canceled after 0s
windows / build (x86_64-pc-windows-msvc) (push) Canceled after 0s
windows-msix / package (arm64, C:\Users\Public\ffmpeg-arm64, --no-default-features, aarch64-pc-windows-msvc, C:\t-a64) (push) Canceled after 0s
windows-msix / package (x64, C:\Users\Public\ffmpeg, , x86_64-pc-windows-msvc, C:\t) (push) Canceled after 0s
windows-host / package (push) Canceled after 0s
windows-host / winget-source (push) Canceled after 0s
windows-drivers / probe-and-proto (push) Canceled after 0s
windows-drivers / driver-build (push) Canceled after 0s
rpm / build-publish (43, bazzite, punktfunk-fedora-rpm) (push) Canceled after 0s
rpm / build-publish (44, fedora-44, punktfunk-fedora44-rpm) (push) Canceled after 0s
flatpak / build-publish (push) Canceled after 0s
docker / build-push (--build-arg FEDORA_VERSION=44, ci, ci/fedora-rpm.Dockerfile, punktfunk-fedora44-rpm) (push) Canceled after 0s
docker / build-push (., web/Dockerfile, punktfunk-web) (push) Canceled after 0s
docker / build-push (ci, ci/fedora-rpm.Dockerfile, punktfunk-fedora-rpm) (push) Canceled after 0s
docker / build-push (ci, ci/rust-ci-noble.Dockerfile, punktfunk-rust-ci-noble) (push) Canceled after 0s
docker / build-push (ci, ci/rust-ci.Dockerfile, punktfunk-rust-ci) (push) Canceled after 0s
docker / build-push (docs-site, docs-site/Dockerfile, punktfunk-docs) (push) Canceled after 0s
docker / build-push-arm64cross (push) Canceled after 0s
docker / deploy-docs (push) Canceled after 0s
decky / build-publish (push) Canceled after 0s
deb / build-publish (push) Canceled after 0s
deb / build-publish-host (push) Canceled after 0s
deb / build-publish-client-arm64 (push) Canceled after 0s
ci / rust (push) Canceled after 0s
ci / rust-arm64 (push) Canceled after 0s
ci / web (push) Canceled after 0s
ci / docs-site (push) Canceled after 0s
ci / bench (push) Canceled after 0s
arch / build-publish (push) Canceled after 0s
apple / swift (push) Canceled after 0s
apple / screenshots (push) Canceled after 0s
android / android (push) Canceled after 0s
`unsafe impl Send`/`Sync` is the highest-risk unsafe category here and the one this program had never looked at: a wrong one is cross-thread UB that is invisible at every call site, with no `unsafe` block to catch a reviewer's eye. 49 of them (41 Send, 8 Sync). Two results. **`MappedView`'s `Sync` proof was factually wrong.** It read "only exposes accessors that are safe under concurrent use" — they are not. `read_u8`/`write_u8`/`read_u16` are plain unaligned accesses through `&self`, and `&MappedView` really is shared across threads: `ChannelState::data()` hands out `&'static MappedView`, and pf-xusb, pf-mouse and pf-gamepad all dispatch `WdfIoQueueDispatchParallel` with `NumberOfPresentedRequests = u32::MAX`. The struct's own doc had the right story — consistency is the channel protocol's job — but the `unsafe impl` stated a different, stronger claim, which is the one a reviewer checking that line would rely on. The impl is still sound, for a reason worth writing down: these bytes are mapped into ANOTHER PROCESS that writes them concurrently, so Rust-level exclusivity over them is unachievable no matter what this type does. Sync fields go through the atomic accessors; the plain ones cover only protocol-fenced bytes. The proof now says that, and states the rule it implies for accessors added later — plain path only for bytes the protocol already fences. **Four `Send` impls carried a one-line aside instead of a proof** — the pf-client-core decoders and `DrmFrameGuard`. All four are sound, and each now says why, including the two facts that make them work and were nowhere stated: libav permits a codec context to be used from a thread other than its creator provided use is serialised (`&mut self` is that serialisation), and D3D11's immediate context is thread-AGNOSTIC rather than thread-safe — it wants serialised use, not one fixed thread. Each also records that it is deliberately not `Sync`, which is the invariant a future `impl Sync` would silently break. Every one of the 49 now carries reasoning. Verified: Linux .21 fmt + both CI clippy steps rc=0; Windows .47 `-p pf-client-core` clippy `-D warnings` rc=0 (it compiles the `video_d3d11` proof the Linux run cannot see). The pf-umdf-util edit is comment-only — confirmed by diff, since that crate needs the WDK, which .47 does not have.
This commit is contained in:
@@ -37,7 +37,22 @@ pub struct MappedView {
|
||||
// none of which require a single-thread owner, so sharing/sending the view across the driver's
|
||||
// callback threads is sound.
|
||||
unsafe impl Send for MappedView {}
|
||||
// SAFETY: as above — `&MappedView` only exposes accessors that are safe under concurrent use.
|
||||
// SAFETY: `&MappedView` IS shared across threads for real — `ChannelState::data()` hands out
|
||||
// `&'static MappedView`, and every driver using it dispatches its queue
|
||||
// `WdfIoQueueDispatchParallel` with `NumberOfPresentedRequests = u32::MAX`, so two callbacks can
|
||||
// hold it at once. What makes that sound is NOT that the accessors are individually race-free:
|
||||
// `read_u8`/`write_u8`/`read_u16`/… are plain unaligned accesses through `&self` and would race if
|
||||
// two threads hit the same offset. It is that these bytes are a section mapped into ANOTHER PROCESS
|
||||
// that writes them concurrently, so no Rust-level exclusivity over them is achievable in the first
|
||||
// place — the peer defeats it regardless of what this type does. Consistency is therefore the
|
||||
// channel protocol's job (seq-fenced publishes, per the struct doc), the cross-process
|
||||
// synchronization fields go through the `load_*`/`store_*` ATOMIC accessors, and each side reads
|
||||
// only fields the protocol says are stable.
|
||||
//
|
||||
// ⚠ The rule this proof implies, for anything added later: a new accessor may use the plain path
|
||||
// ONLY for bytes the protocol already fences. Anything that must be coherent between threads or
|
||||
// between processes belongs in the atomic set — a plain accessor over such a field is a race the
|
||||
// `Sync` here does not cover.
|
||||
unsafe impl Sync for MappedView {}
|
||||
|
||||
impl MappedView {
|
||||
|
||||
Reference in New Issue
Block a user