research-article

Data representation synthesis

Authors:

Kathleen Fisher,

Mooly SagivAuthors Info & Claims

ACM SIGPLAN Notices, Volume 46, Issue 6

Pages 38 - 49

https://doi.org/10.1145/1993316.1993504

Published: 04 June 2011 Publication History

Abstract

We consider the problem of specifying combinations of data structures with complex sharing in a manner that is both declarative and results in provably correct code. In our approach, abstract data types are specified using relational algebra and functional dependencies. We describe a language of decompositions that permit the user to specify different concrete representations for relations, and show that operations on concrete representations soundly implement their relational specification. It is easy to incorporate data representations synthesized by our compiler into existing systems, leading to code that is simpler, correct by construction, and comparable in performance to the code it replaces.

References

[1]

Nawaaz Ahmed, Nikolay Mateev, Keshav Pingali, and Paul Stodghill. A framework for sparse matrix code synthesis from high-level specifications. In Supercomputing, page 58. IEEE Computer Society, November 2000.

Digital Library

[2]

Josh Berdine, Cristiano Calgano, Byron Cook, Dino Distefano, Peter W. O'Hearn, Thomas Wies, and Hongseok Yang. Shape analysis for composite data structures. In CAV, volume 4590 of LNCS, pages 178--192. Springer Berlin / Heidelberg, 2007. 978-3-540-73368-3 22.

Digital Library

[3]

Gavin Bierman and Alisdair Wren. First-class relationships in an object-oriented language. In ECOOP, volume 3586 of LNCS, pages 262--286. Springer Berlin / Heidelberg, 2005.

[4]

Boost. Boost C++ libraries, 2010. URL http://www.boost.org/.

[5]

Jiazhen Cai and Robert A. Paige. "Look ma, no hashing, and no arrays neither". In POPL, pages 143--154, New York, NY, USA, 1991. ACM. ISBN 0-89791-419-8.

Digital Library

[6]

Surajit Chaudhuri and Vivek R. Narasayya. An efficient cost-driven index selection tool for Microsoft SQL Server. In VLDB, pages 146--155, San Francisco, CA, USA, 1997. Morgan Kaufmann Publishers. ISBN 1-55860-470-7.

Digital Library

[7]

Adam Chlipala, Gregory Malecha, Greg Morrisett, Avraham Shinnar, and Ryan Wisnesky. Effective interactive proofs for higher-order imperative programs. In ICFP, pages 79--90, New York, NY, USA, 2009. ACM. ISBN 978-1-60558-332-7.

Digital Library

[8]

Donald Cohen and Neil Campbell. Automating relational operations on data structures. IEEE Software, 10(3):53--60, May 1993. ISSN 0740-7459.

Digital Library

[9]

Robert B. K. Dewar, Arthur Grand, Ssu-Cheng Liu, Jacob T. Schwartz, and Edmond Schonberg. Programming by refinement, as exemplified by the SETL representation sublanguage. ACM Trans. Program. Lang. Syst., 1(1):27--49, January 1979. ISSN 0164-0925.

Digital Library

[10]

Dino Distefano and Matthew J. Parkinson. jStar: towards practical verification for Java. In OOPSLA, pages 213--226, New York, NY, USA, 2008. ACM. ISBN 978-1-60558-215-3.

Digital Library

[11]

Manuel Fähndrich and K. Rustan M. Leino. Heap monotonic typestates. In International Workshop on Alias Confinement and Ownership, July 2003.

[12]

Peter Hawkins, Alex Aiken, Kathleen Fisher, Martin Rinard, and Mooly Sagiv. Data structure fusion. In APLAS, volume 6461 of LNCS, pages 204--221. Springer Berlin / Heidelberg, 2010. 15.

Digital Library

[13]

Uri Juhasz, Noam Rinetzk, Arnd Poetzsch-Heffter, Mooly Sagiv, and Eran Yahav. Modular verification with shared abstractions. In International Workshop on Foundations of Object-Oriented Languages (FOOL), 2009.

[14]

Nils Klarlund and Michael I. Schwartzbach. Graph types. In POPL, pages 196--205, New York, NY, USA, 1993. ACM. ISBN 0-89791-560-7.

Digital Library

[15]

Vladimir Kotlyar, Keshav Pingali, and Paul Stodghill. A relational approach to the compilation of sparse matrix programs. In Euro-Par'97 Parallel Processing, volume 1300 of LNCS, pages 318--327. Springer Berlin / Heidelberg, 1997.

Digital Library

[16]

Jörg Kreiker, Helmut Seidl, and Vesal Vojdani. Shape analysis of low-level C with overlapping structures. In VMCAI, volume 5044 of LNCS, pages 214--230. Springer Berlin / Heidelberg, 2010. 17.

[17]

Victor Kuncak, Patrick Lam, Karen Zee, and Martin Rinard. Modular pluggable analyses for data structure consistency. IEEE Transactions on Software Engineering, 32(12):988--1005, 2006. ISSN 0098-5589.

Digital Library

[18]

Viktor Kuncak, Patrick Lam, and Martin Rinard. Role analysis. In POPL, pages 17--32, New York, NY, USA, 2002. ACM. ISBN 1-58113-450-9.

Digital Library

[19]

Patrick Lam, Viktor Kuncak, and Martin Rinard. Generalized typestate checking for data structure consistency. In VMCAI, volume 3385 of LNCS, pages 430--447. Springer Berlin / Heidelberg, 2005. 28.

[20]

Oukseh Lee, Hongseok Yang, and Rasmus Petersen. Program analysis for overlaid data structures. In CAV, LNCS, 2011. To appear.

Digital Library

[21]

Bill McCloskey, Thomas Reps, and Mooly Sagiv. Statically inferring complex heap, array, and numeric invariants. In Static Analysis, volume 6337 of LNCS, pages 71--99. Springer Berlin / Heidelberg, 2011. 6.

[22]

Eric Meijer, Brian Beckman, and Gavin Bierman. LINQ: Reconciling objects, relations and XML in the .NET framework. In SIGMOD, pages 706--706, New York, NY, USA, 2006. ACM. ISBN 1-59593-434-0.

Digital Library

[23]

Christopher Olston, Benjamin Reed, Utkarsh Srivastava, Ravi Kumar, and Andrew Tomkins. Pig Latin: a not-so-foreign language for data processing. In SIGMOD, pages 1099--1110, New York, NY, USA, 2008. ACM. ISBN 978-1-60558-102-6.

Digital Library

[24]

Robert Paige and Fritz Henglein. Mechanical translation of set theoretic problem specifications into efficient RAM code --- a case study. Journal of Symbolic Computation, 4(2):207--232, 1987. ISSN 0747-7171.

Digital Library

[25]

John C. Reynolds. Separation logic: A logic for shared mutable data structures. In LICS, pages 55--74, 2002. Invited paper.

Digital Library

[26]

Tom Rothamel and Yanhong A. Liu. Efficient implementation of tuple pattern based retrieval. In PEPM, pages 81--90, New York, NY, USA, 2007. ACM. ISBN 978-1-59593-620-2.

Digital Library

[27]

Edmond Schonberg, Jacob T. Schwartz, and Micha Sharir. Automatic data structure selection in SETL. In POPL, pages 197--210, New York, NY, USA, 1979. ACM.

Digital Library

[28]

Ohad Shacham, Martin Vechev, and Eran Yahav. Chameleon: adaptive selection of collections. In PLDI, pages 408--418, New York, NY, USA, 2009. ACM. ISBN 978-1-60558-392-1.

Digital Library

[29]

Yannis Smaragdakis and Don Batory. DiSTiL: a transformation library for data structures. In Conference on Domain-Specific Languages (DSL '97), pages 257--271. USENIX, October 1997.

Digital Library

[30]

Mandana Vaziri, Frank Tip, Stephen Fink, and Julian Dolby. Declarative object identity using relation types. In ECOOP, volume 4609 of LNCS, pages 54--78. Springer Berlin / Heidelberg, 2007. 4.

Digital Library

[31]

Karen Zee, Viktor Kuncak, and Martin Rinard. Full functional verification of linked data structures. In PLDI, pages 349--361, NewYork, NY, USA, 2008. ACM. ISBN 978-1-59593-860-2.

Digital Library

[32]

Karen Zee, Viktor Kuncak, and Martin Rinard. An integrated proof language for imperative programs. In PLDI, pages 338--351, New York, NY, USA, 2009. ACM. ISBN 978-1-60558-392-1.

Digital Library

Cited By

Ouared AAmrani MSchobbens P(2022)COMORP: Rapid prototyping for mathematical database cost models developmentJournal of Computer Languages10.1016/j.cola.2022.10117373(101173)Online publication date: Dec-2022
https://doi.org/10.1016/j.cola.2022.101173
Patil MHoushmand FLesani MSen KNaik M(2020)Learning quantitative representation synthesisProceedings of the 4th ACM SIGPLAN International Workshop on Machine Learning and Programming Languages10.1145/3394450.3397467(29-37)Online publication date: 15-Jun-2020
https://dl.acm.org/doi/10.1145/3394450.3397467
Kang ELafortune STripakis S(2019)Automated Synthesis of Secure Platform MappingsComputer Aided Verification10.1007/978-3-030-25540-4_12(219-237)Online publication date: 12-Jul-2019
https://doi.org/10.1007/978-3-030-25540-4_12
Show More Cited By

Index Terms

Data representation synthesis
1. Information systems
  1. Information storage systems
    1. Record storage systems
      1. Record storage alternatives
2. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
        Abstract data types

Recommendations

Concurrent data representation synthesis
PLDI '12

We describe an approach for synthesizing data representations for concurrent programs. Our compiler takes as input a program written using concurrent relations and synthesizes a representation of the relations as sets of cooperating data structures as ...
Data representation synthesis
PLDI '11: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation

We consider the problem of specifying combinations of data structures with complex sharing in a manner that is both declarative and results in provably correct code. In our approach, abstract data types are specified using relational algebra and ...
Synthesis of AMBA AHB from formal specification: a case study

The standard hardware design flow involves: (a) design of an integrated circuit using a hardware description language, (b) extensive functional and formal verification, and (c) logical synthesis. However, the above-mentioned processes consume ...

Comments

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 46, Issue 6

PLDI '11

June 2011

652 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/1993316

Issue’s Table of Contents

PLDI '11: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation
June 2011
668 pages
ISBN:9781450306638
DOI:10.1145/1993498
General Chair:
Mary Hall
University of Utah
,
Program Chair:
David Padua
University of Illinois at Urbana-Champaign

Copyright © 2011 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: 04 June 2011

Published in SIGPLAN Volume 46, Issue 6

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

74
Total Citations
View Citations
1,091
Total Downloads

Downloads (Last 12 months)53
Downloads (Last 6 weeks)6

Reflects downloads up to 03 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Ouared AAmrani MSchobbens P(2022)COMORP: Rapid prototyping for mathematical database cost models developmentJournal of Computer Languages10.1016/j.cola.2022.10117373(101173)Online publication date: Dec-2022
https://doi.org/10.1016/j.cola.2022.101173
Patil MHoushmand FLesani MSen KNaik M(2020)Learning quantitative representation synthesisProceedings of the 4th ACM SIGPLAN International Workshop on Machine Learning and Programming Languages10.1145/3394450.3397467(29-37)Online publication date: 15-Jun-2020
https://dl.acm.org/doi/10.1145/3394450.3397467
Kang ELafortune STripakis S(2019)Automated Synthesis of Secure Platform MappingsComputer Aided Verification10.1007/978-3-030-25540-4_12(219-237)Online publication date: 12-Jul-2019
https://doi.org/10.1007/978-3-030-25540-4_12
Németh BKelemen Z(2018)Derivable partial locking for algebraic data typesActa Cybernetica10.14232/actacyb.22.1.2015.1022:1(151-169)Online publication date: 20-Dec-2018
https://dl.acm.org/doi/10.14232/actacyb.22.1.2015.10
Loncaric CZimmermann TCleland-Huang JSu Z(2016)Data structure synthesisProceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering10.1145/2950290.2983946(1073-1075)Online publication date: 1-Nov-2016
https://dl.acm.org/doi/10.1145/2950290.2983946
Bernstein GShah CLemire CDevito ZFisher MLevis PHanrahan P(2016)EbbACM Transactions on Graphics10.1145/289263235:2(1-12)Online publication date: 2-May-2016
https://dl.acm.org/doi/10.1145/2892632
Milicevic AEfrati IJackson D(2014)αRby--An Embedding of Alloy in RubyProceedings of the 4th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z - Volume 847710.1007/978-3-662-43652-3_5(56-71)Online publication date: 2-Jun-2014
https://dl.acm.org/doi/10.1007/978-3-662-43652-3_5
Xu G(2013)CoCoProceedings of the 27th European conference on Object-Oriented Programming10.1007/978-3-642-39038-8_1(1-26)Online publication date: 1-Jul-2013
https://dl.acm.org/doi/10.1007/978-3-642-39038-8_1
Enea CSaveluc VSighireanu M(2013)Compositional invariant checking for overlaid and nested linked listsProceedings of the 22nd European conference on Programming Languages and Systems10.1007/978-3-642-37036-6_9(129-148)Online publication date: 16-Mar-2013
https://dl.acm.org/doi/10.1007/978-3-642-37036-6_9
Pailoor SWang YDillig I(2024)Semantic Code Refactoring for Abstract Data TypesProceedings of the ACM on Programming Languages10.1145/36328708:POPL(816-847)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632870
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.

Figures

Tables

Media

View Issue’s Table of Contents