Ogre and Pythia, An invariance proof method for weak consistency models
We design an invariance proof method for concurrent programs parameterised by a weak consistency model. This generalises Lamport/Owicki-Gries methods for sequential consistency. The calculational design of the proof method by abstract interpretation of a truly parallel semantics with separate communications restricted by a communication specification ensures soundness and (relative) completeness. We use the cat language to write specifications of consistency models as well as concurrent program specifications. We show how to design minimal program-specific communication specifications ensuring correctness which can be ported to different architectures by refencing.
Wed 18 Jan Times are displayed in time zone: (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
|10:30 - 10:55|
|10:55 - 11:20|
|11:20 - 11:45|
|11:45 - 12:10|