13 citations · 52 across the 27 of their papers we have counts for
9 papers · 1 filter
A Verified High-Performance Composable Object Library for Remote Direct Memory Access (Extended Version)
Guillaume Ambal, George Hodgkins, Mark Madler +5
Remote Direct Memory Access (RDMA) is a memory technology that allows remote devices to directly write to and read from each other's memory, bypassing components such as the CPU an…
IsaBIL: A Framework for Verifying (In)correctness of Binaries in Isabelle/HOL (Extended Version)
Matt Griffin, Brijesh Dongol, Azalea Raad
This paper presents IsaBIL, a binary analysis framework in Isabelle/HOL that is based on the widely used Binary Analysis Platform (BAP). Specifically, in IsaBIL, we formalise BAP's…
Intel PMDK Transactions: Specification, Validation and Concurrency (Extended Version)
Azalea Raad, Ori Lahav, John Wickerson +2
Software Transactional Memory (STM) is an extensively studied paradigm that provides an easy-to-use mechanism for thread safety and concurrency control. With the recent advent of b…
Rely-Guarantee Reasoning for Causally Consistent Shared Memory (Extended Version)
Ori Lahav, Brijesh Dongol, Heike Wehrheim
Rely-guarantee (RG) is a highly influential compositional proof technique for concurrent programs, which was originally developed assuming a sequentially consistent shared memory.…
Implementing and Verifying Release-Acquire Transactional Memory (Extended Version)
Sadegh Dalvandi, Brijesh Dongol
Transactional memory (TM) is an intensively studied synchronisation paradigm with many proposed implementations in software and hardware, and combinations thereof. However, TM unde…
View-Based Owicki-Gries Reasoning for Persistent x86-TSO (Extended Version)
Eleni Vafeiadi Bila, Brijesh Dongol, Ori Lahav +2
The rise of persistent memory is disrupting computing to its core. Our work aims to help programmers navigate this brave new world by providing a program logic for reasoning about…