News

      • There will be no date for the exam inspection. You may make an appointment for an inspection with Mr. Kaminski until Thursday, April 3.
      • 26.3.2014: Please find the results of the second exam below.
      • 27.2.2014: Please find the updated results (after the inspection) of the first exam below.
      • 26.2.2014: Please find the results of the first exam below.
      • 19.2.2014: The inspection of the first exam will take place on Thursday, February 27, at 14:00h in the i2 seminar room (room 4201b).
      • 5.2.2014: You can find a list of how well you did in the exercises below. Everybody above 50% is admitted to the exam.
      • 22.1.2014: Errata: There have been two small mistakes in the current exercise series, namely one in Exercise 1 (d) and one in Exercise 2. The updated version is now online.
      • 18.12.2013: Note that there will be no lecture on Wednesday, January 15. Furthermore there will be no new exercise series until Tuesday, January 14.
      • 16.12.2013: In addition to the current exercise series, there will be a bonus tutorial series worth 15 bonus points after Thursday's lecture. The solution to this bonus tutorial will be discussed on Thursday, January 16 at 14:15h in the AH I lecture hall.
      • 12.12.2013: The Exercise Series 8 is updated!  Since the last two questions about weak bisimulation haven't been introduced in the lecture so far, they are replaced by questions related to strong bisimulation.
      • 10.12.2013: There will be no lecture on Wednesday, December 11. Instead there will be a lecture on Thursday, December 12.
      • 28.10.2013: Due to the general assembly of the student representatives, next week's exercise class will be shifted to Thursday, November 7 in the AH I.
      • 23.10.2013: Erratum: There has been a small mistake concerning Exercise 2 (a) of Series 1. The corrected version has been uploaded.
      • 16.09.2013: We are online!


      Schedule

      Type

      Day

      Time

      Place

      Start

      Lecturer

      V3

      Wed

      10:15-11:45

      AH 2

      16 Oct

      Thu

      14:15-15:45

      AH 1

      17 Oct

      Ü2

      Tue

      12:15-13:45

      AH 6

      29 Oct


      Contents

      Today, concurrent programming has become mainstream, dictated by need for ever increasing performance which, having reached the end of Moore's law, can only be achieved by parallelism. Indeed, application software from areas such as medicine or natural sciences heavily relies on parallel hardware infrastructure like (GP)GPU accelerators, FPGAs, and multi- and many-core machines.

       

      However, it is also today that we see concurrency faults coming up every day. The simple reason is that writing concurrent programs is difficult. Most programmers "think sequentially" and therefore make mistakes when writing concurrent software. Notorious programming errors include deadlock and violations of atomicity or order of operations, which are mainly caused by the wrong use of synchronization primitives like semaphores or locks. Even worse, the inherent non-deterministic behavior of concurrent software makes bugs difficult to reproduce. Addressing these challenges requires efforts from multiple related disciplines, involving concurrency bug detection, program testing and validation, and programming language design.

       

      Another important area of computer science where concurrency naturally arises is that of reactive systems, which maintain an ongoing interaction with their environment. In contrast to sequential systems whose meaning is defined by the results of finite computations, the behavior of reactive systems is mainly determined by concurrent execution, communication, interaction, and mobility of non-terminating processes. Typical examples include operating systems, control systems for production lines, power plants, or vehicles. As many of such systems are safety critical, their development calls for rigorous formal techniques for design, implementation, and validation.

       

      The aim of this course is to provide a basic understanding of modeling formalisms for concurrent systems. It will address two basic approaches, which are respectively called the interleaving and the true concurrency approach. The former is based on the idea to reduce the phenomenon of concurrency to well-known concepts, by interpreting parallel behavior as non-deterministic merging of sequential execution. It is represented by various process algebras, which provide a formal apparatus for reasoning about structure and behavior of systems in a compositional way. The true concurrency approach mainly comes in the form of Petri nets, which are well suited for explicitly modeling the concurrent behavior of distributed systems.


      Prerequisites

      Basic knowledge in the following areas is expected:

      • Essential concepts of operating systems
      • Formal languages and automata theory
      • Mathematical logic


      Lectures

      No.

      Date

      Topic

      Overlays

      Handout

      1

      16 Oct

      Introduction

      2

      17 Oct

      Calculus of Communicating Systems

      3

      23 Oct

      Hennessy-Milner Logic

      4

      30 Oct

      Hennessy-Milner Logic with Recursion

      5

      31 Oct

      Fixed-Point Theory

      6

      06 Nov

      Application to Hennessy-Milner Logic

      7

      13 Nov

      Mutually Recursive Equational Systems

      8

      14 Nov

      Modelling and Analysing Mutual Exclusion Algorithms

      9

      20 Nov

      Extensions of CCS: Value Passing and Mobility

      10

      21 Nov

      The π-Calculus

      11

      27 Nov

      Variations of π-Calculus & Communicating Sequential Processes

      12

      04 Dec

      Trace Equivalence

      -

      13

      05 Dec

      Strong Bisimulation

      -

      14

      12 Dec

      Bisimulation Games

      -

      15

      18 Dec

      Weak Bisimulation

      -

      16

      19 Dec

      HML and Strong Bisimilarity

      -

      17

      8 Jan

      Interleaving Semantics of Petri Nets

      -

      18

      9 Jan

      True Concurrency Semantics of Petri Nets I

      -

      19*

      16 Jan

      CWB Tutorial

      -

      -

      20

      22 Jan

      True Concurrency Semantics of Petri Nets II

      -

      21

      29 Jan

      From CCS to Petri Nets

      -

      -

      22

      30 Jan

      Timed Modelling & Conclusions


      Exercises

      Series

      Due

      Sheet

      1

      29.10.2013

      2

      07.11.2013 

      3

      12.11.2013

      4

      19.11.2013

      5

      26.11.2013

      6

      03.12.2013

      7

      10.12.2013

      8

      17.12.2013

      9

      07.01.2014

      Bonus

      07.01.2014

      10

      21.01.2014

      11

      28.01.2014

      12

      04.02.2014


      Exercises Results

      Student Number

      Percentage

      263631                    

      61

      281380

      12

      286140

      55

      287374

      61

      287668

      61

      292737

      63

      292844

      69

      293534

      69

      294761

      100

      296709

      82

      297271

      57

      297658

      67

      297684

      67

      300961

      63

      308448

      58

      321845

      57

      327826

      45

      341536

      23


      Exam

      The written exams are scheduled for Friday, 21.02.2014, 11:30-14:00 at AH 2 and Tuesday, 25.03.2014, 10:00-12:30 at AH 1. Registration is possible via Campus.


      Exam Results (updated)

      Student Number

      Grade

      263631             

      3.3

      287374

      3.7

      292737

      3.7

      292844

      5.0

      293534

      2.7

      294761

      1.3

      296709

      2.3

      297271

      2.7

      297658

      1.3

      300961

      2.3

      308448

      4.0

      321845

      5.0

      Average Grade: 3.1

      Failure Rate: 16.7%


      Second Exam Results

      Student Number

      Grade

      286140

      4.0

      292844

      3.0

      297684

      1.3

      321845

      5.0

      Average Grade: 3.325

      Failure Rate: 25%


      Evaluation results


      Literature

      • Luca Aceto, Anna Ingólfsdóttir, Kim Guldstrand Larsen and Jiri Srba: Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, 2007.
      • Wolfgang Reisig: Understanding Petri Nets: Modeling Techniques, Analysis Methods, Case Studies. Springer Verlag, 2012.
      • Maurice Herlihy and Nir Shavit: The Art of Multiprocessor Programming. Elsevier, 2008.
      • Jan Bergstra, Alban Ponse and Scott Smolka (Eds.): Handbook of Process Algebra. Elsevier, 2001.