Struct BfTermPool

pub struct BfTermPool<T: ?Sized> { /* private fields */ }

Provides access to the mCRL2 busy forbidden protocol, where there are thread local busy flags and one central storage for the forbidden flags. Care must be taken to avoid deadlocks since the FFI also uses the same flags.

Implementations

impl<T> BfTermPool<T>

pub fn new(object: T) -> BfTermPool<T>

impl<'a, T: ?Sized> BfTermPool<T>

pub fn read(&'a self) -> BfTermPoolRead<'a, T>

Provides read access to the underlying object.

pub fn write(&'a self) -> BfTermPoolWrite<'a, T>

Provides write access to the underlying object.

pub unsafe fn get(&'a self) -> &'a T

Provides read access to the underlying object.

Safety

Assumes that we are in an exclusive section.

pub unsafe fn write_exclusive(&'a self) -> BfTermPoolThreadWrite<'a, T>

Provides write access to the underlying object

Safety

Provides mutable access given that other threads use write and [read] exclusively. If we are already in an exclusive context then lock can be set to false.

Trait Implementations

impl<T: Markable + ?Sized> Markable for BfTermPool<T>

fn mark(&self, todo: Pin<&mut term_mark_stack>)

Marks all the ATermRefs to prevent them from being garbage collected.

fn contains_term(&self, term: &ATermRef<'_>) -> bool

Should return true iff the given term is contained in the object. Used for runtime checks.

fn len(&self) -> usize

Returns the number of terms in the instance, used to delay garbage collection.

fn is_empty(&self) -> bool

Returns true iff the container is empty.

impl<T: Send> Send for BfTermPool<T>

impl<T: Send> Sync for BfTermPool<T>