Detecting Atomicity Errors in Message Passing Programs

A distributed application can be viewed as a collection of processes that execute a number of atomic actions. Atomicity is the basis for reasoning about the correctness of a program. Atomicity errors in a run typically indicate the presence of program errors. This paper formalizes the notion of atomicity of an action in a message passing program based on a weak-order relation among atoms. An atom can be a single statement or a sequence of statements in a program. Knowing the atoms, the atomicity of a run can be monitored and checked. Serialization of conflicting atoms is another generic correctness requirement. When atoms affect a common property, such as in sharing resources or maintaining a common constraint, they must be serialized in a run. This paper presents two efficient algorithms for dynamically detecting atomicity and serialization errors, accompanied with their proof of correctness.