two more styles of lock spec
3 unresolved threads
3 unresolved threads
Compare changes
theories/locks/lockspecs/atomic_lock.v
0 → 100644
+ 108
− 0
Please add some more comments explaining what is happening here... I think the point of this is just to implement the interface? It's confusing that the interface does not mention TaDA but the implementation does.
It might also be worth saying how this relates to iris_heap_lang/lib/logatom_lock.v, since there's clearly some overlap.
This should be called
_fractional