Peter Hawkins
Alex Aiken
Kathleen Fisher
Martin Rinard
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.
- 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. doi: 10.1109/SC.2000.10033. Google Scholar
Digital Library
- 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. doi: 10.1007/ 978-3-540-73368-3 22. Google ScholarDigital Library
- 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. doi: 10.1007/1153114212. Google ScholarDigital Library
- Boost. Boost C++ libraries, 2010. URL http://www.boost.org/.Google Scholar
- 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. doi: 10.1145/99583.99605. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. doi: 10.1145/1596550.1596565. Google ScholarDigital Library
- Donald Cohen and Neil Campbell. Automating relational operations on data structures. IEEE Software, 10(3):53--60, May 1993. ISSN 0740-7459. doi: 10.1109/52.210604. Google ScholarDigital Library
- 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. doi: 10.1145/357062.357064. Google ScholarDigital Library
- 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. doi: 10.1145/1449764.1449782. Google ScholarDigital Library
- Manuel Fähndrich and K. Rustan M. Leino. Heap monotonic typestates. In International Workshop on Alias Confinement and Ownership, July 2003.Google Scholar
- 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. doi: 10.1007/978-3-642-17164-2 15. Google ScholarDigital Library
- 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.Google Scholar
- Nils Klarlund and Michael I. Schwartzbach. Graph types. In POPL, pages 196--205, New York, NY, USA, 1993. ACM. ISBN 0-89791-560-7. doi: 10.1145/158511.158628. Google ScholarDigital Library
- 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. doi: 10.1007/BFb0002751. Google ScholarDigital Library
- 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. doi: 10.1007/978-3-642-11319-2 17. Google ScholarDigital Library
- 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. doi: 10.1109/TSE.2006.125. Google ScholarDigital Library
- 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. doi: 10.1145/503272.503276. Google ScholarDigital Library
- 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. doi: 10.1007/978-3-540-30579-8 28. Google ScholarDigital Library
- Oukseh Lee, Hongseok Yang, and Rasmus Petersen. Program analysis for overlaid data structures. In CAV, LNCS, 2011. To appear. Google ScholarDigital Library
- 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. doi: 10.1007/978-3-642-15769-1 6. Google ScholarDigital Library
- 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. doi: 10.1145/1142473.1142552. Google ScholarDigital Library
- 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. doi: 10.1145/1376616.1376726. Google ScholarDigital Library
- 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. doi: 10.1016/S0747-7171(87)80066-4. Google ScholarDigital Library
- John C. Reynolds. Separation logic: A logic for shared mutable data structures. In LICS, pages 55--74, 2002. doi: 10.1109/LICS.2002.1029817. Invited paper. Google ScholarDigital Library
- 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. doi: 10.1145/1244381.1244394. Google ScholarDigital Library
- 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. doi: 10.1145/567752.567771. Google ScholarDigital Library
- 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. doi: 10.1145/1542476.1542522. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. doi: 10.1007/978-3-540-73589-2 4. Google ScholarDigital Library
- 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. doi: 10.1145/1375581.1375624. Google ScholarDigital Library
- 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. doi: 10.1145/1542476.1542514. Google ScholarDigital Library
Index Terms
- Data representation synthesis
Recommendations
Concurrent data representation synthesis
PLDI '12: Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and ImplementationWe 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 ...
An introduction to data representation synthesis
We consider the problem of specifying combinations of data structures with complex sharing in a manner that is declarative and results in provably correct code. In our approach, abstract data types are specified using relational algebra and functional ...
Data representation synthesis
PLDI '11We 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 ...
Comments