The new Berkeley project in Programming Systems will improve how software is designed, implemented, tested, and deployed. We will target problematic areas in software ranging from mobile apps to distributed Web systems and consumer robotics. We expect to accelerate development of phone apps, increase the reliability of distributed programs, enable development of high-performance GPU mobile apps, and facilitate robotics programming to end users.
Our research proposition is to integrate the program with a suite of generalized tests from an early stage of program design. Our tools will keep these tests semantically coupled with their software throughout its lifetime, enabling continuous testing and automated synthesis. These tests will take a range of forms: for example, they can be provided by the programmer to serve as the program specification from which program fragments can be synthesized; the tests can be generated by the program itself and maintained to evolve in sync with the program with the goal of continuously testing program correctness.
This section gives an overview of our research approach by summarizing some of the research project and their collaboration relationships:
- The effort headed by Prof. Necula will develop methodologies and tools for creation and maintenance of unit tests. Unit tests have proven to be extremely valuable but expensive to evolve in the face of program changes. In this effort, the programmer will annotate suitable the program points; the program is then executed on the more readily available functional tests and the unit tests are recorded as values observed at the annotated points. These unit tests will be maintained with tool support as the program evolves and used to continuously test the program. Prof. Necula has recently worked in a startup company specializing in distributed Web computation and this effort builds on his expertise in testing complex programs. This synergy with other efforts is in viewing the recorded unit tests as traces of program executions and thus demonstrations of desired program behavior. Other efforts will develop tools for synthesizing programs from such demonstrations of desired behavior.
- The effort headed by Prof. Bodik and Dr. Torlak is developing tools for GPU programmers of mobile applications. Parallel programs require that programmers orchestrate a number of tricky details, from data structure layout to efficient communication. Two technologies are designed to help manage parallel programming complexity: First, rather than writing a complicated program in one sweep, the programmer will code by gradually refining a high-level program until an efficient implementation is obtained. This stepwise development changes a program P into a semantically equivalent program P0 by replacing parts of P with a more efficient implementation. The second technology is program synthesis, which will be used to obtain tricky parallel code fragments. This effort relates to Prof. Necula’s effort because test traces are used to establish semantic equivalence between consecutive refinements: P0 is considered refinement of P if both programs generate the same sequence of values. Using test traces allows us to test that the programmer does not break the program as he optimizes it; it also allows us to more scalably synthesize parallel programs.
- The first project headed by Prof. Sen will develop tools for automatic generation of tests for GUI-based and distributed applications with emphasis on energy efficiency. It is well known that testing of GUI applications is tedious because the interactions with the user are difficult to automate. While automatic test generation tools have been developed (in large part thanks to revolutionary advances made in Prof. Sen’s group), we are not aware of any successful test generation tools for GUI programs. This effort will extend Prof. Sen’s concolic testing methodology to GUI and distributed programs. Furthermore, the testing will not be limited to ascertaining correctness. Instead, it will test energy efficiency of mobile programs by automatically exploring program fragments that might be energy bottlenecks. This effort is synergistic with Prof. Necula’s effort in that it will generate functional tests that may become part of the program for its lifetime.
- The effort headed by Prof. Seshia will facilitate end-user programming of consumer robots. The novel idea is that the robot owner will demonstrate the desired robot behavior, e.g., how to reach the kitchen or unload a dishwasher. By coupling this demonstration with a safety specification, e.g., “do not fall down the stairs,” our synthesizer will generate software that will control the robot. To see the synergy with other efforts, observe that user demonstrations of robot behavior are actually “test traces” of robot’s program execution: the key difference is that these test traces are demonstrated by the user, rather than obtained by executing a program. Given this demonstration, the synthesis will proceed similarly to how parallel programs are synthesized in the effort by Bodik and Torlak. Prof. Seshia’s synthesis differs in that it synthesizes controllers rather than imperative programs. Interactive computer systems are already hybrids of controller logic and high-performance computation and we expect to discover ways to combine the two synthesis systems. The benefit if this synergy could be synthesizers for interactive phone applications. Prof. Seshia has significant expertise with robotic software: he co-designed the Berkeley undergraduate course on Embedded Systems, in which students program networked mobile robots, increasingly using cell phones as robot controllers.
- The second project of Prof. Sen will build a smart IDE for non-expert programmers to rapidly prototype complex phone apps. Programmers will write code by issuing search queries such as “connect to dropbox” or “grab a file”. The IDE will locate relevant code snippets and glue them together. Again, the underlying technology will rely on tests: the composable snippets will come annotated with a battery of tests that will describe their behavior, enabling composition of snippets that can work together. Automated test creation via concolic testing will be used to annotate snippets with a sufficiently large set of descriptive tests. Programmers will also demonstrate how a sequence of tasks can be executed to obtain a desired outcome. The IDE will accumulate such demonstrations and synthesize the final program. In summary, the IDE will actively interact with the programmer to collect demonstration and task description and it will provide instantaneous feedback so that the programmer can get instant gratification about programming progress. We have hands-on experience with the development of a search-based code snippet discovery system called SNIFF.