Skip to main content

Resource

vstd::resource::pcm

Struct Resource 

Source 
pub struct Resource<P: PCM> { /* private fields */ }
Expand description

Interface for PCM / Resource Algebra ghost state.

RA-based ghost state is a well-established theory that is especially useful for verifying concurrent code. An introduction to the concept can be found in Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning or Iris from the ground up.

To embed the concept into Verus, we:

  • Use a trait, PCM, to embed the well-formedness laws of a resource algebra
  • use a “tracked ghost” object, Resource<P> (this page) to represent ownership of a resource.

Most operations are fairly standard, just “translated” from the usual CSL presentation into Verus.

The interface also includes a nontrivial extension for working with shared references to resources. Shared resources do not compose in a “separating” way via P::op, but rather, in a “potentially overlapping” way (join_shared). Shared resources can also be used to “help” perform frame-preserving updates, as long as they themselves do not change (update_with_shared).

§Examples

See:

§See also

The “storage protocol” formalism is an even more significant extension with additional capabilities for interacting with shared resources.

VerusSync provides a higher-level “swiss army knife” for building useful ghost resources.

Implementations§

Source§

impl<P: PCM> Resource<P>

Source

pub uninterp fn value(self) -> P

The underlying value of the resource

Source

pub uninterp fn loc(self) -> Loc

The location of the resource

Source

pub proof fn alloc(value: P) -> tracked out : Self

requires
value.valid(),
ensures
out.value() == value,

Allocate a new resource at a fresh location

Source

pub proof fn join(tracked self, tracked other: Self) -> tracked out : Self

requires
self.loc() == other.loc(),
ensures
out.loc() == self.loc(),
out.value() == P::op(self.value(), other.value()),

We can join together two resources at the same location, where we obtain the combination of the two

Source

pub proof fn split(tracked self, left: P, right: P) -> tracked out : (Self, Self)

requires
self.value() == P::op(left, right),
ensures
out.0.loc() == self.loc(),
out.1.loc() == self.loc(),
out.0.value() == left,
out.1.value() == right,

If a resource holds the result of a composition, we can split it into the components

Source

pub proof fn create_unit(loc: Loc) -> tracked out : Self

ensures
out.value() == P::unit(),
out.loc() == loc,

Create a unit at a particular location

Source

pub proof fn validate(tracked &self)

ensures
self.value().valid(),

Whenever we have a resource, that resource is valid. This intuitively (and inductively) holds because: 1. We only create valid resources (either via alloc or create_unit). 2. We can only update the value of a resource via a frame_preserving_update (see update for more details. Because of the requirement of that updates are frame preserving this means that joins remain valid.

Source

pub proof fn update_nondeterministic(tracked self, new_values: Set<P>) -> tracked out : Self

requires
frame_preserving_update_nondeterministic(self.value(), new_values),
ensures
out.loc() == self.loc(),
new_values.contains(out.value()),

This is a more general version of update.

Source

pub proof fn update(tracked self, new_value: P) -> tracked out : Self

requires
frame_preserving_update(self.value(), new_value),
ensures
out.loc() == self.loc(),
out.value() == new_value,

Update a resource to a new value. This can only be done if the update is frame preserving (i.e., any value that could be composed with the original value can still be composed with the new value).

See frame_preserving_update for more information.

Source

pub proof fn extract(tracked &mut self) -> tracked other : Self

ensures
other.loc() == old(self).loc(),
other.value() == old(self).value(),

Extracts the resource from r, leaving r unspecified and returning a new resource holding the previous value of r.

Source

pub proof fn join_shared<'a>(tracked &'a self, tracked other: &'a Self) -> tracked out : &'a Self

requires
self.loc() == other.loc(),
ensures
out.loc() == self.loc(),
incl(self.value(), out.value()),
incl(other.value(), out.value()),

This is useful when you have two (or more) shared resources and want to learn that they agree, as you can combine this validate, e.g., x.join_shared(y).validate().

Source

pub proof fn weaken<'a>(tracked &'a self, target: P) -> tracked out : &'a Self

requires
incl(target, self.value()),
ensures
out.loc() == self.loc(),
out.value() == target,

Extract a shared reference to a preceding element in the extension order from a shared reference.

Source

pub proof fn validate_2(tracked &mut self, tracked other: &Self)

requires
old(self).loc() == other.loc(),
ensures
*self == *old(self),
P::op(self.value(), other.value()).valid(),

Validate two items at once. If we have two resources at the same location then its composition is valid.

Source

pub proof fn update_nondeterministic_with_shared(tracked self, tracked other: &Self, new_values: Set<P>, ) -> tracked out : Self

requires
self.loc() == other.loc(),
frame_preserving_update_nondeterministic(
    P::op(self.value(), other.value()),
    set_op(new_values, other.value()),
),
ensures
out.loc() == self.loc(),
new_values.contains(out.value()),

We can do a similar update to update_with_shared for non-deterministic updates

Source

pub proof fn join_shared_to_target<'a>(tracked &'a self, tracked other: &'a Self, target: P, ) -> tracked out : &'a Self

requires
self.loc() == other.loc(),
conjunct_shared(self.value(), other.value(), target),
ensures
out.loc() == self.loc(),
out.value() == target,

We can do a similar update to update_with_shared for non-deterministic updates

Source

pub proof fn update_with_shared(tracked self, tracked other: &Self, new_value: P) -> tracked out : Self

requires
self.loc() == other.loc(),
frame_preserving_update(
    P::op(self.value(), other.value()),
    P::op(new_value, other.value()),
),
ensures
out.loc() == self.loc(),
out.value() == new_value,

If x · y --> x · z is a frame-perserving update, and we have a shared reference to x, we can update the y resource to z.

Source

pub proof fn duplicate_previous(tracked &self, value: P) -> tracked out : Self

requires
frame_preserving_update(self.value(), P::op(value, self.value())),
ensures
out.loc() == self.loc(),
out.value() == value,

If x --> x · y is a frame-perserving update, and we have a shared reference to x, we can create a resource to y

Auto Trait Implementations§

§

impl<P> Freeze for Resource<P>

§

impl<P> RefUnwindSafe for Resource<P>
where P: RefUnwindSafe,

§

impl<P> Send for Resource<P>
where P: Send,

§

impl<P> Sync for Resource<P>
where P: Sync,

§

impl<P> Unpin for Resource<P>
where P: Unpin,

§

impl<P> UnsafeUnpin for Resource<P>

§

impl<P> UnwindSafe for Resource<P>
where P: 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, VERUS_SPEC__A> FromSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: From<T>,

Source§

exec fn obeys_from_spec() -> bool

Source§

exec fn from_spec(v: T) -> VERUS_SPEC__A

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, VERUS_SPEC__A> IntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: Into<T>,

Source§

exec fn obeys_into_spec() -> bool

Source§

exec fn into_spec(self) -> T

Source§

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

Source§

open spec fn obeys_into_spec() -> bool

{ <U as FromSpec<Self>>::obeys_from_spec() }
Source§

open spec fn into_spec(self) -> U

{ U::from_spec(self) }
Source§

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

Source§

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, VERUS_SPEC__A> TryFromSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryFrom<T>,

Source§

exec fn obeys_try_from_spec() -> bool

Source§

exec fn try_from_spec( v: T, ) -> Result<VERUS_SPEC__A, <VERUS_SPEC__A as TryFrom<T>>::Error>

Source§

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

Source§

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.
Source§

impl<T, VERUS_SPEC__A> TryIntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryInto<T>,

Source§

exec fn obeys_try_into_spec() -> bool

Source§

exec fn try_into_spec(self) -> Result<T, <VERUS_SPEC__A as TryInto<T>>::Error>

Source§

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

Source§

open spec fn obeys_try_into_spec() -> bool

{ <U as TryFromSpec<Self>>::obeys_try_from_spec() }
Source§

open spec fn try_into_spec(self) -> Result<U, <U as TryFrom<T>>::Error>

{ <U as TryFromSpec<Self>>::try_from_spec(self) }