CS766 : Analysis of concurrent programs 2022

Instructors : Ashutosh Gupta and S. Krishna

Timings : 19:00 Tuesday and Friday
Venue : Online. MSTeams, To join the course team, use team code: b7kp78n

Interaction policy

• Live lectures for first six lectures
• Detailed slides updated in advance

Source material

• Survey: Software model checking
• Book: Model Checking Clarke, Grumberg and Peled
• The Art of Multiprocessor Programming by Nir Shavit
• Text: Lattice theory for computer science Hilary A. Priestley
• Abstract interpretation
• The Art of Multiprocessor Programming by Nir Shavit
• Book: Theory of Linear and Integer Programming, Alexander Schrijver
• Various papers

Evaluation structure

• Quiz : 10%
• Activity 1 : Presentation 1/assignment: 10%
• Activity 2 : Paper presentation/assignment/Class participation (marking policy 10 - Highly active; 8 - Often; 6 Active; 2 Rare) : 10%
• Midterm : 20% (2 hours)

May change later.

Lectures

Principles of veriication

2022-01-07 : Lecture 0/1 - Introduction to course and program semantics

• First meeting on Monday 17:05-17:55@2022-01-03
• Please join MSTeams to get the link for the first meeting
• Introduction to verification, and course content
• A simple language, small step semantics, big step semantics
• slides

2022-01-11 : Lecture 2 - strongest post(sp)

• program staements as formulas, aggregate semantics (strongest post)
• least fixed point, strongest post for loops
• slides

2022-01-14 : Lecture 3 - weakest pre and Hoare logic

• weakest pre(wp), Hoare logic
• slides
• Suggested reading : Wikipedia on wp and sp

Verification methods : Road to CEGAR

2022-01-18 : Lecture 4 - Invariants

• labelled transition system, path constraints, invariants, Verifast tool
• slides

2022-01-21 : Lecture 5 - Abstraction

• slides

2022-01-25 : Lecture 6 - CEGAR

• slides

Concurrenct program analysis

2022-01-28 : Lecture 7 - Intro to Concurrency

• Issues in concurrency
• Understanding mutual exclusion
• Correctness properties and their proofs
• slides
• Suggested reading : Shavit chapter 1 and 2

2022-02-01 : Lecture 8 - Analyzing concurrency: Traces

• Modelling concurrency, happens before relations
• Formal definition of traces
• Analyzing Peterson mutual exclusion protocol using traces
• slides
• Suggested reading : Shavit chapter 1 and 2

2022-02-04 : Lecture 09 - Bounded model-checking(BMC) of concurrent programs

• Basics of BMC
• BMC for concurrent programs
• slides

2022-02-08 : Lecture 10 - Proof system

• Owicki-Gries
• slides

Concurrent objects and linearizability

2022-02-12 : Lecture 11 - Concurrent objects

• slides
• Suggested reading : Shavit chapter 3

2022-02-12 : Lecture 11 - Linearizability

• Thomas wies slides 3(1-102)

Last modified: ()