|
Guerraoui
and Kapalka defined opacity as a safety criterion for transactional
memory algorithms in 2008. Researchers have shown how to prove opacity,
while little is known about pitfalls that can lead to non-opacity. In
this paper, we identify
two problems that lead to non-opacity, we present automatic tool
support for finding those problems, and we prove an impossibility
result. We first show that the well-known TM algorithms DSTM and McRT
don't satisfy opacity. DSTM suffers from a write-skew anomaly, while
McRT suffers from a write-exposure anomaly. We then prove that for
direct-update TM algorithms, opacity is incompatible with a liveness
criterion called local progress, even for fault-free systems. Our
result implies that if TM algorithm designers want both opacity and
local progress, they should avoid direct-update algorithms.
|
|