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.

Additional publications