Кто-Нибудь может сказать S_Access корректна (не имеет UB, безопасна, защищает

от гонок, алиасинга мут ссылок и ещё чего-то о чём я не знаю) для записи и чтения S?
Пожалуйста, не предлагайте мне других вариантов решения, не спрашивайте зачем мне это нужно и т. д.
Просто ответьте "да", "нет" или "не знаю". И если ответ "нет", то аргументируйте пожалуйста.

type T = ...;

static mut S: T = ...;
use S_local::S_Access;

mod S_local {
use core::ops::{DerefMut, Deref};
use core::sync::atomic::{AtomicBool, Ordering};
use core::marker::PhantomData;

pub struct S_Access(PhantomData<super::T>);

static IS_TAKEN: AtomicBool = AtomicBool::new(false);

impl S_Access {
pub fn take() -> Self {
IS_TAKEN.compare_exchange(false, true, Ordering::Acquire, Ordering::Acquire).unwrap();
Self(PhantomData)
}
}

impl Drop for S_Access {
fn drop(&mut self) {
IS_TAKEN.store(false, Ordering::Release);
}
}

impl Deref for S_Access {
type Target = super::T;

fn deref(&self) -> &Self::Target {
unsafe { &super::S }
}
}

impl DerefMut for S_Access {
fn deref_mut(&mut self) -> &mut Self::Target {
unsafe { &mut super::S }
}
}
}

В чем толк от ответа "не знаю"

не знаю - значит надо KANI брать

Согласен, это не нужно.

Если ты из двух тредов берёшь мутабельные ссылки на два разных инстанса S_Access, то по DerefMut получаешь две мутабельные ссылки на static mut.

Два разных не получится получить одновременно, ибо второй должен будет на атомике упасть.

1. Использование Acquire в compare_exchange значит, что запись будет Relaxed. 2. В исходниках spinlock делают SeqCst (ровно для тех же целей, в общем-то) https://docs.rs/spinlock/latest/src/spinlock/lib.rs.html#142 https://docs.rs/spinlock/latest/src/spinlock/lib.rs.html#189

Release-store синхронизируется с Acquire-load, Relaxed нужен только для failure ветки в compare_exchange(_weak)

Разве только для этого? Условно когда много потоков считают количество "хороших" чисел на промежутке, и инкрементируют один атомик, и им нафиг не нужна никакая синхронизация?

Так речь идёт про лок

Может быть, ещё кто-нибудь знает ответ но не видел вопрос? Пока ещё не поступило достаточно утвердительного ответа.