Document Open Access Logo

Lifestate: Event-Driven Protocols and Callback Control Flow

Authors Shawn Meier , Sergio Mover , Bor-Yuh Evan Chang



PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2019.1.pdf
  • Filesize: 0.9 MB
  • 29 pages

Document Identifiers

Author Details

Shawn Meier
  • University of Colorado Boulder, USA
Sergio Mover
  • École Polytechnique, Institute Polytechnique de Paris, Palaiseau, France
Bor-Yuh Evan Chang
  • University of Colorado Boulder, USA

Acknowledgements

Many thanks to Edmund S. L. Lam, Chance Roberts, and Chou Yi for help in gathering traces, as well as Alberto Griggio for a convenient tool for running tests. We also thank Aleksandar Chakarov, Maxwell Russek, the Fixr Team, and the University of Colorado Programming Languages and Verification (CUPLV) Group for insightful discussions, as well as the anonymous reviewers for their helpful comments.

Cite AsGet BibTex

Shawn Meier, Sergio Mover, and Bor-Yuh Evan Chang. Lifestate: Event-Driven Protocols and Callback Control Flow. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 1:1-1:29, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.ECOOP.2019.1

Abstract

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 language 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.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Software verification
Keywords
  • event-driven systems
  • application-programming protocols
  • application framework interfaces
  • callbacks
  • sound framework modeling
  • predictive dynamic verification

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail