Concurrency Theory

News

  • 2019-07-09: we are online!

Schedule

TypeDayTimeHallStartLecturer
LectureMon14:30 – 16:00AH 107 OctKatoen/Noll
 Tue14:30 – 16:00AH 108 OctKatoen/Noll
ExerciseThu14:30 – 16:00505617 OctBatz/Matheja

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 behaviour 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 of the following relevant undergraduate courses is expected:

  • Programming (essential concepts of imperative and object-oriented programming languages and elementary programming techniques)
  • Essential concepts of operating systems
  • Formal Languages and Automata Theory (regular and context-free languages, finite and pushdown automata)
  • Mathematical Logic

Lectures

No.DateLecturerTopicSlides
0107 OctNollIntroductionl01
0208 OctNollCalculus of Communicating Systems (CCS)l02
0314 OctNollHennessy-Milner Logicl03
0415 OctNollHennessy-Milner Logic with Recursionl04
0521 OctNollFixed-Point Theoryl05
0622 OctNollMutually Recursive Equational Systemsl06
0728 OctNollModelling and Analysing Mutual Exclusion Algorithms & Value-Passing CCSl07
0829 OctNollThe π-Calculusl08
095 NovNollExample Reactions in π-Calculusl09
1011 NovNollVariations of π-Calculusl10
1112 NovNollTrace Equivalencel11
1218 NovNollStrong Bisimulationl12
1319 NovNollProperties of Strong Bisimulationl13
1425 NovNollBisimulation as a Fixed Point and Weak Variantsl14
1526 NovNollHennessy-Milner Logic and Bisimilarityl15
1602 DecKatoenInterleaving Semantics of Petri Netsl16
1709 DecKatoenTrue Concurrency Semantics of Petri Nets (1)l17
1810 DecKatoenTrue Concurrency Semantics of Petri Nets (2) l18+l19
1916 DecKatoenMcMillan Prefixes
2017 DecKatoen

Exercises

No.Due DateTopicExercise
0117.10.2019CCSe01
0221.10.2019HMLe02
0331.10.2019FP+HMLe03
0407.11.2019HML+CCS+PiCe04
0514.11.2019CAAL+PiCe05
0621.11.2019Trace Equivalencee06
0728.11.2019Strong Bisimulatione07
0805.12.2019Weak Bisimulatione08
0912.1.2019Petri Netse09
10Old examsex1 / ex2

Exam

  • The form of the exam (written or oral) will be announced later.
  • Registration is possible via RWTHonline; there are no specific requirements for admission.

Evaluation results

Further information

  • The lectures will be given in German or English, depending on the language proficiency of the audience.
  • The slides and other course material will be in English. There are no lecture notes (yet); the course material will consist of slides.

Background 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.