IMPLEMENTATION OF THE SENTRY SYSTEM

The sentry of a concurrent program P is a program that observes the ex ecution of P, and issues a warning if P does not behave correctly with respect to a given set of logical properties (owing to a programming error or a failure), The synchronization between the program and sentr y is such that the program never waits for the sentry, the shared stor age between them is very small (in fact linear in the number of progra m variables being observed), and the snapshots read by the sentry are consistent. To satisfy these three requirements, some snapshots may be overwritten by the program before being read by the sentry, We develo p a family of algorithms that preserve these requirements for properti es involving scalar variables, then extend the algorithms to permit th e observation of large data structures without additional overhead. We describe in detail the annotation language with which the properties can be expressed, and a prototype system that we have implemented to g enerate the sentry automatically for any given concurrent C program. F inally, we present experimental results that show that the overhead in curred by the sentry is on average no worse than ten per cent for snap shots of up to six variables, and that the loss of snapshots prevents the sentry's detection of an single violation in less than four per ce nt of the cases. Recurring errors are detected at a rate of 100 per ce nt.