Concurrency Theory (Seminar)

Seminar in Theoretical CS, Summer Semester 2014

News

  • 10.01.2014: we are online

Schedule

Thu, 20 Feb 2014, 15:00 Introduction at seminar room of i2
-8 weeks Table of contents due
-6 weeks Preliminary version of report due
-4 weeks Final version of report due
-2 weeks Preliminary version of slides due
-1 week Final version of slides due

Overview

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 seminar is to deepen some of the topics that have been introduced in the Concurrency Theory Course in the preceding semester, and to study alternative modeling approaches that have not been discussed before. With respect to the former, additional topics related to process algebras will be studied, which provide a formal apparatus for reasoning about structure and behavior of systems in a compositional way. Also, the seminar will feature additional material on Petri Nets, which are well suited for explicitly modeling the concurrent behavior of distributed systems.

Each of the topics is addressed in a scientific journal or conference article (please refer to the references below). These research articles are the basis on which students have to prepare their report and presentation.

Prerequisites

Basic knowledge in the following areas is expected:

  • Essential concepts of operating systems
  • Formal languages and automata theory
  • Mathematical logic
  • Previous knowledge in Concurrency Theory is helpful but not mandatory

Dates

(all presentations on Tuesdays 16:00-17:00 at I2 seminar room)

Date Topic(s)
22 April 1
13 May 5
27 May 8
3 June 9
24 June 12
1 July 14
8 July 3, 15
15 July 4

Topics

Process Algebras

  1. Timed CCS
  2. Synchronous and Asynchronous CCS
  3. ACP Process Algebra
  4. Decidable Subsets of CCS
  5. The Linear Time-Branching Time Spectrum
  6. Axiomatization of Bisimilarity

Petri Nets

  1. Reachability in Petri Nets
  2. Undecidability of Bisimilarity for Petri Nets
  3. Liveness and Safeness of Petri Nets
  4. Efficient Net Unfolding
  5. Applications of Net Unfolding
  6. Timed Nets
  7. Generalized Stochastic Petri Nets

Other Concurrency Models

  1. Mazurkiewicz Traces
  2. Event Structures
  3. Modeling Concurrency with Partial Orders

Additional Material

Registration

Registration to the seminar is handled between January 14 and 26, 2014, via the central online form at www.graphics.rwth-aachen.de/apse

Contact

Thomas Noll <noll at cs.rwth-aachen.de>