CS766 : Analysis of concurrent programs 2020

Instructors : Ashutosh Gupta and S. Krishna

Timings : 14:00 Monday and Thursday
Venue : CC105

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%
• Presentation 1: 10%
• Midterm : 20% (2 hours)
• Presentation 2/assignment: 10%

May change later.

Lectures

Introduction

2020-01-16 : Lecture 1 - Introduction to course and program semantics

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

Model checking : Road to CEGAR

2020-01-20 : Lecture 2 - strongest post

• Strongest post
• Hoare logic
• slides

2020-01-23 : Lecture 3 - weakest pre

• Weakest pre, Hoare logic
• Hoare logic slides
• Suggested reading : Wikipedia on wp and sp

2020-01-27 : Lecture 4 - Invariants

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

2020-01-30 : Lecture 5 - Abstraction

• slides

2020-02-03 : Lecture 6 - CEGAR

• slides

Concurrency

2020-02-06 : 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 1Thomas wies slides 2
• Suggested reading : Shavit chapter 1 and 2

2020-02-10 : Lecture 8 - Mutual exclusion protocols

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

	Student	Date	Protocol
-	Swapna Sarit Ojha	(no show)
-	Srikanth Gollavilli	(no show)
1	Kalpit Veerwal	2020-02-10	Bakery

• Presentation should include: the protocol, correctness arguments, n-thread version, and discussion about the cost of the protocol
• Presentation should not exceed 15 mins

2020-02-13 : Lecture 9 - Mutual exclusion protocols II

• Student prsentations

	Student	Date	Protocol
2	Tuppe Omkar Vijaykumar	2020-02-13	Dekker
3	Edubilli Praneeth	2020-02-13	Szymanski
4	Rasesh Tongia	2020-02-13	Dijkstra
5	Prateek Agarwal	2020-02-13	Burns
6	Mohammad Afzal	2020-02-17	Lamport

• Student to prove correctness of the following protocols using NuSMV

	Student	Submission due date	Protocol
7	Swaril Singhal	2020-02-20	Lamport
8	Ravikant Kumar Yadav	2020-02-20	Dekker
9	Nitesh Singh	2020-02-20	Szymanski
10	Sahil Mukund Patki	2020-02-20	Dijkstra
11	Nipun Mittal	2020-02-20	Bakery
12	Kaushik Bhalchandra Ganorkar	2020-02-20	Peterson
13	Mudra Sahu	2020-02-20	Burns

• Please also feed a buggy version of protocol and observe the output of the tool
• Students will visit my office to present their solution

2020-02-17 : (cancelled)

2020-02-20 : Lecture 10 - Concurrent objects

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

2018-02-24 : 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!

2020-03-02 : Lecture 11 - Lock-free concurrent objects

• Student prsentations

	Student	Date	Concurrent object
14	AKKABATHULA ABHISHEK	2020-03-02	Non-blocking Michael-Scott queue
15	CHINTHAREDDY SAI CHARITH REDDY	2020-03-02	Lazy set
16	Bhala Basant Kumar	2020-03-02	Herlihy & Wing Queue (presented in section 4.2)

Verification of concurrent programs

2020-03-04 : Lecture 12 - Proof systems for concurrent programs

• Student prsentations

	Student	Date	Concurrent object
17	Karan Kumar	2020-03-04	Elimination stack
18	Farheen Bano	2020-03-04	Treiber Stack

• Proving via CAVE

	Student	Due Date	Concurrent object
19	GUNDA NIKHIL SAMRAT	2020-03-05	Proving linearizability of Triber stack

• Owicki-Gries and Rely-Guarantee
• Francesco Zappa Nardelli slides from 8 to 45

2020-03-12 : Lecture 13 - Bounded model-checking of concurrent programs

• Student prsentations

	Student	Date	Verification method
--	Ashutosh Gupta		Symbolic Predictive Analysis for Concurrent Programs
20	Neeladrishekhar Kanjilal	(no show)	Cseq
21	Durgam Nikhil	2020-03-12	Context-bounded analysis
22	GODBOLE ADWAIT AMIT	2020-03-12	Local linearizability

Presentation 2/Project

• 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 visit my office.
• Deadline : before final grade submission
• Let me know your choice before 2020-03-09
• Paper reading/project

	Student	Date of submission/presentation	Topic
1	Prateek Agarwal		Exploiting Synchrony and Symmetry in Relational Verification, CAV18
2	Tuppe Omkar Vijaykumar		Proving Linearizability Using Forward Simulations, CAV 17
3	Sahil Mukund Patki		A program logic for concurrent objects under fair scheduling, POPL 16
4	Rasesh Tongia		Project: Animating linearizations of Herlihy & Wing Queue
5	Mudra Sahu
6	Mohammad Afzal		On the Completeness of Verifying Message Passing Programs Under Bounded Asynchrony, CAV 18
7	Nipun Mittal		Reachability Analysis for AWS-Based Networks, CAV 19
8	Ravikant Kumar Yadav		Project: Controlling cores of ARM cores
9	Nitesh Singh
10	Kalpit Veerwal		Selective Monitoring, CONCUR 2018
11	Swaril Singhal		Project : topic to be decided?
12	Farheen Bano
13	Kaushik Bhalchandra Ganorkar		Progress of concurrent objects with partial methods, POPL 2017
14	Durgam Nikhil		Project : demonstrate weak memory behavior in ARM/Intela
15	Bhala Basant Kumar
16	GODBOLE ADWAIT AMIT
17	Karan Kumar
18	Edubilli Praneeth
19	GUNDA NIKHIL SAMRAT
20	CHINTHAREDDY SAI CHARITH REDDY
21	AKKABATHULA ABHISHEK
22	Neeladrishekhar Kanjilal

Krishna will start from 2020-03-12

Last modified: ()