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


    John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim (2019)Verifying Correctness of Persistent Concurrent Data Structures, In: 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.

    Mohammadsadegh Dalvandi, Brijesh Dongol (2019)Towards Deductive Verification of C11 Programs with Event-B and ProB, In: 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.

    Brijesh Dongol, Ian Hayes, Larissa Meinicke, Georg Struth (2019)Cylindric Kleene Lattices for Program Construction, In: 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.

    Tsz Yiu Lam, Brijesh Dongol (2020)A blockchain-enabled e-learning platform, In: Interactive learning environmentsahead-of-print(ahead-of-print)pp. 1-23 Routledge

    The properties of a blockchain such as immutability, provenance, and peer-executed smart contracts could bring a new level of security, trust, and transparency to e-learning. In this paper, we introduce our proof-of-concept blockchain-based e-learning platform developed to increase transparency in assessments and facilitate curriculum personalisation in a higher education context. Most notably, our platform could automate assessments and issue credentials. We designed it to be pedagogically neutral and content-neutral in order to showcase the benefits of a blockchain back-end to end users such as students and teaching staff. Our evaluation suggests that our platform could increase trust in online education providers, assessment procedures, education history and credentials.

    Sadegh Dalvandi, Simon Doherty, BRIJESH DONGOL, Heike Wehrheim (2020)Owicki-Gries Reasoning for C11 RAR

    Owicki-Gries reasoning for concurrent programs uses Hoare logic together with an interference freedom rule for concurrency. In this paper, we develop a new proof calculus for the C11 RAR memory model (a fragment of C11 with both relaxed and release-acquire accesses) that allows all Owicki-Gries proof rules for compound statements, including non-interference, to remain unchanged. Our proof method features novel assertions specifying thread-specific views on the state of programs. This is combined with a set of Hoare logic rules that describe how these assertions are affected by atomic program steps. We demonstrate the utility of our proof calculus by verifying a number of standard C11 litmus tests and Peterson’s algorithm adapted for C11. Our proof calculus and its application to program verification have been fully mechanised in the theorem prover

    Keith Clark, BRIJESH DONGOL, Peter Robinson Temporal Logic Semantics for Teleo-Reactive Robotic Agent Programs

    Teleo-Reactive (TR) robotic agent programs comprise sequences of guarded action rules clustered into named parameterised procedures. Their ancestry goes back to the first cognitive robot, Shakey. Like Shakey, a TR programmed robotic agent has a deductive Belief Store comprising constantly changing predicate logic percept facts, and knowledge facts and rules for querying the percepts. In this paper we introduce TR programming using a simple example expressed in the teleo-reactive programming language TeleoR, which is a syntactic extension of QuLog, a typed logic programming language used for the agent’s Belief Store. We give a formal definition of the regression property that rules of TeleoR procedures should satisfy, and an informal operational semantics of the evaluation of a TeleoR procedure call. We then formally express key features of the evaluation in LTL. Finally we show how this LTL formalisation can be used to prove that a procedure’s rules satisfy the regression property by proving it holds for one rule of the example TeleoR program. The proof requires us: to formally link a TeleoR agent’s percept beliefs with sensed configurations of the external environment; to link the agent’s robotic device action intentions with actual robot actions; to specify the eventual physical effects of the robot’s actions on the environment state.

    Emil Sekerinski, Nelma Moreira, José N Oliveira, Daniel Ratiu, Riccardo Guidotti, Marie Farrell, Matt Luckcuck, Diego Marmsoler, José Campos, Troy Astarte, Laure Gonnord, Antonio Cerone, Luis Couto, BRIJESH DONGOL, Martin Kutrib, Pedro Monteiro, David Delmas (2020)Formal Methods. FM 2019 International Workshops, In: Lecture notes in computer science12232 Springer International Publishing

    This book constitutes the refereed proceedings of the workshops which complemented the 23rd Symposium on Formal Methods, FM 2019, held in Porto, Portugal, in October 2019. This volume presents the papers that have been accepted for the following workshops: Third Workshop on Practical Formal Verification for Software Dependability, AFFORD 2019; 8th International Symposium From Data to Models and Back, DataMod 2019; First Formal Methods for Autonomous Systems Workshop, FMAS 2019; First Workshop on Formal Methods for Blockchains, FMBC 2019; 8th International Workshop on Formal Methods for Interactive Systems, FMIS 2019; First History of Formal Methods Workshop, HFM 2019; 8th International Workshop on Numerical and Symbolic Abstract Domains, NSAD 2019; 9th International Workshop on Open Community Approaches to Education, Research and Technology, OpenCERT 2019; 17th Overture Workshop, Overture 2019; 19th Refinement Workshop, Refine 2019; First International Workshop on Reversibility in Programming, Languages, and Automata, RPLA 2019; 10th International Workshop on Static Analysis and Systems Biology, SASB 2019; and the 10th Workshop on Tools for Automatic Program Analysis, TAPAS 2019.

    Eleni Bila, Simon Doherty, Brijesh Dongol, John Derrick, Gerhard Schellhorn, Heike Wehrheim (2020)Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory, In: Formal Techniques for Distributed Objects, Components, and Systems12136pp. 39-58

    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 interest in the design of novel concepts ensuring correctness of concurrent programming abstractions in the face of persistency. So far, this has lead to the design of a number of persistent concurrent data structures, built to satisfy an associated notion of correctness: durable linearizability.

    Brijesh Dongol, Luigia Petre, Graeme Smith (2019)Formal Methods Teaching Springer International Publishing

    This book constitutes the refereed proceedings of the Third International Workshop and Tutorial, FMTea 2019, Held as Part of the Third World Congress on Formal Methods, FM 2019, Porto, Portugal, October 2019. The 14 full papers presented together with 3 abstract papers were carefully reviewed and selected from 22 submissions. The papers are organized in topical sections named: Tutorial lectures; Teaching Program Verification; Teaching Program Development; and Effective Teaching Techniques.

    Brijesh Dongol, Simon Doherty, Heiki Wehrheim, John Derrick (2019)Brief Announcement: Generalising Concurrent Correctness to Weak Memory, In: 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.

    Simon Doherty, Brijesh Dongol, Heike Wehrheim, John Derrick (2019)Verifying C11 Programs Operationally, In: 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.

    Brijesh Dongol, Radha Jagadeesan, James Riely (2019)Modular Transactions: Bounding Mixed Races in Space and Time, In: 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.

    Simon Doherty, Brijesh Dongol, Heike Wehrheim, John Derrick (2018)Making Linearizability Compositional for Partially Ordered Executions, In: Integrated Formal Methods11023pp. 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.

    Additional publications