1
Vote

missing check on claim destruction in atomics

description

The soundness of treating atomic actions as atomic depends on the objects in the closed object list remaining closed for the duration of the atomic. By historical accident, VCC implements this with a coarser check that no objects are unwrapped within an atomic. However, this check is not performed on claim destruction (which is just syntactic sugar for an unwrapping along with some updates), creating an unsoundness. A check should be added that destroyed claims are not mentioned in the closed object list.

comments