Document Open Access Logo

Ensuring Average Recovery with Adversarial Scheduler

Authors Jingshu Chen, Mohammad Roohitavaf, Sandeep S. Kulkarni

PDF

File

Thumbnail PDF
PDF
LIPIcs.OPODIS.2015.23.pdf
  • Filesize: 0.64 MB
  • 18 pages

Document Identifiers

Subject Classification

Keywords
  • Average Recovery Time
  • Hyper-liveness
  • Program Repair

Metrics

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

Abstract

In this paper, we focus on revising a given program so that the average recovery time in the presence of an adversarial scheduler is bounded by a given threshold lambda. Specifically, we consider the scenario where the fault (or other unexpected action) perturbs the program to a state that is outside its set of legitimate states. Starting from this state, the program executes its actions/transitions to recover to legitimate states. However, the adversarial scheduler can force the program to reach one illegitimate state that requires a longer recovery time. 

To ensure that the average recovery time is less than lambda, we need to remove certain transitions/behaviors. We show that achieving this average response time while removing minimum transitions is NP-hard. In other words, there is a tradeoff between the time taken to synthesize the program and the transitions preserved to reduce the average convergence time. We present six different heuristics and evaluate this tradeoff with case studies. Finally, we note that the average convergence time considered here requires formalization of hyperproperties. Hence, this work also demonstrates feasibility of adding (certain) hyperproperties to an existing program.

Cite As Get BibTex

Jingshu Chen, Mohammad Roohitavaf, and Sandeep S. Kulkarni. Ensuring Average Recovery with Adversarial Scheduler. In 19th International Conference on Principles of Distributed Systems (OPODIS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 46, pp. 23:1-23:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.OPODIS.2015.23

Author Details

Jingshu Chen
Mohammad Roohitavaf
Sandeep S. Kulkarni

References

  1. Saba Aflaki, Fathiyeh Faghih, and Borzoo Bonakdarpour. Synthesizing self-stabilizing protocols under average recovery time constraints. In 35th IEEE International Conference on Distributed Computing Systems, ICDCS 2015, Columbus, OH, USA, June 29 - July 2, 2015, pages 579-588, 2015. Google Scholar
  2. Bowen Alpern and Fred B. Schneider. Defining liveness. Inf. Process. Lett., 21(4):181-185, 1985. URL: http://dx.doi.org/10.1016/0020-0190(85)90056-0.
  3. A. Arora and M. G. Gouda. Closure and convergence: A foundation of fault-tolerant computing. IEEE Transactions on Software Engineering, 19(11):1015-1027, 1993. Google Scholar
  4. Gilles Barthe, Pedro R. D'Argenio, and Tamara Rezk. Secure information flow by self-composition. Mathematical Structures in Computer Science, 21(6):1207-1252, 2011. URL: http://dx.doi.org/10.1017/S0960129511000193.
  5. Borzoo Bonakdarpour. Automated Revision of Distributed and Real-Time Programs. PhD thesis, Michigan State University, 2009. Google Scholar
  6. Borzoo Bonakdarpour, Ali Ebnenasir, and Sandeep S. Kulkarni. Complexity results in revising unity programs. ACM Transactions on Autonomous and Adaptive Systems (TAAS), 4(1):5:1-5:28, Feb. 2009. Google Scholar
  7. Borzoo Bonakdarpour, Sandeep S. Kulkarni, and Fuad Abujarad. Symbolic synthesis of masking fault-tolerant distributed programs. Distributed Computing, 25(1):83-108, 2012. URL: http://dx.doi.org/10.1007/s00446-011-0139-3.
  8. Buddy - a binary decision diagram package. URL: http://buddy.sourceforge.net/manual/main.html.
  9. Michael R. Clarkson and Fred B. Schneider. Hyperproperties. Journal of Computer Security, 18(6):1157-1210, 2010. URL: http://dx.doi.org/10.3233/JCS-2009-0393.
  10. Edsger W. Dijkstra. Self-stabilizing systems in spite of distributed control. Commun. ACM, 17(11):643-644, 1974. URL: http://dx.doi.org/10.1145/361179.361202.
  11. Edsger W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976. Google Scholar
  12. Ali Ebnenasir and Aly Farahat. Swarm synthesis of convergence for symmetric protocols. In Cristian Constantinescu and Miguel P. Correia, editors, EDCC, pages 13-24. IEEE, 2012. URL: http://dx.doi.org/10.1109/EDCC.2012.22.
  13. Ali Ebnenasir and Aly Farahat. Swarm synthesis of convergence for symmetric protocols. In Proceedings of the Ninth European Dependable Computing Conference, pages 13-24, 2012. Google Scholar
  14. Ali Ebnenasir and Sandeep S. Kulkarni. Feasibility of stepwise design of multitolerant programs. ACM Trans. Softw. Eng. Methodol., 21(1):1, 2011. URL: http://dx.doi.org/10.1145/2063239.2063240.
  15. Aly Farahat and Ali Ebnenasir. A lightweight method for automated design of convergence in network protocols. ACM Transactions on Autonomous and Adaptive Systems (TAAS), 7(4):38:1-38:36, December 2012. Google Scholar
  16. Aly Farahat and Ali Ebnenasir. Local reasoning for global convergence of parameterized rings. In IEEE International Conference on Distributed Computing Systems (ICDCS), pages 496-505, 2012. Google Scholar
  17. Joseph A. Goguen and José Meseguer. Security policies and security models. In IEEE Symposium on Security and Privacy, pages 11-20, 1982. Google Scholar
  18. Alex Klinkhamer and Ali Ebnenasir. A software tool for swarm synthesis of self-stabilization. URL: http://www.cs.mtu.edu/~apklinkh/protocon/index.html.
  19. Alex Klinkhamer and Ali Ebnenasir. On the complexity of adding convergence. In Farhad Arbab and Marjan Sirjani, editors, FSEN, volume 8161 of Lecture Notes in Computer Science, pages 17-33. Springer, 2013. URL: http://dx.doi.org/10.1007/978-3-642-40213-5_2.
  20. Alex Klinkhamer and Ali Ebnenasir. Synthesizing self-stabilization through superposition and backtracking. In 16th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS), pages 252-267. Springer, 2014. Google Scholar
  21. K. Raymond. A tree-based algorithm for distributed mutual exclusion. ACM Transactions on Computer Systems, 7(1):61-77, 1989. Google Scholar
  22. Amer Tahat and Ali Ebnenasir. A hybrid method for the verification and synthesis of parameterized self-stabilizing protocols. In 24th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR), 2014. 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact