Dr Brijesh Dongol

Senior Lecturer
Room 07 BB 02 (appointments via email)


University roles and responsibilities

  • Level 3 coordinator
  • Alumni and advancement coordinator

    Research projects

    My teaching

    My publications


    Doherty Simon, Dongol Brijesh, Wehrheim Heike, Derrick John (2018) Making Linearizability Compositional for Partially Ordered Executions,Lecture Notes in Computer Science: Proceedings of the 14th International Conference on integrated Formal Methods (IFM 2018)11023pp. 110-129 Springer, Chamonix
    In the interleaving model of concurrency, where events are totally ordered, linearizability is compositional: the composition of two linearizable objects is guaranteed to be linearizable. However, linearizability is not compositional when events are only partially ordered, as in the weak-memory models that describe multicore memory systems. In this paper, we present a generalisation of linearizability for concurrent objects implemented in weak-memory models. We abstract from the details of specific memory models by defining our condition using Lamport's execution structures. We apply our condition to the C11 memory model, providing a correctness condition for C11 objects. We develop a proof method for verifying objects implemented in C11 and related models. Our method is an adaptation of simulation-based methods, but in contrast to other such methods, it does not require that the implementation totally orders its events. We apply our proof technique and show correctness of the Treiber stack that blocks on empty, annotated with C11 release-acquire synchronisation.
    Doherty Simon, Dongol Brijesh, Wehrheim Heike, Derrick John (2019) Verifying C11 Programs Operationally,Proceedings of PPoPP 2019: 24th ACM SIGPLAN Annual Symposium on Principles and Practice of Parallel Programming Association for Computing Machinery (ACM)
    This paper develops an operational semantics for a release-acquire fragment of the C11 memory model with relaxed accesses. We show that the semantics is both sound and complete with respect to the axiomatic model of Batty et al. The semantics relies on a per-thread notion of observability, which allows one to reason about a weak memory C11 program in program order. On top of this, we develop a proof calculus for invariant-based reasoning, which we use to verify the release-acquire version of Peterson?s mutual exclusion algorithm.
    Dongol Brijesh, Jagadeesan Radha, Riely James (2019) Modular Transactions: Bounding Mixed Races in Space and Time,Proceedings of PPoPP 2019: 24th ACM SIGPLAN Annual Symposium on Principles and Practice of Parallel Programming Association for Computing Machinery (ACM)
    We define local transactional race freedom (LTRF), which provides a programmer model for software transactional memory. LTRF programs satisfy the SC-LTRF property, thus allowing the programmer to focus on sequential executions in which transactions execute atomically. Unlike previous results, SCLTRF does not require global race freedom.We also provide a lower-level implementation model to reason about quiescence fences and validate numerous compiler optimizations.
    Dongol Brijesh, Doherty Simon, Wehrheim Heiki, Derrick John (2018) Brief Announcement: Generalising Concurrent Correctness to Weak Memory,32nd International Symposium on Distributed Computing (DISC 2018) Proceedings Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik
    Correctness conditions like linearizability and opacity describe some form of atomicity imposed on concurrent objects. In this paper, we propose a correctness condition (called causal atomicity) for concurrent objects executing in a weak memory model, where the histories of the objects in question are partially ordered. We establish compositionality and abstraction results for causal atomicity and develop an associated refinement-based proof technique.
    Dalvandi Mohammadsadegh, Dongol Brijesh (2019) Towards Deductive Verification of C11 Programs with Event-B and ProB,Proceedings of the 21st Workshop on Formal Techniques for Java-like Programs (FTfJP 2019) Association for Computing Machinery (ACM)
    This paper introduces a technique for modelling and verifying weak memory C11 programs in the Event-B framework. We build on a recently developed operational semantics for the RAR fragment of C11, which we use as a top-level abstraction. In our technique, a concrete C11 program can be modelled by refining this abstract model of the semantics. Program structures and individual operations are then introduced in the refined machine and can be checked and verified using available Event-B provers and model checkers. The paper also discusses how ProB model checker can be used to validate the Event-B model of C11 programs. We applied our technique to the C11 implementation of Peterson?s algorithm, where we discovered that the standard invariant used to characterise mutual exclusion is inadaquate. We therefore propose and verify new invariants necessary for characterising mutual exclusion in a weak memory setting.
    Derrick John, Doherty Simon, Dongol Brijesh, Schellhorn Gerhard, Wehrheim Heike (2019) Verifying Correctness of Persistent Concurrent Data Structures,Proceedings of the 23rd International Symposium on Formal Methods (FM'19) Springer
    Non-volatile memory (NVM), aka persistent memory, is a new paradigm for memory preserving its contents even after power loss. The expected ubiquity of NVM has stimulated interest in the design of persistent concurrent data structures, together with associated notions of correctness. In this paper, we present the first formal proof technique for durable linearizability, which is a correctness criterion that extends linearizability to handle crashes and recovery in the context of NVM. Our proofs are based on refinement of IO-automata representations of concurrent data structures. To this end, we develop a generic procedure for transforming any standard sequential data structure into a durable specification. Since the durable specification only exhibits durably linearizable behaviours, it serves as the abstract specification in our refinement proof. We exemplify our technique on a recently proposed persistent memory queue that builds on Michael and Scott?s lock-free queue.
    Dongol Brijesh, Hayes Ian, Meinicke Larissa, Struth Georg (2019) Cylindric Kleene Lattices for Program Construction,Lecture Notes in Computer Science - Proceedings of the 13th International Conference on Mathematics of Program Construction Springer
    Cylindric algebras have been developed as an algebraisation of equational first order logic. We adapt them to cylindric Kleene lattices and their variants and present relational and relational fault models for these. This allows us to encode frames and local variable blocks, and to derive Morgan's refinement calculus as well as an algebraic Hoare logic for while programs with assignment laws. Our approach thus opens the door for algebraic calculations with program and logical variables instead of domain-specific reasoning over concrete models of the program store. A refinement proof for a small program is presented as an example.

    Additional publications