News
- 2021-09-16: we are online!
Schedule
| Type | Day | Time | Hall | Start | Lecturer |
|---|---|---|---|---|---|
| Lecture | Tue | 10:30 – 12:00 | AH 1 | 12 Oct | Katoen/Noll |
| Fri | 10:30 – 12:00 | AH 1 | 15 Oct | Katoen/Noll | |
| Exercise | Tue | 12:30 – 14:00 | AH 1 | 26 Oct | Batz/Chen |
In accordance with the current university regulations, both lectures and exercise classes will be organised as in-person activities. All participants will be checked for compliance with the so-called 3G regulations when entering their lecture halls. Individuals who are neither fully vaccinated nor have recovered from Covid-19 nor have been negatively tested are not allowed to participate in any face-to-face courses. All teaching activities will be recorded to make them available to students who cannot or do not want to attend in-person courses.
Contents
Today, concurrent programming has become mainstream, dictated by the 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 infrastructures 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 a non-deterministic merging of sequential executions. It is represented by various process algebras, which provide a formal apparatus for reasoning about the 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 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
Lecture Materials
- The lecture materials (videos, slides, exercise sheets, etc.) will be published via the RWTHmoodle classroom during the semester.
- Check out the CAAL Tool developed at Aalborg University which is used in the exercises and/or lectures.
- More tools are listed here.
Exams
| Date | Time | Location | |
|---|---|---|---|
| First exam | 24 Feb | 12:00 | TBA |
| Re-exam | 26 Mar | 14:00 | TBA |
Further Information
- The lectures will be given in English. The slides and other course materials will be in English as well.
- There are no lecture notes (yet); the course materials 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.
- Davide Sangiorgi and David Walker: The Pi-Calculus: A Theory of Mobile Processes. Cambridge University Press, 2001.
- Jan Bergstra, Alban Ponse and Scott Smolka (Eds.): Handbook of Process Algebra. Elsevier, 2001.