Formal Methods Seminar, Fall'22

Guiding theme: weak consistency

Schedule

We meet Tuesdays, 11am, in room 527, 60FA.

Date	Speaker	Topic
Sep 8		Organizational Meeting
Sep 15	Chaitanya Agarwal	Talk PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games
Sep 22	Adam Chen (Stevens)	Talk Veracity: Declarative Multicore Programming with Commutativity
Sep 29	Stefan Leue (Uni. of Konstanz)	Talk Checking Legal Contracts and Repairing Neural Networks
Oct 6	Sebastian Wolff	A.1 Sequential consistency
Oct 13	Zach Destefano	A.2 TSO: Modeling - TSO intro
Oct 20	Nisarg Patel	A.2 TSO: Modeling - TSO characterization
Oct 27	Jacob Salzberg	A.2 TSO: Verification
Nov 3	Daniel Feldan	A.4 Axiomatic models
Nov 10	Devora Chait-Roth	A.3 Promising semantics
Nov 17	Ekanshdeep Gupta	B Non-persistent TSO
Nov 24		Thanksgiving
Dec 1	David Naumann (Stevens)	Talk Towards algebraic foundations for alignment
Dec 8
Dec 15	Kishor Jothimurugan (UPenn)	Talk Specification-guided Reinforcement Learning

Topics

A. Weak Memory Models

• Nagarajan, Sorin, Hill, Wood: Introduction to Consistency and Coherence. Chapter 1 of A Primer on Memory Consistency and Cache Coherence. Springer, 2020.
  [PDF]

A.1. Sequential Consistency (SC)

• Lamport: How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Progranm. IEEE Transactions on Computers, 1979.
  [PDF]

• Nagarajan, Sorin, Hill, Wood: Memory Consistency Motivation and Sequential Consistency. Chapter 3 of A Primer on Memory Consistency and Cache Coherence. Springer, 2020.
  [PDF]

• Lamport: Time, Clocks, and the Ordering of Events in a Distributed System. Communications of the ACM, 1978.
  [PDF]

A.2. Total Store Ordering (TSO)

Modelling

• Nagarajan, Sorin, Hill, Wood: Total Store Order and the x86 Memory Model. Chapter 4 of A Primer on Memory Consistency and Cache Coherence. Springer, 2020.
  [PDF]

• Adve, Hill: A Unified Formalization of Four Shared-Memory Models. IEEE Transactions on Parallel and Distributed Systems, 1993.
  [PDF]

• Owens: Reasoning about the Implementation of Concurrency Abstractions on x86-TSO. ECOOP, 2010.
  [PDF]

• Sewell, Sarkar, Owens, Zappa Nardelli, Myreen: x86-TSO: A Rigorous and Usable Programmer’s Model for x86 Multiprocessors.
  [PDF]

Verification

• Atig, Bouajjani, Burckhardt, Musuvathi: On the Verification Problem for Weak Memory Models. POPL, 2010.
  [PDF]

• Bouajjani, Meyer, Möhlmann: Deciding Robustness against Total Store Ordering. ICALP, 2011.
  [PDF]

• Bouajjani, Derevenetc, Meyer: Checking and Enforcing Robustness against TSO. ESOP, 2013.
  [PDF]

A.3. C11

• Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, Derek Dreyer: A promising semantics for relaxed-memory concurrency. POPL 2017. [pdf]

• Ori Lahav, Nick Giannarakis, Viktor Vafeiadis: Taming release-acquire consistency. POPL 2016. [pdf]

A.4. Axiomatic Memory Models

• Alglave, Maranget, Tautschnig: Herding cats: Modelling, Simulation, Testing, and Data-mining for Weak Memory. TOPLAS 2013. [PDF]

• Alglave, Maranget, Sarkar, Sewell: Fences in Weak Memory Models. CAV 2010. [PDF]

• Alglave. A formal hierarchy of weak memory models. FMSD 2012. [PDF]

B. Non-volatile Memory

• Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar: Deciding reachability under persistent x86-TSO. POPL, 2021 [PDF]

C. Relaxed Consistency in Distributed Systems

TBA.