B649 (Spring 2000)
Principles of Concurrent Systems

Instructor

Scott Stoller

Table of Contents

Hours
Course Description
Readings
Project
Homework Guidelines
Announcements
Grading
Grading Statistics
On-line Course Evaluation

Hours

Lectures: Tue and Thu, 2:30pm - 3:45pm, Ballantine Hall 215.

Office Hours: Tue and Thu, 3:45am - 4:45pm. Lindley Hall 201C.

Section: 1418

Course Description

This course is about concurrency, including multithreaded processes and distributed systems. The focus is on techniques and tools for producing correct concurrent software. Links to some research projects on this topic are included below. We will read papers from those projects and others. The course will be relatively self-contained. Some experience with concurrent programming (e.g., from P536) is desirable. The course will include introductions to program analysis and model checking. Prior knowledge of those topics is helpful but unnecessary; willingness to learn about those topics is essential.

Static program analysis can find common classes of concurrency-related errors, such as race conditions (caused by inappropriate locking) and deadlocks. The FLAVERS tool is a good example of this approach. Other examples: Types for Safe Locking, by Cormac Flanagan and Martin Abadi; Type-Based Race Detection for Java, by Cormac Flanagan and Stephen Freund (LICS '2000).

Testing tools monitor system executions, looking for errors. A good example of this is: Stefan Savage et al., "Eraser: A dynamic data race detector for multi-threaded programs", ACM Transactions on Computer Systems (TOCS), 15(4):391-411, November 1997.

Systematic testing tools explore all possible schedules (interleavings) of the threads and processes in a concurrent system. Two approaches to this are:

Logics for concurrency can be used to prove (manually or with the help of a theorem proving system, such as PVS) that a concurrent program satisfies its requirements. I plan to talk either briefly or not at all about this approach, but I would consider talking about it more if the class is interested.

The overlap with all previous B649s is relatively small.

Readings

Most of the readings will be conference or journal articles. As far as I know, no appropriate textbook exists.

Project

Students will do a course project. One or more suggestions will be made; students are encouraged to suggest their own projects as well. Projects may be theoretical or implementation-oriented (ideally both!).

Homework Guidelines

By default, assignments in this course are due by the end (midnight) of the specified day. To submit a problem set, either email it to b649@cs.indiana.edu or put hardcopy under the door of LH 201C or in the homework drop box near LH 215. If you use the homework drop box, put the instructor's name prominently on the first page, so the staff knows to whom to give your submission.

Grading

Here is a tentative list of weights. It is subject to adjustments, based on the number of homeworks, when we get started on the project, etc.
Project35%
Exams (midterm+final)30%
Homeworks35%

Statistics

The following statistics and histograms may be slightly inaccurate, due to late submissions, score adjustments, etc.

Item Mean Std.Dev. Histogram
hw1 (out of 10) 9.4 0.8
hw2 (out of 10) 9.2 0.4
hw3 (out of 10) 7.6 1.2
hw4 (out of 10) 5.3 2.1
hw5 (out of 10) 8.8 0.6
hw6 (out of 10) 8.6 1.7
hw7 (out of 10) 7.2 0.4
midterm (out of 40) 31.8 (79%) 3.9 histogram

Announcements

Apr 27

Hw8: Part 2 of the solution to hw8 (namely, a proof of Thm 3') is now available in a revised version of TR536. The proof appears at the end of the Appendix.

Apr 26

CS Eval: Deadline for submitting your evaluation is May 5.

Apr 13

Project: If you finish a piece of your module before Apr 19, you are encouraged to post an announcement on the course newsgroup, describing where it is and what it does. This might be useful to the other teams.

Apr 12

Web Page: In case you are interested, more papers about JPF are available via the JPF Home Page.

Virtual Handout: If you didn't receive a copy of this paper in class yesterday, please print it: Applying Model Checking in Java Verification.

Apr 11

Course Eval: Please fill out the On-line Course Evaluation. I put a link to it in the Table of Contents so you can easily find it later. Your comments and suggestions would be greatly appreciated. If you fill out the evaluation and then change your mind, you can revise your answers later.

Apr 10

Project: I revised section 8.12, as per my email message. You can print section 8.12 by itself, or you can re-print the entire document (I just updated tool.ps.gz).

Project: I added a new section 8.12. Please read it before doing any more coding! Comments and suggestions are welcome. You can print section 8.12 by itself, or you can re-print the entire document (I just updated tool.ps.gz). Section 9 has been revised to indicate that responsibility for turning the pseudo-code in section 8.12 into real code is part of module1 (sorry, Sean and Sriram).

Project: Sorry, I think I updated the files incorectly yesterday. The"new" version should have the date 9 Apr or 10 Apr at teh top; if the version you printed says 7 Apr, please re-print.

Apr 9

Project: Please print new version of Implementation of Testing Tool .... Most of the changes are in sections 2.1, 8.2, and 8.3. Also, there is a new section 8.11 that describes a proposed format for the annotation file. Please read those sections carefully.

Apr 7

Project: Please print new version of pages 2-4 of "Implementation of Testing Tool ...", on the meaning of method granularity. You can reprint all of Implementation of Testing Tool for Concurrent Java Programs if you want, or you can wait until I finish the revisions (mainly of section 8.3).

Apr 6

Project: Please print new version of page 22 of "Implementation of Testing Tool ...". Note that these new pages supplement (not replace) pages from the printout of Mar 30.

Virtual Handout: Partial Solution to Homework8 is now available. "Partial" means that there is a solution to prob2 but not prob1.

Apr 5

Project: Please print new versions of page 23 and page 25 of "Implementation of Testing Tool ...".

Project: I suggested in class yesterday changing this.si to this.getSharedInfo() in the arguments of checkMLD in wrappers for instance methods. I recant that suggestion. For people who were not in class yesterday, in the wrapper for run methods in secton 8.5, change super.start to super.run.

Mar 29

Project: Please read the revised version of Implementation of Testing Tool for Concurrent Java Programs.

Mar 27

Project: Please read Implementation of Testing Tool for Concurrent Java Programs.

Mar 20

Project: addfield.java and addmethod.java are in ~stoller/projects/po-mutex-dis .

Mar 20

Virtual Handout: Homework8 is now available. Printouts of the JavaClass manual (~stoller/public/JavaClass/docs/javaclass-report.ps.gz) will be distributed in class tomorrow.

Mar 19

Project: This week we will start discussing how to implement the framework described in TR 536 for model-checking of Java programs. Implementing such a system (or at least a well-defined fragment of one; details later) will be the suggested project. People who have other ideas for projects should submit a rough draft of a project proposal by Monday, 27 Mar; I recommend that you discuss your ideas with me first, if you haven't already (please stop by during office hours, or email me for an appointment).

Mar 15

Virtual Handout: Solution to Midterm is now available.

Mar 13

Grading: Grading statistics have been added above.

Mar 7

Exam: The midterm is open everything. Bring copies of the course handouts, including the 4 papers we discussed.

Virtual Handout: Solution to Homework7 is now available.

Mar 2

Virtual Handout: I corrected some incorrect reasoning in the proof of Theorem 4, specifically, in the proof that s'i+1 is visible.

Virtual Handout: Solution to Homework6 is now available.

26 Feb

Virtual Handout: Today I revised the statement and proof of Theorem 2' of "Model-checking multi-threaded ...", so you might want to print new versions of page 15 and page 20.

24 Feb

Virtual Handout: Homework7 is now available.

23 Feb

Grading: I added some info about Grading.

Midterm: We'll have a midterm on Mar 9 (the Thu before spring break). It will be worth about 15% of the course grade.

21 Feb

Virtual Handout: Here is a Solution to Homework5.

Postponement: Due date of hw6 is postponed to 29 Feb.

17 Feb

Virtual Handout: Homework6 was distributed on 17 Feb.

14 Feb

Virtual Handout: Here is a Solution to Homework4.

10 Feb

Virtual Handout: Homework5 was distributed by email on 10 Feb.

Virtual Handout: Here is a Solution to Homework3.

1 Feb

Virtual Handout: Homework4 was distributed by email on 1 Feb.

Virtual Handout: Here is a Solution to Homework2.

28 Jan

Virtual Handout: Here is a Solution to Homework1.

27 Jan

Virtual Handout: Homework3 was distributed by email on 27 Jan.

25 Jan

URL: The link under 20 Jan points to the first edition of the JVM spec, from which the list of JVM instructions has been removed. After clicking on that link, click on the "second edition" link near the top of the page. Here is a direct link to the second edition.

24 Jan

Virtual Handout: Homework2 was distributed by email on 20 Jan. It is due on 27 Jan.

20 Jan

Reading: You should be finishing reading the paper about Eraser. After that, start reading the handout from Bruening's M.S. thesis (the "ExitBlock paper"); I forgot to put his name on this handout. Also, please bring that handout to the next few classes, since we will be discussing it.

Homework: I added some homework guidelines above.

URL: The JVM spec is available via JDK 1.2 Docs.

13 Jan

Handouts: Homework1.

12 Jan

Handouts: There were 3 handouts on 11 Jan: Eraser, VeriSoft, and part of Bruening's M.S. thesis. If you didn't get them, they are available in a box outside my office door.