CS766 : Analysis of concurrent programs 2021

Instructors : Ashutosh Gupta and S. Krishna

Timings : 17:30 Tuesday and Friday
Venue : MSTeams, To join the course team, use team code: s1kvq03

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

Model checking : Road to CEGAR

2021-01-08/12 : Lecture 1 - Introduction to course and program semantics

• Introduction to verification, and course content
• A simple language, small step semantics, big step semantics
• slides

2021-01-15 : Lecture 2 - strongest post

• slides

2021-01-19 : Lecture 3 - weakest pre and Hoare logic

• slides
• Suggested reading : Wikipedia on wp and sp

2021-01-22 : Lecture 4 - Invariants

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

2021-01-30 : Lecture 5 - Abstraction

• slides

2021-01-02 : Lecture 6 - CEGAR

• slides

Concurrency

2021-02-05 : Lecture 7 - Intro to Concurrency

• Issues in concurrency
• Modelling concurrency, happens before relations
• Correctness properties and their proofs
• Peterson mutual exclusion protocol
• Thomas wies slides 1(slide 15-93)Thomas wies slides 2 (slide 8-76)
• my slides
• Suggested reading : Shavit chapter 1 and 2

2021-02-09 : Lecture 8 - Mutual exclusion protocols

• Student prsentations

	Student	Date	Protocol
1	Darshana Ajit Nafde	2021-02-09	Bakery slides
2	Kulkarni Shantanu	2021-02-09	Dekkerslides
3	Karnika Shivhare	2021-02-09	Szymanskislides
4	Tushar Dhawal Baranwal	2021-02-09	Dijkstraslides
5	Shubham Raju Chaudhari	2021-02-09	Burnsslides
6	Prafulla Santosh Patil	2021-02-12	Lamportsslides

• 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 due date	Protocol
7	Yash Sharma	2021-02-12 (submitted)	Lamport
8	Naman Dixit	2021-02-12 (submitted)	Dekker
9	Kunal Krishna	2021-02-12 (submitted)	Szymanski
10	Saksham Goel	2021-02-12 (submitted)	Dijkstra
11	Sai Sidharth Naik Azmir	2021-02-12 (submitted)	Bakery
12	Patnala Rohit Keerti Teja	2021-02-12 (submitted)	Burns
13	Amadala Saroj Raj	2021-02-12	Lamport
14	Sai Mohit Korabu	2021-02-12 (submitted)	Dekker
15	Nitin Devendra Sisodiya	2021-02-12 (submitted)	Szymanski
16	Ashwani Kumar Yadav	2021-02-12	Dijkstra
17	Shubhamkar Bajrang Ayare	2021-02-12 (submitted)	Bakery
18	Halavath Kalyan Kumar	2021-02-12	Burns

• Please write buggy versions of the programs to find counterexamples; Try as many threads as possible.

2021-02-12 : Lecture 9 - Concurrent objects

• Thomas wies slides 3(1-102)
• Suggested reading : Shavit chapter 3

2021-02-16 : Lecture 10 - Lock-free concurrent objects

• Thomas wies slides 6(1-183)
• Student prsentations

	Student	Date	Concurrent object
19-20	Aayush Sharma and Aviral singh	2021-02-16	Lazy set (slides)
21	Pooja Verma	2021-02-16	Herlihy & Wing Queue (presented in section 4.2) (slides)
22	Aditya	2021-03-05	Elimination stack (slides)
23	Gurudatta Balkrushna Patil	2021-03-05	Non-blocking Michael-Scott queue(slides)
24	Ishit Kulshreshtha	2021-03-05	Time stamped stack(no slides)

Verification of concurrent programs

2021-02-19 : Lecture 11 - Proof systems for concurrent programs

• Owicki-Gries
• slides

2018-02-24 : Midterm week

2021-03-04 : Lecture 12 - Bounded model-checking of concurrent programs

• slides

Activity 2

• You may either choose to present a paper or do a project in groups of two.
• Choose a concurrency paper from last five years of CAV/POPL/CONCUR/TACAS/FMCAD conferences or their workshops
• No weak memory paper; you are yet to learn that
• If interested in a project, please arrange a meeting.
• Deadline : before final grade submission
• Let me know your choice before 2020-03-09
• Paper reading/project

	Student	Date of submission/presentation	Topic
1	Ayush Sharma	2021-03-09	Exploiting Synchrony and Symmetry in Relational Verification, CAV18

Krishna will start from 2021-03-08

Last modified: ()