6. Arbeitstagung Programmiersprachen (ATPS 2013)

Programm

Veranstaltungsort: Kármán-Auditorium, Foyer

08:00 - 08:30   Registrierung

Veranstaltungsort: Kármán-Auditorium, Hörsaal SFo4

08:30 - 08:45   Begrüßung und Eröffnung

• 08:30 - 08:45 Jens Knoop, Janis Voigtländer

08:45 - 09:45   Sitzung 1: Eingeladener Hauptvortrag (Sitzungsleitung: Janis Voigtländer)

• 08:45 - 09:45 Jürgen Giesl. Automated Termination Analysis: From Term Rewriting to Programming Languages.

09:45 - 10:00   Kurze Pause

10:00 - 10:30   Sitzung 2: Parallelität und Funktionale Programmierung (Sitzungsleitung: Clemens Grelck)

• 10:00 - 10:30 Till Berger und David Sabel. Parallelizing DPLL in Haskell.

   

10:30 - 11:00   Kaffeepause

11:00 - 12:30   Sitzung 3: Sprachimplementierung und Programmanalyse (Sitzungsleitung: Wolf Zimmermann)

• 11:00 - 11:30 Gergö Barany. Static and Dynamic Method Unboxing for Python.
• 11:30 - 12:00 Dennis Klassen. ViCE-UPSLA: A Visual High Level Language for Accurate Simulation of Interlocked Pipelined Processors.
• 12:00 - 12:30 Roland Lezuo, Gergö Barany und Andreas Krall. CASM: Implementing an Abstract State Machine based Programming Language.

   

12:30 - 14:00   Mittagspause

14:00 - 15:30   Sitzung 4: Sprachen und Analysen für mobile Systeme (Sitzungsleitung: Michael Leuschel)

• 14:00 - 14:30 Henning Heitkötter, Tim A. Majchrzak und Herbert Kuchen. MD²-DSL - eine domänenspezifische Sprache zur Beschreibung und Generierung mobiler Anwendungen.
• 14:30 - 15:00 Steven Arzt, Kevin Falzon, Andreas Follner, Siegfried Rasthofer, Eric Bodden und Volker Stolz. How useful are existing monitoring languages for securing Android Apps?
• 15:00 - 15:30 Jürgen Graf, Martin Hecker und Martin Mohr. Using JOANA for Information Flow Control in Java Programs - A Practical Guide.

   

15:30 - 16:00   Kaffeepause

16:00 - 17:30   Sitzung 5: Modellierung in Theorie und Anwendung (Sitzungsleitung: Herbert Kuchen)

• 16:00 - 16:30 Reiner Jung, Christian Schneider und Wilhelm Hasselbring. Type-Systems for Domain-specific Languages.

   

• 16:30 - 17:00 Jan Oliver Ringert, Bernhard Rumpe und Andreas Wortmann. From Software Architecture Structure and Behavior Modeling to Implementations of Cyber-Physical Systems.

   

• 17:00 - 17:30 Baltasar Trancón Y Widemann und Markus Lepper. Paisley: A Pattern Matching Library for Arbitrary Object Models.

   

17:30 - 18:30   Sitzung 6: Eingeladenes Impulsreferat mit anschließender Podiums- und Publikumsdiskussion (Sitzungsleitung: Jens Knoop)

• 17:30 - 17:45 Wolf Zimmermann. Modell-basierte Programmgenerierung und Methoden des Übersetzerbaus - Zwei Seiten derselben Medaille?
• 17:45 - 18:30 Podiums- und Publikumsdiskussion.
                        Auf dem Podium: Clemens Grelck, Reiner Jung, Herbert Kuchen, Jan Oliver Ringert, Wolf Zimmermann.

   

18:30 - 18:35   Abschluss und Verabschiedung

• 18:30 - 18:35 Jens Knoop, Janis Voigtländer

Eingeladene Beiträge
 

• Hauptvortrag
  Jürgen Giesl - Automated Termination Analysis: From Term Rewriting to Programming Languages.

  Abstract: Termination is a crucial property of programs. Therefore, techniques to analyze termination automatically are highly important for program verification. Traditionally, techniques for automated termination analysis were mainly studied for declarative programming paradigms such as logic programming and term rewriting. However, in the last years, several powerful techniques and tools have been developed which analyze the termination of programs in many programming languages including Java, C, Haskell, and Prolog.
        In order to re-use the wealth of existing tools and techniques developed for termination analysis of term rewriting (see e.g., [GTSKF06, Zan03]), we developed a transformational methodology to prove termination of programs in different languages. In a front end, the program is automatically transformed into a term rewrite system (TRS) such that termination of the TRS implies termination of the original program. To obtain TRSs which are suitable for automated termination proofs, the front end proceeds in two steps. In the first step, the program is executed symbolically to generate a so-called termination graph. This graph represents all possible evaluations of the program in a finite way. In the second step, the edges of the graph are transformed to rewrite rules. Finally, existing rewriting techniques are used in the back end to prove termination of the resulting TRS.
        We developed such approaches to prove termination of Prolog [GSSK+12, SKGS+10], Haskell [GRSK+11], and Java [BMOG12, BOG11, BOvG10, BSOG12, OBvG10]), and integrated them into our termination tool AProVE [GST06]. As shown at the annual International Termination Competition,¹ AProVE is currently not only the most powerful tool for automated termination analysis of TRSs, but also for Prolog, Haskell, and Java. This shows that the proposed methodology for rewrite-based automated termination analysis indeed leads to competitive results.
   
  ¹See termination-portal.org/wiki/Termination_Competition

• Impulsreferat mit anschließender Podiums- und Publikumsdiskussion
  Wolf Zimmermann - Modell-basierte Programmgenerierung und Methoden des Übersetzerbaus - Zwei Seiten derselben Medaille?

  Abstract: In der vergangenen Dekade hat Modell-basierte Entwicklung in der Softwaretechnik zunehmende Bedeutung gewonnen, vgl. z.B. [TS07, SRC+ 12, JLM+ 12]. Aus Modellen, die in einer formalen Sprache definiert sind (Domänen-spezifische Sprache) wird Code generiert, der die Modelle implementiert. Da Domänen-spezifische Sprachen nicht selten starken Änderungen und Erweiterungen unterworfen sind, haben sich Werkzeugkästen wie beispielsweise das Eclipse Modeling Framework (kurz: EMF) etabliert [SBMP08], mit deren Hilfe die Codegeneratoren selbst generiert werden können. Zur Spezifikation Domänen-spezifischer Sprachen wird ein Metamodell definiert, aus dem dann mittels Modelltransformationen die Transformationsregeln in die Zielsprache spezifiziert werden. Neben dem Codegenerator für eine Domänen-spezifische Sprache werden beispielsweise mit der EMF-Technologie Editoren für die Domänen-spezifische Sprache generiert, die auch durch die Eclipse-Technologie in Programmier- und Anwendungsumgebungen eingebettet werden können.
         Als grundlegende Technologie werden Metamodelle meist in graphischer Form (z.B. UML-Klassendiagrammen) oder durch eine kontextfreie Grammatik [EEK+ 12] definiert. Mittels OCL können Konsistenzbedingungen angegeben werden, die alle Modelle einer Domänen-spezifischen Sprache erfüllen müssen. Meist führen diese zu Laufzeitprüfungen. Oft werden zusätzlich im Code des Modell-basierten Codegenerators noch manuelle Ergänzungen und Änderungen vorgenommen. Gründe können Effizienzsteigerungen in der Codegenerierung oder weitere Überprüfungen sein. Eine Weiterentwicklung einer Domänen-spezifischen Sprache erfordert daher nicht selten eine grundsätzliche Revision und Überarbeitung des Codegenerators.
        Die Aufgabenstellung für Übersetzer ist nahezu identisch: ein Programm in höherer Programmiersprache wird in ein Programm einer Maschinensprache oder einer anderen Hochsprache (Cross-Compiler) transformiert. In einem Übersetzer wird der Quelltext auf korrekte Syntax hin analysiert und in eine interne Datenstruktur, den abstrakten Syntaxbaum transformiert. Anschließend werden Konsistenzbedingungen wie beispielsweise Typkorrektheit analysiert. Im Falle eines Cross-Compilers wird der abstrakte Syntaxbaum in das Zielprogramm transformiert, ansonsten in eine Zwischensprache, die weiter in den Maschinencode übersetzt wird. Hier haben sich z.T. seit Mitte der 1970er Jahre Werkzeuge [Joh75, KHZ82, DUP+82] und Werkzeugkästen zur Generierung von Übersetzern etabliert. Aktuelle Werkzeugkästen sind beispielsweise ANTLRv3 [Par07] oder Eli [KWS07]. Die Syntaxanalyse wird durch Angabe der Lexik als reguläre Ausdrücke, durch eine kontextfreie Grammatik für die konkrete Syntax und der Datenstruktur für die abstrakte Syntax angegeben. Die Konsistenzprüfungen können aus geordneten Attributierten Grammatiken generiert werden, die Transformation in die Zielsprache bzw. Zwischensprache wird aus Baumtransformationen generiert. Im generierten Übersetzer müssen keine Änderungen mehr vorgenommen werden, da Hilfsfunktionen Bestandteil der Spezifikationen sind. Hilfsfunktionen sind bereits in der Wirtssprache (der Sprache, in der der Übersetzer implementiert ist) definiert. Sie können deshalb problemlos eingebunden und geändert werden. Dadurch ist es nicht notwendig, den generierten Code anzufassen, und man kann agil einen Übersetzer Sprachkonzept um Sprachkonzept anreichern.
        Als Fazit ergibt sich eine deutliche Korrespondenz zwischen der Generierung Modellbasierter Codegeneratoren und der Generierung von Übersetzern (vgl. auch [Jör11]): Die Begriffe Metamodell und Abstrakte Syntax sind konzeptuell identisch. Konsistenzbedingungen werden durch unterschiedliche Technologien wie OCL bzw. attributierte Grammatiken definiert und Modelltransformationen entsprechen konzeptuell Baumtransformationen. Für die praktische Entwicklung von Modell-basierten Codegeneratoren kann daher ohne Weiteres Übersetzerbautechnologie verwendet werden. Ein möglicher Vorteil durch die Verwendung von attributierten Grammatiken an Stelle von OCL wäre eine statische Prüfung der Konsistenz der Modelle anstatt dies auf Laufzeitprüfungen zu verlagern. Durch die Definition von Hilfsfunktionen in der Wirtssprache anstelle derer nachträglichen manuellen Integration in den Codegenerator wäre eine agilere und kostengünstigere Entwicklung von Modell-basierten Codegeneratoren möglich. Die für die industrielle Praxis wichtige Generierung der Editoren für Domänen-spezifische Sprachen und deren Einbettung in Programmier- und Anwendungsumgebungen müsste allerdings noch erfolgen, da dies durch Übersetzertechnologie bisher wenig Beachtung gefunden hat.

  Auf dem Podium: Clemens Grelck, Reiner Jung, Herbert Kuchen, Jan Oliver Ringert, Wolf Zimmermann.

Angenommene eingereichte Beiträge (keine besondere Reihenfolge)
 

• Till Berger und David Sabel - Parallelizing DPLL in Haskell

  Abstract: We report on a case study of implementing parallel variants of the Davis-Putnam-Logemann-Loveland algorithm for solving the SAT problem of propositional formulas in the functional programming language Haskell. We explore several state of the art programming techniques for parallel and concurrent programming in Haskell and provide the corresponding implementations. Based on our experimental results, we compare several approaches and implementations.

• Henning Heitkötter, Tim A. Majchrzak und Herbert Kuchen - MD²-DSL - eine domänenspezifische Sprache zur Beschreibung und Generierung mobiler Anwendungen

  Abstract: Entwickler mobiler Anwendungen, sogenannter Apps, stehen einer heterogenen Landschaft an mobilen Plattformen gegenüber, die sich hinsichtlich ihrer Programmierung stark unterscheiden. Häufig sollen zumindest die weit verbreiteten Betriebssysteme iOS und Android unterstützt werden. Dabei sollen Apps dem nativen, plattformtypischen Aussehen und Verhalten genügen oder zumindest nachempfunden werden. Bestehende Cross-Plattform-Lösungen im mobilen Umfeld unterstützen letztere Anforderung nicht, so dass Entwickler oftmals gezwungen sind, dieselbe App parallel für mehrere Plattformen nativ zu entwickeln. Dies erhöht den Entwicklungsaufwand erheblich, zumal die Implementierung auf einem niedrigen Abstraktionsniveau erfolgt. Dieser Beitrag stellt das Framework MD² und die domänenspezifische Sprache MD²-DSL vor, die es ermöglicht, Apps mit vorwiegend geschäftlichem Hintergrund auf einem gehobenen Abstraktionsniveau prägnant zu beschreiben. Der modellgetriebene Ansatz MD² generiert aus den textuellen MD²-DSL-Modellen iOS- und Android-Apps. Die Sprache MD²-DSL enthält Konstrukte zur Abbildung und Umsetzung typischer Anforderungen an Apps und stellt somit eine Alternative zur wiederholten Implementierung einer App auf verschiedenen Plattformen dar.

• Gergö Barany - Static and Dynamic Method Unboxing for Python

  Abstract: The Python programming language supports object-oriented programming using a simple and elegant model that treats member variables, methods, and various metadata as instances of a single kind of 'attribute'. While this allows a simple implementation of an interpreter that supports advanced metaprogramming features, it can inhibit the performance of certain very common special cases. This paper deals with the optimization of code that loads and then calls object methods.
         We modify Python's compiler to emit special bytecode sequences for load/call pairs on object attributes to avoid unnecessary allocation of method objects. This can result in considerable speedups, but may cause slowdowns at call sites that refer to builtin functions or other special attributes rather than methods. We therefore extend this static compile-time approach by a dynamic runtime quickening scheme that falls back to the generic load/call sequence at such call sites.
         The experimental evaluation of dynamic unboxing shows speedups of up to 8% and rare slowdowns caused by as yet unresolved excessive instruction cache misses. A comparison with a common manual optimization of method calls in Python programs shows that our automatic method is not as powerful but more widely applicable.

• Baltasar Trancón Y Widemann und Markus Lepper - Paisley: A Pattern Matching Library for Arbitrary Object Models

  Abstract: Professional development of software dealing with structured models requires more systematic approach and semantic foundation than standard practice in general-purpose programming languages affords. One remedy is to integrate techniques from other programming paradigms, as seamless as possible and without forcing programmers to leave their comfort zone. Here we present a tool for the implementation of pattern matching as fundamental means of automated data extraction from models of arbitrary shape and complexity in a general-purpose programming language. The interface is simple but, thanks to elaborate and rigorous design, is also light-weight, portable, non-invasive, type-safe, modular and extensible. It is compatible with object-oriented data abstraction and has full support for nondeterminism by backtracking. The tool comes as a library consisting of two levels: elementary pattern algebra (generic, highly reusable) and pattern bindings for particular data models (specific, fairly reusable, user-definable). Applications use the library code in a small number of idiomatic ways, making pattern-matching code declarative in style, easily writable, readable and maintainable. Library and idiom together form a tightly embedded domain-specific language; no extension of the host language is required. The current implementation is in Java, but assumes only standard object-oriented features, and can hence be ported to other mainstream languages.

• Jan Oliver Ringert, Bernhard Rumpe und Andreas Wortmann - From Software Architecture Structure and Behavior Modeling to Implementations of Cyber-Physical Systems

  Abstract: Software development for Cyber-Physical Systems (CPS) is a sophisticated activity as these systems are inherently complex. The engineering of CPS requires composition and interaction of diverse distributed software modules. Describing both, a system~s architecture and behavior in integrated models, yields many advantages to cope with this complexity: the models are platform independent, can be decomposed to be developed independently by experts of the respective fields, are highly reusable and may be subjected to formal analysis.
        In this paper, we introduce a code generation framework for the MontiArcAutomaton modeling language. CPS are modeled as Component & Connector architectures with embedded I/O^ω automata. During development, these models can be analyzed using formal methods, graphically edited, and deployed to various platforms. For this, we present four code generators based on the MontiCore code generation framework, that implement the transformation from MontiArcAutomaton models to Mona (formal analysis), EMF Ecore (graphical editing), and Java and Python (deployment). Based on these prototypes, we discuss their commonalities and differences as well as language and application specific challenges focusing on code generator development.

• Steven Arzt, Kevin Falzon, Andreas Follner, Siegfried Rasthofer, Eric Bodden und Volker Stolz - How useful are existing monitoring languages for securing Android Apps?

  Abstract: The Android operating system is currently dominating the mobile device market in terms of penetration and growth rate. An important contributor to its success are a wealth of cheap and easy-to-install mobile applications, known as apps. Today, installing untrusted apps is the norm, though this comes with risks: malware is ubiquitous and can easily leak confidential and sensitive data.
        In this work, we investigate the extent to which we can specify complex information flow properties using existing specification languages for runtime monitoring, with the goal to encapsulate potentially harmful apps and prevent private data from leaking. By modelling a set of representative, Android-specific security policies with Tracematches, JavaMOP, Dataflow Pointcuts and PQL, we are able to identify policylanguage features that are crucial for effectively defining runtime-enforceable Android security properties.
        Our evaluation demonstrates that while certain property languages suit our purposes better than others, they all lack essential features that would, if present, allow users to provide effective security guarantees about apps. We discuss those shortcomings and propose several possible mechanisms to overcome them.

• Reiner Jung, Christian Schneider und Wilhelm Hasselbring - Type-Systems for Domain-specific Languages

  Abstract: Model-driven software development employs models to describe different aspects of a system on different levels of abstraction. These aspects are driven by technology or application domain. Modeling is often done in specific graphical or textual notations, called domain-specific languages (DSL). In recent years such languages became very popular in the modeling community to describe structure and sometimes behavior. In the context of type systems, these structures are called types and the behavior is modeled with expressions. The programming language community has developed many concepts to model and specify type systems and the semantics of expressions. However, in the modeling community this is often neglected when specifying meta models and describing their semantics, what may cause problems in developing checks and generators for DSLs. To address this issue, we present an approach, that provides guidance and support during DSL development based on established knowledge on type systems and generator construction, to ease the integration of type systems in DSL. We evaluate this approach with the Xtext language engineering framework.

• Dennis Klassen - ViCE-UPSLA: A Visual High Level Language for Accurate Simulation of Interlocked Pipelined Processors

  Abstract: Simulation of processors is needed in early stages of development to reduce cost and increase quality of processor designs. Suitable simulators can be generated automatically from high-level specifications of the processor architecture. For this purpose, we have developed the domain specific visual language ViCE-UPSLA. It allows to describe pipeline based register-register, register-memory processor architectures and generates efficient simulators for such processors. In this way a variety of processors can be quickly prototyped for validation and evaluation. We have successfully used ViCE-UPSLA to model and simulate a processor with an ARM [ARM00] like architecture.

• Roland Lezuo, Gergö Barany und Andreas Krall - CASM: Implementing an Abstract State Machine based Programming Language

  Abstract: In this paper we present CASM, a general purpose programming language based on abstract state machines (ASMs). We describe the implementation of an interpreter and a compiler for the language. The demand for efficient execution forced us to modify the definition of ASM and we discuss the impact of those changes. A novel feature for ASM based languages is symbolic execution, which we briefly describe. CASM is used for instruction set simulator generation and for semantic description in a compiler verification project. We report on the experience of using the language in those two projects. Finally we position ASM based programming languages as an elegant combination of imperative and functional programming paradigms which may liberate us from the von Neumann style as demanded by John Backus.

• Jürgen Graf, Martin Hecker und Martin Mohr - Using JOANA for Information Flow Control in Java Programs - A Practical Guide

  Abstract: We present the JOANA (Java Object-sensitive ANAlysis) framework for information flow control (IFC) of Java programs. JOANA can analyze a given Java program and guarantee the absence of security leaks, e.g. that a online banking application does not send sensitive information to third parties. It applies a wide range of program analysis techniques such as dependence graph computation, slicing and chopping of sequential as well as concurrent programs. We introduce the Java Web Start application IFC Console and show how it can be used to apply JOANA to arbitrary programs in order to specify and verify security properties.