-
Reasoning about Interior Mutability in Rust using Library-Defined Capabilities
Authors:
Federico Poli,
Xavier Denis,
Peter Müller,
Alexander J. Summers
Abstract:
Existing automated verification techniques for safe Rust code rely on the strong type-system properties to reason about programs, especially to deduce which memory locations do not change (i.e., are framed) across function calls. However, these type guarantees do not hold in the presence of interior mutability (e.g., when interacting with any concurrent data structure). As a consequence, existing…
▽ More
Existing automated verification techniques for safe Rust code rely on the strong type-system properties to reason about programs, especially to deduce which memory locations do not change (i.e., are framed) across function calls. However, these type guarantees do not hold in the presence of interior mutability (e.g., when interacting with any concurrent data structure). As a consequence, existing verification techniques for safe code such as Prusti and Creusot are either unsound or fundamentally incomplete if applied to this setting. In this work, we present the first technique capable of automatically verifying safe clients of existing interiorly mutable types. At the core of our approach, we identify a novel notion of implicit capabilities: library-defined properties that cannot be expressed using Rust's types. We propose new annotations to specify these capabilities and a first-order logic encoding suitable for program verification. We have implemented our technique in a verifier called Mendel and used it to prove absence of panics in Rust programs that make use of popular standard-library types with interior mutability, including Rc, Arc, Cell, RefCell, AtomicI32, Mutex and RwLock. Our evaluation shows that these library annotations are useful for verifying usages of real-world libraries, and powerful enough to require zero client-side annotations in many of the verified programs.
△ Less
Submitted 14 May, 2024;
originally announced May 2024.
-
A hybrid approach to semi-automated Rust verification
Authors:
Sacha-Élie Ayoun,
Xavier Denis,
Petar Maksimović,
Philippa Gardner
Abstract:
While recent years have been witness to a large body of work on efficient and automated verification of safe Rust code, enabled by the rich guarantees of the Rust type system, much less progress has been made on reasoning about unsafe code due to its unique complexities. We propose a hybrid approach to end-to-end Rust verification in which powerful automated verification of safe Rust is combined w…
▽ More
While recent years have been witness to a large body of work on efficient and automated verification of safe Rust code, enabled by the rich guarantees of the Rust type system, much less progress has been made on reasoning about unsafe code due to its unique complexities. We propose a hybrid approach to end-to-end Rust verification in which powerful automated verification of safe Rust is combined with targeted semi-automated verification of unsafe~Rust. To this end, we present Gillian-Rust, a proof-of-concept semi-automated verification tool that is able to reason about type safety and functional correctness of unsafe~code. Built on top of the Gillian parametric compositional verification platform, Gillian-Rust automates a rich separation logic for real-world Rust, embedding the lifetime logic of RustBelt and the parametric propheciees of RustHornBelt. Using the unique extensibility of Gillian, our novel encoding of these features is fine-tuned to maximise automation and exposes a user-friendly API, allowing for low-effort verification of unsafe code. We link Gillian-Rust with Creusot, a state-of-the-art verifier for safe Rust, by providing a systematic encoding of unsafe code specifications that Creusot may use but not verify, demonstrating the feasibility of our hybrid~approach.
△ Less
Submitted 22 March, 2024;
originally announced March 2024.
-
First branching fraction measurement of the suppressed decay $Ξ_c^0\to π^-Λ_c^+$
Authors:
LHCb collaboration,
R. Aaij,
C. Abellán Beteta,
T. Ackernley,
B. Adeva,
M. Adinolfi,
H. Afsharnia,
C. A. Aidala,
S. Aiola,
Z. Ajaltouni,
S. Akar,
J. Albrecht,
F. Alessio,
M. Alexander,
A. Alfonso Albero,
Z. Aliouche,
G. Alkhazov,
P. Alvarez Cartelle,
S. Amato,
Y. Amhis,
L. An,
L. Anderlini,
G. Andreassi,
A. Andreianov,
M. Andreotti
, et al. (948 additional authors not shown)
Abstract:
The $Ξ_c^0$ baryon is unstable and usually decays into charmless final states by the $c \to s u\overline{d}$ transition. It can, however, also disintegrate into a $π^-$ meson and a $Λ_c^+$ baryon via $s$ quark decay or via $cs\to d c$ weak scattering. The interplay between the latter two processes governs the size of the branching fraction ${\cal{B}}$$(Ξ_c^0\to π^-Λ_c^+)$, first measured here to b…
▽ More
The $Ξ_c^0$ baryon is unstable and usually decays into charmless final states by the $c \to s u\overline{d}$ transition. It can, however, also disintegrate into a $π^-$ meson and a $Λ_c^+$ baryon via $s$ quark decay or via $cs\to d c$ weak scattering. The interplay between the latter two processes governs the size of the branching fraction ${\cal{B}}$$(Ξ_c^0\to π^-Λ_c^+)$, first measured here to be $(0.55\pm 0.02 \pm 0.18)$%, where the first uncertainty is statistical and second systematic. This result is compatible with the larger of the theoretical predictions that connect models of hyperon decays using partially conserved axial currents and SU(3) symmetry with those involving the heavy-quark expansion and heavy-quark symmetry. In addition, the branching fraction of the normalization channel, ${\cal{B}}(Ξ_c^+\to p K^- π^+) = (1.135 \pm 0.002 \pm 0.387)$% is measured.
△ Less
Submitted 11 September, 2020; v1 submitted 23 July, 2020;
originally announced July 2020.
-
First observation of the decay $B^0 \rightarrow D^0 \overline{D}{}^0 K^+ π^-$
Authors:
LHCb collaboration,
R. Aaij,
C. Abellán Beteta,
T. Ackernley,
B. Adeva,
M. Adinolfi,
H. Afsharnia,
C. A. Aidala,
S. Aiola,
Z. Ajaltouni,
S. Akar,
J. Albrecht,
F. Alessio,
M. Alexander,
A. Alfonso Albero,
Z. Aliouche,
G. Alkhazov,
P. Alvarez Cartelle,
A. A. Alves Jr,
S. Amato,
Y. Amhis,
L. An,
L. Anderlini,
G. Andreassi,
A. Andreianov
, et al. (949 additional authors not shown)
Abstract:
The first observation of the decay $B^0 \rightarrow D^0 \overline{D}{}^0 K^+ π^-$ is reported using proton-proton collision data corresponding to an integrated luminosity of 4.7 $\mathrm{fb}^{-1}$ collected by the LHCb experiment in 2011, 2012 and 2016. The measurement is performed in the full kinematically allowed range of the decay outside of the $D^{*-}$ region. The ratio of the branching fract…
▽ More
The first observation of the decay $B^0 \rightarrow D^0 \overline{D}{}^0 K^+ π^-$ is reported using proton-proton collision data corresponding to an integrated luminosity of 4.7 $\mathrm{fb}^{-1}$ collected by the LHCb experiment in 2011, 2012 and 2016. The measurement is performed in the full kinematically allowed range of the decay outside of the $D^{*-}$ region. The ratio of the branching fraction relative to that of the control channel $B^0 \rightarrow D^{*-} D^0 K^+$ is measured to be $\mathcal{R} = (14.2 \pm 1.1 \pm 1.0)\%$, where the first uncertainty is statistical and the second is systematic. The absolute branching fraction of $B^0 \rightarrow D^0 \overline{D}{}^0 K^+ π^-$ decays is thus determined to be $\mathcal{B}(B^0 \rightarrow D^0 \overline{D}{}^0 K^+ π^-) = (3.50 \pm 0.27 \pm 0.26 \pm 0.30) \times 10^{-4}$, where the third uncertainty is due to the branching fraction of the control channel. This decay mode is expected to provide insights to spectroscopy and the charm-loop contributions in rare semileptonic decays.
△ Less
Submitted 22 September, 2020; v1 submitted 8 July, 2020;
originally announced July 2020.
-
Searches for low-mass dimuon resonances
Authors:
LHCb collaboration,
R. Aaij,
C. Abellán Beteta,
T. Ackernley,
B. Adeva,
M. Adinolfi,
H. Afsharnia,
C. A. Aidala,
S. Aiola,
Z. Ajaltouni,
S. Akar,
J. Albrecht,
F. Alessio,
M. Alexander,
A. Alfonso Albero,
Z. Aliouche,
G. Alkhazov,
P. Alvarez Cartelle,
A. A. Alves Jr,
S. Amato,
Y. Amhis,
L. An,
L. Anderlini,
G. Andreassi,
A. Andreianov
, et al. (949 additional authors not shown)
Abstract:
Searches are performed for a low-mass dimuon resonance, $X$, produced in proton-proton collisions at a center-of-mass energy of 13 TeV, using a data sample corresponding to an integrated luminosity of 5.1 fb$^{-1}$ and collected with the LHCb detector. The $X$ bosons can either decay promptly or displaced from the proton-proton collision, where in both cases the requirements placed on the event an…
▽ More
Searches are performed for a low-mass dimuon resonance, $X$, produced in proton-proton collisions at a center-of-mass energy of 13 TeV, using a data sample corresponding to an integrated luminosity of 5.1 fb$^{-1}$ and collected with the LHCb detector. The $X$ bosons can either decay promptly or displaced from the proton-proton collision, where in both cases the requirements placed on the event and the assumptions made about the production mechanisms are kept as minimal as possible. The searches for promptly decaying $X$ bosons explore the mass range from near the dimuon threshold up to 60 GeV, with nonnegligible $X$ widths considered above 20 GeV. The searches for displaced $X \to μ^+μ^-$ decays consider masses up to 3 GeV. None of the searches finds evidence for a signal and 90% confidence-level exclusion limits are placed on the $X \to μ^+μ^-$ cross sections, each with minimal model dependence. In addition, these results are used to place world-leading constraints on GeV-scale bosons in the two-Higgs-doublet and hidden-valley scenarios.
△ Less
Submitted 2 November, 2020; v1 submitted 8 July, 2020;
originally announced July 2020.
-
Observation of structure in the $J/ψ$-pair mass spectrum
Authors:
LHCb collaboration,
R. Aaij,
C. Abellán Beteta,
T. Ackernley,
B. Adeva,
M. Adinolfi,
H. Afsharnia,
C. A. Aidala,
S. Aiola,
Z. Ajaltouni,
S. Akar,
J. Albrecht,
F. Alessio,
M. Alexander,
A. Alfonso Albero,
Z. Aliouche,
G. Alkhazov,
P. Alvarez Cartelle,
A. A. Alves Jr,
S. Amato,
Y. Amhis,
L. An,
L. Anderlini,
G. Andreassi,
A. Andreianov
, et al. (948 additional authors not shown)
Abstract:
Using proton-proton collision data at centre-of-mass energies of $\sqrt{s} = 7$, $8$ and $13\mathrm{\,TeV}$ recorded by the LHCb experiment at the Large Hadron Collider, corresponding to an integrated luminosity of $9\mathrm{\,fb}^{-1}$, the invariant mass spectrum of $J/ψ$ pairs is studied. A narrow structure around $6.9\mathrm{\,GeV/}c^2$ matching the lineshape of a resonance and a broad structu…
▽ More
Using proton-proton collision data at centre-of-mass energies of $\sqrt{s} = 7$, $8$ and $13\mathrm{\,TeV}$ recorded by the LHCb experiment at the Large Hadron Collider, corresponding to an integrated luminosity of $9\mathrm{\,fb}^{-1}$, the invariant mass spectrum of $J/ψ$ pairs is studied. A narrow structure around $6.9\mathrm{\,GeV/}c^2$ matching the lineshape of a resonance and a broad structure just above twice the $J/ψ$ mass are observed. The deviation of the data from nonresonant $J/ψ$-pair production is above five standard deviations in the mass region between $6.2$ and $7.4\mathrm{\,GeV/}c^2$, covering predicted masses of states composed of four charm quarks. The mass and natural width of the narrow $X(6900)$ structure are measured assuming a Breit--Wigner lineshape.
△ Less
Submitted 10 November, 2020; v1 submitted 30 June, 2020;
originally announced June 2020.
