Document Open Access Logo

A Framework for Consistency Algorithms

Authors Peter Chini, Prakash Saivasan

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2020.42.pdf
  • Filesize: 486 kB
  • 17 pages

Document Identifiers

Author Details

Peter Chini
  • TU Braunschweig, Germany
Prakash Saivasan
  • The Institute of Mathematical Sciences, HBNI, Chennai, India

Cite AsGet BibTex

Peter Chini and Prakash Saivasan. A Framework for Consistency Algorithms. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 42:1-42:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.FSTTCS.2020.42

Abstract

We present a framework that provides deterministic consistency algorithms for given memory models. Such an algorithm checks whether the executions of a shared-memory concurrent program are consistent under the axioms defined by a model. For memory models like SC and TSO, checking consistency is NP-complete. Our framework shows, that despite the hardness, fast deterministic consistency algorithms can be obtained by employing tools from fine-grained complexity. The framework is based on a universal consistency problem which can be instantiated by different memory models. We construct an algorithm for the problem running in time 𝒪^*(2^k), where k is the number of write accesses in the execution that is checked for consistency. Each instance of the framework then admits an 𝒪^*(2^k)-time consistency algorithm. By applying the framework, we obtain corresponding consistency algorithms for SC, TSO, PSO, and RMO. Moreover, we show that the obtained algorithms for SC, TSO, and PSO are optimal in the fine-grained sense: there is no consistency algorithm for these running in time 2^{o(k)} unless the exponential time hypothesis fails.

Subject Classification

ACM Subject Classification
  • Theory of computation → Concurrency
  • Theory of computation → Problems, reductions and completeness
Keywords
  • Consistency
  • Weak Memory
  • Fine-Grained Complexity

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. The sparc architecture manual - version 8 and version 9, 1992,1994. Google Scholar
  2. H. Sinha A. Heddaya. Coherence, non-coherence and local consistency in distributed shared memory for parallel computing. Technical Report BU-CS-92-004, Boston University, 1992. Google Scholar
  3. P. A. Abdulla, F. Haziza, L. Holík, B. Jonsson, and A. Rezine. An integrated specification and verification technique for highly concurrent data structures. In TACAS, volume 7795 of Lecture Notes in Computer Science, pages 324-338. Springer, 2013. Google Scholar
  4. M. Ahamad, R. A. Bazzi, R. John, P. Kohli, and G. Neiger. The power of processor consistency. In Proceedings of the Fifth Annual ACM Symposium on Parallel Algorithms and Architectures, page 251–260. ACM, 1993. Google Scholar
  5. J. Alglave. A formal hierarchy of weak memory models. Formal Methods Syst. Des., 41(2):178-210, 2012. Google Scholar
  6. J. Alglave, L. Maranget, and M. Tautschnig. Herding cats: Modelling, simulation, testing, and data mining for weak memory. ACM Trans. Program. Lang. Syst., 36(2):7:1-7:74, 2014. Google Scholar
  7. R. Alur, K. L. McMillan, and D. A. Peled. Model-checking of correctness conditions for concurrent objects. Inf. Comput., 160(1-2):167-188, 2000. Google Scholar
  8. M. F. Atig, A. Bouajjani, S. Burckhardt, and M. Musuvathi. On the verification problem for weak memory models. In POPL, pages 7-18. ACM, 2010. Google Scholar
  9. M. F. Atig, A. Bouajjani, S. Burckhardt, and M. Musuvathi. What’s decidable about weak memory models? In ESOP, volume 7211 of Lecture Notes in Computer Science, pages 26-46. Springer, 2012. Google Scholar
  10. R. Biswas and C. Enea. On the complexity of checking transactional consistency. Proc. ACM Program. Lang., 3(OOPSLA):165:1-165:28, 2019. Google Scholar
  11. A. Bouajjani, C. Enea, R. Guerraoui, and J. Hamza. On verifying causal consistency. In POPL, pages 626-638. ACM, 2017. Google Scholar
  12. A. Bouajjani, C. Enea, and J. Hamza. Verifying eventual consistency of optimistic replication systems. In POPL, pages 285-296. ACM, 2014. Google Scholar
  13. A. Bouajjani, R. Meyer, and E. Möhlmann. Deciding robustness against total store ordering. In ICALP, volume 6756 of Lecture Notes in Computer Science, pages 428-440. Springer, 2011. Google Scholar
  14. G. Calin, E. Derevenetc, R. Majumdar, and R. Meyer. A theory of partitioned global address spaces. In FSTTCS, volume 24 of LIPIcs, pages 127-139. Schloss Dagstuhl, 2013. Google Scholar
  15. J. F. Cantin, M. H. Lipasti, and J. E. Smith. The complexity of verifying memory coherence and consistency. IEEE Transactions on Parallel and Distributed Systems, 16(7):663-671, 2005. Google Scholar
  16. J. Chen, B. Chor, M. Fellows, X. Huang, D. W. Juedes, I. A. Kanj, and G. Xia. Tight lower bounds for certain parameterized np-hard problems. Inf. Comput., 201(2):216-231, 2005. Google Scholar
  17. P. Chini, J. Kolberg, A. Krebs, R. Meyer, and P. Saivasan. On the complexity of bounded context switching. In ESA, volume 87 of LIPIcs, pages 27:1-27:15. Schloss Dagstuhl, 2017. Google Scholar
  18. P. Chini, R. Meyer, and P. Saivasan. Fine-grained complexity of safety verification. In TACAS, volume 10806 of Lecture Notes in Computer Science, pages 20-37. Springer, 2018. Google Scholar
  19. P. Chini, R. Meyer, and P. Saivasan. Complexity of liveness in parameterized systems. In FSTTCS, volume 150 of LIPIcs, pages 37:1-37:15. Schloss Dagstuhl, 2019. Google Scholar
  20. P. Chini and P. Saivasan. A framework for consistency algorithms. CoRR, abs/2007.11398, 2020. Google Scholar
  21. M. Cygan, H. Dell, D. Lokshtanov, D. Marx, J. Nederlof, Y. Okamoto, R. Paturi, S. Saurabh, and M. Wahlström. On problems as hard as CNF-SAT. ACM Trans. Algorithms, 12(3):41:1-41:24, 2016. Google Scholar
  22. M. Cygan, F. V. Fomin, Ł. Kowalik, D. Lokshtanov, D. Marx, M. Pilipczuk, M. Pilipczuk, and S. Saurabh. Parameterized algorithms. Springer, 2015. Google Scholar
  23. E. Derevenetc and R. Meyer. Robustness against power is pspace-complete. In ICALP, volume 8573 of Lecture Notes in Computer Science, pages 158-170. Springer, 2014. Google Scholar
  24. R. G. Downey and M. R. Fellows. Fundamentals of Parameterized Complexity. Springer, 2013. Google Scholar
  25. M. Emmi and C. Enea. Monitoring weak consistency. In CAV, volume 10981 of Lecture Notes in Computer Science, pages 487-506. Springer, 2018. Google Scholar
  26. M. Emmi and C. Enea. Sound, complete, and tractable linearizability monitoring for concurrent collections. Proc. ACM Program. Lang., 2(POPL):25:1-25:27, 2018. Google Scholar
  27. M. Emmi, C. Enea, and J. Hamza. Monitoring refinement via symbolic reasoning. In PLDI, pages 260-269. ACM, 2015. Google Scholar
  28. C. Enea and A. Farzan. On atomicity in presence of non-atomic writes. In TACAS, volume 9636 of Lecture Notes in Computer Science, pages 497-514. Springer, 2016. Google Scholar
  29. A. Farzan and P. Madhusudan. The complexity of predicting atomicity violations. In TACAS, volume 5505 of Lecture Notes in Computer Science, pages 155-169. Springer, 2009. Google Scholar
  30. F. V. Fomin and D. Kratsch. Exact Exponential Algorithms. Texts in Theoretical Computer Science. Springer, 2010. Google Scholar
  31. F. Furbach, R. Meyer, K. Schneider, and M. Senftleben. Memory-model-aware testing: A unified complexity analysis. ACM Trans. Embedded Comput. Syst., 14(4):63:1-63:25, 2015. Google Scholar
  32. P. B. Gibbons and E. Korach. Testing shared memories. SIAM J. Comput., 26(4):1208-1244, 1997. Google Scholar
  33. J. R. Goodman. Cache consistency and sequential consistency. Technical Report 1006, University of Wisconsin-Madison, 1991. Google Scholar
  34. M. Herlihy and J. M. Wing. Linearizability: A correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst., 12(3):463-492, 1990. Google Scholar
  35. R. Impagliazzo and R. Paturi. On the complexity of k-SAT. JCSS, 62(2):367-375, 2001. Google Scholar
  36. A. B. Kahn. Topological sorting of large networks. Commun. ACM, 5(11):558–562, 1962. Google Scholar
  37. L. Lamport. Time, clocks, and the ordering of events in a distributed system. Commun. ACM, 21(7):558-565, 1978. Google Scholar
  38. L. Lamport. How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Computers, 28(9):690-691, 1979. Google Scholar
  39. D. Lokshtanov, D. Marx, and S. Saurabh. Slightly superexponential parameterized problems. In SODA, pages 760-776. SIAM, 2011. Google Scholar
  40. S. Mador-Haim, L. Maranget, S. Sarkar, K. Memarian, J. Alglave, S. Owens, R. Alur, M. M. K. Martin, P. Sewell, and D. Williams. An axiomatic memory model for POWER multiprocessors. In CAV, volume 7358 of Lecture Notes in Computer Science, pages 495-512. Springer, 2012. Google Scholar
  41. J. Manson, W. Pugh, and S. V. Adve. The java memory model. In POPL, pages 378-391. ACM, 2005. Google Scholar
  42. U. Mathur, A. Pavlogiannis, and M. Viswanathan. The complexity of dynamic data race prediction. In LICS, pages 713-727. ACM, 2020. Google Scholar
  43. C. H. Papadimitriou. The serializability of concurrent database updates. J. ACM, 26(4):631-653, 1979. Google Scholar
  44. J. S. Sandberg R. J. Lipton. PRAM: A scalable shared memory. Technical Report CS-TR-180-88, Princeton University, 1988. Google Scholar
  45. S. Sarkar, P. Sewell, J. Alglave, L. Maranget, and D. Williams. Understanding POWER multiprocessors. In PLDI, pages 175-186. ACM, 2011. Google Scholar
  46. R. C. Steinke and G. J. Nutt. A unified theory of shared memory consistency. J. ACM, 51(5):800-849, 2004. Google Scholar
  47. D. B. Terry, M. Theimer, K. Petersen, A. J. Demers, M. Spreitzer, and C. Hauser. Managing update conflicts in bayou, a weakly connected replicated storage system. In SOSP, pages 172-183. ACM, 1995. Google Scholar
  48. H. Wei, Y. Huang, J. Cao, X. Ma, and J. Lu. Verifying PRAM consistency over read/write traces of data replicas. CoRR, abs/1302.5161, 2013. Google Scholar
  49. P. Wolper. Expressing interesting properties of programs in propositional temporal logic. In POPL, pages 184-193. ACM, 1986. Google Scholar
  50. R. Zennou, A. Bouajjani, C. Enea, and M. Erradi. Gradual consistency checking. In CAV, volume 11562 of Lecture Notes in Computer Science, pages 267-285. Springer, 2019. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact