RwLock

[rikosellic]

KVerus Prompt:
You need to add the type invariant of RWLock in ostd\src\sync\rwlock.rs, which is defined in the function closed spec fn wf(self) -> bool.

The RwLock structure's lock field has the type of lock: AtomicUsize<_, Option<RwFrac<T>>,_>,, which extends the ordinary atomic usize with a ghost RwFrac permission. The RWFrac type is an alias of type Frac<pcell::PointsTo<T>,MAX_READER_U64>. Frac is the classical fraction permission, whose definition can be found in vstd/tokens/frac.rs; pcell::PointsTo is the permission to access a cell, which is defined in vstd/cell/pcell.rs.

You should analyze the behaviour of the SpinLock methods (commented in the same file), including new, read, write, upread, try_read, try_write, try_upread, and write the correct invariant between the AtomicaUsize's value and the ghost RwFrac permission. To learn the syntax of the invariant and how it is used, you can refer to the SpinLock inostd\src\sync\spin.rs as an example.

[rikosellic]

Very interesting, I will check it later.

[rikosellic]

There are two issues in the code transformed by KVerus:

• It added & before self.lock, which should be consistent with the source code.
• It extracted the atomic_with_ghost into a separate assignment, which is actually unnecessary for compilation because one can directly use it in the if expression.