Hostname: page-component-74656f9884-j7cmm Total loading time: 0 Render date: 2026-11-11T03:01:02.121Z Has data issue: false hasContentIssue false
  • English
  • Français

Certified Graph View Maintenance with Regular Datalog

Published online by Cambridge University Press:  10 August 2018

ANGELA BONIFATI ,
STEFANIA DUMBRAVA Open the ORCID record for STEFANIA DUMBRAVA [Opens in a new window]  and
EMILIO JESÚS GALLEGO ARIAS
ANGELA BONIFATI
Affiliation:
LIRIS, Université Lyon 1, France
STEFANIA DUMBRAVA
Affiliation:
LIRIS, Université Lyon 1, France
EMILIO JESÚS GALLEGO ARIAS
Affiliation:
MINES ParisTech, PSL Research University, France
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

We employ the Coq proof assistant to develop a mechanically-certified framework for evaluating graph queries and incrementally maintaining materialized graph instances, also called views. The language we use for defining queries and views is Regular Datalog (RD) – a notable fragment of non-recursive Datalog that can express complex navigational queries, with transitive closure as native operator. We first design and encode the theory of RD and then mechanize a RD-specific evaluation algorithm capable of fine-grained, incremental graph view computation, which we prove sound with respect to the declarative RD semantics. By using the Coq extraction mechanism, we test an OCaml version of the verified engine on a set of preliminary benchmarks. Our development is particularly focused on leveraging existing verification and notational techniques to: a) define mechanized properties that can be easily understood by logicians and database researchers and b) attain formal verification with limited effort. Our work is the first step towards a unified, machine-verified, formal framework for dynamic graph query languages and their evaluation engines.

Keywords

Regular DatalogGraph QueriesGraph ViewsIncremental MaintenanceFinite SemanticsTheorem Proving

Information

Type
Original Article
Information
Theory and Practice of Logic Programming , Volume 18 , Special Issue 3-4: 34th International Conference on Logic Programming , July 2018 , pp. 372 - 389
Copyright
Copyright © Cambridge University Press 2018 

References

Abiteboul, S., Hull, R. and Vianu, V., Eds. 1995. Foundations of Databases: The Logical Level, 1st ed. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA.Google Scholar
Aluç, G., Hartig, O., Özsu, M. T., and Daudjee, K. 2014. Diversified stress testing of RDF data management systems. In The Semantic Web (ISWC 2014), Mika, P., Tudorache, T., Bernstein, A., Welty, C., Knoblock, C., Vrandečić, D., Groth, P., Noy, N., Janowicz, K., and Goble, C., Eds. LNCS, vol. 8796. Springer International Publishing, Cham, 197–212.Google Scholar
Alviano, M., Calimeri, F., Dodaro, C., Fuscà, D., Leone, N., Perri, S., Ricca, F., Veltri, P., and Zangari, J. 2017. The ASP system DLV2. In Logic Programming and Nonmonotonic Reasoning LPNMR 2017. 215–221.Google Scholar
Anand, A., Appel, A. W., Morrisett, G., Paraskevopoulou, Z., Pollack, R., Bélanger, O. S., Sozeau, M., and Weaver, M. 2017. Certicoq: A verified compiler for Coq. In CoqPL 2017: The 3rd International Workshop on Coq for Programming Languages.Google Scholar
Angles, R., Arenas, M., Barceló, P., Hogan, A., Reutter, J. L., and Vrgoc, D. 2017. Foundations of modern query languages for graph databases. In ACM Comput. Surv. Vol. 50. 68:1–68:40.Google Scholar
Aref, M., tenCate, B. Cate, B., Green, T. J., Kimelfeld, B., Olteanu, D., Pasalic, E., Veldhuizen, T. L., and Washburn, G. 2015. Design and implementation of the LogicBlox system. In Proceedings of ACM SIGMOD. 1371–1382.Google Scholar
Auerbach, J. S., Hirzel, M., Mandel, L., Shinnar, A. and Siméon, J. 2017. Handling environments in a nested relational algebra with combinators and an implementation in a verified query compiler. In Proceedings of the 2017 ACM International Conference on Management of Data. SIGMOD '17. ACM, New York, NY, USA, 1555–1569.Google Scholar
Bagan, G., Bonifati, A., Ciucanu, R., Fletcher, G. H. L., Lemay, A., and Advokaat, N. 2017. gMark: Schema-driven generation of graphs and queries. IEEE Transactions on Knowledge and Data Engineering 29, 4 (April), 856–869.Google Scholar
Benzaken, V., Contejean, E., and Dumbrava, S. 2014. A Coq formalization of the relational data model. In Proceedings of the 23rd European Symposium on Programming Languages and Systems - Volume 8410. Springer-Verlag New York, Inc., New York, NY, USA, 189–208.Google Scholar
Benzaken, V., Contejean, E., and Dumbrava, S. 2017. Certifying standard and stratified Datalog inference engines in SSReflect. In Interactive Theorem Proving. LNCS, vol. 10499. Springer International Publishing, 171–188.Google Scholar
Beyhl, T. and Giese, H. 2016. Incremental view maintenance for deductive graph databases using generalized discrimination networks. In GaM@ETAPS. EPTCS, vol. 231. 57–71.Google Scholar
Cai, Y., Giarrusso, P. G., Rendel, T., and Ostermann, K. 2014. A theory of changes for higher-order languages: Incrementalizing λ-calculi by static differentiation. In Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI '14. ACM, New York, NY, USA, 145–155.Google Scholar
Cayley. https://github.com/cayleygraph/cayley (visited: 2018-02).Google Scholar
Ceri, S., Gottlob, G., and Tanca, L. 1989. What you always wanted to know about Datalog (and never dared to ask). IEEE Transactions on Knowledge and Data Engineering 1, 1, 146–166.Google Scholar
Chu, S., Weitz, K., Cheung, A., and Suciu, D. 2017. HoTTSQL: Proving query rewrites with univalent SQL semantics. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI 2017. ACM, New York, NY, USA, 510–524.Google Scholar
Clark, K. L. 1977. Negation as failure. In Logic and Data Bases, Gallaire and Minker, Eds. Plenum Press, 293–322.Google Scholar
Cohen, C. and Théry, L. 2017. Full script of Tarjan SCC Coq/SSreflect proof. Tech. rep., INRIA. https://github.com/CohenCyril/tarjan (visited: 2018-02).Google Scholar
Cypher. https://www.opencypher.org/ (visited: 2018-02).Google Scholar
Erling, O., Averbuch, A., Larriba-Pey, J., Chafi, H., Gubichev, A., Prat, A., Pham, M.-D., and Boncz, P. 2015. The LDBC social network benchmark: Interactive workload. In Proceedings of the 2015 ACM SIGMOD International Conference on Management of Data. SIGMOD '15. ACM, New York, NY, USA, 619–630.Google Scholar
Fan, W., Hu, C., and Tian, C. 2017. Incremental graph computations: Doable and undoable. In Proceedings of the 2017 ACM International Conference on Management of Data. SIGMOD '17. ACM, New York, NY, USA, 155–169.Google Scholar
FlockDB. https://github.com/twitter-archive/flockdb (visited: 2018-02).Google Scholar
G-Core. https://github.com/ldbc/ldbc_gcore_parser (visited: 2018-02).Google Scholar
Giraph. http://giraph.apache.org/ (visited: 2018-02).Google Scholar
Gonthier, G., Asperti, A., Avigad, J., Bertot, Y., Cohen, C., Garillot, F., Roux, S. L., Mahboubi, A., O'Connor, R., Biha, S. O., Pasca, I., Rideau, L., Solovyev, A., Tassi, E., and Théry, L. 2013. A machine-checked proof of the odd order theorem. In Interactive Theorem Proving. LNCS. Springer Berlin Heidelberg, Berlin, Heidelberg, 163–179.Google Scholar
GraphQL. http://graphql.org/ (visited: 2018-02).Google Scholar
Greenlaw, R., Hoover, H. J., and Ruzzo, W. L. 1995. Limits to Parallel Computation: P-completeness Theory. Oxford University Press, Inc., New York, NY, USA.Google Scholar
Gremlin. http://tinkerpop.apache.org/ (visited: 2018-02).Google Scholar
Gupta, A., Mumick, I. S., and Subrahmanian, V. S. 1993. Maintaining views incrementally. SIGMOD Rec. 22, 2, 157–166.Google Scholar
Jagadish, H. V., Agrawal, R., and Ness, L. 1987. A study of transitive closure as a recursion mechanism. SIGMOD Rec. 16, 3, 331–344.Google Scholar
Leroy, X. 2009. Formal verification of a realistic compiler. Commun. ACM 52, 7, 107–115.Google Scholar
Letouzey, P. 2008. Extraction in Coq: An overview. In Proceedings of the 4th Conference on Computability in Europe: Logic and Theory of Algorithms. CiE '08. Springer-Verlag, Berlin, Heidelberg, 359–369.Google Scholar
Mullen, E., Pernsteiner, S., Wilcox, J. R., Tatlock, Z., and Grossman, D. 2018. Œuf: Minimizing the Coq extraction TCB. In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs. CPP 2018. ACM, New York, NY, USA, 172–185.Google Scholar
Neo4j. https://neo4j.com/ (visited: 2018-02).Google Scholar
Oracle PGX. http://www.oracle.com/technetwork/oracle-labs/parallel-graph- analytix (visited: 2018-02).Google Scholar
Ramalingam, G. and Reps, T. W. 1996. On the computational complexity of dynamic graph problems. Theoretical Computer Science 158, 1&2, 233–277.Google Scholar
Reutter, J. L., Romero, M., and Vardi, M. Y. 2017. Regular queries on graph databases. Theory of Computing Systems 61, 1, 31–83.Google Scholar
SPARQL. https://www.w3.org/TR/sparql11-query/ (visited: 2018-02).Google Scholar
The Coq Development Team. 2018. The Coq proof assistant, version 8.7.2.Google Scholar