CS766 : Analysis of concurrent programs 2023

Instructors : Ashutosh Gupta and S. Krishna

Timings : Monday 11:35, Tuesday 8:30, Thursday 09:30(Slot 4)
Venue : CC105

Interaction policy

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

• Weekly quiz: 10%
• Quiz : 10%
• Presentation/Assignment: 10%
• Midterm : 20% (2 hours)

May change later.

Lectures

Principles of verification

2023-01-03T11:35 : Week1 - Introduction to course and program semantics

• First meeting on Tuesday 2023-01-03T11:35 at CC103
• Introduction to verification, and course content
• A simple language, small step semantics, big step semantics
• slides

2023-01-09 : Week 2 - strongest post(sp), weakest pre, and Hoare logic

• program staements as formulas, aggregate semantics (strongest post)
• least fixed point, strongest post for loops
• weakest pre(wp), Hoare logic
• slides strongest post
• slides weakest pre
• Suggested reading : Wikipedia on wp and sp

Verification methods : Road to CEGAR

2023-01-16 : Week 3+ Invariants, Abstraction, CEGAR

• labelled transition system, path constraints, invariants, Verifast tool
• Abstraction, CEGAR
• Invariants slides
• Abstraction slides
• CEGAR slides

2023-01-25T08:30 (Wednesday) : Quiz 1

Concurrenct program analysis

2023-01-28 : Week 4-5 - Intro to Concurrency and Traces

• Issues in concurrency
• Understanding mutual exclusion
• Correctness properties and their proofs
• Modelling concurrency, happens before relations
• Formal definition of traces
• Analyzing Peterson mutual exclusion protocol using traces
• Introduction slides
• Traces slides
• Suggested reading : Shavit chapter 1 and 2

2023-01-31 : Quiz 1

• Quiz 1 on basics of verification
• Open slides; no internet; no small devices; bring a loptop with charged battery

2023-02-06 : Week 6 - Bounded model-checking(BMC) of concurrent programs, Proof system

• Basics of BMC
• BMC for concurrent programs
• Owicki-Gries proof system
• BMC slides
• Owicki slides

2023-02-05T11:00 : Student prsentations

	Student	Date	Protocol
1	Supriya Bhide	2023-02-05	Bakery
2	Pranjal*	2023-02-05	Dekker
3	Namrita	2023-02-05	Szymanski
4	Shreya*	2023-02-05	Dijkstra
5	Ranjan*	2023-02-05	Burns
6	Kumar Shaswat	2023-02-05	Lamports

• Presentation should include: the protocol, correctness arguments, n-thread version, and discussion about the cost of the protocol
• Presentation should not exceed 15 mins
• The following students to prove correctness of the following protocols using NuSMV

	Student	Submission date	Protocol
7	Jawaad		Lamport
8	Jeel Manishbhai Nathani		Dekker
9	Aman Singh		Szymanski
10	Vatsal		Dijkstra
11	Rishabh		Bakery
12	Aastik		Burns
13	Akshit		Lamport
14	Ayush Kumar Singh		Dekker
15	Aniket Agarwal		Szymanski
16	Suraj Munjani		Dijkstra
17	Abhay		Bakery
18	Anmol		Burns
19	Osim		Dijkstra

• Please write buggy versions of the programs to find counterexamples; Try as many threads as possible.
• Please write n-thread versions of the algorithms also. There will be marks for creative experiments
• Submission due date: 2023-02-09

2023-02-13 : Week 7 - Concurrent objects and linearizability

• Concurrent objects slides
• Thomas wies slides 3(30-102)
• Example of linearizability slides
• Thomas wies slides 6(1-183) (could not finish the topic in the class)
• Suggested reading : Shavit chapter 3

2018-02-22 : Midterm week

• Open slides, any book, or paper; STRICTLY no internet; STRICTLY no small devices; bring a loptop with charged battery
• Download everything in your device before hand!
• Solution of Q5

2023-02-18 Handover to Krishna (1 lecture before midterm)

Last modified: ()