Victor Bushkov
ABSTRACT
The history of distributed computing is full of trade-offs between safety and liveness. For instance, one of the most celebrated results in the field, namely the impossibility of consensus in an asynchronous system basically says that we cannot devise an algorithm that deterministically ensures consensus agreement and validity (i.e., safety) on the one hand, and consensus wait-freedom (i.e., liveness) on the other hand. The motivation of this work is to study the extent to which safety and liveness properties inherently exclude each other. More specifically, we ask, given any safety property S, whether we can determine the strongest (resp. weakest) liveness property that can (resp. cannot) be achieved with S. We show that, maybe surprisingly, the answers to these safety-liveness exclusion questions are in general negative. This has several ramifications in various distributed computing contexts. In the context of consensus for example, this means that it is impossible to determine the strongest (resp. the weakest) liveness property that can (resp. cannot) be ensured with linearizability.
However, we present a way to circumvent these impossibilities and answer positively the safety-liveness question by considering a restricted form of liveness. We consider a definition that gathers generalized forms of obstruction-freedom and lock-freedom while enabling to determine the strongest (resp. weakest) liveness property that can (resp. cannot) be implemented in the context of consensus and transactional memory.
- B. Alpern and F. B. Schneider. Defining liveness. Information Processing Letters, 21(4), 1985.Google Scholar
- H. Attiya and J. Welch. Distributed Computing: Fundamentals, Simulations and Advanced Topics. John Wiley & Sons, 2004. Google ScholarDigital Library
- E. Borowsky and E. Gafni. Generalized flp impossibility result for t-resilient asynchronous computations. In ACM STOC, 1993. Google ScholarDigital Library
- V. Bushkov and R. Guerraoui. Safety-liveness exclusion in distributed computing. Technical Report 207929, EPFL, 2015.Google Scholar
- V. Bushkov, R. Guerraoui, and M. Kapałka. On the liveness of transactional memory. In ACM PODC, 2012. Google ScholarDigital Library
- B. Chor, A. Israeli, and M. Li. On processor coordination using asynchronous hardware. In ACM PODC, 1987. Google ScholarDigital Library
- F. Ellen, P. Fatourou, E. Kosmas, A. Milani, and C. Travers. Universal constructions that ensure disjoint-access parallelism and wait-freedom. In ACM PODC, 2012. Google ScholarDigital Library
- F. Fich and E. Ruppert. Hundreds of impossibility results for distributed computing. Distrib. Comput., 16(2--3), 2003. Google ScholarDigital Library
- M. J. Fischer, N. A. Lynch, and M. S. Paterson. Impossibility of distributed consensus with one faulty process. J. ACM, 32(2), 1985. Google ScholarDigital Library
- K. Fraser. Practical lock freedom. In PhD thesis, Cambridge University Computer Laboratory, 2003.Google Scholar
- P. Ganty, R. Majumdar, and A. Rybalchenko. Verifying liveness for asynchronous programs. In ACM POPL, 2009. Google ScholarDigital Library
- S. Gilbert and N. Lynch. Brewer's conjecture and the feasibility of consistent, available, partition-tolerant web services. SIGACT News, 33(2), 2002. Google ScholarDigital Library
- S. Gilbert and N. A. Lynch. Perspectives on the cap theorem. Computer, 45(2), 2012. Google ScholarDigital Library
- D. S. Greenberg, G. Taubenfeld, and D.-W. Wang. Choice coordination with multiple alternatives (preliminary version). In WDAG, 1992. Google ScholarDigital Library
- R. Guerraoui and M. Kapalka. On obstruction-free transactions. In ACM SPAA, 2008. Google ScholarDigital Library
- R. Guerraoui and M. Kapalka. On the correctness of transactional memory. In ACM PPoPP, 2008. Google ScholarDigital Library
- R. Guerraoui and E. Ruppert. Anonymous and fault-tolerant shared-memory computing. Distributed Computing, 20(3):165--177, 2007.Google ScholarDigital Library
- T. Harris, J. R. Larus, and R. Rajwar. Transactional Memory, 2nd edition. Morgan and Claypool, 2010. Google ScholarDigital Library
- M. Herlihy. Wait-free synchronization. ACM Trans. Program. Lang. Syst., 13(1), 1991. Google ScholarDigital Library
- M. Herlihy, V. Luchangco, and M. Moir. Obstruction-free synchronization: Double-ended queues as an example. In IEEE ICDCS, 2003. Google ScholarDigital Library
- M. Herlihy, V. Luchangco, M. Moir, and W. N. Scherer, III. Software transactional memory for dynamic-sized data structures. In ACM PODC, 2003. Google ScholarDigital Library
- M. Herlihy and N. Shavit. The topological structure of asynchronous computability. J. ACM, 46(6), 1999. Google ScholarDigital Library
- M. Herlihy and N. Shavit. On the nature of progress. In OPODIS, 2011. Google ScholarDigital Library
- M. P. Herlihy and J. M. Wing. Linearizability: a correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst., 12(3), 1990. Google ScholarDigital Library
- D. Imbs, M. Raynal, and G. Taubenfeld. On asymmetric progress conditions. In ACM PODC, 2010. Google ScholarDigital Library
- L. Lamport. Using time instead of timeout for fault-tolerant distributed systems. ACM Trans. Program. Lang. Syst., 6(2), 1984. Google ScholarDigital Library
- B. W. Lampson. How to build a highly available system using consensus. In WDAG, 1996. Google ScholarDigital Library
- M. C. Loui and H. H. Abu-Amara. Memory requirements for agreement among unreliable asynchronous processes, volume 4. JAI press, 1987.Google Scholar
- N. A. Lynch. Distributed Algorithms. Morgan Kaufmann Publishers Inc., 1996. Google ScholarDigital Library
- S. Owicki and L. Lamport. Proving liveness properties of concurrent programs. ACM Trans. Program. Lang. Syst., 4(3), 1982. Google ScholarDigital Library
- C. H. Papadimitriou. The serializability of concurrent database updates. J. ACM, 26(4), 1979. Google ScholarDigital Library
- F. B. Schneider. Implementing fault-tolerant services using the state machine approach: a tutorial. ACM Comput. Surv., 22(4), 1990. Google ScholarDigital Library
- R. Segala, R. Gawlick, J. Søgaard-Andersen, and N. Lynch. Liveness in timed and untimed systems. Inf. Comput., 141(2), 1998. Google ScholarDigital Library
- N. Shavit and D. Touitou. Software transactional memory. In ACM PODC, 1995. Google ScholarDigital Library
- G. Taubenfeld. On the computational power of shared objects. In OPODIS, 2009. Google ScholarDigital Library
- G. Taubenfeld. The computational structure of progress conditions. In DISC, 2010. Google ScholarDigital Library
- G. Taubenfeld and S. Moran. Possibility and impossibility results in a shared memory environment. Acta Inf, 33, 1996. Google ScholarDigital Library
- H. Völzer and D. Varacca. Defining fairness in reactive and concurrent systems. J. ACM, 59(3), 2012. Google ScholarDigital Library
Index Terms
- Safety-Liveness Exclusion in Distributed Computing
Recommendations
Safety of Deferred Update in Transactional Memory
ICDCS '13: Proceedings of the 2013 IEEE 33rd International Conference on Distributed Computing SystemsTransactional memory allows the user to declare sequences of instructions as speculative transactions that can either commit or abort. If a transaction commits, it appears to be executed sequentially, so that the committed transactions constitute a ...
Disjoint-Access Parallelism: Impossibility, Possibility, and Cost of Transactional Memory Implementations
PODC '15: Proceedings of the 2015 ACM Symposium on Principles of Distributed ComputingDisjoint-Access Parallelism (DAP) is considered one of the most desirable properties to maximize the scalability of Transactional Memory (TM). This paper investigates the possibility and inherent cost of implementing a DAP TM that ensures two properties ...
On the liveness of transactional memory
PODC '12: Proceedings of the 2012 ACM symposium on Principles of distributed computingDespite the large amount of work on Transactional Memory (TM), little is known about how much liveness it could provide. This paper presents the first formal treatment of the question. We prove that no TM implementation can ensure local progress, the ...
Comments