Skip to content

Latest commit

 

History

History
141 lines (104 loc) · 5.02 KB

README.md

File metadata and controls

141 lines (104 loc) · 5.02 KB

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.