Safety property (source code)

= Safety property

A requirement whose violation has a finite execution prefix that no continuation can repair. Two <software threads> simultaneously inside a protected <critical section> already violate <mutual exclusion>; later leaving does not erase that violation. This contrasts with a <liveness property>, for which a long finite wait alone does not establish failure.<Defining Liveness by Bowen Alpern and others>[pp. 181–182: finite irremediable prefixes]{ref}