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
{{ message }}
Repository navigation
Challenge 7: Safety of Methods for Atomic Types & Atomic Intrinsics #83
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?
changed the title [-]Challenge 7: Safety of Methods for Atomic Types and `ReentrantLock`[/-][+]Challenge 7: Safety of Methods for Atomic Types & Atomic Intrinsics[/+]on Dec 2, 2024
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.
@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.
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.
@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.
@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.
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.
Activity
suaviloquence commentedon Dec 2, 2024
For the
from_ptrmethods a safety condition is that the*const Tis alive for the entire lifetime'aof the returned reference. Is that something currently expressible with kani, or would a different tool be necessary here?[-]Challenge 7: Safety of Methods for Atomic Types and `ReentrantLock`[/-][+]Challenge 7: Safety of Methods for Atomic Types & Atomic Intrinsics[/+]carolynzech commentedon Dec 2, 2024
@suaviloquence That's correct, Kani doesn't track reference lifetimes, so a different tool would be necessary.
btj commentedon Jan 27, 2025
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 verifiedatomic_store,AtomicBool::from_ptr, andAtomicBool::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:
atomic_storedoes 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-unsafeclient code.btj commentedon May 9, 2025
@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 commentedon May 13, 2025
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 commentedon May 15, 2025
@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 commentedon May 15, 2025
@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 commentedon Jul 16, 2025
@btj how close are you to submit a PR for the Atomics Challenge ?
btj commentedon Jul 16, 2025
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.
Challenge 7: Verify safety of Atomic from_ptr methods