Dr Brijesh Dongol
Academic and research departmentsFaculty of Engineering and Physical Sciences, Department of Computer Science.
I have a BSc in Computer Science and Mathematics and a BSc (Hons) in Logic and Computation, both from Victoria University of Wellington, New Zealand. In 2009, I received a PhD on formal derivations of concurrent algorithms at the University of Queensland, Australia. After this, I held postdoctorate positions at the University of Queensland and then at the University of Sheffield. I was a lecturer at Brunel University London (2014-18).
My research is on formal techniques and verification methods for concurrent and real-time systems. This includes concurrent objects, transactional memory and associated correctness conditions; weak memory models; algebraic techniques; and hybrid systems.
I am actively seeking good PhD students. Please contact me for further details.
Research projects EP/R032556/1 Verifiably Correct Transactional Memory Multi-core computing architectures have become ubiquitous over the last decade. This has been driven by the demand for continual performance improvements to cope with the ever-increasing sophistication of applications, combined with physical limitations on chip designs, whereby speedup via higher clock speeds has become infeasible. The inherent parallelism that multi-core architectures entail offers great technical opportunities, however, exploiting these opportunities presents a number of technical challenges.
To ensure correctness, concurrent programs must be properly synchronised, but synchronisation invariably introduces sequential bottlenecks, causing performance to suffer. Fully exploiting the potential for concurrency requires optimisations to consider executions at low levels of abstraction, e.g., the underlying memory model, compiler optimisations, cache-coherency protocols etc. The complexity of such considerations means that checking correctness with a high degree of confidence is extremely difficult. Concurrency bugs have specifically been attributed to disasters such as a power blackout in north eastern USA, Nasdaq's botched IPO of Facebook shares, and the near failure of NASA's Mars Pathfinder mission. Other safety-critical errors have manifested from using low-level optimisations, e.g., the double-checked locking bug and the Java Parker bug.
This project improves programmability of concurrent programs through the use of transactional memory (TM), which is a concurrency mechanism that makes low-level optimisations available to general application programmers. TM is an adaptation of transactions from databases. TM operations are highly concurrent (which improves efficiency), yet manage synchronisation on behalf of a programmer to provide an illusion of atomicity. Thus, by using TM, the focus of a programmer switches from what should be made atomic, as opposed to how atomicity should be guaranteed. EP/R025134/1 RoboTest: Systematic Model-Based Testing and Simulation of Mobile Autonomous Robots Mobile and autonomous robots have an increasingly important role in industry and the wider society; from driverless vehicles to home assistance, potential applications are numerous. The UK government identified robotics as a key technology that will lead us to future economic growth (tinyurl.com/q8bhcy7). They have recognised, however, that autonomous robots are complex and typically operate in ever-changing environments (tinyurl.com/o2u2ts7). How can we be confident that they perform useful functions, as required, but are safe? It is standard practice to use testing to check correctness and safety. The software-development practice for robotics typically includes testing within simulations, before robots are built, and then testing of the actual robots. Simulations have several benefits: we can test early, and test execution is cheaper and faster. For example, simulation does not require a robot to move physically. Testing with the real robots is, however, still needed, since we cannot be sure that a simulation captures all the important aspects of the hardware and environment. EP/R019045/1 Verifiably correct concurrency abstractions This is an overseas travel grant funded by the EPSRC.
COM1026 Foundations of Computing
COM2022 Computer Networking
COM3028 Systems Verification
COM3001 Professional Project
COMM002 MSc Dissertation
Professional Training (Computer Science)
Deductive verification techniques for C11 programs have advanced significantly in recent years with the development of operational semantics and associated logics for increasingly large fragments of C11. However, these semantics and logics have been developed in a restricted setting to avoid the thin-air-read problem. In this paper, we propose an operational semantics that leverages an intra-thread partial order (called semantic dependencies) induced by a recently developed denotational event-structure-based semantics. We prove that our operational semantics is sound and complete with respect to the denotational semantics. We present an associated logic that generalises a recent Owicki-Gries framework for RC11 (repaired C11), and demonstrate the use of this logic over several example proofs.
Secure speculation is an information flow security hyperproperty that prevents transient execution attacks such as Spectre, Meltdown and Foreshadow. Generic compiler mitigations for secure speculation are known to be insufficient for eliminating vulnerabilities. Moreover, these mitigation techniques often overprescribe speculative fences, causing the performance of the programs to suffer. Recently Cheang et al. have developed an operational semantics of program execution capable of characterising speculative executions as well as a new class of information flow hyperproperties named TPOD that ensure secure speculation. This paper presents a framework for verifying TPOD using the Isabelle/HOL proof assistant by encoding the operational semantics of Cheang et al. We provide translation tools for automatically generating the required Isabelle/HOL theory templates from a C-like program syntax, which speeds up verification. Our framework is capable of proving the existence of vulnerabilities and correctness of secure speculation. We exemplify our framework by proving the existence of secure speculation bugs in 15 victim functions for the MSVC compiler as well as correctness of some proposed fixes.
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.
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.
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.
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.
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.
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
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.
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.
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.
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.
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.
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.
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.
 J. Derrick, G. Smith, L. Groves, and B. Dongol. A proof method for linearizability on TSO architectures. In Provably Correct Systems, NASA Monographs in Systems and Software Engineering, pages 61--91. Springer, 2017.
 B. Dongol, R. Jagadeesan, and J. Riely. Transactions in relaxed memory architectures. PACMPL, 2(POPL):18:1--18:29, 2018.
 B. Dongol and R. M. Hierons. Decidability and complexity for quiescent consistency and its variations. Information and Computation, 2017. In press.
 J. Derrick, S. Doherty, B. Dongol, G. Schellhorn, O. Travkin, and H. Wehrheim. Mechanized proofs of opacity: A comparison of two techniques. Formal Aspects of Computing, 2017. Accepted 21 July, 2017 (Mechanisations available here: https://swt.informatik.uni-augsburg.de/swt/projects/Opacity-TML.html).
 B. Dongol, V. B. F. Gomes, I. J. Hayes, and G. Struth. Partial semigroups and convolution algebras. Archive of Formal Proofs, 2017, 2017.
 B. Dongol, I. J. Hayes, and G. Struth. Convolution as a unifying concept: Applications in separation logic, interval calculi, and concurrency. ACM Trans. Comput. Log., 17(3):15:1--15:25, 2016.
 B. Dongol and J. Derrick. Verifying linearisability: A comparative survey. ACM Comput. Surv., 48(2):19, 2015.
 B. Dongol and J. Derrick. Interval-based data refinement: A uniform approach to true concurrency in discrete and real-time systems. Sci. Comput. Program., 111:214--247, 2015.
 B. Dongol, I. J. Hayes, and P. J. Robinson. Reasoning about goal-directed real-time teleo-reactive programs. Formal Asp. Comput., 26(3):563--589, 2014.
 B. Dongol, I. J. Hayes, and J. Derrick. Deriving real-time action systems with multiple time bands using algebraic reasoning. Sci. Comput. Program., 85:137--165, 2014.
 I. J. Hayes, A. Burns, B. Dongol, and C. B. Jones. Comparing degrees of non-determinism in expression evaluation. Comput. J., 56(6):741--755, 2013.
 B. Dongol and I. J. Hayes. Deriving real-time action systems in a sampling logic. Sci. Comput. Program., 78(11):2047--2063, 2013.
 R. Colvin and B. Dongol. A general technique for proving lock-freedom. Sci. Comput. Program., 74(3):143--165, 2009.
B. Dongol and A. J. Mooij. Streamlining progress-based derivations of concurrent programs. Formal Asp. Comput., 20(2):141--160, 2008.
B. Dongol and D. Goldson. Extending the theory of Owicki and Gries with a logic of progress. Logical Methods in Computer Science, 2(1), 2006.
Refereed Conference Publications
 S. Doherty, B. Dongol, H. Wehrheim, and J. Derrick. Brief announcement: Generalising concurrent correctness to weak memory. In DISC, 2018. To appear.
 S. Doherty, B. Dongol, H. Wehrheim, and J. Derrick. Making linearizability compositional for partially ordered executions. In iFM, Lecture Notes in Computer Science. Springer, 2018. To appear.
 B. Dongol, R. Jagadeesan, J. Riely, and A. Armstrong. On abstraction and compositionality for weak-memory linearisability. In VMCAI, volume 10747 of Lecture Notes in Computer Science, pages 183--204. Springer, 2018.
 A. Armstrong and B. Dongol. Modularising opacity verification for hybrid transactional memory. In FORTE, volume 10321 of Lecture Notes in Computer Science, pages 33--49. Springer, 2017.
 A. Armstrong, B. Dongol, and S. Doherty. Proving opacity via linearizability: A sound and complete method. In FORTE, volume 10321 of Lecture Notes in Computer Science, pages 50--66. Springer, 2017. (Previous version: https://arxiv.org/abs/1610.01004).
 S. Doherty, B. Dongol, J. Derrick, G. Schellhorn, and H. Wehrheim. Proving opacity of a pessimistic STM. In OPODIS, volume 70 of LIPIcs, pages 35:1--35:17. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016.
 B. Dongol. An interval logic for stream-processing functions: A convolution-based construction. In FTSCS, volume 694 of Communications in Computer and Information Science, pages 20--35, 2016.
 B. Dongol and L. Groves. Contextual trace refinement for concurrent objects: Safety and progress. In ICFEM, volume 10009 of Lecture Notes in Computer Science, pages 261--278, 2016.
 B. Dongol and R. M. Hierons. Decidability and complexity for quiescent consistency. In LICS, pages 116--125. ACM, 2016.
 B. Dongol and L. Groves. Towards linking correctness conditions for concurrent objects and contextual trace refinement. In Refine@FM, volume 209 of EPTCS, pages 107--111, 2015.
 J. Derrick, B. Dongol, G. Schellhorn, O. Travkin, and H. Wehrheim. Verifying opacity of a transactional mutex lock. In N. Bjørner and F. D. de Boer, editors, FM, volume 9109 of LNCS, pages 161--177. Springer, 2015.
 B. Dongol, V. B. F. Gomes, and G. Struth. A program construction and verification tool for separation logic. In R. Hinze and J. Voigtländer, editors, MPC, volume 9129 of LNCS, pages 137--158. Springer, 2015.
 B. Dongol, J. Derrick, L. Groves, and G. Smith. Defining correctness conditions for concurrent objects in multicore architectures. In J. T. Boyland, editor, ECOOP, volume 37 of LIPIcs, pages 470--494. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015.
 J. Derrick, G. Smith, L. Groves, and B. Dongol. Using coarse-grained abstractions to verify linearizability on TSO architectures. In E. Yahav, editor, HVC, volume 8855 of LNCS, pages 1--16. Springer, 2014.
 G. Smith, J. Derrick, and B. Dongol. Admit your weakness: Verifying correctness on TSO architectures. In I. Lanese and E. Madelaine, editors, FACS, volume 8997 of LNCS, pages 364--383. Springer, 2014.
 J. Derrick, G. Smith, and B. Dongol. Verifying linearizability on TSO architectures. In E. Albert and E. Sekerinski, editors, iFM, volume 8739 of LNCS, pages 341--356. Springer, 2014.
 B. Dongol, J. Derrick, and G. Smith. Reasoning algebraically about refinement on TSO architectures. In G. Ciobanu and D. Méry, editors, ICTAC, volume 8687 of LNCS, pages 151--168. Springer, 2014.
 J. Derrick, B. Dongol, G. Schellhorn, B. Tofan, O. Travkin, and H. Wehrheim. Quiescent consistency: Defining and verifying relaxed linearizability. In C. B. Jones, P. Pihlajasaari, and J. Sun, editors, FM, volume 8442 of LNCS, pages 200--214. Springer, 2014.
 B. Dongol and J. Derrick. Simplifying proofs of linearisability using layers of abstraction. ECEASST, 66, 2013.
 B. Dongol, O. Travkin, J. Derrick, and H. Wehrheim. A high-level semantics for program execution under total store order memory. In Z. Liu, J. Woodcock, and H. Zhu, editors, ICTAC, volume 8049 of LNCS, pages 177--194. Springer, 2013.
 B. Dongol and J. Derrick. Data refinement for true concurrency. In J. Derrick, E. A. Boiten, and S. Reeves, editors, Refine, volume 115 of EPTCS, pages 15--35, 2013.
 B. Dongol, J. Derrick, and I. J. Hayes. Fractional permissions and non-deterministic evaluators in interval temporal logic. ECEASST, 53, 2012.
 B. Dongol, I. J. Hayes, L. Meinicke, and K. Solin. Towards an algebra for real-time programs. In W. Kahl and T. G. Griffin, editors, RAMICS, volume 7560 of LNCS, pages 50--65. Springer, 2012.
 B. Dongol and I. J. Hayes. Deriving real-time action systems controllers from multiscale system specifications. In J. Gibbons and P. Nogueira, editors, MPC, volume 7342 of LNCS, pages 102--131. Springer, 2012.
 B. Dongol and I. J. Hayes. Rely/guarantee reasoning for teleo-reactive programs over multiple time bands. In J. Derrick, S. Gnesi, D. Latella, and H. Treharne, editors, IFM, volume 7321 of LNCS, pages 39--53. Springer, 2012.
 B. Dongol and I. J. Hayes. Approximating idealised real-time specifications using time bands. ECEASST, 46:1--16, 2012. 11th International Workshop on Automated Verification of Critical Systems.
 B. Dongol and I. J. Hayes. Compositional action system derivation using enforced properties. In C. Bolduc, J. Desharnais, and B. Ktari, editors, MPC, volume 6120 of LNCS, pages 119--139. Springer, 2010.
 B. Dongol and I. J. Hayes. Enforcing safety and progress properties: An approach to concurrent program derivation. In ASWEC, pages 3--12. IEEE Computer Society, 2009.
 R. Colvin and B. Dongol. Verifying lock-freedom using well-founded orders. In C. B. Jones, Z. Liu, and J. Woodcock, editors, ICTAC, volume 4711 of LNCS, pages 124--138. Springer, 2007.
 B. Dongol. Formalising progress properties of non-blocking programs. In Z. Liu and J. He, editors, ICFEM, volume 4260 of LNCS, pages 284--303. Springer, 2006.
 B. Dongol. Towards simpler proofs of lock-freedom. In Preliminary Proceedings of the 1st Asian Working Conference on Verified Software, pages 136--146, 2006.
 B. Dongol. Derivation of Java monitors. In ASWEC, pages 211--220. IEEE Computer Society, 2006.
 B. Dongol and A. J. Mooij. Progress in deriving concurrent programs: Emphasizing the role of stable guards. In T. Uustalu, editor, MPC, volume 4014 of LNCS, pages 140--161. Springer, 2006.
 D. Goldson and B. Dongol. Concurrent program design in the extended theory of Owicki and Gries. In M. D. Atkinson and F. K. H. A. Dehne, editors, CATS, volume 41 of CRPIT, pages 41--50. Australian Computer Society, 2005.
 B. Dongol. Progress-based verification and derivation of concurrent programs. PhD thesis, School of Information Technology and Electrical Engineering, The University of Queensland, Qld, Australia, October 2009.
Technical reports (not elsewhere published)
B. Dongol, I. J. Hayes, and G. Struth. Relational Convolution, Generalised Modalities and Incidence Algebras. ArXiv e-prints, February 2017.
B. Dongol and J. Derrick. Proving linearisability via coarse-grained abstraction. CoRR, abs/1212.5116, 2012.
B. Dongol and I. J. Hayes. Reasoning about teleo-reactive programs under parallel composition. Technical Report SSE-2011-01, Division of Systems and Software Engineering Research, School of Information Technology and Electrical Engineering, The University of Queensland, QLD 4072, Australia, April 2011.
B. Dongol and I. J. Hayes. Trace semantics for the Owicki-Gries theory integrated with the progress logic from UNITY. Technical Report SSE-2007-02, Division of Systems and Software Engineering Research, School of Information Technology and Electrical Engineering, The University of Queensland, QLD 4072, Australia, April 2007.