Verifying commit-atomicity using model-checking

摘要: The notion that certain procedures are atomic provides a valuable partial specification for many multithreaded software systems. Several existing tools verify atomicity by showing every interleaved execution reduces to an equivalent serial (in which the actions of each procedure not with other threads). However, experiments these have highlighted number interesting that, although atomic, reducible.