MODELS FOR CONCURRENCY

Spring 2014

Lecture notes taken by students.
General information on the course.
Course meetings: Monday 10-12 205/34, Wednesday 18-20 123/90
Office: Alon, 204.
If you want to discuss course material, come anytime, just check that I am in my office. (6472711).

Lectures, announcements, exercises, reading material etc.

1) First lecture: an introduction, about modelling, and a painting by Matisse.

2) First exercise, about the notions of states and invariant. You have to prove the correctness of the Insertion Sort algorithm.
It is necessary to file in the missing proofs in the following latex file, and to submit the pdf of your work.
Do not forget to add your name to the \author part. Here is the latex file.

3) The material for the week of 9.3.2014:

A simple ping-pong algorithm for two processes.
Do the exercise when you can, it is not for submission, but I expect you to know how to do it. Here is the latex file.

4) For the week of 16.3.2014

5) A short introduction to Logic.
Read this material, and pay especiall attention to the notion of structure isomorphism.

6) The notion of multisorted structures is particularly important for us in this course. Please read the following material. And do Exercises 0.5 and 0.6 (due April 4).
Here is the Latex file.

7) The example is very important. Please read and understand the proofs.

8) EXERCISE three. Another interesting example for a correctness proof that is based on the notion of states and history is in the following pdf file on concurrent buffer. The corresponding latex file is here. Do exercises 2.1 and 2.3. Date Due: Wed. 23 May.

9) The notion of time-representation is very important. This is the topic of the week of 31 March. My lectures on Time contain more material than presented in class. I suggest that you read section 3, understand the Russell-Wiener property, do Exercise 3.9, read the proof in 3.1, understand the finiteness conditions, and read Theorem 3.23 if you are mathematical inclined.

10) In our lectures of April 7 and 9 we spoke about system executions and the different types of registers. Please read this material and do the exercises (but do not submit them).

11) The material for the midterm (2 May 2014) Two ways to prove the mutual exclusion of Peterson's algorithm The automaton chart doesn't come well in the pdf file, so here is the Latex file. If you generate the dvi file, the chart comes well. You need the mutex latex file to represent the automaton.

12) Exercise 4 is optional: if you do it, its grade can only improve your midterm grade by taking the average. Latex file. If you generate the dvi file, the chart comes well. You need the mutex latex file to represent the automaton.

13) Exercise 5 is about the ABD algorithm. (Register simulation). You may want the latex file for your answer. Submission date is May 26.

14) Exercise 6. Read the lecture notes on the snapshot algorithm, and do the three exercises 1-3. pdf file. The latex file is here. Submission is 15 June.

15)The last topic in the course is about the question of agreement. Please read the following introduction to consensus.
Then read about the synchronous consensus algorithm.

Material for the final exam:

Different notions that were defined in the course. You have to know their definitions and how to employ them. For example, states, histories, invariants. Linearizability. Tarskian system executions (moment based and event based) etc.
You have to understand how to use formal first order language in order to specify statements about distributed systems. I can give some properties in plain English and ask you to write them in a formal way in some logical language.
Item 3 in the list above (A simple ping-pong algorithm for two processes.
Item 7 above. How to specify queues and stacks.
Item 9 On Time. There is a lot of material in this article, but you have to know only the following. Notions of Interval ordering, representation of a partial ordering into an interval ordering, the Russell--Wiener property (Definition 3.5), Theorem 3.6 (and its proof as given there with maximal antichains) Exercise 3.9. You have to understand Theorem 3.22 and how to use it, but I will not ask for its proof.
Item 10: about the specification with sysem executions of different types of registers: safe, regular, serial, atomic (within the framework of linearizability).
Item 13 The ABD algorithm.
I will not ask about the FLP impossibility result. From consensus you have to know only the synchroneous algorithm from item 15 above.

The take-home exam. pdf file. The latex file is here. Submission is after the university resumes its activities and any time before the end of moed aleph.