J. Alglave & P. Cousot, IFIP-WG 2.3 Château de Villebrumier meeting, 2—7 September 2016, Château de Villebrumier, France

Jade Alglave and Patrick Cousot.
Semantics and invariance proof method for weakly consistent parallelism.
IFIP-WG 2.3 Château de Villebrumier meeting, 2—7 September 2016, Château de Villebrumier, France.
Abstract of the 50 mn talk : We introduce a hierarchy of semantics of weakly consistent parallelism and provide more details on analytic semantics where communications are separated from states and events and communicated values are recorded by Pythia variables. A sound and complete invariance proof method for weakly consistent parallelism is derived by calculational design by abstraction of this semantics. We show how the weakest hypotheses on weak consistent for the program to be correct can be formulated by a communication invariant derived from the program specification. We then show that a stronger correctness condition implying the communication invariant can be formulated in a weak consistency modelling language such as cat. This may introduce incompleteness since e.g. the notion of cut might not be exactly expressible or because too strong fences may have to be introduced. The proof method is illustrated by Peterson mutual exclusion algorithm
Slides: 2016-10-03-WG23-AlglaveCousot.pdf.

Bibliography (to reference the talks):

\bibitem{Cousot03-WG-2-3-Villebrumier}
J{.} Alglave and P{.} Cousot.
\newblock Semantics and invariance proof method for weakly consistent parallelism.
\newblock IFIP WG 2.3 metting, 2—7 September 2016, Château de Villebrumier, France.

@unpublished{Cousot03-WG-2-3-Villebrumier,
   author = {J{.} Alglave and P{.} Cousot},
   title  = {Semantics and invariance proof method for weakly consistent parallelism},
   note   = {IFIP WG 2.3 metting, 2—7 September 2016, Château de Villebrumier, France},
}

copyright notice.
Last modified: Sun Sep 24 10:42:49 EST 2016

Sunday, 27-Nov-2016 10:48:33 EST