Skip to content

Commit a1a6c17

Browse files
committed
Auto merge of rust-lang#2993 - Vanille-N:tb-protector, r=RalfJung
TB: Redefine trigger condition for protectors The Coq formalization revealed that as currently implemented, read accesses did not always commute. Indeed starting from a lazily initialized `Active` protected tag, applying a foreign read then a child read produces `Frozen`, but child read then foreign read triggers UB (because the child read initializes _before_ the `Active -> Frozen`). This reformulation of when protectors trigger fixes that issue: - instead of `Active + foreign read -> Frozen` and `Active -> Frozen` when protected is UB - we do `Active + foreign read -> if protected { Disabled } else { Frozen }` There is already precedent for transitions being dependent on the presence of a protector (`Reserved + foreign read -> if protected { Frozen } else { Reserved }`), and this has the nice side-effect of simplifying the protector trigger condition to just an equality check against `Disabled` since now there is protector UB iff a protected tag becomes `Disabled`. In order not to introduce an extra `if`, it was decided that `Disabled -> Disabled` would be UB when protected, which was not the case previously. This is merely a theoretical for now because a protected `Disabled` is unreachable in the first place. The extra test is not directly related to this modification, but also checks things related to protectors and lazy initialization.
2 parents 8bf6142 + e6f9a2b commit a1a6c17

File tree

0 file changed

+0
-0
lines changed

    0 file changed

    +0
    -0
    lines changed

    0 commit comments

    Comments
     (0)