Struct Resource 

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

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.

• alloc to allocate a resource.
• join to combine two resources via P::op, and split, its inverse.
• validate to assert the validity of any held resource.
• update or update_nondeterministic to perform a frame-preserving update.

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:

• Any of the examples in this directory
• The source code for the fractional resource library

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.