Rollback Atomicity

We introduce a new non-interference criterion for concurrent programs: rollback atomicity. Similarly to other definitions of atomicity, rollback atomicity of a given concurrent execution requires that there be a matching serial execution. Rollback atomicity differs from other definitions of atomicity in two key regards. First, it is formulated as a special case of view refinement. As such, it requires a correspondence between the states of a concurrent and a serial execution for each atomic block rather than only at quiescent states. Second, it designates a subset of shared variables as peripheral and has more relaxed requirements for peripheral variables than previous non-interference criteria. In this paper, we provide the motivation for rollback atomicity. We formally define it and compare it with other notions of atomicity and noninterference criteria. We built a runtime checker for rollback atomicity integrated into the refinement checking tool, VYRD. This implementation was...

• Type: Conference
• Year: 2007
• Where: RV
• Authors: Serdar Tasiran, Tayfun Elmas
• Keywords: Concurrent Executions, Rollback Atomicity, Rollback Atomicity Differs, RV 2007