The course begins on Tuesday, 2017-08-29 at 12:15 in classroom SG 312.
|date||Reading CA||Reading EB||exercises||new topic|
|2017-12-05||RL OSc CL|
|2017-11-30||JH MT HT|
|2017-11-29||AK MK TS|
|2017-11-28||OSa LS MS|
|2017-11-23||113, …, 116|
|2017-11-22||110, 111, 112, 106, 107, 108|
|2017-11-21||96, 98, 99, 102, 103, 105||branching bisimilarity|
|2017-11-16||103, …, 108||branching bisimilarity|
|2017-11-15||97, …, 102||operational determinism|
|2017-11-14||37, …, 39||observation equivalence|
|2017-11-09||90, 96||observation equivalence|
|2017-11-08||34, …, 37||85, 86, (87, 88, 89), 92, 94, 95||CFFD-preorder|
|2017-11-07||29||(79), 80, …, 84, 91, 93|
|2017-11-02||80, …, 84||CFFD-preorder|
|2017-11-01||25, …, 28||31, …, 34||(62), (64), 76, …, 79||congruence, CFFD-equivalence|
|2017-10-31||(62), (64), 69, 71, …, 75||62, 64 if there is time|
|2017-10-26||25||28, …, 31||66, …, 71||stable failures|
|2017-10-25||24||27, …, 28||51, 62, …, 65||traces|
|2017-10-24||ASSET again, intro to traces|
|2017-10-12||Preparation for ASSET projects|
|2017-10-11||58, …, 65||These are new problems!|
|2017-10-10||47, …, 52, 56||Use new version of 52!|
|2017-10-05||49, …, 51|
|2017-10-04||22, …, 24||52, …, 57|
|2017-10-03||21, …, 22||44, …, 48||Peterson's algorithm|
|2017-09-28||26, …, 28||44, …, 48||traces|
|2017-09-27||22, …, 26||36, …, 40|
|2017-09-26||29, 30, 32, …, 35||synchronization rules|
|2017-09-21||15, …, 22||28, …, 31||parallel composition, etc. of state machines|
|2017-09-20||14, …, 21||21, …, 27||parallel composition, etc., of LTSs|
|2017-09-19||8, …, 14||13, …, 15||17, …, 20||modelling for ASSET|
|2017-09-14||16, …, 20||bisimilarity|
|2017-09-13||A sequence …||rest of … 15|
|2017-09-12||ASSET||10, …, 13||(8), 9, …, 15||(exercises)|
|2017-09-05||4, 5, 7||unfolding|
|2017-08-31||6, …, 8||7, …, 10||2, …, 7||state machines|
|2017-08-30||1, …, 6||1, …, 7||concurrent systems|
|2017-08-29||course practicalities, concurrency in programming|
At an abstract level, the purpose or meaning of a sequential program is clear: it computes a partial function from the inputs to the outputs1. There is, however, no common agreement as to what would be a similar abstract notion for concurrent programs. This course studies the purpose or meaning of concurrent programs, with applications to the checking of their correctness. The material also applies to some extent to hardware.
1. This is not always strictly true because of nondeterministic programming constructs, such as random number generators.
The course is intended for students who are interested in theoretical aspects of computer science or information technology. It is also suitable for students of discrete mathematics. Basic notation from set theory and logic will be used. Most of the material does not require deep mathematical skills. Knowledge of finite automata and their languages is useful but not a must.
Strong background in mathematics is not necessary, but willingness to think in abstract terms and learn to use mathematical concepts is necessary.
The course is on periods 1 ja 2. Every week there are three meetings of two hours each. The meetings are flexibly used for lectures, exercises, and discussion.
|Tuesdays||12:15–14:00||SG 312||first: 2017-08-29|
|Thursdays||08:15–10:00||TB 206||last: 2017-12-07|
There are no meetings on 2017-09-06, 2017-09-07 (conference), 2017-10-17, 2017-10-18, 2017-10-19 (mid-term break), and 2017-12-06 (public holiday).
If the number of students is small, the course is passed by solving many enough weekly exercise problems. Otherwise there will be an examination.
The main reading material of the course are the following two tutorials:
The exercise problems and other material is distributed via this web page.
The teacher of the course is Antti Valmari.
The goal is that the course is passed by being present, solving traditional and ASSET problems, and giving talks as follows, so that there is no examination.
The course is worth 7 credit units. Officially, that means 187 hours of student work (including both the meetings and the work done at home). That makes more than 13 hours / week! In my opinion that is too much, but ≈ 10 hours / week seems justified. That means 6 hours for the meetings and ≈ 4 hours homework / week.
There are altogether 39 meetings. Without any special arrangements, the student may be absent from at most 4 meetings and not from more than two successive meetings. Permission to be absent more than this may be negotiated, but then the student has to solve additional problems or give additional talks. The need for this may arise, for instance, if the student has to be absent every Thursday.
Problems and talk topics will be designed as the course goes on. The goal is to find problems and topics that are suitable for students at different levels. Every student must do at least one problem (or group of small problems) or talk each week except the first week. If the student fails a problem or talk, then (s)he may try again another day. It is also possible to change the topic if necessary. An incomplete solution of a medium-level or difficult problem may be accepted as a point at a lower level. The mark of the course is determined by the difficulty of the topics the student chose and the performance in them.
I suggest the following marking system. We should discuss at the meetings whether this is okay. At the time of making the suggestion, approximately ¼ of the meetings had taken place. The system has been designed to make it relatively easy to pass the course, while at the same time emphasizing M- and D-points when aiming at a high mark.
To pass the course, the student must do the following:
If the ASSET solution or talk is very weak, the student may have to improve it until it is acceptable.
Points are earned as follows:
Also the ASSET exercise and talk yield points, with the maximum being 30.