Placeholder image for staff profiles

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.

Additional publications