Static verification of data-consistency properties

摘要: Writing correct shared-memory concurrent programs is hard. Not only must a programmer reason about the correctness of sequential execution code, but also possible side effects caused by interleaved concurrently executing threads. Incorrect use synchronization primitives can lead to data-consistency errors, which have drastic consequences (cf. Northeast Blackout 2003). This dissertation presents techniques verify statically that programmer's preserves data consistency. The notion consistency used throughout atomic-set serializability (AS-serializability), was first proposed Vaziri et al. (2006). AS-serializability property program execution, and relaxation serializability. An serializable if its outcome equivalent an where all transactions are executed serially. relaxes be with respect specific memory locations. The approach taken software model checking every AS-serializable. First, abstract generated from concrete program. defined such it over-approximates set behaviors Second, checker explores executions program. The challenge define abstractions account for multitude sources unboundedness in Concrete dynamic allocation, recursion, thread creation, reentrant locks, name few. The contributions generic permit performed presence several unboundedness. My research addressed problem determining whether certain class models Java Somewhat surprisingly, given many allowed considered, I able show decidable, gave practical algorithm problem. technique has been implemented tool called EMPIRE, find known bugs programs.