13 citations · 52 across the 27 of their papers we have counts for
7 papers · 1 filter
FlintKV: A Fast Durable Storage Engine for Modern Databases
Sergey Egorov, Gregory Chockler, Brijesh Dongol +2
Byte-addressable non-volatile memory (NVM) offers an opportunity to rethink storage engine architectures. While recent NVM key-value stores achieve high throughput for ingestion an…
Specifying and Verifying RDMA Synchronisation (Extended Version)
Guillaume Ambal, Max Stupple, Brijesh Dongol +1
Remote direct memory access (RDMA) allows a machine to directly read from and write to the memory of remote machine, enabling high-throughput, low-latency data transfer. Ensuring c…
What Cannot Be Implemented on Weak Memory?
Armando Castañeda, Gregory Chockler, Brijesh Dongol +1
We present a general methodology for establishing the impossibility of implementing certain concurrent objects on different (weak) memory models. The key idea behind our approach l…
On Strong Observational Refinement and Forward Simulation
John Derrick, Simon Doherty, Brijesh Dongol +2
Hyperproperties are correctness conditions for labelled transition systems that are more expressive than traditional trace properties, with particular relevance to security. Recent…
Modularising Verification Of Durable Opacity
Eleni Bila, John Derrick, Simon Doherty +3
Non-volatile memory (NVM), also known as persistent memory, is an emerging paradigm for memory that preserves its contents even after power loss. NVM is widely expected to become u…
Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory
Eleni Bila, Simon Doherty, Brijesh Dongol +3
Non-volatile memory (NVM), aka persistent memory, is a new paradigm for memory that preserves its contents even after power loss. The expected ubiquity of NVM has stimulated intere…