Publications
32 results found
Raad A, Lahav O, Wickerson J, et al., 2024, Intel PMDK Transactions: Specification, Validation and Concurrency, Programming Languages and Systems, Publisher: Springer Nature Switzerland, Pages: 150-179, ISBN: 9783031572661
<jats:title>Abstract</jats:title><jats:p>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 byte-addressable persistent memory, a natural question to ask is whether STM systems can be adapted to support <jats:italic>failure atomicity</jats:italic>. In this paper, we answer this question by showing how STM can be easily integrated with Intel’s Persistent Memory Development Kit (PMDK) transactional library (which we refer to as <jats:sc>txPMDK</jats:sc>) to obtain STM systems that are both concurrent and persistent. We demonstrate this approach using known STM systems, <jats:sc>TML</jats:sc> and <jats:sc>NOrec</jats:sc>, which when combined with <jats:sc>txPMDK</jats:sc> result in persistent STM systems, referred to as <jats:sc>PMDK-TML</jats:sc> and <jats:sc>PMDK-NORec</jats:sc>, respectively. However, it turns out that existing correctness criteria are insufficient for specifying the behaviour of <jats:sc>txPMDK</jats:sc> and our concurrent extensions. We therefore develop a new correctness criterion, <jats:italic>dynamic durable opacity</jats:italic>, that extends the previously defined notion of durable opacity with dynamic memory allocation. We provide a model of <jats:sc>txPMDK</jats:sc>, then show that this model satisfies dynamic durable opacity. Moreover, dynamic durable opacity supports concurrent transactions, thus we also use it to show correctness of both <jats:sc>PMDK-TML</jats:sc> and <jats:sc>PMDK-NORec</jats:sc>.</jats:p>
Raad A, Lahav O, Wickerson J, et al., 2024, Artifact Report: Intel PMDK Transactions: Specification, Validation and Concurrency, Programming Languages and Systems, Publisher: Springer Nature Switzerland, Pages: 180-184, ISBN: 9783031572661
<jats:title>Abstract</jats:title><jats:p>This report extends §6 of the main paper by providing further details of the mechanisation effort.</jats:p>
Cho K, Jeon S, Raad A, et al., 2023, Memento: A Framework for Detectable Recoverability in Persistent Memory, Proceedings of the ACM on Programming Languages, Vol: 7
Persistent memory (PM) is an emerging class of storage technology that combines the performance of DRAM with the durability of SSD, offering the best of both worlds. This had led to a surge of research on persistent objects in PM. Among such persistent objects, concurrent data structures (DSs) are particularly interesting thanks to their performance and scalability. One of the most widely used correctness criteria for persistent concurrent DSs is detectable recoverability, ensuring both thread safety (for correctness in non-crashing concurrent executions) and crash consistency (for correctness in crashing executions). However, the existing approaches to designing detectably recoverable concurrent DSs are either limited to simple algorithms or suffer from high runtime overheads. We present Memento: A general and high-performance programming framework for detectably recoverable concurrent DSs in PM. To ensure general applicability to various DSs, Memento supports primitive operations such as checkpoint and compare-And-swap and their composition with control constructs. To ensure high performance, Memento employs a timestamp-based recovery strategy that requires fewer writes and flushes to PM than the existing approaches. We formally prove that Memento ensures detectable recoverability in the presence of crashes. To showcase Memento, we implement a lock-free stack, list, queue, and hash table, and a combining queue that detectably recovers from random crashes in stress tests and performs comparably to existing hand-Tuned persistent DSs with and without detectable recoverability.
D'Osualdo E, Raad A, Vafeiadis V, 2023, The Path to Durable Linearizability, Proceedings of the ACM on Programming Languages, Vol: 7, Pages: 748-774
There is an increasing body of literature proposing new and efficient persistent versions of concurrent data structures ensuring that a consistent state can be recovered after a power failure or a crash. Their correctness is typically stated in terms of durable linearizability (DL), which requires that individual library operations appear to be executed atomically in a sequence consistent with the real-time order and, moreover, that recovering from a crash return a state corresponding to a prefix of that sequence. Sadly, however, there are hardly any formal DL proofs, and those that do exist cover the correctness of rather simple persistent algorithms on specific (simplified) persistency models. In response, we propose a general, powerful, modular, and incremental proof technique that can be used to guide the development and establish DL. Our technique is (1) general, in that it is not tied to a specific persistency and/or consistency model, (2) powerful, in that it can handle the most advanced persistent algorithms in the literature, (3) modular, in that it allows the reuse of an existing linearizability argument, and (4) incremental, in that the additional requirements for establishing DL depend on the complexity of the algorithm to be verified. We illustrate this technique on various versions of a persistent set, leading to the link-free set of Zuriel et al.
Le QL, Raad A, Villard J, et al., 2022, Finding real bugs in big programs with incorrectness logic, Proceedings of the ACM on Programming Languages, Vol: 6, Pages: 1-27, ISSN: 2475-1421
Incorrectness Logic (IL) has recently been advanced as a logical theory for compositionally proving the presence of bugs—dual to Hoare Logic, which is used to compositionally prove their absence. Though IL was motivated in large part by the aim of providing a logical foundation for bug-catching program analyses, it has remained an open question: is IL useful only retrospectively (to explain existing analyses), or can it actually be useful in developing new analyses which can catch real bugs in big programs?In this work, we develop Pulse-X, a new, automatic program analysis for catching memory errors, based on ISL, a recent synthesis of IL and separation logic. Using Pulse-X, we have found 15 new real bugs in OpenSSL, which we have reported to OpenSSL maintainers and have since been fixed. In order not to be overwhelmed with potential but false error reports, we develop a compositional bug-reporting criterion based on a distinction between latent and manifest errors, which references the under-approximate ISL abstractions computed by Pulse-X, and we investigate the fix rate resulting from application of this criterion. Finally, to probe the potential practicality of our bug-finding method, we conduct a comparison to Infer, a widely used analyzer which has proven useful in industrial engineering practice.
Bila E, Dongol B, Lahav O, et al., 2022, View-based Owicki-Gries reasoning for persistent x86-TSO, European Symposium on Programming (ESOP) 2020, Publisher: Springer, Pages: 234-261, ISSN: 0302-9743
The rise of persistent memory is disrupting computing toits core. Our work aims to help programmers navigate this brave newworld by providing a program logic for reasoning about x86 code thatuses low-level operations such as memory accesses and fences, as well aspersistency primitives such as flushes. Our logic, Pierogi, benefits from asimple underlying operational semantics based on views, is able to handleoptimised flush operations, and is mechanised in the Isabelle/HOL proofassistant. We detail the proof rules of Pierogi and prove them sound.We also show how Pierogi can be used to reason about a range ofchallenging single- and multi-threaded persistent programs
Raad A, Berdine J, Dreyer D, et al., 2022, Concurrent incorrectness separation logic, Proceedings of the ACM on Programming Languages, Vol: 6, Pages: 1-29, ISSN: 2475-1421
Incorrectness separation logic (ISL) was recently introduced as a theory of under-approximate reasoning, with the goal of proving that compositional bug catchers find actual bugs. However, ISL only considers sequential programs. Here, we develop concurrent incorrectness separation logic (CISL), which extends ISL to account for bug catching in concurrent programs. Inspired by the work on Views, we design CISL as a parametric framework, which can be instantiated for a number of bug catching scenarios, including race detection, deadlock detection, and memory safety error detection. For each instance, the CISL meta-theory ensures the soundness of incorrectness reasoning for free, thereby guaranteeing that the bugs detected are true positives.
Raad A, Maranget L, Vafeiadis V, 2022, Extending Intel-x86 consistency and persistency: formalising the semantics of Intel-x86 memory types and non-temporal stores, Proceedings of the ACM on Programming Languages, Vol: 6, Pages: 1-31, ISSN: 2475-1421
Existing semantic formalisations of the Intel-x86 architecture cover only a small fragment of its available features that are relevant for the consistency semantics of multi-threaded programs as well as the persistency semantics of programs interfacing with non-volatile memory.We extend these formalisations to cover: (1) non-temporal writes, which provide higher performance and are used to ensure that updates are flushed to memory; (2) reads and writes to other Intel-x86 memory types, namely uncacheable, write-combined, and write-through; as well as (3) the interaction between these features. We develop our formal model in both operational and declarative styles, and prove that the two characterisations are equivalent. We have empirically validated our formalisation of the consistency semantics of these additional features and their subtle interactions by extensive testing on different Intel-x86 implementations.
Cho K, Lee S-H, Raad A, et al., 2021, Revamping hardware persistency models: view-based and axiomatic persistency models for Intel-x86 and Armv8, PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Publisher: ACM, Pages: 16-31
Non-volatile memory (NVM) is a cutting-edge storage technology that promises the performance of DRAM with the durability of SSD. Recent work has proposed several persistency models for mainstream architectures such as Intel-x86 and Armv8, describing the order in which writes are propagated to NVM. However, these models have several limitations; most notably, they either lack operational models or do not support persistent synchronization patterns.We close this gap by revamping the existing persistency models. First, inspired by the recent work on promising semantics, we propose a unified operational style for describing persistency using views, and develop view-based operational persistency models for Intel-x86 and Armv8, thus presenting the first operational model for Armv8 persistency. Next, we propose a unified axiomatic style for describing hardware persistency, allowing us to recast and repair the existing axiomatic models of Intel-x86 and Armv8 persistency. We prove that our axiomatic models are equivalent to the authoritative semantics reviewed by Intel and Arm engineers. We further prove that each axiomatic hardware persistency model is equivalent to its operational counterpart. Finally, we develop a persistent model checking algorithm and tool, and use it to verify several representative examples.
Kokologiannakis M, Kaysin I, Raad A, et al., 2021, PerSeVerE: persistency semantics for verification under ext4., Proceedings of the ACM on Programming Languages, Vol: 5, Pages: 1-29, ISSN: 2475-1421
Although ubiquitous, modern filesystems have rather complex behaviours that are hardly understood by programmers and lead to severe software bugs such as data corruption. As a first step to ensure correctness of software performing file I/O, we formalize the semantics of the Linux ext4 filesystem, which we integrate with the weak memory consistency semantics of C/C++. We further develop an effective model checking approach for verifying programs that use the filesystem. In doing so, we discover and report bugs in commonly-used text editors such as vim, emacs and nano.
Raad A, Lahav O, Vafeiadis V, 2020, Persistent owicki-gries reasoning: a program logic for reasoning about persistent programs on Intel-x86, Proceedings of the ACM on Programming Languages, Vol: 4, Pages: 1-28, ISSN: 2475-1421
The advent of non-volatile memory (NVM) technologies is expected to transform how software systems are structured fundamentally, making the task of correct programming significantly harder. This is because ensuring that memory stores persist in the correct order is challenging, and requires low-level programming to flush the cache at appropriate points. This has in turn resulted in a noticeable verification gap.To address this, we study the verification of NVM programs, and present Persistent Owicki-Gries (POG), the first program logic for reasoning about such programs. We prove the soundness of POG over the recent Intel-x86 model, which formalises the out-of-order persistence of memory stores and the semantics of the Intel cache line flush instructions. We then use POG to verify several programs that interact with NVM.
Xiong S, Cerone A, Raad A, et al., 2020, Data Consistency in Transactional Storage Systems: a Centralised Approach, 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI '20)
Raad A, Wickerson J, Neiger G, et al., 2020, Persistency semantics of the Intel-x86 architecture, Proceedings of the ACM on Programming Languages (POPL2020), Vol: 4, Pages: 11:1-11:31, ISSN: 2475-1421
Emerging non-volatile memory (NVM) technologies promise the durability of disks with the performance of RAM. To describe the persistency guarantees of NVM, several memory persistency models have been proposed in the literature. However, the persistency semantics of the ubiquitous x86 architecture remains unexplored to date. To close this gap, we develop the Px86 (‘persistent x86’) model, formalising the persistency semantics of Intel-x86 for the first time. We formulate Px86 both operationally and declaratively, and prove that the two characterisations are equivalent. To demonstrate the application of Px86, we develop two persistent libraries over Px86: a persistent transactional library, and a persistent variant of the Michael–Scott queue. Finally, we encode our declarative Px86 model in Alloy and use it to generate persistency litmus tests automatically.
Raad A, Berdine J, Dang H-H, et al., 2020, Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic., Publisher: Springer, Pages: 225-252
Raad A, Wickerson J, Vafeiadis V, 2019, Weak persistency semantics from the ground up: formalising the persistency semantics of ARMv8 and transactional models, OOPSLA 2019, Publisher: Association for Computing Machinery (ACM), ISSN: 2475-1421
Emerging non-volatile memory (NVM) technologies promise the durability of disks with the performance of volatile memory (RAM). To describe the persistency guarantees of NVM, several memory persistency models have been proposed in the literature. However, the formal persistency semantics of mainstream hardware is unexplored to date. To close this gap, we present a formal declarative framework for describing concurrency models in the NVM context, and then develop the PARMv8 persistency model as an instance of our framework, formalising the persistency semantics of the ARMv8 architecture for the first time. To facilitate correct persistent programming, we study transactions as a simple abstraction for concurrency and persistency control. We thus develop the PSER (persistent serialisability) persistency model, formalising transactional semantics in the NVM context for the first time, and demonstrate that PSER correctly compiles to PARMv8. This then enables programmers to write correct, concurrent and persistent programs, without having to understand the low-level architecture-specific persistency semantics of the underlying hardware.
Xiong S, Cerone A, Raad A, et al., 2019, Data consistency in transactional storage systems: a centralised approach., Publisher: arXiv
We introduce an interleaving operational semantics for describing the client-observable behaviour of atomic transactions on distributed key-value stores. Our semantics builds on abstract states comprising centralised, global key-value stores and partial client views. We provide operational definitions of consistency models for our key-value stores which are shown to be equivalent to the well-known declarative definitions of consistency model for execution graphs. We explore two immediate applications of our semantics: specific protocols of geo-replicated databases (e.g. COPS) and partitioned databases (e.g. Clock-SI) can be shown to be correct for a specific consistency model by embedding them in our centralised semantics; programs can be directly shown to have invariant properties such as robustness results against a weak consistency model.
Kokologiannakis M, Raad A, Vafeiadis V, 2019, Effective lock handling in stateless model checking., Proceedings of the ACM on Programming Languages, Vol: 3, Pages: 173:1-173:26, ISSN: 2475-1421
Stateless Model Checking (SMC) is a verification technique for concurrent programs that checks for safety violations by exploring all possible thread interleavings. SMC is usually coupled with Partial Order Reduction (POR), which exploits the independence of instructions to avoid redundant explorations when an equivalent one has already been considered. While effective POR techniques have been developed for many different memory models, they are only able to exploit independence at the instruction level, which makes them unsuitable for programs with coarse-grained synchronization mechanisms such as locks.We present a lock-aware POR algorithm, LAPOR, that exploits independence at both instruction and critical section levels. This enables LAPOR to explore exponentially fewer interleavings than the state-of-the-art techniques for programs that use locks conservatively. Our algorithm is sound, complete, and optimal, and can be used for verifying programs under several different memory models. We implement LAPOR in a tool and show that it can be exponentially faster than the state-of-the-art model checkers.
Raad A, Wickerson J, Vafeiadis V, 2019, Weak persistency semantics from the ground up: formalising the persistency semantics of ARMv8 and transactional models, Proceedings of the ACM on Programming Languages, ISSN: 2475-1421
Kokologiannakis M, Raad A, Vafeiadis V, 2019, Model checking for weakly consistent libraries., PLDI19, Publisher: Association for Computing Machinery (ACM), Pages: 96-110
Raad A, Lahav O, Vafeiadis V, 2019, On the semantics of snapshot isolation, 20th International Conference, VMCAI, Publisher: Springer, Pages: 1-23, ISSN: 0302-9743
Snapshot isolation (SI) is a standard transactional consistency model used in databases, distributed systems and software transactional memory (STM). Its semantics is formally defined both declaratively as an acyclicity axiom, and operationally as a concurrent algorithm with memory bearing timestamps.We develop two simpler equivalent operational definitions of SI as lock-based reference implementations that do not use timestamps. Our first locking implementation is prescient in that requires a priori knowledge of the data accessed by a transaction and carries out transactional writes eagerly (in-place). Our second implementation is non-prescient and performs transactional writes lazily by recording them in a local log and propagating them to memory at commit time. Whilst our first implementation is simpler and may be better suited for developing a program logic for SI transactions, our second implementation is more practical due to its non-prescience. We show that both implementations are sound and complete against the declarative SI specification and thus yield equivalent operational definitions for SI.We further consider, for the first time formally, the use of SI in a context with racy non-transactional accesses, as can arise in STM implementations of SI. We introduce robust snapshot isolation (RSI), an adaptation of SI with similar semantics and guarantees in this mixed setting. We present a declarative specification of RSI as an acyclicity axiom and analogously develop two operational models as lock-based reference implementations (one eager, one lazy). We show that these operational models are both sound and complete against the declarative RSI model.
Raad A, Doko M, Rozic L, et al., 2019, On library correctness under weak memory consistency: specifying and verifying concurrent libraries under declarative consistency models, ACM Principles of Programming Languages, Publisher: Association for Computing Machinery (ACM), Pages: 68: 1-68: 31, ISSN: 2475-1421
Concurrent libraries are the building blocks for concurrency. They encompass a range of abstractions (locks, exchangers, stacks, queues, sets) built in a layered fashion: more advanced libraries are built out of simpler ones. While there has been a lot of work on verifying such libraries in a sequentially consistent (SC) environment, little is known about how to specify and verify them under weak memory consistency (WMC).We propose a general declarative framework that allows us to specify concurrent libraries declaratively, and to verify library implementations against their specifications compositionally. Our framework is sufficient to encode standard models such as SC, (R)C11 and TSO. Additionally, we specify several concurrent libraries, including mutual exclusion locks, reader-writer locks, exchangers, queues, stacks and sets. We then use our framework to verify multiple weakly consistent implementations of locks, exchangers, queues and stacks.
Cook M, Raad A, 2019, Hyperstate Space Graphs for Automated Game Analysis., Publisher: IEEE, Pages: 1-8
Raad A, Vafeiadis V, 2018, Persistence semantics for weak memory: integrating epoch persistency with the TSO memory model., ACM Object-Oriented Programming, Systems, Languages & Applications (OOPSLA18), Publisher: Association for Computing Machinery (ACM), Pages: 137:1-137:27, ISSN: 2475-1421
Emerging non-volatile memory (NVM) technologies promise the durability of disks with the performance of volatile memory (RAM). To describe the persistency guarantees of NVM, several memory persistency models have been proposed in the literature. However, the formal semantics of such persistency models in the context of existing mainstream hardware has been unexplored to date. To close this gap, we integrate the buffered epoch persistency model with the 'total-store-order' (TSO) memory model of the x86 and SPARC architectures. We thus develop the PTSO ('persistent' TSO) model and formalise its semantics both operationally and declaratively. We demonstrate that the two characterisations of PTSO are equivalent. We then formulate the notion of persistent linearisability to establish the correctness of library implementations in the context of persistent memory. To showcase our formalism, we develop two persistent implementations of a queue library, and apply persistent linearisability to show their correctness.
Cook M, Colton S, Raad A, 2018, Inferring Design Constraints From Game Ruleset Analysis., Publisher: IEEE, Pages: 1-8
Raad A, Lahav O, Vafeiadis V, 2018, On Parallel Snapshot Isolation and Release/Acquire Consistency., Publisher: Springer, Pages: 940-967
Raad A, Hobor A, Villard J, et al., 2016, Verifying concurrent graph algorithms, Asian Symposium on Programming Languages and Systems, Publisher: Springer Verlag, Pages: 314-334, ISSN: 0302-9743
We show how to verify four challenging concurrent fine-grained graph-manipulating algorithms, including graph copy, a speculatively parallel Dijkstra, graph marking and spanning tree. We develop a reasoning method for such algorithms that dynamically tracks the contributions and responsibilities of each thread operating on a graph, even in cases of arbitrary recursive thread creation. We demonstrate how to use a logic without abstraction ( Open image in new window ) to carry out abstract reasoning in the style of iCAP, by building the abstraction into the proof structure rather than incorporating it into the semantic model of the logic.
Raad A, Fragoso Santos J, Gardner P, 2016, DOM: Specification and Client Reasoning, Asian Symposium on Programming Languages and Systems, Publisher: Springer Verlag, Pages: 401-422, ISSN: 0302-9743
We present an axiomatic specification of a key fragment of DOM using structural separation logic. This specification allows us to develop modular reasoning about client programs that call the DOM.
Gardner PA, Raad A, Villard J, 2015, CoLoSL: Concurrent Local Subjective Logic, 24th European Symposium on Programming, ESOP 2015, Publisher: Springer, Pages: 710-735, ISSN: 0302-9743
Gardner P, Raad A, Wheelhouse M, et al., 2014, Abstract Local Reasoning for Concurrent Libraries: Mind the Gap, Mathematical Foundations of Programming Semantics Thirtieth Conference, MFPS 2014
Cook M, Colton S, Raad A, et al., 2013, Mechanic Miner: Reflection-Driven Game Mechanic Discovery and Level Design., Publisher: Springer, Pages: 284-293
This data is extracted from the Web of Science and reproduced under a licence from Thomson Reuters. You may not copy or re-distribute this data in whole or in part without the written consent of the Science business of Thomson Reuters.