Abstract
We consider the problem of specifying 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; a novel fuse operation on relational indexes specifies where the underlying physical data structure representation has sharing. We permit the user to specify different concrete shared representations for relations, and show that the semantics of the relational specification are preserved.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Beeri, C., Fagin, R., Howard, J.H.: A complete axiomatization for functional and multivalued dependencies in database relations. In: SIGMOD, pp. 47–61. ACM, New York (1977)
Berdine, J., Calcagno, C., Cook, B., Distefano, D., O’Hearn, P., Wies, T., Yang, H.: Shape analysis for composite data structures. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 178–192. Springer, Heidelberg (2007)
Bierman, G., Wren, A.: First-class relationships in an object-oriented language. In: Black, A.P. (ed.) ECOOP 2005. LNCS, vol. 3586, pp. 262–286. Springer, Heidelberg (2005)
Cai, J., Paige, R.: Look ma, no hashing, and no arrays neither. In: POPL, pp. 143–154 (1991)
Chlipala, A.J., Malecha, J.G., Morrisett, G., Shinnar, A., Wisnesky, R.: Effective interactive proofs for higher-order imperative programs. In: ICFP, pp. 79–90 (2009)
Codd, E.F.: A relational model of data for large shared data banks. Commun. ACM 13(6), 377–387 (1970)
Dewar, R.B.K., Grand, A., Liu, S.-C., Schwartz, J.T., Schonberg, E.: Programming by refinement, as exemplified by the SETL representation sublanguage. ACM Trans. Program. Lang. Syst. 1(1), 27–49 (1979)
Distefano, D., Parkinson, M.J.: jStar: towards practical verification for Java. In: OOPSLA, pp. 213–226 (2008)
Fahndrich, M., Leino, R.: Heap monotonic typestates. In: Int. Work. on Alias Confinement and Ownership (July 2003)
Hawkins, P., Aiken, A., Fisher, K., Rinard, M., Sagiv, M.: Data structure fusion, full (2010), http://theory.stanford.edu/~hawkinsp/papers/rel-full.pdf
Klarlund, N., Schwartzbach, M.I.: Graph types. In: POPL, Charleston, South Carolina, pp. 196–205. ACM, New York (1993)
Kreiker, J., Seidl, H., Vojdani, V.: Shape analysis of low-level C with overlapping structures. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol. 5944, pp. 214–230. Springer, Heidelberg (2010)
Kuncak, V., Lam, P., Rinard, M.: Role analysis. In: POPL, pp. 17–32 (2002)
Lam, P., Kuncak, V., Rinard, M.C.: Generalized typestate checking for data structure consistency. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 430–447. Springer, Heidelberg (2005)
Meijer, E., Beckman, B., Bierman, G.: LINQ: Reconciling objects, relations and XML in the .NET framework. In: SIGMOD, p. 706. ACM, New York (2006)
Olston, C., et al.: Pig Latin: A not-so-foreign language for data processing. In: SIGMOD (June 2008)
Paige, R., Henglein, F.: Mechanical translation of set theoretic problem specifications into efficient RAM code. J. Sym. Com. 4(2), 207–232 (1987)
J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In LICS (2002) (invited paper)
Rothamel, T., Liu, Y.A.: Efficient implementation of tuple pattern based retrieval. In: PEPM, pp. 81–90. ACM, New York (2007)
Schonberg, E., Schwartz, J.T., Sharir, M.: Automatic data structure selection in SETL. In: POPL, pp. 197–210 (1979)
Shacham, O., Vechev, M., Yahav, E.: Chameleon: adaptive selection of collections. In: PLDI, pp. 408–418 (2009)
Zee, K., Kuncak, V., Rinard, M.C.: Full functional verification of linked data structures. In: PLDI, pp. 349–361 (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hawkins, P., Aiken, A., Fisher, K., Rinard, M., Sagiv, M. (2010). Data Structure Fusion. In: Ueda, K. (eds) Programming Languages and Systems. APLAS 2010. Lecture Notes in Computer Science, vol 6461. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-17164-2_15
Download citation
DOI: https://doi.org/10.1007/978-3-642-17164-2_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-17163-5
Online ISBN: 978-3-642-17164-2
eBook Packages: Computer ScienceComputer Science (R0)