We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Was making a basic lock example, and after I got done I realized I forgot a 'mut' somewhere and Verus didn't complain.
use vstd::prelude::*; use vstd::atomic_ghost::*; use vstd::cell; use vstd::cell::*; use vstd::modes::*; verus!{ struct_with_invariants!{ struct Lock<T> { pub atomic: AtomicBool<_, Option<cell::PointsTo<T>>, _>, pub cell: PCell<T>, } spec fn wf(self) -> bool { invariant on atomic with (cell) is (v: bool, g: Option<cell::PointsTo<T>>) { match g { None => { // When there's no PointsTo, the lock must be taken, thus // the boolean value is 'true'. v == true } Some(points_to) => { points_to.id() == cell.id() && points_to.is_init() && v == false } } } } } impl<T> Lock<T> { fn new(t: T) -> (lock: Self) ensures lock.wf() { let (cell, Tracked(cell_perm)) = PCell::new(t); let atomic = AtomicBool::new(Ghost(cell), false, Tracked(Some(cell_perm))); Lock { atomic, cell } } fn acquire(&self) -> (points_to: Tracked<cell::PointsTo<T>>) requires self.wf(), ensures [email protected]() == self.cell.id(), [email protected]_init() { loop invariant self.wf(), { let tracked points_to_opt = None; // Verus/Rust should be complaining there's no 'mut' here. let res = atomic_with_ghost!(&self.atomic => compare_exchange(false, true); ghost points_to_inv => { tracked_swap(&mut points_to_opt, &mut points_to_inv); } ); if res.is_ok() { return Tracked(points_to_opt.tracked_unwrap()); } } } fn release(&self, points_to: Tracked<cell::PointsTo<T>>) requires self.wf(), [email protected]() == self.cell.id(), [email protected]_init() { atomic_with_ghost!(&self.atomic => store(false); ghost points_to_inv => { points_to_inv = Some(points_to.get()); } ); } } } fn main() { }
The text was updated successfully, but these errors were encountered:
No branches or pull requests
Was making a basic lock example, and after I got done I realized I forgot a 'mut' somewhere and Verus didn't complain.
The text was updated successfully, but these errors were encountered: