Wed 17 Jul 2019 10:30 - 10:50 at Mancy - Language Design and Implementation Chair(s): John Wickerson

Developing interactive applications (apps) against event-driven software frameworks such as Android is notoriously difficult. To create apps that behave as expected, developers must follow complex and often implicit asynchronous programming protocols. Such protocols intertwine the proper registering of callbacks to receive control from the framework with appropriate application- programming interface (API) calls that in turn affect the set of possible future callbacks. An app violates the protocol when, for example, it calls a particular API method in a state of the framework where such a call is invalid. What makes automated reasoning hard in this domain is largely what makes programming apps against such frameworks hard: the specification of the protocol is unclear, and the control flow is complex, asynchronous, and higher-order. In this paper, we tackle the problem of specifying and modeling event-driven application-programming protocols. In particular, we formalize a core meta-model that captures the dialogue between event-driven frameworks and application callbacks. Based on this meta-model, we define a lan- guage called lifestate that permits precise and formal descriptions of application-programming protocols and the callback control flow imposed by the event-driven framework. Lifestate unifies modeling what app callbacks can expect of the framework with specifying rules the app must respect when calling into the framework. In this way, we effectively combine lifecycle constraints and typestate rules. To evaluate the effectiveness of lifestate modeling, we provide a dynamic verification algorithm that takes as input a trace of execution of an app and a lifestate protocol specification to either produce a trace witnessing a protocol violation or a proof that no such trace is realizable.

Wed 17 Jul

Displayed time zone: Belfast change

10:30 - 12:10
Language Design and ImplementationResearch Papers at Mancy
Chair(s): John Wickerson Imperial College London
10:30
20m
Research paper
Lifestate: Event-Driven Protocols and Callback Control Flow
Research Papers
Shawn Meier University of Colorado, Boulder, Sergio Mover Ecole Polytechnique, Bor-Yuh Evan Chang University of Colorado Boulder
DOI Media Attached
10:50
20m
Research paper
Godot: All the Benefits of Implicit and Explicit Futures
Research Papers
Kiko Fernandez-Reyes Uppsala University, Einar Broch Johnsen University of Oslo, Dave Clarke Uppsala Univ. Sweden and KU Leuvern, Ludovic Henrio CNRS, Tobias Wrigstad Uppsala University
DOI Media Attached
11:10
20m
Research paper
Towards Language-Parametric Semantic Editor Services based on Declarative Type System SpecificationsBrave New Idea
Research Papers
Daniel A. A. Pelsmaeker Delft University of Technology, Netherlands, Hendrik van Antwerpen TU Delft, Eelco Visser Delft University of Technology
DOI Media Attached
11:30
20m
Research paper
Multitier Modules
Research Papers
Pascal Weisenburger Technische Universität Darmstadt, Guido Salvaneschi TU Darmstadt
DOI Media Attached
11:50
20m
Research paper
Scopes and Frames Improve Meta-Interpreter Specialization
Research Papers
Vlad Vergu TU Delft, Eelco Visser Delft University of Technology, Andrew Tolmach Portland State University
DOI Media Attached