Abstract
In this paper, we concentrate on distributed algorithms for automated synthesis of fault-tolerant programs in the high atomicity model, where all processes can read and write all program variables in one atomic step. Although there has recently been an increasing interest in using parallel and distributed techniques in the model checking community, these technique have not been investigated in program synthesis. Developing such techniques is crucial as a means to cope with the state explosion problem in the context of program synthesis and transformation as well. We propose two distributed multithreaded algorithms for adding two levels of fault-tolerance, namely failsafe and masking, to existing fault-intolerant programs whose state space is distributed over a network or cluster of workstations.
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 to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bonakdarpour, B., Kulkarni, S.S.: Exploiting symbolic techniques in automated synthesis of distributed programs with large state space. In: ICDCS. IEEE International Conference on Distributed Computing Systems, pp. 3–10 (2007)
Bonakdarpour, B., Kulkarni, S.S.: Incremental synthesis of fault-tolerant real-time programs. In: Datta, A.K., Gradinariu, M. (eds.) SSS 2006. LNCS, vol. 4280, pp. 122–136. Springer, Heidelberg (2006)
Bonakdarpour, B., Kulkarni, S.S.: Automated incremental synthesis of timed automata. In: Brim, L., Haverkort, B., Leucker, M., van de Pol, J. (eds.) FMICS 2006. LNCS, vol. 4346, pp. 261–276. Springer, Heidelberg (2007)
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 (2005)
Kulkarni, S.S., Ebnenasir, A.: Automated synthesis of multitolerance. In: DSN. International Conference on Dependable Systems and Networks, pp. 209–219 (2004)
Kulkarni, S.S., Arora, A., Chippada, A.: Polynomial time synthesis of Byzantine agreement. In: SRDS. Symposium on Reliable Distributed Systems, pp. 130–140 (2001)
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)
Emerson, E.A., Clarke, E.M.: Using branching time temporal logic to synthesize synchronization skeletons. Science of Computer Programming 2(3), 241–266 (1982)
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)
Garavel, H., Mateescu, R., Smarandache, I.: Parallel state space construction for model-checking. In: Dwyer, M.B. (ed.) Model Checking Software. LNCS, vol. 2057, pp. 217–234. Springer, Heidelberg (2001)
Stern, U., Dill, D.L.: Parallelizing the murϕ verifier. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 256–278. Springer, Heidelberg (1997)
Heyman, T., Geist, D., Grumberg, O., Schuster, A.: Achieving scalability in parallel reachability analysis of very large circuits. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 20–35. Springer, Heidelberg (2000)
Leucker, M., Somla, R., Weber, M.: Parallel model checking for LTL, CTL*, and L\(_2^{\mu}\). In: PDMC. International Workshop on Parallel and Distributed Model Checking (2003)
Chung, M.-Y., Ciardo, G.: A dynamic firing speculation to speedup distributed symbolic state-space generation. In: IPDPS. International Parallel and Distributed Processing Symposium (2006)
Alpern, B., Schneider, F.B.: Defining liveness. Information Processing Letters 21, 181–185 (1985)
Arora, A., Gouda, M.G.: Closure and convergence: A foundation of fault-tolerant computing. IEEE Transactions on Software Engineering 19(11), 1015–1027 (1993)
Kulkarni, S.S.: Component-based design of fault-tolerance. PhD thesis, Ohio State University (1999)
Mattern, F.: Algorithms for distributed termination detection. Journal of Distributed Computing 2(3), 161–175 (1987)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bonakdarpour, B., Kulkarni, S.S., Abujarad, F. (2007). Distributed Synthesis of Fault-Tolerant Programs in the High Atomicity Model. In: Masuzawa, T., Tixeuil, S. (eds) Stabilization, Safety, and Security of Distributed Systems. SSS 2007. Lecture Notes in Computer Science, vol 4838. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-76627-8_5
Download citation
DOI: https://doi.org/10.1007/978-3-540-76627-8_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-76626-1
Online ISBN: 978-3-540-76627-8
eBook Packages: Computer ScienceComputer Science (R0)