Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
12345678910111213141516171819202122232425262728293031323334353637383940414243444546474849505152535455565758596061626364656667686970717273747576777879808182838485868788899091929394959697989910010110210310410510610710810911011111211311411511611711811912012112212312412512612712812913013113213313413513613713813914014114214314414514614714814915015115215315415515615715815916016116216316416516616716816917017117217317417517617717817918018118218318418518618718818919019119219319419519619719819920020120220320420520620720820921021121221321421521621721821922022122222322422522622722822923023123223323423523623723823924024124224324424524624724824925025125225325425525625725825926026126226326426526626726826927027127227327427527627727827928028128228328428528628728828929029129229329429529629729829930030130230330430530630730830931031131231331431531631731831932032132232332432532632732832933033133233333433533633733833934034134234334434534634734834935035135235335435535635735835936036136236336436536636736836937037137237337437537637737837938038138238338438538638738838939039139239339439539639739839940040140240340440540640740840941041141241341441541641741841942042142242342442542642742842943043143243343443543643743843944044144244344444544644744844945045145245345445545645745845946046146246346446546646746846947047147247347447547647747847948048148248348448548648748848949049149249349449549649749849950050150250350450550650750850951051151251351451551651751851952052152252352452552652752852953053153253353453553653753853954054154254354454554654754854955055155255355455555655755855956056156256356456556656756856957057157257357457557657757857958058158258358458558658758858959059159259359459559659759859960060160260360460560660760860961061161261361461561661761861962062162262362462562662762862963063163263363463563663763863964064164264364464564664764864965065165265365465565665765865966066166266366466566666766866967067167267367467567667767867968068168268368468568668768868969069169269369469569669769869970070170270370470570670770870971071171271371471571671771871972072172272372472572672772872973073173273373473573673773873974074174274374474574674774874975075175275375475575675775875976076176276376476576676776876977077177277377477577677777877978078178278378478578678778878979079179279379479579679779879980080180280380480580680780880981081181281381481581681781881982082182282382482582682782882983083183283383483583683783883984084184284384484584684784884985085185285385485585685785885986086186286386486586686786886987087187287387487587687787887988088188288388488588688788888989089189289389489589689789889990090190290390490590690790890991091191291391491591691791891992092192292392492592692792892993093193293393493593693793893994094194294394494594694794894995095195295395495595695795895996096196296396496596696796896997097197297397497597697797897998098198298398498598698798898999099199299399499599699799899910001001100210031004100510061007100810091010101110121013101410151016101710181019102010211022102310241025102610271028102910301031103210331034103510361037103810391040104110421043104410451046104710481049105010511052105310541055105610571058105910601061106210631064106510661067106810691070107110721073107410751076107710781079108010811082108310841085108610871088108910901091109210931094109510961097109810991100110111021103110411051106110711081109111011111112111311141115111611171118111911201121112211231124112511261127112811291130113111321133113411351136113711381139114011411142114311441145114611471148114911501151115211531154115511561157115811591160116111621163116411651166116711681169117011711172117311741175117611771178117911801181118211831184118511861187118811891190119111921193119411951196119711981199120012011202120312041205120612071208120912101211121212131214121512161217121812191220#![allow(unused_imports)]
use core::sync::atomic::{ AtomicBool, AtomicI8, AtomicI16, AtomicI32, AtomicIsize, AtomicPtr, AtomicU8, AtomicU16, AtomicU32, AtomicUsize, Ordering,};
#[cfg(target_has_atomic = "64")]use core::sync::atomic::{AtomicI64, AtomicU64};
use super::modes::*;use super::pervasive::*;use super::prelude::*;use super::raw_ptr::PointsTo;use super::view::*;use super::wrapping::*;
macro_rules! make_unsigned_integer_atomic { ($at_ident:ident, $p_ident:ident, $p_data_ident:ident, $rust_ty: ty, $value_ty: ty, $modname:ident) => { atomic_types!($at_ident, $p_ident, $p_data_ident, $rust_ty, $value_ty); #[cfg_attr(verus_keep_ghost, verus::internal(verus_macro))] impl $at_ident { atomic_common_methods!($at_ident, $p_ident, $p_data_ident, $rust_ty, $value_ty, []); atomic_integer_methods!($at_ident, $p_ident, $rust_ty, $value_ty, $modname); } };}
macro_rules! make_signed_integer_atomic { ($at_ident:ident, $p_ident:ident, $p_data_ident:ident, $rust_ty: ty, $value_ty: ty, $modname:ident) => { atomic_types!($at_ident, $p_ident, $p_data_ident, $rust_ty, $value_ty); #[cfg_attr(verus_keep_ghost, verus::internal(verus_macro))] impl $at_ident { atomic_common_methods!($at_ident, $p_ident, $p_data_ident, $rust_ty, $value_ty, []); atomic_integer_methods!($at_ident, $p_ident, $rust_ty, $value_ty, $modname); } };}
macro_rules! make_bool_atomic { ($at_ident:ident, $p_ident:ident, $p_data_ident:ident, $rust_ty: ty, $value_ty: ty) => { atomic_types!($at_ident, $p_ident, $p_data_ident, $rust_ty, $value_ty); #[cfg_attr(verus_keep_ghost, verus::internal(verus_macro))] impl $at_ident { atomic_common_methods!($at_ident, $p_ident, $p_data_ident, $rust_ty, $value_ty, []); atomic_bool_methods!($at_ident, $p_ident, $rust_ty, $value_ty); } };}
macro_rules! atomic_types { ($at_ident:ident, $p_ident:ident, $p_data_ident:ident, $rust_ty: ty, $value_ty: ty) => { verus! {
#[verifier::external_body] /* vattr */ pub struct $at_ident { ato: $rust_ty, }
#[verifier::external_body] /* vattr */ pub tracked struct $p_ident { no_copy: NoCopy, unused: $value_ty, }
pub ghost struct $p_data_ident { pub patomic: int, pub value: $value_ty, }
impl $p_ident { #[verifier::external_body] /* vattr */ pub uninterp spec fn view(self) -> $p_data_ident;
pub open spec fn is_for(&self, patomic: $at_ident) -> bool { self.view().patomic == patomic.id() }
pub open spec fn points_to(&self, v: $value_ty) -> bool { self.view().value == v }
#[verifier::inline] pub open spec fn value(&self) -> $value_ty { self.view().value }
#[verifier::inline] pub open spec fn id(&self) -> AtomicCellId { self.view().patomic } }
} };}
macro_rules! atomic_types_generic { ($at_ident:ident, $p_ident:ident, $p_data_ident:ident, $rust_ty: ty, $value_ty: ty) => { verus! {
#[verifier::accept_recursive_types(T)] #[verifier::external_body] /* vattr */ pub struct $at_ident <T> { ato: $rust_ty, }
#[verifier::accept_recursive_types(T)] #[verifier::external_body] /* vattr */ pub tracked struct $p_ident <T> { no_copy: NoCopy, unusued: $value_ty, }
#[verifier::accept_recursive_types(T)] pub ghost struct $p_data_ident <T> { pub patomic: int, pub value: $value_ty, }
impl<T> $p_ident <T> { #[verifier::external_body] /* vattr */ pub uninterp spec fn view(self) -> $p_data_ident <T>;
pub open spec fn is_for(&self, patomic: $at_ident <T>) -> bool { self.view().patomic == patomic.id() }
pub open spec fn points_to(&self, v: $value_ty) -> bool { self.view().value == v }
#[verifier::inline] pub open spec fn value(&self) -> $value_ty { self.view().value }
#[verifier::inline] pub open spec fn id(&self) -> AtomicCellId { self.view().patomic } }
} };}
pub type AtomicCellId = int;
macro_rules! atomic_common_methods { ($at_ident: ty, $p_ident: ty, $p_data_ident: ty, $rust_ty: ty, $value_ty: ty, [ $($addr:tt)* ]) => { verus_impl!{
pub uninterp spec fn id(&self) -> int;
#[inline(always)] #[verifier::external_body] /* vattr */ pub const fn new(i: $value_ty) -> (res: ($at_ident, Tracked<$p_ident>)) ensures equal(res.1@.view(), $p_data_ident{ patomic: res.0.id(), value: i }), { let p = $at_ident { ato: <$rust_ty>::new(i) }; (p, Tracked::assume_new()) }
#[inline(always)] #[verifier::external_body] /* vattr */ #[verifier::atomic] /* vattr */ pub fn load(&self, Tracked(perm): Tracked<&$p_ident>) -> (ret: $value_ty) requires equal(self.id(), perm.view().patomic), ensures equal(perm.view().value, ret), opens_invariants none no_unwind { self.ato.load(Ordering::SeqCst) }
#[inline(always)] #[verifier::external_body] /* vattr */ #[verifier::atomic] /* vattr */ pub fn store(&self, Tracked(perm): Tracked<&mut $p_ident>, v: $value_ty) requires equal(self.id(), old(perm).view().patomic), ensures equal(final(perm).view().value, v) && equal(self.id(), final(perm).view().patomic), opens_invariants none no_unwind { self.ato.store(v, Ordering::SeqCst) }
#[inline(always)] #[verifier::external_body] /* vattr */ #[verifier::atomic] /* vattr */ pub fn compare_exchange(&self, Tracked(perm): Tracked<&mut $p_ident>, current: $value_ty, new: $value_ty) -> (ret: Result<$value_ty, $value_ty>) requires equal(self.id(), old(perm).view().patomic), ensures equal(self.id(), final(perm).view().patomic) && match ret { Result::Ok(r) => current $($addr)* == old(perm).view().value $($addr)* && equal(final(perm).view().value, new) && equal(r, old(perm).view().value), Result::Err(r) => current $($addr)* != old(perm).view().value $($addr)* && equal(final(perm).view().value, old(perm).view().value) && equal(r, old(perm).view().value), }, opens_invariants none no_unwind { self.ato.compare_exchange(current, new, Ordering::SeqCst, Ordering::SeqCst) }
#[inline(always)] #[verifier::external_body] /* vattr */ #[verifier::atomic] /* vattr */ pub fn compare_exchange_weak(&self, Tracked(perm): Tracked<&mut $p_ident>, current: $value_ty, new: $value_ty) -> (ret: Result<$value_ty, $value_ty>) requires equal(self.id(), old(perm).view().patomic), ensures equal(self.id(), final(perm).view().patomic) && match ret { Result::Ok(r) => current $($addr)* == old(perm).view().value $($addr)* && equal(final(perm).view().value, new) && equal(r, old(perm).view().value), Result::Err(r) => equal(final(perm).view().value, old(perm).view().value) && equal(r, old(perm).view().value), }, opens_invariants none no_unwind { self.ato.compare_exchange_weak(current, new, Ordering::SeqCst, Ordering::SeqCst) }
#[inline(always)] #[verifier::external_body] /* vattr */ #[verifier::atomic] /* vattr */ pub fn swap(&self, Tracked(perm): Tracked<&mut $p_ident>, v: $value_ty) -> (ret: $value_ty) requires equal(self.id(), old(perm).view().patomic), ensures equal(final(perm).view().value, v) && equal(old(perm).view().value, ret) && equal(self.id(), final(perm).view().patomic), opens_invariants none no_unwind { self.ato.swap(v, Ordering::SeqCst) }
#[inline(always)] #[verifier::external_body] /* vattr */ pub fn into_inner(self, Tracked(perm): Tracked<$p_ident>) -> (ret: $value_ty) requires equal(self.id(), perm.view().patomic), ensures equal(perm.view().value, ret), opens_invariants none no_unwind { self.ato.into_inner() }
} };}
macro_rules! atomic_integer_methods { ($at_ident:ident, $p_ident:ident, $rust_ty: ty, $value_ty: ty, $modname:ident) => { verus_impl!{
// Note that wrapping-on-overflow is the defined behavior for fetch_add and fetch_sub // for Rust's atomics (in contrast to ordinary arithmetic)
#[inline(always)] #[verifier::external_body] /* vattr */ #[verifier::atomic] /* vattr */ pub fn fetch_add_wrapping(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty) requires equal(self.id(), old(perm).view().patomic), ensures equal(old(perm).view().value, ret), final(perm).view().patomic == old(perm).view().patomic, final(perm).view().value as int == $modname::wrapping_add(old(perm).view().value, n), opens_invariants none no_unwind { self.ato.fetch_add(n, Ordering::SeqCst) }
#[inline(always)] #[verifier::external_body] /* vattr */ #[verifier::atomic] /* vattr */ pub fn fetch_sub_wrapping(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty) requires equal(self.id(), old(perm).view().patomic), ensures equal(old(perm).view().value, ret), final(perm).view().patomic == old(perm).view().patomic, final(perm).view().value as int == $modname::wrapping_sub(old(perm).view().value, n), opens_invariants none no_unwind { self.ato.fetch_sub(n, Ordering::SeqCst) }
// fetch_add and fetch_sub are more natural in the common case that you // don't expect wrapping
#[inline(always)] #[verifier::atomic] /* vattr */ pub fn fetch_add(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty) requires equal(self.id(), old(perm).view().patomic), (<$value_ty>::MIN as int) <= old(perm).view().value + n, old(perm).view().value + n <= (<$value_ty>::MAX as int), ensures equal(old(perm).view().value, ret), final(perm).view().patomic == old(perm).view().patomic, final(perm).view().value == old(perm).view().value + n, opens_invariants none no_unwind { self.fetch_add_wrapping(Tracked(&mut *perm), n) }
#[inline(always)] #[verifier::atomic] /* vattr */ pub fn fetch_sub(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty) requires equal(self.id(), old(perm).view().patomic), (<$value_ty>::MIN as int) <= old(perm).view().value - n, old(perm).view().value - n <= <$value_ty>::MAX as int, ensures equal(old(perm).view().value, ret), final(perm).view().patomic == old(perm).view().patomic, final(perm).view().value == old(perm).view().value - n, opens_invariants none no_unwind { self.fetch_sub_wrapping(Tracked(&mut *perm), n) }
#[inline(always)] #[verifier::external_body] /* vattr */ #[verifier::atomic] /* vattr */ pub fn fetch_and(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty) requires equal(self.id(), old(perm).view().patomic), ensures equal(old(perm).view().value, ret), final(perm).view().patomic == old(perm).view().patomic, final(perm).view().value == (old(perm).view().value & n), opens_invariants none no_unwind { self.ato.fetch_and(n, Ordering::SeqCst) }
#[inline(always)] #[verifier::external_body] /* vattr */ #[verifier::atomic] /* vattr */ pub fn fetch_or(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty) requires equal(self.id(), old(perm).view().patomic), ensures equal(old(perm).view().value, ret), final(perm).view().patomic == old(perm).view().patomic, final(perm).view().value == (old(perm).view().value | n), opens_invariants none no_unwind { self.ato.fetch_or(n, Ordering::SeqCst) }
#[inline(always)] #[verifier::external_body] /* vattr */ #[verifier::atomic] /* vattr */ pub fn fetch_xor(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty) requires equal(self.id(), old(perm).view().patomic), ensures equal(old(perm).view().value, ret), final(perm).view().patomic == old(perm).view().patomic, final(perm).view().value == (old(perm).view().value ^ n), opens_invariants none no_unwind { self.ato.fetch_xor(n, Ordering::SeqCst) }
#[inline(always)] #[verifier::external_body] /* vattr */ #[verifier::atomic] /* vattr */ pub fn fetch_nand(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty) requires equal(self.id(), old(perm).view().patomic), ensures equal(old(perm).view().value, ret), final(perm).view().patomic == old(perm).view().patomic, final(perm).view().value == !(old(perm).view().value & n), opens_invariants none no_unwind { self.ato.fetch_nand(n, Ordering::SeqCst) }
#[inline(always)] #[verifier::external_body] /* vattr */ #[verifier::atomic] /* vattr */ pub fn fetch_max(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty) requires equal(self.id(), old(perm).view().patomic), ensures equal(old(perm).view().value, ret), final(perm).view().patomic == old(perm).view().patomic, final(perm).view().value == (if old(perm).view().value > n { old(perm).view().value } else { n }), opens_invariants none no_unwind { self.ato.fetch_max(n, Ordering::SeqCst) }
#[inline(always)] #[verifier::external_body] /* vattr */ #[verifier::atomic] /* vattr */ pub fn fetch_min(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty) requires equal(self.id(), old(perm).view().patomic), ensures equal(old(perm).view().value, ret), final(perm).view().patomic == old(perm).view().patomic, final(perm).view().value == (if old(perm).view().value < n { old(perm).view().value } else { n }), opens_invariants none no_unwind { self.ato.fetch_min(n, Ordering::SeqCst) }
} };}
macro_rules! atomic_bool_methods { ($at_ident:ident, $p_ident:ident, $rust_ty: ty, $value_ty: ty) => { verus!{
#[inline(always)] #[verifier::external_body] /* vattr */ #[verifier::atomic] /* vattr */ pub fn fetch_and(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty) requires equal(self.id(), old(perm).view().patomic), ensures equal(old(perm).view().value, ret) && final(perm).view().patomic == old(perm).view().patomic && final(perm).view().value == (old(perm).view().value && n), opens_invariants none no_unwind { self.ato.fetch_and(n, Ordering::SeqCst) }
#[inline(always)] #[verifier::external_body] /* vattr */ #[verifier::atomic] /* vattr */ pub fn fetch_or(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty) requires equal(self.id(), old(perm).view().patomic), ensures equal(old(perm).view().value, ret) && final(perm).view().patomic == old(perm).view().patomic && final(perm).view().value == (old(perm).view().value || n), opens_invariants none no_unwind { self.ato.fetch_or(n, Ordering::SeqCst) }
#[inline(always)] #[verifier::external_body] /* vattr */ #[verifier::atomic] /* vattr */ pub fn fetch_xor(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty) requires equal(self.id(), old(perm).view().patomic), ensures equal(old(perm).view().value, ret) && final(perm).view().patomic == old(perm).view().patomic && final(perm).view().value == ((old(perm).view().value && !n) || (!old(perm).view().value && n)), opens_invariants none no_unwind { self.ato.fetch_xor(n, Ordering::SeqCst) }
#[inline(always)] #[verifier::external_body] /* vattr */ #[verifier::atomic] /* vattr */ pub fn fetch_nand(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty) requires equal(self.id(), old(perm).view().patomic), ensures equal(old(perm).view().value, ret) && final(perm).view().patomic == old(perm).view().patomic && final(perm).view().value == !(old(perm).view().value && n), opens_invariants none no_unwind { self.ato.fetch_nand(n, Ordering::SeqCst) }
} };}
macro_rules! ptr_atomic_methods { ($at_ty: ty, $rust_ty: ty, $value_ty: ty, $width: literal) => { // `from_ptr` requires alignment to `$rust_ty`; the caller holds a // `PointsTo<$value_ty>`, which guarantees only `align_of::<$value_ty>()` // (`PointsTo::is_aligned`). `target_has_atomic_primitive_alignment` is // rustc's name for those two being equal at a given width, so define // these only where it holds. #[cfg(target_has_atomic_primitive_alignment = $width)] const _: () = assert!( core::mem::align_of::<$value_ty>() == core::mem::align_of::<$rust_ty>(), concat!( stringify!($at_ty), ": align_of::<", stringify!($value_ty), ">() differs from align_of::<", stringify!($rust_ty), ">() on this target", ) );
#[cfg(target_has_atomic_primitive_alignment = $width)] verus!{ impl $at_ty { /// Store a value via a raw pointer using atomic store. /// /// This is useful if a user wants to implement lockless algorithm for a /// struct where elements are linked through pointers. In that /// case, PointsTo<$value_ty> might be stored in AtomicInvariant. /// /// The specification is similar to raw_ptr::ptr_mut_ref, /// but the implementation is atomic and so we can mark it as verifier::atomic, /// and so it can be used in open_atomic_invariant!. #[inline(always)] #[verifier::atomic] #[verifier::external_body] pub fn from_ptr_store(ptr: *mut $value_ty, value: $value_ty, Tracked(perm): Tracked<&mut PointsTo<$value_ty>>) requires old(perm).ptr() == ptr, ensures value == final(perm).value(), old(perm).ptr() == final(perm).ptr(), final(perm).is_init(), opens_invariants none no_unwind { unsafe { $rust_ty::from_ptr(ptr).store(value, Ordering::SeqCst) } }
/// Create a copy of the value via atomic load. #[inline(always)] #[verifier::atomic] #[verifier::external_body] pub fn from_ptr_load(ptr: *mut $value_ty, perm: Tracked<&PointsTo<$value_ty>>) -> (ret: $value_ty) requires perm.ptr() == ptr, perm.is_init(), ensures ret == perm.value(), opens_invariants none no_unwind { unsafe { $rust_ty::from_ptr(ptr).load(Ordering::SeqCst) } }
/// Swap the value via atomic swap. /// /// The swap reads the old value, so the memory must already be /// initialized; it writes `v`, so it is initialized on return. #[inline(always)] #[verifier::external_body] /* vattr */ #[verifier::atomic] /* vattr */ pub fn from_ptr_swap(ptr: *mut $value_ty, Tracked(perm): Tracked<&mut PointsTo<$value_ty>>, v: $value_ty) -> (ret: $value_ty) requires ptr == old(perm).ptr(), old(perm).is_init(), ensures final(perm).value() == v, final(perm).is_init(), old(perm).value() == ret, ptr == final(perm).ptr(), opens_invariants none no_unwind { unsafe { $rust_ty::from_ptr(ptr).swap(v, Ordering::SeqCst)} } }} };}
#[cfg(target_has_atomic = "64")]ptr_atomic_methods!(PAtomicU64, AtomicU64, u64, "64");
ptr_atomic_methods!(PAtomicU32, AtomicU32, u32, "32");ptr_atomic_methods!(PAtomicU16, AtomicU16, u16, "16");ptr_atomic_methods!(PAtomicU8, AtomicU8, u8, "8");ptr_atomic_methods!(PAtomicUsize, AtomicUsize, usize, "ptr");
#[cfg(target_has_atomic = "64")]ptr_atomic_methods!(PAtomicI64, AtomicI64, i64, "64");
ptr_atomic_methods!(PAtomicI32, AtomicI32, i32, "32");ptr_atomic_methods!(PAtomicI16, AtomicI16, i16, "16");ptr_atomic_methods!(PAtomicI8, AtomicI8, i8, "8");ptr_atomic_methods!(PAtomicIsize, AtomicIsize, isize, "ptr");
make_bool_atomic!(PAtomicBool, PermissionBool, PermissionDataBool, AtomicBool, bool);
make_unsigned_integer_atomic!(PAtomicU8, PermissionU8, PermissionDataU8, AtomicU8, u8, u8_specs);make_unsigned_integer_atomic!( PAtomicU16, PermissionU16, PermissionDataU16, AtomicU16, u16, u16_specs);make_unsigned_integer_atomic!( PAtomicU32, PermissionU32, PermissionDataU32, AtomicU32, u32, u32_specs);
#[cfg(target_has_atomic = "64")]make_unsigned_integer_atomic!( PAtomicU64, PermissionU64, PermissionDataU64, AtomicU64, u64, u64_specs);make_unsigned_integer_atomic!( PAtomicUsize, PermissionUsize, PermissionDataUsize, AtomicUsize, usize, usize_specs);
make_signed_integer_atomic!(PAtomicI8, PermissionI8, PermissionDataI8, AtomicI8, i8, i8_specs);make_signed_integer_atomic!( PAtomicI16, PermissionI16, PermissionDataI16, AtomicI16, i16, i16_specs);make_signed_integer_atomic!( PAtomicI32, PermissionI32, PermissionDataI32, AtomicI32, i32, i32_specs);
#[cfg(target_has_atomic = "64")]make_signed_integer_atomic!( PAtomicI64, PermissionI64, PermissionDataI64, AtomicI64, i64, i64_specs);make_signed_integer_atomic!( PAtomicIsize, PermissionIsize, PermissionDataIsize, AtomicIsize, isize, isize_specs);
atomic_types_generic!(PAtomicPtr, PermissionPtr, PermissionDataPtr, AtomicPtr<T>, *mut T);
#[cfg_attr(verus_keep_ghost, verifier::verus_macro)]impl<T> PAtomicPtr<T> { atomic_common_methods!( PAtomicPtr::<T>, PermissionPtr::<T>, PermissionDataPtr::<T>, AtomicPtr::<T>, *mut T, [ .view().addr ] );}
impl<X, Y, Pred> core::fmt::Debug for AtomicUpdate<X, Y, Pred> { fn fmt(&self, f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result { f.debug_struct("AtomicUpdate").finish_non_exhaustive() }}
/// Mark the `AtomicUpdate` as `Send` if both `X` and `Y` are also `Send`.////// # SAFETY/// While the `AtomicUpdate` is only a stand-in for a stack of nested callback functions,/// when the AU is moved to another thread, e.g. by moving it in and out of an atomic invariant,/// it allows resources to cross thread boundaries with it,/// so we must ensure the AU is only `Send` when `X: Send` and `Y: Send`.////// The predicate type we generate as part of the atomic specification only contains/// a ghost copy of function arguments, and ghost-mode data is always fine to move between threads./// There is no need to restrict it, as it is safe by construction.unsafe impl<X: Send, Y: Send, Pred> Send for AtomicUpdate<X, Y, Pred> {}
/// Unconditionally mark the `AtomicUpdate` as `Sync`.////// # SAFETY/// A shared reference to an `AtomicUpdate` is pretty much useless./// The only thing the user can do with an AU is open it, which requires full ownership./// All methods provided by this type are spec-mode,/// meaning they can already be used with a much weaker ghost copy of the AU.unsafe impl<X, Y, Pred> Sync for AtomicUpdate<X, Y, Pred> {}
verus! {
#[doc(hidden)]#[verifier::external_body]pub struct AtomicUpdateLifetimeMarker<'a> { _marker: core::marker::PhantomData<fn (&'a ())>,}
/// The **atomic update (AU)** is a ghost object which encapsulates the linearization point of a logically atomic function.////// Logical atomicity is a proof technique that allows us to treat a function as if it was atomic, i.e. as if it evaluates in a single atomic step, even though it might perform multiple `exec`-mode operations internally./// The key idea is that a logically atomic function contains a **linearization point (LP)**, that is, a point in the function which updates the state of the program in a single atomic step of computation./// We specify the behavior of such a function by describing the state of the program at four distinct points in time, specifically:/// - **(private pre)** at the start of the function,/// - **(atomic pre)** just before the linearization point,/// - **(atomic post)** just after the linearization point,/// - **(private post)** at the end of the function./// ```/// linearization point/// 🠗/// ├──────────────────────────────┤●├─────────────────────────┤/// private atomic atomic private/// pre pre post post/// ```/// The `AtomicUpdate` ghost object is the central abstraction for our implementation if logical atomicity, as it encapsulates the behavior of the function at the linearization point./// The atomic update is declared by the atomic specification, it is constructed by the atomic function call (i.e. the "client"), and it is opened/destructed at the linearization point of the logically atomic function (i.e. the "library").#[verifier::reject_recursive_types(X)]#[verifier::reject_recursive_types(Y)]#[verifier::reject_recursive_types(Pred)]#[verifier::external_body]pub struct AtomicUpdate<X, Y, Pred> { pred: Pred, _dummy: core::marker::PhantomData<fn (fn (X) -> Y)>, _not_send_sync: core::marker::PhantomData<*const ()>,}
impl<X, Y, Pred> AtomicUpdate<X, Y, Pred> { /// The predicate of the atomic update. /// /// See [`UpdatePredicate`] for more information. #[rustc_diagnostic_item = "verus::vstd::atomic::AtomicUpdate::pred"] pub uninterp spec fn pred(self) -> Pred;
/// A prophesy variable which indicates that an atomic update has been resolved. /// /// Initially, the value of this function is unknown, i.e. we can neither prove that it is `true` or `false`. /// Once the atomic update has been committed using the [`try_open_atomic_update`] macro, we learn that `au.resolves()` is `true`. /// /// We must be able to prove that `au.resolves()` when the logically atomic function exits. #[rustc_diagnostic_item = "verus::vstd::atomic::AtomicUpdate::resolves"] pub uninterp spec fn resolves(self) -> bool;
/// A prophesy variable for the input value of the atomic update. /// /// When the atomic update is committed, this variable is resolved to the input value of the atomic update. /// This variable is used internally in the (private) postcondition of the logically atomic function. #[rustc_diagnostic_item = "verus::vstd::atomic::AtomicUpdate::input"] pub uninterp spec fn input(self) -> X;
/// A prophesy variable for the output value of the atomic update. /// /// When the atomic update is committed, this variable is resolved to the output value of the atomic update. /// This variable is used internally in the (private) postcondition of the logically atomic function. #[rustc_diagnostic_item = "verus::vstd::atomic::AtomicUpdate::output"] pub uninterp spec fn output(self) -> Y;}
impl<X, Y, Pred: UpdatePredicate<X, Y>> AtomicUpdate<X, Y, Pred> { #[rustc_diagnostic_item = "verus::vstd::atomic::AtomicUpdate::req"] pub open spec fn req(self, x: X) -> bool { self.pred().req(x) }
#[rustc_diagnostic_item = "verus::vstd::atomic::AtomicUpdate::ens"] pub open spec fn ens(self, x: X, y: Y) -> bool { self.pred().ens(x, y) }
#[rustc_diagnostic_item = "verus::vstd::atomic::AtomicUpdate::outer_mask"] pub open spec fn outer_mask(self) -> ISet<int> { self.pred().outer_mask() }
#[rustc_diagnostic_item = "verus::vstd::atomic::AtomicUpdate::inner_mask"] pub open spec fn inner_mask(self) -> ISet<int> { self.pred().inner_mask() }}
#[cfg(verus_keep_ghost)]#[rustc_diagnostic_item = "verus::vstd::atomic::pred_args"]#[doc(hidden)]pub uninterp spec fn pred_args<Pred, Args>(pred: Pred) -> Args;
/// Trait used to specify the update predicate for the [`AtomicUpdate`].////// This trait is implemented automatically by Verus when a logically atomic function is defined./// ```/// exec fn function(px: PX) -> (py: PY)/// atomically (atomic_update) {/// type PredType,////// (ax: AX) -> (ay: AY),////// requires atomic_pre(px, ax),/// ensures atomic_post(px, ax, ay),////// outer_mask Eo,/// inner_mask Ei,/// },/// requires private_pre(px),/// ensures private_post(px, ax, ay, py),/// ```/// The above code snipped generates (roughly) the type and trait implementation below./// ```/// struct PredType { px: Ghost<PX> }////// impl UpdatePredicate<AX, AY> for PredType {/// open spec fn req(self, x: X) -> bool { atomic_pre }/// open spec fn ens(self, x: X, y: Y) -> bool { atomic_post }////// open spec fn outer_mask(self) -> ISet<int> { Eo }/// open spec fn inner_mask(self) -> ISet<int> { Ei }/// }/// ```pub trait UpdatePredicate<X, Y>: Sized { /// The atomic pre-condition. spec fn req(self, x: X) -> bool;
/// The atomic post-condition. spec fn ens(self, x: X, y: Y) -> bool;
/// The outer mask of the atomic update. open spec fn outer_mask(self) -> ISet<int> { ISet::empty() }
/// The inner mask of the atomic update. open spec fn inner_mask(self) -> ISet<int> { ISet::empty() }}
/// The control flow corresponding to the atomic update output.pub enum UpdateControlFlow { /// The update output value indicates that the atomic update has been committed. /// /// This means [`try_open_atomic_update`] will consume the atomic update (i.e. return `Ok(())`), /// and the atomic function call has to `break`. Commit, /// The update output value indicates that the atomic update has been aborted. /// /// This means [`try_open_atomic_update`] will give back the atomic update (i.e. return `Err(Tracked(au))`), /// and the atomic function call has to `continue`. Abort,}
impl UpdateControlFlow { pub open spec fn is_commit(self) -> bool { match self { UpdateControlFlow::Commit => true, UpdateControlFlow::Abort => false, } }
pub open spec fn is_abort(self) -> bool { !self.is_commit() }}
pub trait UpdateTry { spec fn branch(self) -> UpdateControlFlow;}
impl<T, E> UpdateTry for Result<T, E> { open spec fn branch(self) -> UpdateControlFlow { match self { Ok(_) => UpdateControlFlow::Commit, Err(_) => UpdateControlFlow::Abort, } }}
/// A trivial wrapper type which indicates a commit.////// This is useful for logically atomic functions which do not require an abort case.#[derive(Debug)]pub struct Commit<T>(pub T);
impl<T> Commit<T> { pub proof fn get(tracked self) -> (tracked out: T) ensures self@ == out, { self.0 }}
impl<T> View for Commit<T> { type V = T;
#[verifier::inline] open spec fn view(&self) -> T { self.0 }}
impl<T> UpdateTry for Commit<T> { open spec fn branch(self) -> UpdateControlFlow { UpdateControlFlow::Commit }}
impl UpdateTry for () { open spec fn branch(self) -> UpdateControlFlow { UpdateControlFlow::Commit }}
#[cfg(verus_keep_ghost)]#[rustc_diagnostic_item = "verus::vstd::atomic::branch_bool"]#[doc(hidden)]pub open spec fn branch_bool<T: UpdateTry>(this: T) -> bool { this.branch().is_commit()}
// Definition for atomic function call#[cfg(verus_keep_ghost)]#[rustc_diagnostic_item = "verus::vstd::atomic::atomically"]#[doc(hidden)]#[verifier::external]pub fn atomically<X, Y: UpdateTry, P: UpdatePredicate<X, Y>>( _body: impl FnOnce(fn (X) -> Y, Ghost<AtomicUpdate<X, Y, P>>),) -> AtomicUpdate<X, Y, P> { arbitrary()}
// Definitions for `try_open_atomic_update` macro#[doc(hidden)]pub struct BlockGuard<T> { _inner: core::marker::PhantomData<T>,}
#[cfg(verus_keep_ghost)]#[doc(hidden)]#[verifier::external] /* vattr */pub fn bind_lifetime_internal<'a, X: 'a, Y, P>( _block_guard: &'a BlockGuard<AtomicUpdate<X, Y, P>>,) -> X { unimplemented!()}
#[cfg(verus_keep_ghost)]#[rustc_diagnostic_item = "verus::vstd::atomic::try_open_atomic_update_begin"]#[doc(hidden)]#[verifier::external] /* vattr */pub fn try_open_atomic_update_begin<X, Y: UpdateTry, P: UpdatePredicate<X, Y>>( _atomic_update: AtomicUpdate<X, Y, P>,) -> BlockGuard<AtomicUpdate<X, Y, P>> { unimplemented!()}
#[cfg(verus_keep_ghost)]#[rustc_diagnostic_item = "verus::vstd::atomic::try_open_atomic_update_end"]#[doc(hidden)]#[verifier::external] /* vattr */pub fn try_open_atomic_update_end<X, Y: UpdateTry, P: UpdatePredicate<X, Y>>( _guard: BlockGuard<AtomicUpdate<X, Y, P>>, _y: Tracked<Y>,) -> Tracked<Result<(), AtomicUpdate<X, Y, P>>> { unimplemented!()}
// Macro definitions#[macro_export]macro_rules! open_atomic_update { ($($tail:tt)*) => { { let _ = ::verus_builtin_macros::verus_exec_open_au_macro_exprs!( $crate::atomic::try_open_atomic_update_internal!( $($tail)*, @EXEC, au_commit_wrap_exec ) ); } };}
#[macro_export]macro_rules! open_atomic_update_in_proof { ($($tail:tt)*) => { { let _ = ::verus_builtin_macros::verus_ghost_open_au_macro_exprs!( $crate::atomic::try_open_atomic_update_internal!( $($tail)*, @PROOF, au_commit_wrap_proof ) ); } };}
#[macro_export]macro_rules! peek_atomic_update { ($($tail:tt)*) => { { #[verifier::exec] let err_au = ::verus_builtin_macros::verus_exec_open_au_macro_exprs!( $crate::atomic::try_open_atomic_update_internal!( $($tail)*, @EXEC, au_abort_wrap_exec ) );
match () { #[cfg(verus_keep_ghost_body)] _ => $crate::atomic::au_abort_unwrap_exec(err_au),
#[cfg(not(verus_keep_ghost_body))] _ => ::verus_builtin::Tracked::assume_new_fallback(|| ::core::unreachable!()), } } };}
#[macro_export]macro_rules! peek_atomic_update_in_proof { ($($tail:tt)*) => { { #[verifier::proof] let err_au = ::verus_builtin_macros::verus_ghost_open_au_macro_exprs!( $crate::atomic::try_open_atomic_update_internal!( $($tail)*, @PROOF, au_abort_wrap_proof ) );
match () { #[cfg(verus_keep_ghost_body)] _ => $crate::atomic::au_abort_unwrap_proof(err_au),
#[cfg(not(verus_keep_ghost_body))] _ => ::verus_builtin::Tracked::assume_new_fallback(|| ::core::unreachable!()), } } };}
#[macro_export]macro_rules! try_open_atomic_update { ($($tail:tt)*) => { ::verus_builtin_macros::verus_exec_open_au_macro_exprs!( $crate::atomic::try_open_atomic_update_internal!($($tail)*) ) };}
#[macro_export]macro_rules! try_open_atomic_update_in_proof { ($($tail:tt)*) => { ::verus_builtin_macros::verus_ghost_open_au_macro_exprs!( $crate::atomic::try_open_atomic_update_internal!($($tail)*) ) };}
#[macro_export]macro_rules! try_open_atomic_update_internal { ($au:expr, $x:pat => $body:block, @EXEC, $wrap_fn:ident) => { $crate::atomic::try_open_atomic_update_internal!($au, $x => { #[verifier::exec] let v = $body;
match () { #[cfg(verus_keep_ghost_body)] _ => $crate::atomic::$wrap_fn(v),
#[cfg(not(verus_keep_ghost_body))] _ => ::verus_builtin::Tracked::assume_new_fallback(|| ::core::unreachable!()), } }) };
($au:expr, $x:pat => $body:block, @PROOF, $wrap_fn:ident) => { $crate::atomic::try_open_atomic_update_internal!($au, $x => { #[verifier::proof] let v = $body;
match () { #[cfg(verus_keep_ghost_body)] _ => $crate::atomic::$wrap_fn(v),
#[cfg(not(verus_keep_ghost_body))] _ => ::verus_builtin::Tracked::assume_new_fallback(|| ::core::unreachable!()), } }) };
($au:expr, $x:pat => $body:block) => { #[cfg_attr(verus_keep_ghost, verifier::open_au_block)] /* vattr */ { #[cfg(verus_keep_ghost_body)] let guard = $crate::atomic::try_open_atomic_update_begin($au); #[cfg(verus_keep_ghost_body)] let $x = $crate::atomic::bind_lifetime_internal(&guard); let res = $body;
match res { #[cfg(verus_keep_ghost_body)] res => $crate::atomic::try_open_atomic_update_end(guard, res),
#[cfg(not(verus_keep_ghost_body))] _ => ::verus_builtin::Tracked::assume_new_fallback(|| ::core::unreachable!()), } } };}
#[doc(hidden)]pub use {try_open_atomic_update_internal};pub use { open_atomic_update, open_atomic_update_in_proof, peek_atomic_update, peek_atomic_update_in_proof, try_open_atomic_update, try_open_atomic_update_in_proof,};
impl<T> PAtomicPtr<T> { #[inline(always)] #[verifier::external_body] /* vattr */ #[verifier::atomic] /* vattr */ #[cfg(any(verus_keep_ghost, feature = "strict_provenance_atomic_ptr"))] pub fn fetch_and(&self, Tracked(perm): Tracked<&mut PermissionPtr<T>>, n: usize) -> (ret: *mut T) requires equal(self.id(), old(perm).view().patomic), ensures equal(old(perm).view().value, ret), final(perm).view().patomic == old(perm).view().patomic, final(perm).view().value@.addr == (old(perm).view().value@.addr & n), final(perm).view().value@.provenance == old(perm).view().value@.provenance, final(perm).view().value@.metadata == old(perm).view().value@.metadata, opens_invariants none no_unwind { self.ato.fetch_and(n, Ordering::SeqCst) }
#[inline(always)] #[verifier::external_body] /* vattr */ #[verifier::atomic] /* vattr */ #[cfg(any(verus_keep_ghost, feature = "strict_provenance_atomic_ptr"))] pub fn fetch_xor(&self, Tracked(perm): Tracked<&mut PermissionPtr<T>>, n: usize) -> (ret: *mut T) requires equal(self.id(), old(perm).view().patomic), ensures equal(old(perm).view().value, ret), final(perm).view().patomic == old(perm).view().patomic, final(perm).view().value@.addr == (old(perm).view().value@.addr ^ n), final(perm).view().value@.provenance == old(perm).view().value@.provenance, final(perm).view().value@.metadata == old(perm).view().value@.metadata, opens_invariants none no_unwind { self.ato.fetch_xor(n, Ordering::SeqCst) }
#[inline(always)] #[verifier::external_body] /* vattr */ #[verifier::atomic] /* vattr */ #[cfg(any(verus_keep_ghost, feature = "strict_provenance_atomic_ptr"))] pub fn fetch_or(&self, Tracked(perm): Tracked<&mut PermissionPtr<T>>, n: usize) -> (ret: *mut T) requires equal(self.id(), old(perm).view().patomic), ensures equal(old(perm).view().value, ret), final(perm).view().patomic == old(perm).view().patomic, final(perm).view().value@.addr == (old(perm).view().value@.addr | n), final(perm).view().value@.provenance == old(perm).view().value@.provenance, final(perm).view().value@.metadata == old(perm).view().value@.metadata, opens_invariants none no_unwind { self.ato.fetch_or(n, Ordering::SeqCst) }}
} // verus!