Patrick Cousot, The hierarchy of analytic semantics of weakly consistent parallelism

Jade Alglave and Patrick Cousot.
The hierarchy of analytic semantics of weakly consistent parallelism
In Invited talks, IMDEA, Madrid, Spain, May 24, 2016.
Slides of the 50mn seminar:
- 1 slide per landscape page, 12.3 Mb,
Abstract:
Most definitions of weak consistency models (WCM) in the literature are specific to one style of semantics description (e.g. transition systems), one language (e.g. x86 assembly), and one computer architecture (e.g. ARM). This makes generality a difficult goal: each verification, static analysis, or transformation technique has to be reinvented if any of these three parameters changes.
In contrast, our work provides a wide variety of semantics definitions, all under the same framework. More precisely, we view the semantics of a parallel program P under a WCM as two-fold:
- a computation part, i.e. an architecture and language independent instruction semantics;
- a communication part, i.e. a set of constraints on communications.
   More precisely a WCM is the intersection (in the formal sense) of its computation and communication parts. Its computation part is said to be anarchic since it imposes no constraint on communications. To describe its communication part, we choose to use the cat domain specific language, which allows a user to list a set of constraints on communication in a concise manner.
   We define a hierarchy of computation semantics from ground valued to (un)interpreted symbolic execution, from interleaved to true parallelism, from event to state-based, from trace to transition-based, etc. Each level of the hierarchy is an abstraction of the bottom computation semantics (so called anarchic semantics since there are no restrictions on possible communications).
   Although the abstractions in the hierarchy do loose information in general (for example w.r.t. program termination), they do not loose any information w.r.t. the bottom/anarchic semantics. Moreover, all the abstractions preserve the cat specification of communications, viz. a given cat specification forbids exactly the same behaviours on any two abstractions.
   This allows us to provide a wide variety of semantics definitions: each and every computation semantics (whether state-based or not, trace-based or not) can be married to any communication semantics as described by a cat specification. Thus we can provide, for example, two (or more) definitions of TSO, Power or ARM, adjusted to the taste of the user, or the practicality w.r.t. verification techniques.
Keywords:
Parallel Program, Sequential consistency, Weak memory model, Weak consistency model, Semantics, Hierarchy of semantics, Analytic semantics, Computational semantics, Communication semantics, cat specification, Exactness, cat-preservation, Abstraction, Interleaving, True Parallelism, State, Prefix, Transition system, Abstract interpretation.

Bibliographic reference:

@inproceedings{AlglaveCousot-IMDEA-05-2016,
  author    = {Jade Alglave and Patrick Cousot},
  title     = {The hierarchy of analytic semantics of weakly consistent parallelism},
  booktitle = {Invited talks},
  year      = {2016},
  publisher = {{IMDEA Software, Madrid, Spain}},
  url       = {http://software.imdea.org/events/invited_talks_2016.html},
}

\bibitem{AlglaveCousot-IMDEA-05-2016}
Jade Alglave and Patrick Cousot.
\newblock The hierarchy of analytic semantics of weakly consistent parallelism.
\newblock In \emph{Invited talks, IMDEA Software, Madrid, Spain}, May 24, 2016.

copyright notice
Last modified: Wed May 25 08:51:57 CEST 2016