Data representation synthesis
Abstract/Contents
- Abstract
- This dissertation introduces Data Representation Synthesis, a technique for 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 a programmer to specify different concrete representations for relations, and show that operations on concrete representations soundly implement their relational specification. Decompositions also give new insight into the problem of writing safe and efficient concurrent code. We introduce lock placements, which describe, for each heap location, which lock guards the location, and under what circumstances. By incorporating lock placements into decompositions, a compiler can automatically explore the space of possible legal data representations and locking strategies, while simultaneously guaranteeing correctness, serializability of relational operations, and deadlock-freedom. 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. We describe our experience with a prototype compiler; code generated by our system can easily be dropped into existing systems in place of complex hand-written implementations with comparable performance.
Description
| Type of resource | text |
|---|---|
| Form | electronic; electronic resource; remote |
| Extent | 1 online resource. |
| Publication date | 2012 |
| Issuance | monographic |
| Language | English |
Creators/Contributors
| Associated with | Hawkins, Peter James |
|---|---|
| Associated with | Stanford University, Computer Science Department |
| Primary advisor | Aiken, Alexander |
| Thesis advisor | Aiken, Alexander |
| Thesis advisor | Dill, David L |
| Thesis advisor | Fisher, Kathleen |
| Advisor | Dill, David L |
| Advisor | Fisher, Kathleen |
Subjects
| Genre | Theses |
|---|
Bibliographic information
| Statement of responsibility | Peter Hawkins. |
|---|---|
| Note | Submitted to the Department of Computer Science. |
| Thesis | Thesis (Ph.D.)--Stanford University, 2012. |
| Location | electronic resource |
Access conditions
- Copyright
- © 2012 by Peter James Hawkins
- License
- This work is licensed under a Creative Commons Attribution Non Commercial 3.0 Unported license (CC BY-NC).
Also listed in
Loading usage metrics...