SACRED-MA: Safe And seCure REmote Direct Memory Access
Lead Research Organisation:
IMPERIAL COLLEGE LONDON
Department Name: Computing
Abstract
Abstracts are not currently available in GtR for all funded research. This is normally because the abstract was not required at the time of proposal submission, but may be because it included sensitive information such as personal details.
Publications
Ambal G
(2025)
Sufficient Conditions for Robustness of {RDMA} Programs
Ambal G
(2026)
A Verified High-Performance Composable Object Library for Remote Direct Memory Access
in Proceedings of the ACM on Programming Languages
Ambal G
(2024)
Semantics of Remote Direct Memory Access: Operational and Declarative Models of RDMA on TSO Architectures
in Proceedings of the ACM on Programming Languages
Ascari F
(2026)
U-Turn: Enhancing Incorrectness Analysis by Reversing Direction
in Proceedings of the ACM on Programming Languages
Cho K
(2023)
Memento: A Framework for Detectable Recoverability in Persistent Memory
in Proceedings of the ACM on Programming Languages
D'Osualdo E
(2023)
The Path to Durable Linearizability
in Proceedings of the ACM on Programming Languages
De Vilhena P
(2024)
Extending the C/C++ Memory Model with Inline Assembly - Technical Appendix
De Vilhena P
(2024)
Extending the C/C++ Memory Model with Inline Assembly
in Proceedings of the ACM on Programming Languages
| Description | Collaboration with NVIDIA |
| Organisation | NVIDIA |
| Country | Global |
| Sector | Private |
| PI Contribution | A formal semantic model for RDMA programming |
| Collaborator Contribution | Expertise in RDMA programming and understanding of the semantics |
| Impact | We have a preprint that is under submission. |
| Start Year | 2023 |
| Description | Collaboration with Tel Aviv University |
| Organisation | Tel Aviv University |
| Country | Israel |
| Sector | Academic/University |
| PI Contribution | A formal semantic model for RDMA programming. |
| Collaborator Contribution | Expertise in the area and contacts at NVIDIA |
| Impact | We have a pre-print that is under submission. |
| Start Year | 2023 |
| Description | University of Colorado, USA |
| Organisation | University of Colorado Boulder |
| Country | United States |
| Sector | Academic/University |
| PI Contribution | I am working with George Hodgkins, Mark Madler and Joe Izraelevitz from University of Colorado to develop a formally verified library for building multi-node objects on RDMA and a modular declarative verification framework called Mowgli with the RDMA memory model, to be used to verify the correctness of LOCO libraries. |
| Collaborator Contribution | They have supported the development of the modular declarative verification framework. |
| Impact | Conference Paper at Principles of Programming Languages (POPL), 2026: A Verified High-Performance Composable Object Library for Remote Direct Memory Access, jointly authored with Guillaume Ambal, George Hodgkins, Mark Madler, Gregory Chockler, Brijesh Dongol, Joe Izraelevitz, and Viktor Vafeiadis https://www.soundandcomplete.org/papers/POPL2026/Mowgli/mowgli.pdf |
| Start Year | 2025 |
| Description | University of Pisa |
| Organisation | University of Pisa |
| Country | Italy |
| Sector | Academic/University |
| PI Contribution | I am working with Flavio Ascari, Roberto Bruni and Roberta Gori on a combination of Incorrectness Logic and Sufficient Incorrectness Logic to formalize a mixed forward/backward analysis that is able to both highlight the presence of bugs and finding their sources. |
| Collaborator Contribution | We have developed new avenues for embedding incorrectness insights into scalable, expressive, automated code contracts, resulting in our POPL paper U-Turn: Enhancing Incorrectness Analysis by Reversing Direction, published in Proceedings of the ACM on Programming Languages (POPL) 2026 |
| Impact | POPL 2026 paper: U-Turn: Enhancing Incorrectness Analysis by Reversing Direction https://dl.acm.org/doi/abs/10.1145/3776688 |
| Start Year | 2025 |
| Description | University of Surrey |
| Organisation | University of Surrey |
| Country | United Kingdom |
| Sector | Academic/University |
| PI Contribution | i am currently collaborating with Brijesh Dongol and Gregory Chockler from University of Surrey on Library of Composable Objects (LOCO), a formally verified library for building multi-node objects on RDMA, which fills the gap between shared memory and distributed system programming. called Mowgli, that is flexible enough to model multinode objects and is independent of a memory consistency model. Work to instantiate Mowgli with the RDMA memory model, and use it to verify correctness of LOCO libraries. |
| Collaborator Contribution | Work on Library of Composable Objects (LOCO), and Mowgli verification framework. |
| Impact | Conference Paper at European Symposium on Programming (ESOP), 2026 (to appear): Specifying and Verifying RDMA Synchronisation, jointly authored with Guillaume Ambal, Max Stupple, Brijesh Dongol https://www.soundandcomplete.org/papers/ESOP2026/rdma-rmw.pdf Conference Paper at Principles of Programming Languages (POPL), 2026: A Verified High-Performance Composable Object Library for Remote Direct Memory Access, jointly authored with Guillaume Ambal, George Hodgkins, Mark Madler, Gregory Chockler, Brijesh Dongol, Joe Izraelevitz, and Viktor Vafeiadis https://www.soundandcomplete.org/papers/POPL2026/Mowgli/mowgli.pdf |
| Start Year | 2024 |