Enhanced sharing analysis techniques: a comprehensive evaluation

Roberto Bagnara; Enea Zaffanella; Patricia M. Hill

Home/Archive/arXiv

arXiv · cs/0401022

Enhanced sharing analysis techniques: a comprehensive evaluation

Roberto Bagnara·Enea Zaffanella·Patricia M. Hill

View original source ↗Read source document ↗Export metadata ↓

Abstract

Sharing, an abstract domain developed by D. Jacobs and A. Langen for the analysis of logic programs, derives useful aliasing information. It is well-known that a commonly used core of techniques, such as the integration of Sharing with freeness and linearity information, can significantly improve the precision of the analysis. However, a number of other proposals for refined domain combinations have been circulating for years. One feature that is common to these proposals is that they do not seem to have undergone a thorough experimental evaluation even with respect to the expected precision gains. In this paper we experimentally evaluate: helping Sharing with the definitely ground variables found using Pos, the domain of positive Boolean formulas; the incorporation of explicit structural information; a full implementation of the reduced product of Sharing and Pos; the issue of reordering the bindings in the computation of the abstract mgu; an original proposal for the addition of a new mode recording the set of variables that are deemed to be ground or free; a refined way of using linearity to improve the analysis; the recovery of hidden information in the combination of Sharing with freeness information. Finally, we discuss the issue of whether tracking compoundness allows the computation of more sharing information.

Explore related subjects

cs.PL

Keep this discovery

Explore connections, maps & timelines

BibTeX RIS

Roberto Bagnara, Enea Zaffanella, Patricia M. Hill. 2004-01-26. Enhanced sharing analysis techniques: a comprehensive evaluation. https://arxiv.org/abs/cs/0401022

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

A Physically-Realisable Quantum Programming Language with Quantum-Controlled Quantum Channels

In contrast to a classical bit, which can only take the value $0$ or $1$, its quantum counterpart---a qubit---can exist in a superposition of $0$ and $1$. This is a superposition of data values, and it is then tempting to superpose programs as well. Indeed, a particular superposition of programs, known as the quantum SWITCH, has attracted considerable attention. A natural way to superpose programs is conditional branching on quantum data, and several studies have pursued this idea. However, there is a well-known semantic difficulty with this approach, and the fundamental question of whether the languages proposed in prior work can be physically realised remains open. This paper proposes a physically realisable quantum programming language with quantum branching over quantum channels. We first analyse the semantic difficulty from an implementation perspective and show that the difficulty is caused by arbitrariness in the implementation. We then design a language that is free from this arbitrariness. As expected from its implementation-oriented design, our language is physically realisable. We argue for this from two directions: first, we give a method for compiling programs into quantum circuits; and second, we show that our programs stay within the physically admissible range, namely, that they neither yield probabilities greater than one nor violate causal inequalities. The absence of such violations is established through the inclusion of our language in QC-QC, a notion of realisability studied in physics.

cs.PL↗

arXiv2026

Nothing Is Shared Until You Synchronise: Reinterpreting Java for Data-Race Freedom

In mainstream shared-memory languages, programmers use synchronisation mechanisms such as locks to isolate shared data accesses across threads to avoid data races. Yet synchronisation enforces only a temporal ordering, while shared memory still communicates updates between threads at every ordinary read and write. To achieve isolation, programmers therefore need to understand the connection between ordering and communication, and to apply synchronisation correctly and consistently, while compilers and hardware optimise assuming they have. When programmers synchronise incorrectly, they lose isolation, and the semantics of their programs change without notice. We propose Sync-as-Share, a memory model built on isolation and communication rather than on the ordering of accesses to shared memory. We start from thread isolation, where each thread reads and writes a private view of memory, and reinterpret programs' existing synchronisation actions to also communicate updates explicitly. As nothing is communicated outside synchronisation actions, data races become impossible by construction. Instead, conflicting updates are detected at synchronisation points. Viewing synchronisation as explicit communication exposes the design decisions of what should be communicated, to whom, and what counts as a conflict. We propose two communication topologies with different trade-offs. We instantiate Sync-as-Share for Java by making the synchronisation actions already defined by its memory model the only points at which threads communicate, so Java programs can adopt Sync-as-Share unmodified. We formalise this instantiation as version-controlled memory, in which synchronisation actions push and pull updates between private views, and mechanise it in Rocq. We show that Java programs that are correctly synchronised under the Java memory model behave identically under shared memory and Sync-as-Share.

cs.PL↗

arXiv2026

GUARDTs: Decentralized Access Control for Replicated Data Types

Replicated data types providing strong eventual consistency offer a principled foundation for developing decentralized software. Yet existing approaches to programming such data types leave access control unresolved: they either provide none at all, delegate it to a trusted coordinator, reintroducing the centralization they were designed to avoid, or tie it to specific data-type constructions, while typically assuming non-Byzantine replicas and static policies. We present GUARDTs: Guarded Unforgeable Algebraic Replicated Data Types, which embed fine-grained permissions directly into the application data model, operate without a central authority, support dynamic policy evolution, and tolerate Byzantine replicas. We formally prove that GUARDTs guarantee confidentiality, integrity, and availability and show empirically that their access control adds negligible overhead on top of the cost of Byzantine-resilient replication itself.

cs.PL↗