Refined Ownership: Fine-grained controlled internal sharing
2015 (English)In: Formal Methods for Multicore Programming, 2015, Vol. 9104, 179-210 p.Conference paper (Refereed)
Ownership type systems give a strong notion of separation between aggregates. Objects belonging to different owners cannot be aliased, and thus a mutating operation internal to one object is guaranteed to be invisible to another. This naturally facilitates reasoning about correctness on a local scale, but also proves beneficial for coarse-grained parallelism as noninterference between statements touching different objects is easily established. For fine-grained parallelism, ownership types fall short as owner-based disjointness only allows separation of the innards of different aggregates, which is very coarse-grained. Concretely: ownership types can reason about the disjointness of two different data structures, but cannot reason about the internal structure or disjointness within the data structure, without resorting to static and overly constraining measures. For similar reasons, ownership fails to determine internal disjointness of external pointers to objects that share a common owner. In this paper, we introduce the novel notion of refined ownership which overcomes these limitations by allowing precise local reasoning about a group of objects even though they belong to the same external owner. Using refined ownership, we can statically check determinism of parallel operations on tree-shaped substructures of a data structure, including operations on values external to the structure, without imposing any non-local alias restrictions.
Place, publisher, year, edition, pages
2015. Vol. 9104, 179-210 p.
, Lecture Notes in Computer Science, ISSN 0302-9743 ; 9104
IdentifiersURN: urn:nbn:se:uu:diva-266673DOI: 10.1007/978-3-319-18941-3_5ISI: 000362511600005ISBN: 978-3-319-18941-3ISBN: 978-3-319-18940-6OAI: oai:DiVA.org:uu-266673DiVA: diva2:868449
15th International School on Formal Methods for the Design of Computer, Communication, and Software Systems; SFM 2015, June 15–19, Bertinoro, Italy