Skip to main content

Revising Distributed UNITY Programs Is NP-Complete

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 5401))

Abstract

We focus on automated revision techniques for adding Unity properties to distributed programs. We show that unlike centralized programs, where multiple safety properties along with one progress property can be simultaneously added in polynomial-time, addition of only one safety or one progress property to distributed programs is NP-complete. We also propose an efficient symbolic heuristic for adding a leads-to property to a distributed program. We demonstrate the application of this heuristic in automated synthesis of recovery paths in fault-tolerant distributed programs.

This work was partially sponsored by NSF CAREER CCR-0092724 and ONR Grant N00014-01-1-0744.

This is a preview of subscription content, log in via an institution.

Buying options

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Arora, A., Attie, P.C., Emerson, E.A.: Synthesis of fault-tolerant concurrent programs. In: Principles of Distributed Computing (PODC), pp. 173–182 (1998)

    Google Scholar 

  2. Arora, A., Kulkarni, S.S.: Component based design of multitolerant systems. IEEE Transactions on Software Engineering 24(1), 63–78 (1998)

    Article  Google Scholar 

  3. Attie, P., Emerson, E.A.: Synthesis of concurrent programs for an atomic read/write model of computation. ACM Transactions on Programming Languages and Systems (TOPLAS) 23(2), 187–242 (2001)

    Article  Google Scholar 

  4. Bonakdarpour, B., Kulkarni, S.S.: Exploiting symbolic techniques in automated synthesis of distributed programs with large state space. In: IEEE International Conference on Distributed Computing Systems (ICDCS), pp. 3–10 (2007)

    Google Scholar 

  5. Bonakdarpour, B., Kulkarni, S.S.: SYCRAFT: A tool for synthesizing fault-tolerant distributed programs. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 167–171. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  6. Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers 35(8), 677–691 (1986)

    Article  MATH  Google Scholar 

  7. Chandy, K.M., Misra, J.: Parallel program design: a foundation. Addison-Wesley Longman Publishing Co., Inc., Boston (1988)

    MATH  Google Scholar 

  8. Ebnenasir, A., Kulkarni, S.S., Bonakdarpour, B.: Revising UNITY programs: Possibilities and limitations. In: Anderson, J.H., Prencipe, G., Wattenhofer, R. (eds.) OPODIS 2005. LNCS, vol. 3974, pp. 275–290. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  9. Emerson, E.A., Clarke, E.M.: Using branching time temporal logic to synthesize synchronization skeletons. Science of Computer Programming 2(3), 241–266 (1982)

    Article  MATH  Google Scholar 

  10. Emerson, E.A., Lei, C.L.: Efficient model checking in fragments of the propositional model mu-calculus. In: Logic in Computer Science (LICS), pp. 267–278 (1986)

    Google Scholar 

  11. Jobstmann, B., Griesmayer, A., Bloem, R.: Program repair as a game. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 226–238. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  12. Kulkarni, S.S., Arora, A.: Automating the addition of fault-tolerance. In: Joseph, M. (ed.) FTRTFT 2000. LNCS, vol. 1926, pp. 82–93. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  13. Kulkarni, S.S., Ebnenasir, A.: The complexity of adding failsafe fault-tolerance. In: International Conference on Distributed Computing Systems (ICDCS), pp. 337–344 (2002)

    Google Scholar 

  14. Lamport, L., Shostak, R., Pease, M.: The Byzantine generals problem. ACM Transactions on Programming Languages and Systems (TOPLAS) 4(3), 382–401 (1982)

    Article  MATH  Google Scholar 

  15. Manna, Z., Wolper, P.: Synthesis of communicating processes from temporal logic specifications. ACM Transactions on Programming Languages and Systems (TOPLAS) 6(1), 68–93 (1984)

    Article  MATH  Google Scholar 

  16. Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Principles of Programming Languages (POPL), pp. 179–190 (1989)

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bonakdarpour, B., Kulkarni, S.S. (2008). Revising Distributed UNITY Programs Is NP-Complete. In: Baker, T.P., Bui, A., Tixeuil, S. (eds) Principles of Distributed Systems. OPODIS 2008. Lecture Notes in Computer Science, vol 5401. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-92221-6_26

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-92221-6_26

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-92220-9

  • Online ISBN: 978-3-540-92221-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics