Files

Résumé

This paper asks how much liveness a transactional memory (TM) implementation can guarantee. We first devise a formal framework for reasoning about liveness properties of TMs. Then, we prove that the strongest liveness property that a TM can ensure in an asynchronous system with transaction crashes is a property that we call "global progress". This property is analogous to lock-freedom for shared-memory objects and is indeed guaranteed by certain TM implementations, e.g., OSTM. We also prove that the presence of zombie transactions, which perform infinitely many operations but never attempt to commit, does not impact our result. In fact, we show that zombie transactions are, in a precise sense, equivalent to crashed transactions.

Détails

PDF