This paper defines the notion of hybrid atomicity for nested transacti
on systems, and presents and verifies an algorithm providing this prop
erty. Hybrid atomicity is a modular property; it allows the correctnes
s of a system to be deduced from the fact that each object is implemen
ted to have the property. It allows more concurrency than dynamic atom
icity, by assigning timestamps to transactions at commit. The Avalon s
ystem provides exactly this facility. The results in this paper extend
earlier work using the same model for locking and timestamp-based alg
orithms, providing further evidence for the generality of the approach
. However, there are some subtle differences with the definitions used
in earlier work, showing the difficulties of developing precise gener
al models for nested transaction systems.