Brijesh Dongol

Dr Brijesh Dongol


Senior Lecturer
Room 07BB02 (appointments via e-mail)

Biography

University roles and responsibilities

  • Level 3 coordinator
  • Alumni and advancement coordinator

Research projects

My teaching

My publications

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) 11023 pp. 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