D-CON 2011 in Münster

Programm

Es gibt jetzt ein überarbeitetes vorläufiges Programm mit mehr Informationen zu den Örtlichkeiten.

Doodle

Wie schon im letzten Jahr haben wir ein Doodle aufgesetzt um einen Überblick über die Präferenzen zu bekommen. Es sollten alle abstimmen, die sich zur D-CON angemeldet haben, damit wir beim Planen des Ablaufs auf möglichst vollständige Informationen zurückgreifen können. Die Abstimmung sollte bis zum 11.02.2011 erfolgt sein.

http://doodle.com/v2uw2g377xyh4q26

Die Abstracts zu den einzelnen Themenvorschlägen findet ihr unten.

Themenvorschläge

Ergänzungen: Für Ergänzungen, Korrekturen, etc. wendet euch an alexander.wenner AT uni-muenster.de

Analysis and Verification of Concurrent Systems based on Graph Decompositions

Sessionleiter:

Für die Analyse und Verifikation nebenläufiger Systeme werden heutzutage oftmals Graphen und Graphtransformationssysteme eingesetzt. Dabei wird die statische Form dieser Systeme als Graph beschrieben. Die Dynamik solcher Systeme kann durch Graphtransformationsregeln spezifiziert werden, die sowohl das Entstehen und Verschwinden von Komponenten, als auch die Umstrukturierung der Topologie beschreiben können.

Um in diesem Zusammenhang zu modellieren, welche Komponenten des Systems mit der Umgebung interagieren können, werden häufig Graphen mit zusätzlichen Interfaces betrachtet. Dabei beschreiben diese Interfaces die nach außen hin sichtbaren Teile des Systems, wobei die Anzahl der Interfaces im Allgemeinen nicht beschränkt ist. Dadurch ist es möglich komplexe Modelle durch Komposition von kleineren Modellen aufzubauen. Dazu werden die Teilmodelle über ihren Interfaces verklebt. Mit Hilfe geeigneter Techniken, die die Korrektheit von Teilsystemen in beliebigen Kontexten überprüfen, ist es somit möglich, komplexe Modelle zu verifizieren, indem man die Korrektheit der einzelnen Teilmodelle nachweist.

Wenn man solche Graphtransformationssysteme im Rahmen des algebraischen Ansatzes untersucht, können die Interfaces wiederum als Graphen ausgefasst werden, die mittels Graphmorphismen in den Modellgraphen eingebettet werden. In unserer Session wollen wir einige Möglichkeiten und Anwendungen dieser Idee vorstellen und diskutieren. Unter anderem:

Decidability Results for Graph Transformation Systems

Sessionleiter:

Aufgrund ihrer Flexibilität können Graphen zur Modellierung sehr verschiedener Systeme verwendet werden. Dynamische Veränderungen der Systeme werden dabei durch Graphtransformationen realisiert. Die Ausdrucksmächtigkeit von Graphtransformationssystemen erschwert jedoch gleichzeitig ihre Analyse und Verifikation. Bereits grundlegende Probleme, wie das Erreichbarkeitsproblem oder das Überdeckbarkeitsproblem sind für Graphtransformationssysteme unentscheidbar, falls unendlich viele Graphen erreichbar sind. Neben der Frage, welche Probleme für Graphtransformationssysteme entscheidbar sind, stellt sich auch die Frage nach geeigneten Einschränkungen, die bewirken, dass wichtige Fragestellungen über Graphtransformationssysteme entscheidbar werden. Beispielsweise ist das Erreichbarkeitsproblem entscheidbar, wenn die Regeln des Graphtransformationssystems weder Knoten noch Kanten löschen. Auch die Frage nach einer Hierarchie zwischen den verschieden eingeschränkten Graphtransformationssystemen kommt in diesem Zusammenhang auf. Im Falle der Erreichbarkeit und Überdeckbarkeit konnte bis jetzt keine solche Hierarchie entdeckt werden, da es ebenso eingeschränkte Graphtransformationssysteme gibt für die Erreichbarkeit entscheidbar ist und Überdeckbarkeit nicht, wie für den umgekehrten Fall.

In meiner Session soll es daher um mögliche Einschränkungen gehen, wie Regeln, die nur löschen, nicht löschen oder das Label der Knoten und Kanten verändern dürfen, und um deren Auswirkungen auf die Ausdrucksmächtigkeit des Graphtransformationssystems.

Parallel Verification Algorithms

Sessionleiter:

Recent trends in hardware architecture - namely multi-core CPUs, many-core GPUs and GPGPUs - have made it necessary to redesign algorithms in order to exploit the full performance of such systems. Even though much theoretical research has been conducted in the field of concurrency theory, the practical application still remains a challenge. In the field of formal verification it also makes sense to consider parallel computation in order to deal with larger state spaces, take advantage of work sharing and push the boundary further towards industrial-strength problem specifications.

The session is intended to give an overview of current approaches exploiting parallelism in formal verification and lead to a discussion about opportunities, shortcomings and perspectives of parallel verification.

Mission Impossible

Sessionleiter:

A well-known result by Palamidessi tells us that the synchronous pi-calculus is more expressive than its asynchronous variant. Based on this result there are several proofs that there is no good encoding from the synchronous pi-calculus into the asynchronous pi-calculus with respect to different conditions on the notion of a good encoding, for example divergence reflection in combination with uniformity or strong operational correspondence. Gorla argues that these conditions are too hard and that many practical interesting and well accepted encodings do not meet such hard conditions. Instead he identifies a combination of five criteria that an encoding should satisfy, conjectures that these five criteria suffice to prove the inability to encode synchrony and gives some proofs that add only slightly stronger assumptions. Albeit impossible, we will nevertheless present an encoding from the synchronous pi-calculus into the asynchronous pi-calculus that meets all five criteria.

Causalities and their Role in Encoding Synchrony

Sessionleiter:

We will present an encoding of synchrony in two different formalisms of concurrency, namely for petri nets and the pi-calculus. As already stated (at least for the petri net encoding) these two encodings preserve the linear time semantics and also interleaving semantics of the original term to some extent but they do not preserve branching time semantics. Moreover it turns out that both encodings induce some kind of new causalities compared with the original term. We want to discuss the role of causalities within encodings from synchronous into asynchronous interactions. More precisely we conjecture that any divergence reflecting encoding of synchrony respects neither branching time equivalences nor causality respecting equivalences. Showing that this feature holds for both concurrent formalisms indicates that it might be a general feature of synchrony.

Erzeugung fehlender Komponenten (Submoduleconstruction)

Sessionleiter:

Abstract als PDF

Modellierung und maschinelle Verifikation verteilter Algorithmen

Sessionleiter:

In verteilten Algorithmen werden mit Hilfe lokaler Berechnungen globale Ziele erreicht. Daher erfolgt die Spezifikation der gewünschten Eigenschaft eines konkreten Algorithmus in der Regel als globale Eigenschaft. Dagegen liegt der Algorithmus meist als lokale Spezifikation vor, häufig als pseudocodeähnliche Prozessbeschreibung. Der unterschiedliche Beschreibungsansatz (lokal vs. global) sowie die wenig formale Beschreibung des Algorithmus (Pseudocode) erschweren die Beweisführung und die Nachvollziehbarkeit von Korrektheitsbeweisen für diese Algorithmen. In der Dissertation von Rachele Fuzzati wurden zwei Konsensus-Algorithmen untersucht, indem sowohl die Eigenschaften als auch der Algorithmus in einem formaleren Modell formuliert wurden. Wir haben dieses Modell in ein Modell für den Theorembeweiser Isabelle/HOL übertragen, die Korrektheitsbeweise nachvollzogen und analysiert, welche Teile des Modells für eine formale (maschinelle) Verifikation günstig sind und wie man Teile des Modells verändern müsste, um die Beweisführung zu erleichtern. Dazu ist es notwendig zunächst allgemeine Merkmale der Beweise und häufig auftretende Probleme zu analysieren und zu bewerten, wie diese durch die Wahl des Modells beeinflusst werden. Ziel der Session ist daher diese Merkmale aufzuzeigen und für die gefundenen Probleme Lösungsansätze darzustellen und zu erweitern.

Comparing two speculative memory model semantics

Sessionleiter:

The Java memory model (JMM) aims to be a formal specification of how compiler and hardware optimizations may alter the standard interleaving semantics of multi-threaded Java programs.
It is today well-known that the JMM fails to fulfil several of its design-goals. One aspect that has been unsatisfactorily implemented in the JMM is speculative execution (out-of-order execution) of instructions. Therefore, several different proposals have been made to formally capture speculative execution. It is, however, unclear, how, and if at all, these proposals relate to each other. In this talk, I will formally compare two speculative semantics, which differ significantly in their technical approach, by means of a suitable simulation relation.

Using the Goblint's dataflow analysis to detect parallelization issues in C++ modules

Sessionleiter:

It can be difficult for companies with large code bases, to find out what must be done to parallelize their single-threaded systems, even if they can identify subtasks that they believe to be mostly functionally independent. We consider systems that run a number of state machines that are implemented as C++ classes.

We designed a sound dependency analysis in our data flow analysis framework Goblint, that locates possible dependencies on outside data of a given C++ class. From the analysis we can infer that a class is definitely thread safe or give warnings where thread safety cannot be guaranteed. Because Goblint works on C code, we used LLVM to lower the given C++ classes to C.

Using the result of our analysis we can estimate, how much the code needs to be changed. By using our proposed analysis, we suggest a workflow so that the parallelization work can be done in a gradual manner.

FunkyImp, Semi functional language design for parallel programming
Alternative Title: Lock-free Parallel Programming in an Event-driven and Side-effecting World

Sessionleiter:

Abstract als PDF

The Isabelle Collection Framwork

Sessionleiter:

Modern interactive theorem provers like Isabelle, Coq, and ACL2 support for extracting executable code from the proofs. The extracted code is usually in some functional programming language. In order to get efficient executable code, one needs to use efficient functional data structures. In this session, we focus on Isabelle/HOL. Here, the Isabelle Collection Framework specifies interfaces on common collection datastructures, like sets, maps, queues, and priority queues, and provides various implementations like red-black trees, finger trees, and binomial queues. In order to generate executable code, it features a data refinement approach, first proving the correctness of the algorithm on the interface level (or even on some more abstract level), and then refining the algorithm and its correctness statement to the concrete implementation. The refinement step is canonical, and can be done mostly automatic.

In the first part of this session, we give a short overview of the Isabelle Collection Framework and present the formalization of Dijkstra's shortest paths algorithm as an example. The second part of the session is discussion.

Von der Theorie zur Implementierung

Sessionleiter:

Im Rahmen von Concurrency hat man oft mit State-Explosion zu kämpfen hat, und daher sind selbst kleine Beispiele zur Veranschaulichung neuer Verfahren in der Regel so komplex, dass man sie nicht von Hand durchrechnen möchte. In solchen Fällen ist eine Prototypische Implementierung hilfreich. Bei direkter Umsetzung erhält man meistens einen Prototypen, der zwar für kleine Beispiele das gewünschte liefert, aber bei größeren Anwendungen in die Knie geht. Ein Prototyp sollte aber vielleicht auch andeuten, dass es mit etwas mehr Aufwand durchaus möglich ist eine effiziente Implementierung zu erreichen. Ein möglicher Ausweg ist die Verwendung symbolischer statt expliziter Darstellungen, z.B. in Form von BDDs. Diese erfordern meiner Erfahrung nach jedoch direkt mehr Zeitaufwand durch überlegungen zur Codierung, Variablenordnung, etc. und sind in der Bedienung sehr aufwendig. Daher erlauben sie es nicht mal schnell einen Prototypen zu erstellen. Ich will in der Sitzung zum Austausch von Erfahrungen zu prototypischen Implementierungen von Analysen im Umfeld von Concurrency anregen und insbesondere auch von Erfahrungen mit Bibliotheken zum symbolischen Rechnen.

Graphbasierte Verifikation

Sessionleiter:

Heapbasierte Datenstrukturen werden heute in vielen Softwareprojekten eingesetzt. Durch einen theoretisch unbeschränkten Heap wird ein unendlicher Zustandsraum induziert, den Standard Verifikationsverfahren nicht handhaben können. Abstraktion ist ein häufig genutztes Hilfsmittel für die Analyse unendliche Zustandsräume. Einen vielversprechende Verfahren zur Abstraktion heapbasierten Datenstrukturen nutzt Hyperkantenersetzungsgrammatiken. Hierbei werden Ersetzungsregeln genutzt um Heapstrukturen partiell zu abstrahieren bzw. zu konkretisieren.

Ich werde die Abstraktion im Detail vorstellen. Insbesondere werde ich hierbei auf die verschiedene Anforderungen an die genutzten Grammatiken eingehen. Diese Anforderungen sind nötig um die Korrektheit zu garantieren, stellen aber keine Einschränkungen dar.

Geometrische Ansätze zur Beschleunigung von Überdeckbarkeitsalgorithmen in Linearen Whileprogrammen

Sessionleiter:

Lineare Whileprogramme sind ein Modell nebenläufiger Berechnungen, welches unter anderem Petrinetze verallgemeinert. Wichtige Fragen wie Deadlockfreiheit oder wechselweiser Ausschluss lassen sich für Whileprogramme auf die Überdeckbarkeit von Zuständen zurückführen. Diese Arbeit schlägt eine geometrische Interpretation von Zustandsmengen als konvexes Polyeder vor, um die Effizienz von Überdeckungsalgorithmen zu steigern. Die Betrachtung erlaubt eine effiziente Berechnung der Vorgänger einer Zustandsmenge. Ferner lassen sich mit ihrer Hilfe Grenzwerte von Transitionsfolgen direkt, ohne Interation, berechnen. Schließlich liefert die geometrische Sicht eine konservative Verallgemeinerung von S-Invarianten für Petrinetze auf lineare Whileprogramme, welche zum Pruning in der Rückwärtssuche benutzt werden können.

Verfügbarkeitssprachen für Netzwerkanwendungen

Sessionleiter:

Verifikation von Netzwerkanwendungen geht oft idealisiert von vollständiger Verfügbarkeit der Komponenten aus. Diese Annahme ist in der Regel zu restriktiv, da sie auch bei kurzzeitigen Ausfällen keine Aussagen über die Korrektheit des Systems mehr erlaubt. Wir haben ein formalsprachliches Modell entwickelt, das Verfügbarkeit über Anzahlbedingungen ausdrückt und so in die Verifikation einfließen lässt. Für diese regulären Verfügbarkeitssprachen konnte eine automatentheoretische Charakterisierung angegeben werden, und auch das für die Verifikation dringliche Problem der Komplementierung wurde positiv beantwortet. Nun stellen wir einen Ansatz vor, der Verfügbarkeitssprachen über eine Erweiterung von MSO logisch fasst. Wir hoffen, dass er uns einen Zugang zum Model-Checking eröffnet und die Beantwortung noch offener Entscheidbarkeitsfragen ermöglicht.


Alexander Wenner
Last modified: Fr Feb 4 11:25:59 CET 2011