Smart-phones and tablets have recently entered our lives and have gained popularity in an unprecedented rapidness. So has the variety and amount of application that run on mobile devices. Programming for mobile devices encounters some obstacles that are absent in programming for traditional computers. For instance, mobile operating systems such as Andorid and iOS are updated in a frequent manner, requiring the program and its analysis be robust to such changes. Another example has to do with visualization, as applications run both on a varienty of screens with different sizes and proportions, and on very small screens, each phenomenon incurring its own set of difficulties. These, and other obstacles unique to mobile apps, offer an opportunity to leverage ExCAPE synthesis solutions to improve productivity of programmers on mobile platforms.
We have been working on applying synthesis to the problem of identifying bugs in mobile applications. The challenge in finding bugs in such applications is that symbolic execution, the workhorse of modern bug-finding techniques, has trouble scaling to the complex code that makes up a mobile platform such as Android. The traditional solution to this problem has been to create models of the framework that expose only those aspects of the platform that are necessary to analyze an application. Our goal is to use synthesis to produce such models from traces of the interaction between the application and the platform together with high-level input provided by the user.
As a starting point, we have focused on synthesizing models involving the observer pattern, a design pattern pervasive not just in Android, but also in many UI frameworks such as swing. We have developed a prototype tool called Pasket (for Pattern Sketcher) that synthesizes executable models of observers from three artifacts provided by the user: 1. An annotated API of the framework we want to model. The API tells Pasket which classes and methods need to be synthesized; what their types are; and which of them may participate in the observer pattern. 2. Sample applications that exercise the framework in similar ways as the target programs we eventually want to analyze. 3. Auxiliary models that are needed to analyze the tutorial program but that do not involve the observer pattern. Over time, as we are able to synthesize more code we expect the size of this auxiliary information to decrease.
As a first step, we decided to try Pasket on Swing, a UI framework that is simpler than Android but shares many of the same design patterns. Using Pasket, we successfully synthesized models of the Swing framework involving JButton and JComboBox. Synthesis took less than two minutes, and the resulting code worked correctly under Java PathFinder (JPF), a Java symbolic executor. We also found that, while JPF includes models of Swing that the JPF developers wrote by hand, they are insufficient to do the same symbolic execution because they neglected models of two methods; this shows some of the benefits of automatic model synthesis. In addition to helping us find bugs in existing Android applications, these models will be crucial in helping us synthesize applications that correctly use the Android platform [JQFS14].
This project develops a programming-by-demonstration system for making browsers more useful by avoiding repetitive tasks. Avoiding repetitive tasks, such as scraping data from the web, is especially important on the phone form factor, where screen are smaller and the browsers load pages more slowly than on laptops. Our system, called Ringer, records user’s interaction with the browser and uses this demonstration to synthesize a script program that replays this demonstration. The script can also be generalized to repeat the process on related data. For example, the user’s demonstration may select one item from the web page (eg, the name of a school) and then enter the school name into another web site that returns the test scores for this school. The script can be generalized under user guidance to repeat the process for all schools on the first web site.
To provide a compelling case study, we have started collaboration with the School of Social Welfare at Berkeley . Our goal is to help social scientists collect data and make inferences form them. From a computer scientist’s perspective, the computational challenges faced by social welfare differ from the challenges addressed in big-data research agendas, presenting unique opportunities. First, key sources of data is not readily available in extant databases and must be collected by crawling, for instance, school web sites, parent-teacher meetings, court records, newspaper stories on local DUI incidents and child maltreatment, community photographs, and other sources that together facilitate inference about, say, the state of order or disorder in a neighborhood. In our research we are building tools that social scientists can guide, without any programming, to collect diverse data of interest, on a large scale, and longitudinally. Second, the computer programming needed to join these data sources is more advanced than the typical expertise of a social scientist with R or Python. Rather than require this expertise, we will work on analyzing data by demonstration. Finally, to facilitate model inference, we will allow scientists to express skeletons of models that will be completed with machine learning and software synthesis.
This project developed a synthesizer of relational queries for data stored in spreadsheets. The specification is a demonstration from the end-user who, by interacting with the synthesizer, gives examples of outputs (both positive and negative). In additional to allowing non-programmers to create complex queries with joins, the synthesizer simplifies work with data on mobile platforms with small displays and tiny keyboards. We have demonstrated the tool on an Android tablet. This work was released as an MS thesis [LB13] and will continue in the context of developing big-data tools for social scientists.
This project develops components of fast, parallel web browser. The motivation to accelerate web browsers is to make them fast enough to serve as application platforms on mobile phones; currently, phone apps are developed with iOS or Android, and browsers would make apps portable across phone ecosystems. Recently, in [MTAB13], we focused on web document layout, a problem that includes data visualization. We examined how to synthesize a parallel schedule of traversals over document trees. Our document layout programs are declaratively specified as attribute grammars and parallel traversals for GPUs and multicore CPUs are synthesized. To allow the programmer to control the schedule, we defined a declarative language of schedules where programmers may sketch any part of the schedule and the synthesizer will complete the rest. For the same motivation, the synthesizer answers debugging queries about if and how schedules may be completed and enumerates scheduling choices for autotuning.
Programming By Manipulation (PBM) is a new approach to layout programming which relies on guided exploration of candidate layouts [HBR14]. For layout, this means that designers can progressively customize visual elements by directly editing the layout of candidate engines. The key novelty is in the interaction model: synthesis is used not in simply turning demonstrations to programs but instead in helping the user navigate the space possible visualizations [see here two short demonstrating videos]. Manipulating rather than demonstrating addresses the problem of users not knowing what programs are expressible (cf. Tessa Lau's Why PBD Systems Fail).
- T. Hottelier, R. Bodik and K. Ryokai. Programming by Manipulation for Layout . Berkeley Technical Report, Aug 2014.
- J. Jeon, X. Qiu, J. S. Foster and A. Solar-Lezama. PASKET: Synthesizing Models of the Observer Pattern for Event-Driven Frameworks. Under review.
- E. Lu and Ras Bodík. Quicksilver: Automatic synthesis of relational queries. Technical report, University of California, Berkeley, Technical Report No. UCB/EECS-2013-68, 2013.
- L. A. Meyerovich, M. E. Torok, E. Atkinson, and R. Bodík. Parallel schedule synthesis for attribute grammars. In Alex Nicolau, Xiaowei Shen, Saman P. Amarasinghe, and Richard Vuduc, editors, PPOPP, pages 187–196. ACM, 2013.