
Transactional
memory (TM) algorithms are subtle and the TM correctness conditions are
intricate. Decomposition of the correctness condition can bring
modularity to TM algorithm design and verification. We present a
decomposition of opacity called markability as a conjunction of
separate intuitive invariants. We prove the equivalence of opacity and
markability. The proofs of markability of TM algorithms can be aided by
and mirror the algorithm design intuitions. As an example, we prove the
markability and hence opacity of the TL2 algorithm. In addition, based
on one of the invariants, we present lower bound results for the time
complexity of TM algorithms.

