Theoretical Computer Science

D-CON 2012

Veranstaltungsort und Programm

Das fertige Programm findet sich als pdf hier. Update: Die ersten beiden Vorträge in der Rotunde haben sich geändert. Die zugehörigen Zusammenfassungen findet Ihr am Ende dieser Seite.

Bitte lasst uns wissen, ob Ihr am informellen Abendessen des 07. März teilnehmen möchtet.

Am Mittwoch 19:30 Uhr werden wir im Restaurant Flammkuche (Ludwigstraße 40, 67657 Kaiserslautern) essen.

Am Donnerstag 19:30 Uhr werden wir im Restaurant Spinnrädl (Schillerstraße 1, 67655 Kaiserslautern) erwartet.

Eingeladener Vortrag

Abstract: We investigate the decidability of the state reachability problem in finite-state programs running under weak memory models. In a previous work, we have shown that this problem is decidable for TSO and its extension with the write-to-write order relaxation, but beyond these models nothing is known to be decidable. Moreover, we have shown that relaxing the program order by allowing reads or writes to overtake reads leads to undecidability.

In this work, we refine these results by sharpening the (un)decidability frontiers on both sides. On the positive side, we introduce a new memory model NSW (for non-speculative writes) that extends TSO with the write-to-write relaxation, the read-to-read relaxation, and support for partial fences. We present a backtrack-free operational model for NSW, and prove that it does not allow causal cycles (thus barring pathological out-of-thin-air effects). On the negative side, we show that adding the read-to-write relaxation to TSO causes undecidability, and that adding non-atomic writes to NSW also causes undecidability.

Our results establish that NSW is the first known hardware-centric memory model that is relaxed enough to permit both delayed execution of writes and early execution of reads for which the reachability problem is decidable.

This is joint work with Mohamed Faouzi Atig, Sebastian Burckhardt, and Madan Musuvathi.

Anmeldung und angemeldete Vorträge

1. Decidability of some Information Flow Security Properties for Unbounded Place Transition Nets
   Thomas Strathmann, Uni Oldenburg (Englisch/Deutsch)

Information flow security is concerned with specifying the flow of information between different security domains in a system. Typically, the goal is to make sure that a non-authorized person can deduce classified information by observing visible (unclassified) parts of the system behaviour. In this talk I will briefly describe a set of information flow properties called "Basic Security Predicates" (or BSPs for short) introduced by Heiko Mantel as building blocks for the specification of complex information flow policies. The focus is on a discussion of the decidability of these properties for infinite-state systems modeled as place/transition Petri nets.

2. Interface Automata with Error States
   Ferenc Péter Bujtor, Uni Augsburg (Englisch)

De Alfaro and Henzinger developed interface automata to model and study behavioural types, which describe communication patterns of systems while abstracting from data. They define a parallel composition for these I/O-automata with the following feature: if in some state s one component could make an output which the other is not ready to receive, s is considered an error state and removed during composition, along with some other states leading to it; this is called output pruning. They also define a refinement relation using alternating simulation; this allows to leave out outputs freely. We study the basic setting in order to analyse the design decisions made by de Alfaro and Henzinger: we consider the same parallel composition, but without output pruning. Instead we leave the error states in place and mark them as such. For our refinement relation, we just require two things: if the specification is error free, the implementation should be as well; if we exchange one component for a refinement, then the new composition should be a refinement of the original one. More precisely, we determine the coarsest precongruence satisfying our first requirement. It turns out that this precongruence is just trace based, but it justifies output pruning. In fact there are several variations what preservation of error freeness means and we have studied just one of them. In future work we will look at others. We will also consider variations which enforce implementation of at least some outputs.

3. On the downward-closure of pumpable languages
   Maximilian Schlund, TU München (Englisch)

The downward-closure of languages has nice applications as regular overapproximations of system behavior. It is well known that the downward-closure of every language is regular but not necessarily computable. We present a new approach for proving the effective regularity of the downward-closure for languages satisfying a certain kind of pumping lemma. This method can be used to prove the effective regularity of language families like the Context-free, Petri net and Control languages in an easy and uniform way.

4. Trace Semantics for Probabilistic Transition Systems
   Henning Kerstan, Uni Duisburg-Essen (Englisch/Deutsch)

Probabilistic transition systems, short PTS, are labelled transition systems where each transition depends on an alphabet symbol and occurs with a given probability. We will introduce four slightly different versions of PTS, two with explicit termination (i.e. there is a dedicated final state) and two without any final states. In all four versions we allow arbitrary sets of states and do not restrict our considerations to finite or countably infinite state sets. In order to analyze the behaviour of these systems we define the trace of a state. While this concept of trace semantics is easy to grasp for e.g. finite automata, traces for PTS are somewhat complicated. Based on simple examples we will try to convey an intuitive understanding of traces of states of PTS and will then generalize and formalize these ideas using measure and integration theory to obtain a mathematically sound definition of traces for all of our four version of PTS. During this process we will recognize that even for PTS with finite state spaces, measure theory is an absolute necessity if we consider systems without explicit termination whereas the need for integration theory arises only for systems with non-discrete state spaces. While all the steps up to this point are more or less obvious (although they require some background in measure and integration theory), we conclude our presentation with a short category-theoretic excursion: various types of labelled transition systems (including e.g. finite automata) can be represented as coalgebras. Depending on the choices we make for this representation, the category-theoretic concept of a final coalgebra (whenever it exists) captures different notions of behaviour. Our main result states that, after choosing a suitable representation of PTS, our definition of a trace of a PTS is exactly an instance of this general concept.

5. fLTL - Temporal Logic and Relative Frequency
   Normann Decker, Uni Lübeck (Englisch/Deutsch)

We propose fLTL, an extension to linear-time temporal logic (LTL) that allows for expressing relative frequencies by a generalization of temporal operators. This facilitates the specification of requirements such as the deadlines in a real-time system must be met in at least 95% of all cases. For our novel logic, we establish an undecidability result regarding the satisfiability problem but identify a decidable fragment which strictly increases the expressiveness of LTL by allowing, e.g., to express non-context-free properties.

6. Putting DPNs to Work, Reachability Analysis for Concurrent Java Programs
   Benedikt Nordhoff, Uni Münster (Englisch/Deutsch)

DPNs (Dynamic Push-Down Networks) have been around for some time as a clean theoretical model for concurrent programs with dynamic thread creation and recursive procedures. Their extension to Monitor-DPNs allows to precisely model the effects of synchronization via well nested reentrant locks. Reachability of configurations with tree-regular properties (e.g. data races) can be decided using tree automata based techniques. In my diploma thesis I exploited this approach to analyse real Java programs. This comprised generating a DPN model from Java-Bytecode and implementing the actual analyses. In this session I will give some theoretical background on DPNs and their analysis, sketch some issues and details which accompanied the implementation and give a small tool demonstration of an Eclipse plugin capable of detecting possible data races in Java programs.

7. Static Analysis of Numerical Properties of Multithreaded Programs
   Alexander Wenner, Uni Münster (Englisch/Deutsch)

Static analysis of multithreaded programs, especially of numerical properties, can be used to proof absence of runtime errors, for example division by zero or buffer overflow. Techniques to discover such errors based on abstract interpretation have been well studied for sequential programs. Numerous abstract domains for inferring numerical properties, like for example interval analysis for computing bounds on variables or weakly relational domains like octagons to infer relations between variables, have been developed. The challenge or question is now, whether one can leverage these domains to also discover invariants of multithreaded programs without losing too much precision. After a short recap of the sequential case, we are going to take a look at some published approaches that try to lift the sequential domains to parallel programs. I will add to this by sketching some new ideas to improve upon these methods, using for example results on reachability analysis of multithreaded programs.

8. Translational Expressiveness -- Comparing Process Calculi using Encodings
   Kirstin Peters, TU Berlin (Englisch/Deutsch)

The existence or absence of "good" encodings is a frequently used criterion to compare the expressive power of process calculi. Problematic is here the terminus "good". It is used to rule out trivial or meaningless encodings. But there is no common agreement about what criteria turn an encoding into a "good" encoding. Hence most of the given translational results are incomparable. I will shortly revisit the most common criteria of translational results, like full abstraction or operational correspondence, as well as the 5 criteria presented by Gorla to provide a general framework. Then I would like to discuss with the audience how such a framework should look like and whether or why Gorla's criteria are suited.

9. Models in Bigraphs / Applications of Bigraphs
   Christian Hammerschmidt, TU Berlin (Englisch/Deutsch)

This talk aims at giving an introduction to bigraphs, a model intended as a unifying model for concurrent and pervasive systems. A bigraph consists of a superposition of two indepentent structures, a set of nested nodes and a hypergraph. Distinguished elements allow to define composition and an algebra for bigraphs. For a bigraphical system, a LTS bisimulation which is a congruence can be derived automatically. Many models, including the pi-calculus, mobile ambients and 1-safe petri nets were recovered with bigraphs. I will demonstrate, guided by examples, how well studied models are described and point out current research on and with bigraphs. I hope to discuss ideas and the need for meta models in general as well as bigraphs as an instance of such a model with the audience. (The talk is intended for an audience without any familiarity with bigraphs.)

10. Distributability and the Join-Calculus
    Stephan Mennicke, TU Braunschweig (Englisch/Deutsch)

We investigate distributability of concurrent yet synchronous specifications. The join-calculus is a formal process-algebraic specification language claiming to be asynchronous and distributable. There are results on distributability of Petri nets. It is therefore interesting to look at a Petri net semantics for the join-calculus and discuss its distributability in terms of Petri net representations. We provide an operational Petri net semantics for the join-calculus and use it as a basis for our discussion.

11. Deciding Markov Automata Equivalence in Polynomial Time
    Andrea Turrini, Uni Saarland (Englisch)

Markov Automata (MA) tightly integrate Probabilistic Automata (PA) and Interactive Markov Chains (IMC). The latter concurrency model has seen practical applications in a variety of industrial and academic settings, together with an evaluation trajectory that rests on an effective weak bisimilarity quotienting algorithm. For Markov Automata, weak bisimilarity is a conservative extension of Interactive Markov Chain weak bisimilarity, and also extends probabilistic bisimulation on Probabilistic Automata. Different from standard bisimilarity notions, weak bisimilarity is defined as a relation over distributions instead of states.
We present two new results about weak bisimulations and Markov Automata:
• a novel approach of weakening bisimulation conditions in a probabilistic context, which leads to an an alternative state-based characterization of the Markov automata weak bisimulation,
• a polynomial decision procedure for weak bisimilarity on Markov Automata following the widely used partition refinement approach.
As a side result, we give a positive answer to the 10-years old open problem whether probabilistic weak bisimilarity, as defined by Segala, can be decided with sub-exponential complexity.

12. Analysis and Verification of Heap-Manipulating Programs
    Stefan Rieger, Uni Bamberg (Englisch/Deutsch)

Today's object oriented programming languages make heavy use of heap-allocated memory. Thus, when statically analyzing such programs dynamically evolving heap structures have proven to be a major challenge. The (theoretical) unboundedness of the heap due to dynamic allocation and deallocation of memory leads to potentially infinite state spaces that prohibit the use of standard verification techniques such as model checking.
Our talk gives an introduction to our graph grammar-based framework "Juggrnaut" that allows for abstracting unbounded heap structures to obtain finite state spaces that may be used as input for standard model checkers. In addition we will present some concepts of our current research that aim at extending the framework in its applicability and expressive power.

13. Structural Logics for Process Calculi
    Sven Linker, Uni Oldenburg (Englisch/Deutsch)

The analysis of concurrent processes was traditionally concerned with the process behavior. But many interesting distinctions between process arise not on the behavioral but on the structural level. For example, in the pi-calculus the process 0 is behaviorally equivalent to every deadlocked process. Only a structural investigation can differentiate both. Logics to express such differences have been introduced and studied recently, and are of growing importance. The focus of the session is on giving an introduction to such logics and on the discussion of decidable subsets. As a the semantic foundation, only very basic familiarity with the pi-calculus or similar process algebras is assumed.

14. Language-Theoretic Abstraction Refinement
    Georgel Calin, TU Kaiserslautern (Englisch)

We give a language-theoretic counterexample-guided abstraction refinement (CEGAR) algorithm for the safety verification of recursive multi-threaded programs. First, we reduce safety verification to the (undecidable) language emptiness problem for the intersection of context-free languages. Initially, our CEGAR procedure overapproximates the intersection by a context-free language. If the overapproximation is empty, we declare the system safe. Otherwise, we compute a bounded language from the overapproximation and check emptiness for the intersection of the context free languages and the bounded language (which is decidable). If the intersection is non-empty, we report a bug. If empty, we refine the overapproximation by removing the bounded language and try again. The key idea of the CEGAR loop is the language-theoretic view: different strategies to get regular overapproximations and bounded approximations of the intersection give different implementations. We give concrete algorithms to approximate context-free languages using regular languages and to generate bounded languages representing a family of counterexamples. We have implemented our algorithms and provide an experimental comparison on various choices for the regular overapproximation and the bounded underapproximation.

15. Enforcing Robustness against Total Store Ordering
    Egor Derevenetc, Fraunhofer ITWM and TU Kaiserslautern (Englisch)

We present algorithms for checking and enforcing robustness of a concurrent program against the relaxed memory model Total Store Ordering (TSO). A program is robust if its visible behaviors under TSO are the same as under Sequential Consistency (SC). We reduce checking robustness against TSO to SC reachability in several instrumented versions of the program. The translation is linear, source-to-source, independent from the program’s data domain, and from the length of store buffers in the TSO semantics. Moreover, it yields reachability checks that can be executed in parallel. As a second result, we provide an algorithm for computing a minimal set of fence locations that enforce robustness. The algorithms are implemented in a tool chain that we successfully apply to analyzing and correcting several concurrent algorithms.

Themensitzungen

Die Idee der Themensitzungen ist in folgender E-Mail von Gerald, Michael und Markus erläutert:

"Nach unserer momentanen Planung werden wir 8-10 Themensitzungen (maximal zwei parallel) ausrichten können. Jede Themensitzung dauert 60 Minuten. Wie im letzten Jahr soll eine Themensitzung von einem Doktoranden oder einer Doktorandengruppe vorgeschlagen werden und einen Theme Leader haben, der die Sitzung leitet. An einer solchen Sitzung kann dann jeder teilnehmen, den das Thema interessiert.

Wie eine Themensitzung dann konkret ausgestaltet ist können die Theme Leader selbst festlegen: Beispielsweise eine Diskussionsrunde mit Moderator, ein einführender Überblicksvortrag mit anschließenden informellen Einzelbeiträgen der Teilnehmer an der Tafel/Whiteboard, oder ein klassischer Fachvortrag mit ausführlicher Diskussion.

Die Aufteilung in parallele Sitzungen hat den Vorteil, dass wir kleinere Gruppen bekommen und mehr Themen zur Auswahl anbieten können. Wir stellen uns vor, dass von jeder Forschungsgruppe mindestens ein Vorschlag kommen sollte. Je mehr desto besser. Diese Vorschläge sammeln wir und doodeln im Vorfeld Eure Präferenzen. Wir planen dann entsprechend dem Abstimmungsergebnis.

Wenn ein Vorschlag zu wenig Teilnehmer anzieht, wird er also noch rechtzeitig vor dem Workshop gestrichen, so dass sich niemand unnötig vorbereitet. Auch die potentiellen Teilnehmer können sich gegebenenfalls vorbereiten wollen. Vielleicht möchte ja jemand in einer Sitzung ein ungelöstes Problem behandeln und mit den Teilnehmern über eine Lösung diskutieren?"

Unterkunft

Die Hotels sind zentral gelegen, die Fußgängerzone ist nur wenige Schritte entfernt und die TU leicht per Bus zu erreichen (mit Buslinien 105, 115 oder andere).

Art Hotel Lauterbach an Fruchthallstraße 15, 67655 Kaiserslautern: 4 Zimmer à 72€ inkl. Frühstück und 2 Zimmer à 80€ inkl. Frühstück. Parken: QPark Theaterparkhaus, 7,50€.

Hotel Lautertaler Hof an Mühlstraße 31, 67659 Kaiserslautern: 15 Zimmer à 69€ inkl. Frühstück. Parken: 5€.

Alcatraz Hotel am Japanischen Garten an Morlautererstraße 1, 67657 Kaiserslautern: 15 Zimmer à 76€ inkl. Frühstück + Parkplatz

SAKS Urban Design Hotel an Stiftsplatz 11, 67655 Kaiserslautern: 14 Zimmer à 85€ exkl. Frühstück. "Im Zimmerpreis inbegriffen ist die Nutzung unserer Gym, unserer Guest Lounge, in der Ihnen Croissants, Obst und Snacks sowie verschiedene Getränke und Kaffeespezialitäten kostenfrei zur Verfügung stehen." Parken: Tiefgarage Stiftsplatz, 12€.