Viktor Vafeiadis
Results
3
comments of
Viktor Vafeiadis
I also disliked the multiple thread steps for each machine step approach, but the alternative seems worse. It seems that you will lose read-acquire after write elimination, which is allowed...
You are right: the index should be `length l`.
The only reason to use `doma`/`domb` is automation. It's easier to prove facts stated in terms of `doma r d` than about `dom_rel r ⊆₁ d` by `[e]auto`. The point...