Jens Palsberg - US grants

ABSTRACT
Proposal #01122628
Purdue Research
Palsberg,Jens

Static Timing of Interrupt-driven Software

Real-time, reactive and embedded systems are widely and increasingly used throughout society (e.g., flight control, railway signaling, vehicle management systems, medical devices). This trend is likely to continue, as applications that would have been unthinkable only a few short years ago come into the reach of ever more complex processors. Many such applications are long lived, interact with their environment continuously, and are under important real-time constraints. As these reactive systems permeate our lives, bringing us everything from intelligent pace-makers to tiny freshness-tracking devices in groceries, the need for cost-effective, confidence-inspiring software validation techniques grows proportionately. This project focuses on building new tools for checking a common class of reactive real-time systems known as interrupt-driven systems. This proposed research has four facets that complement and support each other. The first continues our preliminary work on analyzing seven commercial microcontrollers to identify a static timing analysis that is sufficiently precise for a single interrupt handler. Second, ways of specifying and checking timing properties for multiple interrupt handlers are being investigated. Third, a typed assembly language is being developed with time bounds in which timing properties can be specified in a modular way, one handler at a time. Fourth, a timed interrupt-handler calculus is being designed that will embody our results in a language-independent way and make it tractable to prove key properties. The new tools will automatically derive a model of the software by static analysis and type checking, and submit the result to a model checker. The tools can lead to significantly reduced testing requirements, and provide support for maintenance throughout the system
life-cycle.

CCR-0306401
Foundations of ILP-based Static Analysis
Jens Palsberg

Compilers are an important part of today's computational infrastructure as software is ever-increasingly written in high-level programming languages. Compiler correctness is generally desirable but absolutely essential for embedded systems like sensor networks, medical implants, and fly-by-wire/drive-by-wire systems. Many commonly used compiler techniques lack proven foundations despite substantial advances in the field of proving compiler correctness. This project will focus on the foundations of static analysis based on integer linear programming (ILP), a technique commonly used by compilers for embedded systems.
This project will investigate key correctness properties of ILP-based analyses, including (1) soundness: is the analysis sound with respect to a formal semantics? (2) preservation: is the analysis preserved after program transformations? and (3) composition: can analyses be combined in ways that preserve basic properties of the program? Foundational results about the correctness of ILP-based analyses will lead to increased confidence in generated code, principles for developing new analyses, increased understanding of how to combine analyses, and ILP-based code certification, in the spirit of proof-carrying code, typed assembly language, and Java bytecode verification.

Abstract
Proposal 0427202
U of Cal Los Angeles

PIs: Jens Palsberg, Eddie Kohler, Rupak Majumdar, Todd Millstein
Event-Driven Software Quality

Event-driven programming, where tasks are divided into cooperatively-scheduled "handlers" that react to external events, has found pervasive acceptance from high-performance servers to embedded systems
as an efficient method for interacting with the world. Unfortunately, the loose coupling of handlers obscures program control flow and interdependencies, making programs hard to debug, maintain, and validate.
This research program investigates a new generation of programming language and tool support for event-driven programs constructed out of modular components. As representative test systems, it focuses on Click, a performance-constrained modular software router, and TinyOS, a resource-constrained operating system for embedded wireless sensors. All phases of the programming process are addressed, from the languages used to write event-driven programs, through automated verifiers and analyses that
ensure safety properties (such as bounding the latency required to handle an event), to optimizers that reduce code size, optimize system structures, and meet global resource constraints. Next-generation language and tool support will lead to increased confidence in a wide variety of event-driven systems, including Web servers, sensor networks, medical implants, engine control, and fly-by-wire/drive-by-wire systems, and will make this important methodology easier to teach. New compilers and analysis tools will be made publicly available.

ABSTRACT

Directorate for Computer and Information Science and Engineering (CISE)
Division Computer and Network Systems (CNS)
Science of Design (SoD) Program

Proposal Number: 0725354
P/I: Todd Millstein
PI Department: Computer Science
Institution: University of California - Los Angeles
Award: $ 800,000

Title: ""SoD: An Electronic Design Automation Approach to Embedded Networked Software""

This project adapts design approaches from the Electronic Design Automation (EDA) domain to improve the reliability and flexibility of software-intensive systems. In particular, the project develops methodologies, languages, and tools for designing embedded networked (EN) systems software. This project (based in UCLA with a sub-award to USC) is motivated by the EDA top-down design methodologies employed for hardware; the project develops languages and tools that adapt the EDA approach to the design and implementation of software systems. EN systems (which consist of a distributed collection of computing resources embedded in the physical world) are becoming increasingly important in both scientific and social applications (for example, earthquake prediction, contaminant tracking in ground water, soil erosion detection, traffic monitoring, etc.). The EDA design methodology is a logical foundation for designing software intensive systems because it articulates a design flow that contains a number of stages, which successively lower a high-level design until a fully specified hardware system is produced. Developers of EN systems need to describe the global behavior of their designs independent of the nonfunctional constraints, to make important domain knowledge and constraints from the physical world explicit, and to incorporate these properties into the development process in a staged manner. As EN systems move into the mainstream and software engineers outside of research laboratories take on the challenge of building of such systems, the need for sound software design methodologies and tools grows. The approach pursued with this project can greatly simplify the design of software for this important class of systems and thereby accelerate adoption.


Program Manager: Anita J. La Salle
Date: June 6, 2007

Proposal number: 0820245

Title: Certification of Medical Device Software

PI: Jens Palsberg
Co-PI: Majid Sarrafzadeh

A medical device should not crash or confuse. A device crash can be anything from inconvenient to life threatening, while confusing device behavior can lead a user to draw an incorrect medical conclusion. While rigorous testing will remain essential, new approaches to design, implementation, and certification have great potential to increase our confidence in medical devices. At the end of the rainbow in this research area lays a design for certifiability paradigm in which programmers think of certification from day one and create designs and code that can be certified by static error checking tools. The project's goal is to develop languages and tools for designing, building, and certifying medical device software in elegant and powerful new ways. The project focuses on a common class of medical devices called medical monitoring devices. The investigators envision a certification tool that can meet challenges related to space bounds, soft-real-time response, life time, and meaningful results. The project's goal is to take a major step towards design for certifiability and to bring closer the day when the FDA will use static error checking tools frequently and routinely. One of the outcomes of the project will be open-source versions of medical device software, along with implementations of the new language and certification tools. The result is a platform for experimenting with software for medical devices that may open up new possibilities for researchers.

"This award is funded under the American Recovery and Reinvestment Act of 2009
(Public Law 111-5)."


Customizable Domain-Specific Computing
To meet ever-increasing computing needs and overcome power density limitations, the computing industry has entered the era of parallelization, with tens to hundreds of computing cores integrated into a single processor; and hundreds to thousands of computing servers connected in warehouse-scale data centers. However, such highly parallel, general-purpose computing systems still face serious challenges in terms of performance, energy, heat dissipation, space, and cost. In this project we look beyond parallelization and focus on domain-specific customization as the next disruptive technology to bring orders-of-magnitude power-performance efficiency improvement to important application domains.
The intellectual merit of this project includes development of a general methodology for creating novel customizable architecture platforms and the associated compilation tools and runtime management environment to support domain-specific computing to: 1) achieve orders-of-magnitude computing efficiency improvement for applications in a specific domain; and 2) demon-strate that such improvement can be obtained with little or no impact on design productivity, so that it can be deployed in a wide range of application domains. Our proposed domain-specific customizable computing platform includes: 1) a wide range of customizable computing elements, from heterogeneous fixed cores to coarse-grain customizable cores, and to fine-grain field-programmable circuit fabrics; 2) customizable high-performance radio frequency interconnects; 3) highly automated compilation tools and runtime management software systems for application development; and 4) a general, reusable methodology for customizable computing applicable across different domains. By combining these critical capabilities, we shall deliver a super-computer-in-a-box that is customized to a particular application domain to enable disruptive innovations in that domain. This approach will be demonstrated in several important application domains in healthcare.
The broader impact of this project will be measured by the new digital revolution enabled by customized computing. We will demonstrate the feasibility and advantages of the proposed research in the domain of healthcare, given its significant impact on the national economy and quality of life issues. In particular, we focus our effort on revolutionizing the role of medical imaging and hemodynamic modeling in healthcare, providing much more cost-efficient, convenient solutions for preventative, diagnostic, and therapeutic procedures to dramatically improve healthcare quality, efficiency, and patient outcomes. The broader impact of this project also includes the integration of research and education, exposing graduate, undergraduate, and high school stu-dents to the new concepts and research from this project via several new courses jointly developed and shared by researchers in our newly established Center for Domain-Specific Computing (CSDC). Summer research fellowship programs to support high school and undergraduate students will be provided by CSDC. Our goal is to train a new generation of students who are prepared for customized parallelization and computing, and can effectively apply such techniques to many areas of our society, thus furthering the digital revolution. Special efforts are being made to attract underrepresented students at all levels via partnerships with campus organizations focused on diversity, such as the UCLA Center for Excellence in Engineering and Diversity.
This research will be carried out as a collaborative effort between four universities: UCLA (the lead institution), Rice, UC Santa Barbara, and Ohio State. The research team consists of a group of highly accomplished researchers with diversified backgrounds, including computer science and engineering, electrical engineering, medicine, and applied mathematics. For more information, please visit http://cdsc.cs.ucla.edu.

Static type checking has brought us more reliable software. Types make programs more readable, prevent entire classes of mistakes, and help compilers optimize data layout and data access. Types also make it easier to use libraries and to design interfaces, and they make it harder to misuse data and write bad programs. An entirely different trend is as old as programming: self-application. In particular, self-application is popular in the form of implementing a language in itself. When the trends of types and self-application meet, a fundamental challenge for type systems arises. For example, what is the type of an interpreter that can interpret a representation of itself? And what is the type of a compiler that can compile a representation of itself? The goal of the project is to enable the next generation of typed, self-applicable interpreters, compilers, and partial evaluators. This next generation will guarantee that the output represents a typed program, and that the type of the output program is related to the type of the input program. The result will be self-applicable meta-programs that are more reliable and have all the benefits of static type checking.

Many popular languages have a self-interpreter, that is, an interpreter for the language written in itself; examples include Standard ML, Haskell, Scheme, JavaScript, Python, and Ruby. Similarly, many languages have self-compilers, that is, a compiler for the language written in itself. Also, some languages have a virtual machine written in itself, including Java and Self. The project will bring static type checking to self-applicable interpreters, compilers, and partial evaluators, and take such meta-programs to a higher level of reliability by ensuring that the output programs type check and therefore cannot contain entire classes of mistakes. The investigator will teach the results to students as part of existing undergraduate and graduate courses.

The past decade has witnessed a sea change in the way that computing systems are designed, programmed, implemented, and evaluated. The advent of multicore technologies has fundamentally reshaped the long-standing contract between hardware and software - no longer can we simply rely on improvements in clock speeds to have our programs run faster. Instead, the burden for improvements in program performance now falls squarely on software and algorithms. Devising new techniques to efficiently and safely exploit multiple cores is the central question facing language designers, compiler writers, and system architects.

To help address these challenges, this NSF sponsored workshop will identify future research directions related to High-Level Programming Models for Parallelism, and the transition of such research to industrial practice. The workshop will bring together researchers from academia, industry, and government research labs working in the area of parallelism, including algorithms, architecture, language design and implementation, and runtime systems. The workshop will identify primary challenges in the field, both foundational and infrastructural, and will address the transition of ideas from research to practice.

This planning project will plan an infrastructure called the National Java Resource (NJR), which will be a collection of (on the order of) 10,000 Java projects that build and run out of the box, and for which popular static and dynamic analysis tools succeed and have cached outputs. The tasks of writing build scripts and otherwise preparing Java projects and tools for the repository will be largely automated. A prototype was developed to serve the DARPA MUSE project, but that project is ending soon and does not have plans to establish the NJR. A large and diverse set of Java-based research projects will be able to use it, providing an experimental platform and benchmarks, and eliminating barriers to performing the research. It is expected that the project will open up new areas of research that have been impeded by the lack of a high-quality corpus of such programs that can be easily compiled, run, and analyzed. The NJR repository has the potential to push forward research on a wide range of Java-based tools, such as bug finders, code repair tools, code synthesizers, software evolution, software repository mining, along with other code analysis tools.

The planning activity will involve running workshops at major programming languages conferences and possibly the major software engineering conference, with a goal to engage users and fully understand their requirements. The project will also continue experimenting with how to make downloading, compiling, and running projects less painful, i.e., more automatic, and to improve the success rate of how many projects are amenable to automatic builds, compilation and execution. There is potential for additional communities to benefit if the outreach can be extended to program comprehension, testing, and mining software repositories conferences.

Research in programming languages and software engineering has increasingly become a "big data" science ("Big Code") is which researchers want to use large code bases to experiment with new techniques. Specifically, Big Code will enable novel tools in areas such as security enhancers, bug finders, and code synthesizers. This project will build a community resource of 100,000 executable Java programs together with a set of working tools and an environment for conducting such research. This Normalized Java Resource (NJR) will lower the barrier to implementation of new tools, speed up research, and ultimately help advance research frontiers. Additionally, NJR can be the foundation of new courses on software tools that take advantage of Big Code. Finally, NJR can be the centerpiece of a discussion about better benchmark suites in general. The two investigators will work with collaborators from five countries.

Researchers get significant advantages from using NJR. They can write scripts that base their new tool on NJR's already-working tools, and they can search NJR for programs with desired characteristics. They will receive the search result as a container that they can run either locally or on a cloud service. Additionally, they benefit from NJR's normalized representation of each Java program, which enables scalable running of tools on the entire collection. Finally, they will find that NJR's collection of programs is diverse because of the investigators' efforts to run clone detection and near-duplicate removal.

This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.