Sentries for the execution of concurrent programs

The sentry of a concurrent program P is a program that executes concurrently with P, periodically takes snapshots of P, and issues a warning if it detects that some snapshot does not satisfy a predefined predicate. The sentry is unique among snapshot-taking systems in its low-overhead. First, the shared storage between the observed program P and the sentry is linear in the number of P variables that are being observed. Second, the observed program P never waits for the sentry. Third, the mutual exclusion between the observed program and the sentry is achieved without using any special hardware or software constructs. In this paper, we present a family of two sentries. One sentry can be used for taking snapshots of scalar variables (and can check whether these snapshots satisfy a given propositional predicate), and the other sentry can be used for taking snapshots of complex variables such as arrays (and can check whether these snapshots satisfy a given first-order predicate). We briefly describe a system prototype for automatically generating sentries for any given concurrent program, and present some encouraging empirical results that we obtained from this prototype