Modules§
Structs§
- Invariant
Predicate_ auto_ RwLock_ exc - Invariant
Predicate_ auto_ RwLock_ rc - Read
Handle - Handle obtained for a shared read-lock from an
RwLock
. - RwLock
- A verified implementation of a reader-writer lock, implemented using atomics and a reference count.
- Write
Handle - Handle obtained for an exclusive write-lock from an
RwLock
.