Abstract
Declarative Networking is a recent, viable approach to make distributed programming easier, which is becoming increasingly popular in systems and networking community. It offers the programmer a declarative, rule-based language, called P2, for writing distributed applications in an abstract, yet expressive way. This approach, however, imposes new challenges on analysis and verification methods when they are applied to P2 programs. Reasoning about P2 computations is beyond the scope of existing tools since it requires handling of program states defined in terms of collections of relations, which store the application data, together with multisets of tuples, which represent communication events in-flight. In this paper, we propose a cardinality abstraction technique that can be used to analyze and verify P2 programs. It keeps track of the size of relations (together with projections thereof) and multisets defining P2 states, and provides an appropriate treatment of declarative operations, e.g., indexing, unification, variable binding, and negation. Our cardinality abstraction-based verifier successfully proves critical safety properties of a P2 implementation of the Byzantine fault tolerance protocol Zyzzyva, which is a representative and complex declarative networking application.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Arons, T., Pnueli, A., Ruah, S., Xu, J., Zuck, L.D.: Parameterized verification with automatically computed inductive assertions. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 221. Springer, Heidelberg (2001)
Bagnara, R., Hill, P.M., Zaffanella, E.: The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Science of Computer Programming (2008)
Balaban, I., Pnueli, A., Zuck, L.D.: Invisible safety of distributed protocols. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol. 4052, pp. 528–539. Springer, Heidelberg (2006)
Ball, T., Rajamani, S.K.: The Slam project: Debugging system software via static analysis. In: POPL (2002)
Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker blast. STTT (2007)
Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: PLDI (2003)
Bogudlov, I., Lev-Ami, T., Reps, T.W., Sagiv, M.: Revamping TVLA: Making parametric shape analysis competitive. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 221–225. Springer, Heidelberg (2007)
Braem, C., Charlier, B.L., Modart, S., van Hentenryck, P.: Cardinality analysis of Prolog. In: ILPS (1994)
Bruynooghe, M.: A practical framework for the abstract interpretation of logic programs. J. Log. Program. (1991)
Castro, M., Liskov, B.: Practical Byzantine Fault Tolerance (1999)
Chu, D., Popa, L., Tavakoli, A., Hellerstein, J.M., Levis, P., Shenker, S., Stoica, I.: The design and implementation of a declarative sensor network system. In: SenSys (2007)
Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855. Springer, Heidelberg (2000)
Colón, M., Sankaranarayanan, S., Sipma, H.: Linear invariant generation using non-linear constraint solving. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 420–432. Springer, Heidelberg (2003)
Condie, T., Chu, D., Hellerstein, J.M., Maniatis, P.: Evita raced: metacompilation for declarative networks. In: PVLDB (2008)
Condie, T., Gay, D.E., Loo, B.T., et al.: P2: Declarative networking website (2008), http://p2.cs.berkeley.edu/
Cook, B., Podelski, A., Rybalchenko, A.: Terminator: Beyond safety. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 415–418. Springer, Heidelberg (2006)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, ACM, New York (1977)
Cousot, P., Cousot, R.: Abstract interpretation and application to logic programs. J. Log. Program. (1992)
Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL (1978)
German, S.M., Sistla, A.P.: Reasoning about systems with many processes. J. ACM (1992)
Gobert, F.: Towards Putting Abstract Interpretation of Prolog Into Practice. Ph.D thesis, Université catholique de Louvain (2007)
Graf, S., Saïdi, H.: Construction of abstract state graphs with pvs. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254. Springer, Heidelberg (1997)
Gulwani, S., Lev-Ami, T., Sagiv, M.: A combination framework for tracking partition sizes. In: POPL (2009)
Hermenegildo, M.V., Puebla, G., Bueno, F., López-García, P.: Program development using abstract interpretation (and the Ciao system preprocessor). In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 127–152. Springer, Heidelberg (2003)
Killian, C., Anderson, J.W., Braud, R., Jhala, R., Vahadat, A.: Mace: Language support for building distributed systems. In: PLDI (2007)
Killian, C.E., Anderson, J.W., Jhala, R., Vahdat, A.: Life, death, and the critical transition: Finding liveness bugs in systems code. In: NSDI (2007)
Lalire, G., Argoud, M., Jeannet, B.: The interproc analyzer, http://pop-art.inrialpes.fr/people/bjeannet/bjeannet-forge/interproc/index.html
Lamport, L.: The Part-Time Parliament. ACM Transactions on Computer Systems (1998)
Loo, B.T., Condie, T., Garofalakis, M., Gay, D.E., Hellerstein, J.M., Maniatis, P., Ramakrishnan, R., Roscoe, T., Stoica, I.: Declarative networking: Language, execution and optimization. In: SIGMOD (2006)
Loo, B.T., Condie, T., Hellerstein, J.M., Maniatis, P., Roscoe, T., Stoica, I.: Implementing declarative overlays. In: SIGOPS (2005)
Miné, A.: The octagon abstract domain. Higher-Order and Symb. Comp. (2006)
Musuvathi, M., Engler, D.R.: Model checking large network protocol implementations. In: NSDI (2004)
Musuvathi, M., Park, D.Y.W., Chou, A., Engler, D.R., Dill, D.L.: CMC: A pragmatic approach to model checking real code. In: OSDI (2002)
Navarro, J.A., Rybalchenko, A.: Operational semantics for declarative networking. In: PADL (2009)
Pnueli, A., Ruah, S., Zuck, L.D.: Automatic deductive verification with invisible invariants. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, p. 82. Springer, Heidelberg (2001)
Pnueli, A., Xu, J., Zuck, L.D.: Liveness with (0, 1, infty)-counter abstraction. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 107. Springer, Heidelberg (2002)
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS (2002)
Sagiv, S., Reps, T.W., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst. (2002)
Singh, A., Das, T., Maniatis, P., Druschel, P., Roscoe, T.: BFT protocols under fire. In: NSDI (2008)
Singh, A., Maniatis, P., Roscoe, T., Druschel, P.: Using queries for distributed monitoring and forensics. In: EuroSys, Leuven, Belgium (2006)
Wang, A., Basu, P., Loo, B.T., Sokolsky, O.: Declarative networking verification. In: PADL (2009)
Wood, T., Singh, R., Venkataramani, A., Shenoy, P.: ZZ: Cheap Practical BFT Using Virtualization. Technical Report TR14-08, University of Massachusetts (2008)
Yang, H., Lee, O., Berdine, J., Calcagno, C., Cook, B., Distefano, D., O’Hearn, P.W.: Scalable shape analysis for systems code. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 385–398. Springer, Heidelberg (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pérez, J.A.N., Rybalchenko, A., Singh, A. (2009). Cardinality Abstraction for Declarative Networking Applications. In: Bouajjani, A., Maler, O. (eds) Computer Aided Verification. CAV 2009. Lecture Notes in Computer Science, vol 5643. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02658-4_43
Download citation
DOI: https://doi.org/10.1007/978-3-642-02658-4_43
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02657-7
Online ISBN: 978-3-642-02658-4
eBook Packages: Computer ScienceComputer Science (R0)