Challenge 7: Safety of Methods for Atomic Types & Atomic Intrinsics

[carolynzech]

Link to PR: #82

[suaviloquence]

For the from_ptr methods a safety condition is that the *const T is alive for the entire lifetime 'a of the returned reference. Is that something currently expressible with kani, or would a different tool be necessary here?

[carolynzech]

@suaviloquence That's correct, Kani doesn't track reference lifetimes, so a different tool would be necessary.

[btj]

I have made a start of attacking this challenge with VeriFast. So far, I have written (safety) specs for intrinsics::{atomic_store_relaxed, atomic_store_release, atomic_store_seqcst} and verified atomic_store, AtomicBool::from_ptr, and AtomicBool::store, using this type interpretation for AtomicBool. As far as I can tell, the other atomic types will be extremely similar. (In fact, they will be simpler because AtomicBool is the only type that involves a nontrivial invariant (saying that the internal u8 is either 0 or 1).) The main difficulty that I see is dealing with the fact that the atomic integer types are generated using a macro.

But maybe I'm missing something. A few things in the challenge confused me:

• The challenge asks to "verify" the intrinsics. What do you mean by that?
• The challenge asks to verify that atomic_store does not panic. But this seems to contradict the statement at the top that "The goal of this challenge is to verify that these methods are safe. [1]", where [1] says that "safe" means absence of UB. Panicking is not UB. VeriFast does not verify absence of panics, and adding a precondition to AtomicBool::store would run counter to the goal of verifying semantic well-typedness, i.e. safety in the presence of arbitrary non-unsafe client code.

[btj]

@carolynzech Could I perhaps get some feedback as to whether I’m on the right track? Good news: the refinement checker will allow me to deal with the macro problem. The verified version will have the macros expanded. This will be tedious work but not complex.

[patricklam]

On a not so related note, I was thinking that static analysis could be useful on the client side in terms of checking that atomics are used properly and don't cause undefined behaviour, but that is a whole other issue (not unrelated with the paper that my collaborators and I just got into TOPLAS for presentation at PLDI 2025). We should talk about that sometime.

[carolynzech]

@btj I opened #357 to address your feedback about the challenge; feel free to suggest changes if you'd like. As for feedback on your proofs so far, @remi-delmas-3000 said he'd take a look.

[carolynzech]

@patricklam Yes, sounds interesting! We're chatting about that bit in #357 re: verifying the absence of data races, so feel free to comment there if you have further thoughts.

[remi-delmas-3000]

@btj how close are you to submit a PR for the Atomics Challenge ?

[btj]

Since I finished the refinement-checked LinkedList proof, I’ve been working on the RawVec challenge, because it’s more interesting, IMHO. But I’ll try to make progress on this one as well.