More Web Proxy on the site http://driver.im/

research-article

Toward a verified relational database management system

Authors:

Gregory Malecha,

Greg Morrisett,

Avraham Shinnar,

Ryan WisneskyAuthors Info & Claims

ACM SIGPLAN Notices, Volume 45, Issue 1

Pages 237 - 248

https://doi.org/10.1145/1707801.1706329

Published: 17 January 2010 Publication History

Abstract

We report on our experience implementing a lightweight, fully verified relational database management system (RDBMS). The functional specification of RDBMS behavior, RDBMS implementation, and proof that the implementation meets the specification are all written and verified in Coq. Our contributions include: (1) a complete specification of the relational algebra in Coq; (2) an efficient realization of that model (B+ trees) implemented with the Ynot extension to Coq; and (3) a set of simple query optimizations proven to respect both semantics and run-time cost. In addition to describing the design and implementation of these artifacts, we highlight the challenges we encountered formalizing them, including the choice of representation for finite relations of typed tuples and the challenges of reasoning about data structures with complex sharing. Our experience shows that though many challenges remain, building fully-verified systems software in Coq is within reach.

References

[1]

Serge Abiteboul, Richard Hull, and Victor Vianu. Database Foundations. Addison-Wesley, 1995.

[2]

Yves Bertot and Pierre Castéran. Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer Verlag, 2004.

Digital Library

[3]

R. Bornat, C. Calcagno, and P. OHearn. Local Reasoning, Separation and Aliasing. Proc. SPACE, volume 4, 2004.

[4]

Stephen Brookes. A semantics for concurrent separation logic. Theor. Comput. Sci., 375(1--3):227--270, 2007.

Digital Library

[5]

Adam Chlipala, Gregory Malecha, Greg Morrisett, Avraham Shinnar, and Ryan Wisnesky. Effective interactive proofs for higher-order imperative programs. In Proc. ICFP, 2009.

Digital Library

[6]

C. J. Date. Introduction to Database Systems. Addison-Wesley Longman Publishing Co., Inc., 2002.

Digital Library

[7]

Ramez Elmasri and Shamkant B. Navathe. Fundamentals of Database Systems (5th Edition). Addison Wesley, 2006.

Digital Library

[8]

Parke Godfrey, Jarek Gryz, and Calisto Zuzarte. Exploiting constraint-like data characterizations in query optimization. In Proc. SIGMOD, 2001.

Digital Library

[9]

Carlos Gonzalia. Relations in Dependent Type Theory. PhD Thesis, Chalmers University of Technology, 2006.

[10]

Conor Mcbride. Elimination with a motive. In Proc. TYPES, 2000.

Digital Library

[11]

Conor McBride and James McKinna. The view from the left. J. Functional Programming, 14(1):69--111, 2004.

Digital Library

[12]

James Mckinna and Joel Wright. A type-correct, stack-safe, provably correct expression compiler in epigram. In J. Functional Programming, 2006.

[13]

Aleksandar Nanevski, Paul Govereau, and Greg Morrisett. Towards type-theoretic semantics for transactional concurrency. In Proc. TLDI, 2009.

Digital Library

[14]

Aleksandar Nanevski, Greg Morrisett, and Lars Birkedal. Polymorphism and separation in hoare type theory. In Proc. ICFP, 2006.

Digital Library

[15]

Aleksandar Nanevski, Greg Morrisett, Avraham Shinnar, Paul Govereau, and Lars Birkedal. Ynot: Dependent types for imperative programs. In Proc. ICFP, 2008.

Digital Library

[16]

Ulf Norell. Towards a Practical Programming Language Based on Dependent Type Theory. PhD thesis, Chalmers University of Technology, 2007.

[17]

Peter W. O'Hearn. Resources, concurrency, and local reasoning. Theor. Comput. Sci., 375(1--3):271--307, 2007.

Digital Library

[18]

Peter W. O'Hearn, John C. Reynolds, and Hongseok Yang. Local reasoning about programs that alter data structures. In Proc. CSL, 2001.

Digital Library

[19]

Nicolas Oury and Wouter Swierstra. The power of pi. Proc. ICFP, 2008.

Digital Library

[20]

Sharon E. Perl and Margo Seltzer. Data management for internet-scale single-sign-on. In Proc. WORLDS, 2006.

Digital Library

[21]

P. Rajagopalan and C. P. Tsang. A generic algebra for data collections based on constructive logic. In Algebraic Methodology and Software Technology, volume 936 of LNCS, pages 546--560. Springer Berlin / Heidelberg, 1995.

Digital Library

[22]

John C. Reynolds. Separation logic: A logic for shared mutable data structures. In Proc. LICS, 2002.

Digital Library

[23]

Alan Sexton and Hayo Thielecke. Reasoning about b+ trees with operational semantics and separation logic. Electron. Notes Theor. Comput. Sci., 218:355--369, 2008.

Digital Library

[24]

Alan Sexton and Hayo Thielecke. Reasoning about b+ trees with operational semantics and separation logic. Electron. Notes Theor. Comput. Sci., 218:355--369, 2008.

Digital Library

[25]

Carsten Sinz. System description: Ara - an automatic theorem prover for relation algebras. In Proc. CADE-17, 2000.

Digital Library

[26]

Matthieu Sozeau. Program-ing finger trees in coq. In Proc. ICFP, 2007.

Digital Library

[27]

Matthieu Sozeau and Nicolas Oury. First-class type classes. In Proc. TPHOLs, 2008.

Digital Library

Cited By

Schellhorn GBodenmüller SReif W(2023)Refinement and Separation: Modular Verification of Wandering TreesiFM 202310.1007/978-3-031-47705-8_12(214-234)Online publication date: 6-Nov-2023
https://doi.org/10.1007/978-3-031-47705-8_12
Ricciotti WCheney J(2022)A Formalization of SQL with NullsJournal of Automated Reasoning10.1007/s10817-022-09632-466:4(989-1030)Online publication date: 27-Jul-2022
https://doi.org/10.1007/s10817-022-09632-4
Alam MHalder RPinto J(2021)A deductive reasoning approach for database applications using verification conditionsJournal of Systems and Software10.1016/j.jss.2020.110903175(110903)Online publication date: May-2021
https://doi.org/10.1016/j.jss.2020.110903
Show More Cited By

Index Terms

Recommendations

Toward a verified relational database management system
POPL '10: Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

We report on our experience implementing a lightweight, fully verified relational database management system (RDBMS). The functional specification of RDBMS behavior, RDBMS implementation, and proof that the implementation meets the specification are all ...
Verified heap theorem prover by paramodulation
ICFP '12

We present VeriStar, a verified theorem prover for a decidable subset of separation logic. Together with VeriSmall [3], a proved-sound Smallfoot-style program analysis for C minor, VeriStar demonstrates that fully machine-checked static analyses ...
A relational modal logic for higher-order stateful ADTs
POPL '10: Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

The method of logical relations is a classic technique for proving the equivalence of higher-order programs that implement the same observable behavior but employ different internal data representations. Although it was originally studied for pure, ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 45, Issue 1

POPL '10

January 2010

500 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/1707801

Issue’s Table of Contents

POPL '10: Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
January 2010
520 pages
ISBN:9781605584799
DOI:10.1145/1706299
General Chair:
Manuel Hermenegildo
IMDEA-Software and T.U. of Madrid, Spain
,
Program Chair:
Jens Palsberg
UCLA, University of California, Los Angeles

Copyright © 2010 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 17 January 2010

Published in SIGPLAN Volume 45, Issue 1

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

68
Total Citations
View Citations
947
Total Downloads

Downloads (Last 12 months)62
Downloads (Last 6 weeks)5

Reflects downloads up to 10 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Schellhorn GBodenmüller SReif W(2023)Refinement and Separation: Modular Verification of Wandering TreesiFM 202310.1007/978-3-031-47705-8_12(214-234)Online publication date: 6-Nov-2023
https://doi.org/10.1007/978-3-031-47705-8_12
Ricciotti WCheney J(2022)A Formalization of SQL with NullsJournal of Automated Reasoning10.1007/s10817-022-09632-466:4(989-1030)Online publication date: 27-Jul-2022
https://doi.org/10.1007/s10817-022-09632-4
Alam MHalder RPinto J(2021)A deductive reasoning approach for database applications using verification conditionsJournal of Systems and Software10.1016/j.jss.2020.110903175(110903)Online publication date: May-2021
https://doi.org/10.1016/j.jss.2020.110903
Alam MHalder R(2021)Formal Verification of Database Applications Using Predicate AbstractionSN Computer Science10.1007/s42979-020-00426-22:3Online publication date: 1-May-2021
https://dl.acm.org/doi/10.1007/s42979-020-00426-2
Zieliński BMaślanka P(2017)Relational Transition System in MaudeBeyond Databases, Architectures and Structures. Towards Efficient Solutions for Data Analysis and Knowledge Representation10.1007/978-3-319-58274-0_39(497-511)Online publication date: 27-Apr-2017
https://doi.org/10.1007/978-3-319-58274-0_39
Malecha GBengtson J(2016)Extensible and Efficient Automation Through Reflective TacticsProgramming Languages and Systems10.1007/978-3-662-49498-1_21(532-559)Online publication date: 2016
https://doi.org/10.1007/978-3-662-49498-1_21
Lu ZSteinmuller CMukhopadhyay S(2013)Towards Formal Verification of a Commercial Wireless Router FirmwareProceedings of the 2013 IEEE 37th Annual Computer Software and Applications Conference10.1109/COMPSAC.2013.103(639-647)Online publication date: 22-Jul-2013
https://dl.acm.org/doi/10.1109/COMPSAC.2013.103
Clark JDonaldson AWickerson JRigger M(2024)Validating Database System Isolation Level Implementations with Version Certificate RecoveryProceedings of the Nineteenth European Conference on Computer Systems10.1145/3627703.3650080(754-768)Online publication date: 22-Apr-2024
https://dl.acm.org/doi/10.1145/3627703.3650080
Benzaken VContejean ÉHachmaoui MKeller CMandel LShinnar ASiméon J(2022)Translating canonical SQL to imperative code in CoqProceedings of the ACM on Programming Languages10.1145/35273276:OOPSLA1(1-27)Online publication date: 29-Apr-2022
https://dl.acm.org/doi/10.1145/3527327
Pardalos MHerklotz YWickerson J(2022)Resource Sharing for Verified High-Level Synthesis2022 IEEE 30th Annual International Symposium on Field-Programmable Custom Computing Machines (FCCM)10.1109/FCCM53951.2022.9786208(1-6)Online publication date: 15-May-2022
https://doi.org/10.1109/FCCM53951.2022.9786208
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents