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

Concurrent systems are notoriously difficult to analyze, and technologicaladvances such as weak memory architectures greatly compound this problem. Thishas renewed interest in partial order semantics as a theoretical foundation forformal verification techniques. Among these, symbolic techniques have beenshown to be particularly effective at finding concurrency-related bugs becausethey can leverage highly optimized decision procedures such as SAT/SMT solvers.This paper gives new fundamental results on partial order semantics forSAT/SMT-based symbolic encodings of weak memory concurrency. In particular, wegive the theoretical basis for a decision procedure that can handle a fragmentof concurrent programs endowed with least fixed point operators. In addition,we show that a certain partial order semantics of relaxed sequentialconsistency is equivalent to the conjunction of three extensively studied weakmemory axioms by Alglave et al. An important consequence of this equivalence isan asymptotically smaller symbolic encoding for bounded model checking whichhas only a quadratic number of partial order constraints compared to thestate-of-the-art cubic-size encoding.

On partial order semantics for SAT/SMT-based symbolic encodings of weak memory concurrency