Patrick Cousot, The analytic semantics of weakly consistent parallelism

Jade Alglave and Patrick Cousot.
The analytic semantics of weakly consistent parallelism
In Symposium on "Programming: Logics, Models, Algorithms and Concurrency, Jayadev Misra’s Fest, Austin, TX, USA, April 29-30, 2016.
Slides of the 15mn presentation at Jayadev Misra’s Fest:
- 1 slide per landscape page, 6 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.
   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 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{JayadevMISRAFest2016,
  author    = {Jade Alglave and Patrick Cousot},
  title     = {The analytic semantics of weakly consistent parallelism},
  booktitle = {Symposium on ``Programming: Logics, Models, Algorithms and Concurrency'',
               Jayadev Misra’s Fest, Austin, TX, USA, April 29-30, 2016.},
  year      = {2016},
  publisher = {{Department of Computer Science The University of Texas at Austin}},
  url       = {http://www.cs.utexas.edu/symposium/},
}

\bibitem{JayadevMISRAFest2016}
Jade Alglave and Patrick Cousott.
\newblock The analytic semantics of weakly consistent parallelism.
\newblock In \emph{Symposium on ``Programming: Logics, Models, Algorithms and Concurrency'',
          Jayadev Misra’s Fest}, Austin, TX, USA, April 29-30, 2016.

copyright notice
Last modified: Fri Apr 29 11:47:53 CDT 2016