Struct vstd::rwlock::RwLockToks::State

source · 
pub struct State<K, V, Pred: InvariantPredicate<K, V>> {
    pub k: K,
    pub pred: PhantomData<Pred>,
    pub flag_exc: bool,
    pub flag_rc: nat,
    pub storage: Option<V>,
    pub pending_writer: Option<()>,
    pub writer: Option<()>,
    pub pending_reader: Multiset<()>,
    pub reader: Multiset<V>,
}

Fields§

§k: K§pred: PhantomData<Pred>§flag_exc: bool§flag_rc: nat§storage: Option<V>§pending_writer: Option<()>§writer: Option<()>§pending_reader: Multiset<()>§reader: Multiset<V>

Implementations§

source§

impl<K, V, Pred: InvariantPredicate<K, V>> State<K, V, Pred>

source

pub fn initialize_full(post: Self, k: K, t: V) -> bool

source

pub fn initialize_full_enabled(k: K, t: V) -> bool

source

pub fn acquire_read_start(pre: Self, post: Self) -> bool

source

pub fn acquire_read_start_strong(pre: Self, post: Self) -> bool

source

pub fn acquire_read_start_enabled(pre: Self) -> bool

source

pub fn acquire_read_end(pre: Self, post: Self) -> bool

source

pub fn acquire_read_end_strong(pre: Self, post: Self) -> bool

source

pub fn acquire_read_end_enabled(pre: Self) -> bool

source

pub fn acquire_read_end_asserts(pre: State<K, V, Pred>)

source

pub fn acquire_read_abandon(pre: Self, post: Self) -> bool

source

pub fn acquire_read_abandon_strong(pre: Self, post: Self) -> bool

source

pub fn acquire_read_abandon_enabled(pre: Self) -> bool

source

pub fn acquire_read_abandon_asserts(pre: State<K, V, Pred>)

source

pub fn acquire_exc_start(pre: Self, post: Self) -> bool

source

pub fn acquire_exc_start_strong(pre: Self, post: Self) -> bool

source

pub fn acquire_exc_start_enabled(pre: Self) -> bool

source

pub fn acquire_exc_start_asserts(pre: State<K, V, Pred>)

source

pub fn acquire_exc_end(pre: Self, post: Self) -> bool

source

pub fn acquire_exc_end_strong(pre: Self, post: Self) -> bool

source

pub fn acquire_exc_end_enabled(pre: Self) -> bool

source

pub fn acquire_exc_end_asserts(pre: State<K, V, Pred>)

source

pub fn release_exc(pre: Self, post: Self, x: V) -> bool

source

pub fn release_exc_strong(pre: Self, post: Self, x: V) -> bool

source

pub fn release_exc_enabled(pre: Self, x: V) -> bool

source

pub fn release_exc_asserts(pre: State<K, V, Pred>, x: V)

source

pub fn read_guard_asserts(pre: State<K, V, Pred>, x: V)

source

pub fn read_match_asserts(pre: State<K, V, Pred>, x: V, y: V)

source

pub fn release_shared(pre: Self, post: Self, x: V) -> bool

source

pub fn release_shared_strong(pre: Self, post: Self, x: V) -> bool

source

pub fn release_shared_enabled(pre: Self, x: V) -> bool

source

pub fn release_shared_asserts(pre: State<K, V, Pred>, x: V)

source

pub fn next_by( pre: State<K, V, Pred>, post: State<K, V, Pred>, step: Step<K, V, Pred> ) -> bool

source

pub fn next(pre: State<K, V, Pred>, post: State<K, V, Pred>) -> bool

source

pub fn next_strong_by( pre: State<K, V, Pred>, post: State<K, V, Pred>, step: Step<K, V, Pred> ) -> bool

source

pub fn next_strong(pre: State<K, V, Pred>, post: State<K, V, Pred>) -> bool

source

pub fn init_by(post: State<K, V, Pred>, step: Config<K, V, Pred>) -> bool

source

pub fn init(post: State<K, V, Pred>) -> bool

source

pub fn invariant(&self) -> bool

source

pub open spec fn exc_bit_matches(&self) -> bool

{
    (if self.flag_exc { 1 } else { 0 as int })
        == (if self.pending_writer.is_Some() { 1 } else { 0 as int }) as int
            + (if self.writer.is_Some() { 1 } else { 0 as int }) as int
}
source

pub open spec fn count_matches(&self) -> bool

{
    self.flag_rc
        == self.pending_reader.count(()) + self.reader.count(self.storage.get_Some_0())
}
source

pub open spec fn reader_agrees_storage(&self) -> bool

{
    forall |t: V| imply(
        #[trigger] self.reader.count(t) > 0,
        equal(self.storage, Option::Some(t)),
    )
}
source

pub open spec fn writer_agrees_storage(&self) -> bool

{ imply(self.writer.is_Some(), self.storage.is_None()) }
source

pub open spec fn writer_agrees_storage_rev(&self) -> bool

{ imply(self.storage.is_None(), self.writer.is_Some()) }
source

pub open spec fn sto_user_inv(&self) -> bool

{ self.storage.is_some() ==> Pred::inv(self.k, self.storage.unwrap()) }

Auto Trait Implementations§

§

impl<K, V, Pred> RefUnwindSafe for State<K, V, Pred>
where K: RefUnwindSafe, Pred: RefUnwindSafe, V: RefUnwindSafe,

§

impl<K, V, Pred> Send for State<K, V, Pred>
where K: Send, Pred: Send, V: Send,

§

impl<K, V, Pred> Sync for State<K, V, Pred>
where K: Sync, Pred: Sync, V: Sync,

§

impl<K, V, Pred> Unpin for State<K, V, Pred>
where K: Unpin, Pred: Unpin, V: Unpin,

§

impl<K, V, Pred> UnwindSafe for State<K, V, Pred>
where K: UnwindSafe, Pred: UnwindSafe, V: UnwindSafe,

Blanket Implementations§

source§

impl<T> Any for T
where T: 'static + ?Sized,

source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
source§

impl<T> Borrow<T> for T
where T: ?Sized,

source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
source§

impl<T> BorrowMut<T> for T
where T: ?Sized,

source§

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more
source§

impl<T> From<T> for T

source§

fn from(t: T) -> T

Returns the argument unchanged.

source§

impl<T, U> Into<U> for T
where U: From<T>,

source§

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

source§

impl<T, U> TryFrom<U> for T
where U: Into<T>,

§

type Error = Infallible

The type returned in the event of a conversion error.
source§

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

Performs the conversion.
source§

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,

§

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.
source§

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.