English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Trace theory is a principled framework for defining equivalence relations forconcurrent program runs based on a commutativity relation over the set ofatomic steps taken by individual program threads. Its simplicity, elegance, andalgorithmic efficiency makes it useful in many different contexts includingprogram verification and testing. We study relaxations of trace equivalencewith the goal of maintaining its algorithmic advantages.  We first prove that the largest appropriate relaxation of trace equivalence,an equivalence relation that preserves the order of steps taken by each threadand what write operation each read operation observes, does not yield efficientalgorithms. We prove a linear space lower bound for the problem of checking, ina streaming setting, if two arbitrary steps of a concurrent program run arecausally concurrent (i.e. they can be reordered in an equivalent run) orcausally ordered (i.e. they always appear in the same order in all equivalentruns). The same problem can be decided in constant space for trace equivalence.Next, we propose a new commutativity-based notion of equivalence called grainequivalence that is strictly more relaxed than trace equivalence, and yetyields a constant space algorithm for the same problem. This notion ofequivalence uses commutativity of grains, which are sequences of atomic steps,in addition to the standard commutativity from trace theory. We study the twodistinct cases when the grains are contiguous subwords of the input program runand when they are not, formulate the precise definition of causal concurrencyin each case, and show that they can be decided in constant space, despitebeing strict relaxations of the notion of causal concurrency based on traceequivalence.

Coarser Equivalences for Causal Concurrency