Skip to content

Add reference-counting reader-writer lock implementation

Isaac van Bakel requested to merge ivanbakel/iris:rw_lock into master

As suggested for contribution by @jung.

This HeapLang reader-writer lock allows for fractional predicates to be shared by one or more readers, or wholly taken by some writer. The physical lock state is controlled by an atomically-accessed reference counter, linked to an authoritative multiset which is used to issue existential fractions to readers.

Possible changes

A canonical lock construction

This lock is almost a lock, if we try for any predicate P to construct it with the badly-behaved "fractional" predicate λ _, P. This construction should allow us to use just the writer API as a plain lock, since only the reader API ever actually requires that the predicate being handled is fractional. However, this implementation requires a Fractional instance in the lock construction, rather than just at the use sites for acquiring and releasing the reader lock. This may be a good reason for changing the approach, but I'm not sure one way or the other.

Edited by Isaac van Bakel

Merge request reports