In this course, the textbook plays an important role, and the lectures will be keyed to it whenever possible. We will use slides from the book as well as slides of our own. These will not in general be available before the lecture, as the content of each lecture is decided dynamically depending on classroom discussions, Many of these discussions will use the blackboard.
It is therefore important that you bring a notebook and make your own notes, and that you understand that the slides are in no sense "lecture notes", or any kind of substitute for the textbook or even for the lectures. Slides are visual aides for the lecture, that is all. After the lecture, they may help you remember what was discussed.
In order to get an idea of the material we will cover in the course you can have a look at the lectures in previous editions of the course.
Today we spent 30 mins on the practicalities of the course. Next, we looked at parallelism in music, concurrency in cinema, and looked at logical or physical stories/themes/motifs, as well as how time holds everything together, or is at least the dimension in which everything exists. We looked at how to deal with the absence of sensible debugging in concurrent programs.
The lecture notes are available in the post "Partial lecture notes - Lecture 21st Jan" in the google group of the course.
We spent half the lecture on an introduction to functional programming, together with a study of what "variables" mean in mathematics and imperative programming. The reading plan from the textbook is
Chaps from Ben-Ari (for 21, 23, and 26 Jan)
Today we spent a lot of time with slides from the textbook, from Sections 2.2, 2.5, 2.12, 2.13, 3.1, 3.2, 3.3, 3.4, 3.5 and 6.1.
Reading notes: Try to read all of Chap 1 and Chap 2 now, and do the exercises. We will return to Chap 3, but the immediate need to read ahead is from Chap 6.
I may send out a few lecture notes, but even if I do, they will not be voluminous, as the textbook provides the needed reading material.
The lecture notes are available in the post "Lecture notes - Lecture 23rd Jan" in the google group of the course.
Sections from the textbook:
a. Recently covered in lectures: 3.1 -3.6, 6.1 - 6.4
b. Upcoming: 6.5 - 6.7, 6.9, 7.1 - 7.10 (week starting Mon 2 Feb)
You should now be able to read Chap 8.1 through 8.4. We will cover the rest of Chap 8, and all of Chap 9 soon.
Starting next week, we will make a second pass through the book, covering the bits we missed: the latter part of Chap 3, all of Chap 4, part of Chap 5, and the more formal proofs in Chaps 6 through 9.
We will also do a tutorial on SPIN/Promela. and use them as teaching aids. But they are not part of the exam material, nor is broadcast communication.
The lecture notes are available in the post "Lecture notes - Lecture 9th Feb" in the google group of the course.
Plans for Monday: SPIN/Promela tutorial (Chaps 2 - 4 in the book, examples from all chapters 1 - 9). Wednesday: Linda (Chap 9), maybe more channel stuff (Chap 8).
General plan for remaining lectures: finish Chaps 3, then do 4 and a bit of 5. Do examples.
Please see the Google post of 11 Feb, entitled The lecture Q&A thread.
Today, we did several small examples, and illustrated several concurrency concepts, using the SPIN model checker. Behrouz will post links, code, etc., and I will post further comments and notes, on the Google group.
The lecture notes are available in the post "Contents from SPIN / Promela lecture Monday 16 Feb" in the google group of the course.
Today, we spent the first half doing Ex 8.1 and 8.2 from the book, with plenty of discussion. The pseudo-code and Promela code have been posted in the Google group, along with much of the discussion included as comments in the Promela files.
We then began to look at Alg 4.1 from the book and consider how to state the properties we would like to prove it has. We did a brief introduction to modal (temporal) logic. In addition to the material in the book, look at the Wikipedia page on modal logic
particularly the sections on semantics and temporal logic (we need only the F and G operators, equivalent to diamond and box). In the semantics, the frame G is for us the state diagram, and the relation R is the transition relation linking states. Try this and ask me questions on Wednesday.
Reading notes: Chaps 3 and 4 from the book. We can also do more examples from Chap 8 and 9 if you like. Mail me on the Lecture Q&A thread.
Today we discussed the 2014 exam. Answer sketch posted to Google group. We also started discussing Sec 5.1 from the book.
Reading notes for remaining lectures (Mar 4, and possibly Mar 9 and Mar 11 - depending on interest and agenda, but I think we're pretty much done now): Sec 5.1, and, if time permits, revision. Otherwise, please post to the Lecture Q&A thread what you would like to see discussed. There are already a few outstanding items there.
We went through the 2011 exam (most of it). We did the Bakery algorithm (Sec 5.1 in the book), the second and third attempts at the CS problem from Chap 3, and Dekker's algorithm.
Sketches for all these have been posted to the Google group