Title: Coarser Equivalences for Causal Concurrency

Speaker: Azadeh Farzan    (bio) (bio)

Azadeh Farzan is a Professor in the Computer Science Department of University of Toronto. She received her PhD from the University of Illinois at Urbana-Champaign. Her interests are in Software Verification, Programming Languages, Formal Methods, and Security, with an emphasis on concurrency-related issues.

When: Tuesday, 02 April 2024 at 1900 hrs (IST)       

Abstract:
In this talk, I will discuss relaxations of trace equivalence with the goal of maintaining its algorithmic advantages. Specifically, for the problem of checking, in a streaming setting, if two arbitrary steps of a concurrent program run are causally concurrent (i.e. they can be reordered in an equivalent run) or causally ordered (i.e. they always appear in the same order in all equivalent runs), trace equivalence yields constant-space algorithms. I will discuss how certain relaxations, provably, do not yield similar efficient algorithms. Then, I will introduce a new commutativity-based notion of equivalence called grain equivalence that is strictly more relaxed than trace equivalence, and yet yields a constant space algorithm for the same problem. This notion of equivalence uses commutativity of grains, which are sequences of atomic steps, in addition to the standard commutativity from trace theory. I will discuss two distinct cases when the grains are contiguous subwords of the input program run and when they are not, formulate the precise definition of causal concurrency in each case, and show that they can be decided in constant space, despite being strict relaxations of the notion of causal concurrency based on trace equivalence.