Skip to content

Avoid using specific `G` classes for locks, always use the projection `lockG` of `lock`.

Robbert Krebbers requested to merge robbert/lock_G_Σ into master

This MR is a follow up of !979 (merged).

Always preferring the projections is similar to the way we use acquire/release/etc.

This MR also adjusts the subG instance to use lockG instead of spin_lockG, and tests that the conditions are resolved automatically when using adequacy.

TODO: I have only done this for spin lock, the same remains to be done for ticket lock, rw lock, atomic heap.

Merge request reports