COMP6752 — 2020 — Course outline

Lectures and handouts Notes Topics
This course is given every other year; the last time was Trimester 2, 2020. Tutorials Piazza Homework HW Submissions

Modelling Concurrent Systems

Time & Place:
The official time and place, which can be found in the UNSW time table, is moot, due the current mobility restrictions. Instead, recordings of teaching are made available from this webpage (see link above), and students can watch them whenever they like.
However, the tutorial is delivered synchronously, Thursdays 14:00 - 15:00, via zoom. June 4 to July 2, and July 16 to August 6.
Moreover, some students may choose to deliver their similar presentation to the class synchronously, via zoom, or something equivalent. This will happen during scheduled class hours, Mondays between 15:00 and 17:00, and/or Tuesdays between 14:00 and 16:00.
Units of credit: 6 (= ⅛ standard annual study load)
Instructor:
Rob van Glabbeek, Data61, CSIRO, tel. 9490 5938. Email: rvg@cse.unsw.edu.au
Cameraman:
Liam O'Connor
Tutor:
Ryan Barry
Aim:
This course tries to make students familiar with state-of-the-art techniques in modelling concurrent systems. This is done by comparing some of the more successful semantic models of concurrency found in the literature. The focus will be on the rationale behind the design decisions underlying those models, viewed from philosophical, mathematical and computational perspectives. The course contains important background knowledge for students aiming at a scientific career in which the design of mathematical models of system behaviour is a component.
Learning Outcomes:
By the end of the course students should be able to accurately model simple concurrent systems, in particular by being able to make an informed choice, out of the many types of models available, as to which one is (most) suitable for the task at hand. Additionally, they should be able to prove elementary properties of systems modelled thusly.
Method:
Lecturing; distribution of scientific handouts inviting to self-study; challenging homework assignments that invite students to mix the mastered techniques with their own creativity; and seminar presentations in which students learn how to digest and present relevant material.
Teaching Rationale (item required by school):
The course is being taught this way because I think this is the best way to achieve the learning outcomes.
Mode of teaching:
My mode of lecturing consist of talking while making drawings on the blackboard (or whiteboard). I normally aim for an interactive style of teaching where students understand the material at the time it is delivered. Hereby I try to discourage taking notes with the mere aim of deciphering them later. Students should ask questions at the time that something is less than 100% clear. Occasionally I may ask a student to explain to the rest of the class something I just talked about, thereby assuming that the mere fact they didn't interrupt with a question indicates full understanding.
All of that is moot with the current restrictions on classroom teaching. Instead of interactive lectures there will be recorded ones. Students should stop the recording when something is unclear and try to figure it out before continuing. This takes the place of interrupting with questions. For this reason the recordings of lectures are not as long as the allocated teaching hours.
The lectures go hand in hand with these notes. The notes give precise definitions of the concepts I teach, whereas the lectures are more hand-waving and try to illustrate their use. It is not possible to master the material while skipping reading the notes, and it is (almost) impossible to master the material without listening to the lectures. To reduce duplicate efforts, in the lectures I normally skip any formal definitions that can be found in the notes, and the notes normally skip examples and illustrations that are done in the lectures.
Tutorial:
Each Thursday from 2 to 3pm there will be an interactive 1-hour tutorial on zoom. You will gain access by means of the password 386800. It will be used to discuss homework solutions or anything else that is unclear. By default we only discuss items that are raised by one of the students attending the tutorial, and often delegate answering of questions to students as well.
On-line chat
The prime spot for asking questions is the COMP 6752 piazza exchange forum. All students are encouraged to answer the questions of other students in this forum.
Topics covered:
Models of concurrent and distributed systems (e.g. labelled transition systems, process algebra, event structures, Petri nets), operational and denotational semantics, semantic equivalences and refinement relations (linear versus branching time, interleaving versus partial order semantics), modal and temporal logic for concurrent systems (proof theory and applications).
Related courses:
COMP3151/9191 also addresses the modelling of concurrent systems, but with more emphasis on communication via shared variables, and the solutions of classical problems like mutual exclusion.
COMP3153/9153, taught in T1, focuses more on the applications of theories of concurrency than on their design. This course describes several automatic verification techniques, the algorithms they are based on, and the tools that support them. It discusses examples to which the techniques have been applied, and provides experience with the use of several tools.
Prerequisites:
The ability to understand and deliver formal mathematical proofs.
Course material:
Scientific papers to be handed out, and the webpage Notes. Moreover, there will be recordings of lectures.
Seminar presentations:
Some lectures will consist of seminar presentations by students taking the class. Every student is anticipated to present (at least) one seminar, roughly 30 minutes long. Upon request, the possibility exists to split presentations over multiple weeks.
In preparation for your presentation you select a topic, read one or more papers or (parts of) books on that topic, and make a summary to be presented to the class. You have a choice to present the material synchronously via zoom or a similar platform, or to prepare a recording, that others in the class can watch in their own time. Slides or some other form of a concise message for the class are welcome. By default, these presentations are part of the material taught in this class, and exam questions about them cannot be excluded.
A list of suggested topics, with books and papers on each topic, is being compiled here. Deviations from these suggestions are encouraged. Please inform me of your choice as soon as possible, to make sure that your topic has not yet been claimed by another student.
I anticipate roughly 1 seminar presentation per Monday and Tuesday lecture, starting from June 30. A schedule will be compiled on the page Lectures and handouts. Do select a slot by emailing me.
Homework:
Assignments will be posted here each week. Each weekly homework comes in two batches; one following each of the two lectures given that week. The solutions should be uploaded here as PDF by 10:00am the following Monday. Here is my late policy.
Sometimes homework may be labelled "test", meaning that it can be regarded as a small take-home exam. Such tests (like the final exam) must be done without any collaboration whatsoever. For the normal homework, collaboration is allowed as long as (1) you acknowledge in writing all the people you discussed the problem with, and (2) each student writes up his/her own solution without looking at any writeup/notes from another student.
Exams:
Tuesday 18-08-2020 from 10:15-13:15am. That day (if not changed) at 9am the exam will appear on this webpage, linked from here, and at noon the same day you are supposed to upload a scan of your answers as PDF in the homework collection interface. Do let me know asap if you foresee a problem with that. You may use piazza if you find an exam question ambiguous, but I will not answer general questions about the material during the exam. The university guidelines say "No Exam Materials permitted". However, this is an open book exam, and you are free consult all your notes, as well as static internet nets. (And if you find the answer there, please add a citation.) But you may not consult other people in any way.
In addition, there will be a short oral exam via Skype or Zoom. This will occur right after the final exams have been corrected. I will ask you to select a time slot that is convenient for all concerned. During the oral exam I may ask you some questions on the overall material taught in this course, as well as specific questions on your own answers to the final exam.
Course credit plan:
Tests + Homework 40%, written exam 30%, oral exam 10%, seminar 20%. Your answers to the oral exam can also alter your written exam score (in both directions).
Course Evaluation and Development: response to class evaluation
The only criticism on this course in the last two evaluations was the lack of a textbook, given that there is a steep learning curve. Unfortunately there is no textbook that covers all aspects of this course, and prescribing a handful of textbooks while treating only a chapter or two from each of them appears needlessly expensive.
WWW page:
http://www.cse.unsw.edu.au/~rvg/6752/
Course notes:
This file will keep track of the material covered so far, and list the handouts distributed to date.

Rob van Glabbeek rvg@cse.unsw.edu.au