Recent events

Fundamental Algorithmic Problems and Challenges in Dynamical and Cyber-Physical Systems

Joël Ouaknine
Max Planck Institute for Software Systems
Joint Lecture Series
06 Dec 2017, 12:15 pm - 1:15 pm
Saarbrücken building E1 5, room 002
Dynamical and cyber-physical systems, whose continuous evolution is subject to differential equations, permeate vast areas of engineering, physics, mathematics, and computer science. In this talk, I consider a selection of fundamental algorithmic problems for such systems, such as reachability, invariant synthesis, and controllability. Although the decidability and complexity of many of these problems are open, some partial and conditional results are known, occasionally resting on certain number-theoretic hypotheses such as Schanuel's conjecture. More generally, the study of algorithmic problems for dynamical and cyber-physical systems draws from an eclectic array of mathematical tools, ranging from Diophantine approximation to algebraic geometry. I will present a personal and select overview of the field and discuss areas of current active research.

Blocking Analysis of Spin Locks under Partitioned Fixed-Priority Scheduling

Alexander Wieder
Max Planck Institute for Software Systems
SWS Student Defense Talks - Thesis Defense
29 Nov 2017, 4:00 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 111
Partitioned fixed-priority scheduling is widely used in embedded multicore real-time systems. In multicore systems, spin locks are one well-known technique used to synchronize conflicting accesses from different processor cores to shared resources (e.g., data structures). The use of spin locks can cause blocking. Accounting for blocking is a crucial part of static analysis techniques to establish correct temporal behavior.

In this thesis, we consider two aspects inherent to the partitioned fixed-priority scheduling of tasks sharing resources protected by spin locks: (1) the assignment of tasks to processor cores to ensure correct timing, and (2) the blocking analysis required to derive bounds on the blocking.

Heuristics commonly used for task assignment fail to produce assignments that ensure correct timing when shared resources protected by spin locks are used. We present an optimal approach that is guaranteed to find such an assignment if it exists (under the original MSRP analysis). Further, we present a well-performing and inexpensive heuristic.

For most spin lock types, no blocking analysis is available in prior work, which renders them unusable in real-time systems. We present a blocking analysis approach that supports eight different types and is less pessimistic than prior analyses, where available. Further, we show that allowing nested requests for FIFO- and priority-ordered locks renders the blocking analysis problem NP-hard.

Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations

Hugo Férée
University of Kent
SWS Colloquium
22 Nov 2017, 10:30 am - 12:00 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 113
Formal reasoning about computational complexity turns out to be quite cumbersome as it often requires to manipulate explicit time bounds for a specific machine model. Implicit Computational Complexity is a research area which provides techniques and complexity classes characterisations to avoid this. We have formally verified the soundness (and part of the completeness) of such a technique - called quasi-interpretations - using the Coq proof assistant. In particular, we turned this into a tool to help guarantee the polynomial complexity of programs (here, term rewriting systems).