Search

Theories of higher-order must-alias analysis, often under the guise of environment analysis, provide deep behavioral insight. But these theories---in particular those that are most insightful otherwise---can reason about recursion only in limited cases. This weakness is not inherent to the theories but to the frameworks in which they're defined: machine models which thread the heap through evaluation. Since these frameworks allocate each abstract resource in the heap, the constituent theories of environment analysis conflate co-live resources identified in the abstract, such as recursively-created bindings. We present heap fragments as a general technique to allow these theories to reason about recursion in a general and robust way. We instantiate abstract counting in a heap-fragment framework and compare its performance to a precursor entire-heap framework. We also sketch an approach to realizing binding invariants, a more powerful environment analysis, in the heap-fragment framework.

Google v. Oracle is a case involving the meaning of a copyright in computer software. The trial determined that Google copied many thousands of lines of code that had been written by Oracle. The code that was taken defined the existence of specific computing functions, determining which of two number is the larger one, as an example. Although Google did take these definitions, its programmers re-wrote the code that was needed to perform the function. Once taken, the code was used by Google to create (and then sell) the Android system for cell phones. The first major issue in the case is understanding what owning a copyright in computer software means. All agree that a copyright only protects an “expression” and does not protect any underlying ideas. The first dispute is whether the defining code is an expression or an idea. The second issue in the case is the meaning of the “fair use” defense where copying is allowed even though the copyright exists. Here, the main question is whether allowing computer programs to be written in a way that favors easy interoperability constitutes fair use. The brief submitted by the team of researchers based at U.Mass. Dartmouth and U.Mass. Lowell and written by Professor Clifford of the U.Mass. Law School only address the first issue. It argues that the declaring code that was taken is clearly expressive based on the Team’s research findings that there is significant variation of expression shown in all computer programs, even the most basic.

This paper presents a Coq library that lifts an abstract yet precise notion of running-time into the type of a function. Our library is based on a monad that counts abstract steps. The monad's computational content, however, is simply that of the identity monad so programs written in our monad (that recur on the natural structure of their arguments) extract into idiomatic OCaml code. We evaluated the expressiveness of the library by proving that red-black tree insertion and search, merge sort, insertion sort, various Fibonacci number implementations, iterated list insertion, various BigNum operations, and Okasaki's Braun Tree algorithms all have their expected running times.

As the software industry enters the era of language-oriented programming, it needs programmable programming languages.

Data-race detection is the problem of determining if a concurrent program has a data-race in some execution and input; it has been long studied and often solved. The research in this paper reprises the problem in the context of task parallel programs with the intent to prove, via model checking, the absence of data-race on any feasible schedule for a given input. Many of the correctness properties afforded by task parallel programming models such as OpenMP, Cilk, X10, Chapel, Habanero, etc. rely on data-race freedom. Model checking for data-race, presented here, is in contrast to recent work using run-time monitoring, log analysis, or static analysis which are complete or sound but never both. The model checking algorithm builds a happens-before relation from the program execution and uses that relation to detect data-race similar to many solutions that reason over a single observed execution. Unlike those solutions, model checking generates additional program schedules sufficient to prove data-race freedom over all schedules on the given input. The approach is evaluated in a Java implementation of Habanero using the JavaPathfinder model checker. The results, when compared to existing data-race detectors in Java Pathfinder, show a significant reduction in the time required for proving data race freedom.

Enumerations represented as bijections between the natural numbers and elements of some given type have recently garnered interest in property-based testing because of their efficiency and flexibility. There are, however, many ways of defining these bijections, some of which are better than others. This paper offers a new property of enumeration combinators calledfairnessthat identifies enumeration combinators that are better suited to property-based testing. Intuitively, the result of a fair combinator indexes into its argument enumerations equally when constructing its result. For example, extracting thenth element from our enumeration of three-tuples indexes about$\sqrt[3]{n}$elements into each of its components instead of, say, indexing$\sqrt[2]{n}$into one and$\sqrt[4]{n}$into the other two, as you would if a three-tuple were built out of nested pairs. Similarly, extracting thenth element from our enumeration of a three-way union returns an element that is$\frac{n}{3}$into one of the argument enumerators. The paper presents a semantics of enumeration combinators, a theory of fairness, proofs establishing fairness of our new combinators and that some combinations of fair combinators are not fair. We also report on an evaluation of fairness for the purpose of finding bugs in programming-language models. We show that fair enumeration combinators have complementary strengths to an existing, well-tuned ad hoc random generator (better on short time scales and worse on long time scales) and that using unfair combinators is worse across the board.

With the right tools, floating-point code can be debugged like any other code, drastically improving its accuracy and reliability.

Exploring Computer Science (ECS) is a high school introductory computer science class designed to increase student interest in CS. Utah is the first state to offer ECS statewide and use it to meet a high school graduation requirement. Over the past four years, 150 teachers have been trained as Utah ECS teachers and over 10,000 Utah students have taken the class. The Utah initiative is unique because it is the first to deploy ECS in a non-urban environment and with a modified half-year curriculum that includes no additional equipment costs. This paper discusses how the Utah deployment was organized, reports its results and unique difficulties, and offers lessons for deployments with similar characteristics: statewide, rural, and limited resources.

This paper presents a Coq library that lifts an abstract yet precise notion of running-time into the type of a function. Our library is based on a monad that counts abstract steps, controlled by one of the monadic operations. The monad’s computational content, however, is simply that of the identity monad so programs written in our monad (that recur on the natural structure of their arguments) extract into idiomatic OCaml code. We evaluated the expressiveness of the library by proving that red-black tree insertion and search, merge sort, insertion sort, Fibonacci, iterated list insertion, BigNum addition, and Okasaki’s Braun Tree algorithms all have their expected running times.

The PLT Scheme Web Server uses continuations to enable a natural, console-like program development style. We describe the implementation of the server and its use in the development of an application for managing conference paper reviews. In the process of developing this application, we encountered subtle forms of interaction not directly addressed by using continuations. We discuss these subtleties and offer solutions that have been successfully deployed in our application. Finally, we present some details on the server's performance, which is comparable to that of the widely-used Apache Web server.

Many probabilistic programming languages allow programs to be run under constraints in order to carry out Bayesian inference. Running programs under constraints could enable other uses such as rare event simulation and probabilistic verification—except that all such probabilistic languages are necessarily limited because they are defined or implemented in terms of an impoverished theory of probability. Measure-theoretic probability provides a more general foundation, but its generality makes finding computational content difficult.

Asynchronous message passing is an important paradigm in writing applications for embedded heterogeneous multicore systems. The Multicore Association (MCA), an industry consortium promoting multicore technology, is working to standardize message passing into a single API, MCAPI, for bare metal implementation and portability across platforms. Correctness in such an API is difficult to reason about manually, and testing against reference solutions is equally difficult as reference solutions implement an unknown set of allowed behaviors, and programmers have no way to directly control API internals to expose or reproduce errors. This paper provides a way to encode an MCAPI execution as a Satisfiability Modulo Theories (SMT) problem, which if satisfiable, yields a feasible execution schedule on the same trace, such that it resolves non-determinism in the MCAPI runtime in a way that it now fails user provided assertions. The paper proves the problem is NP-complete. The encoding is useful for test, debug, and verification of MCAPI program execution. The novelty in the encoding is the direct use of match pairs (potential send and receive couplings). Match-pair encoding for MCAPI executions, when compared to other encoding strategies, is simpler to reason about, results in significantly fewer terms in the SMT problem, and captures feasible behaviors that are ignored in previously published techniques. Further, to our knowledge, this is the first SMT encoding that is able to run in infinite-buffer semantics, meaning the runtime has unlimited internal buffering as opposed to no internal buffering. Results demonstrate that the SMT encoding, restricted to zero-buffer semantics, uses fewer clauses when compared to another zero-buffer technique, and it runs faster and uses less memory. As a result the encoding scales well for programs with high levels of non-determinism in how sends and receives may potentially match.

Given the widespread use of memory-safe languages, students must understand garbage collection well. Following a constructivist philosophy, an effective approach would be to have them implement garbage collectors. Unfortunately, a full implementation depends on substantial knowledge of compilers and runtime systems, which many courses do not cover or cannot assume.This paper presents an instructive approach to teaching GC, where students implement it atop a simplified stack and heap. Our approach eliminates enormous curricular dependencies while preserving the essence of GC algorithms. We take pains to enable testability, comprehensibility, and facilitates debugging. Our approach has been successfully classroom-tested for several years at several institutions.

Formal models serve in many roles in the programming language community. In its primary role, a model communicates the idea of a language design; the architecture of a language tool; or the essence of a program analysis. No matter which role it plays, however, a faulty model doesn't serve its purpose. One way to eliminate flaws from a model is to write it down in a mechanized formal language. It is then possible to state theorems about the model, to prove them, and to check the proofs. Over the past nine years, PLT has developed and explored a lightweight version of this approach, dubbed Redex. In a nutshell, Redex is a domain-specific language for semantic models that is embedded in the Racket programming language. The effort of creating a model in Redex is often no more burdensome than typesetting it with LaTeX; the difference is that Redex comes with tools for the semantics engineering life cycle.

This paper presents a formal modeling paradigm that is callable from C, the dominant language for embedded systems programming, for message passing APIs that provides reasonable assurance that the model correctly captures intended behavior. The model is a suitable reference solution for the API, and it supports putative what-if queries over API scenarios for behavior exploration, reproducibility for test and debug, full exhaustive search, and other advanced model checking analysis methods for C programs that use the API. This paper illustrates the modeling paradigm on the MCAPI interface, a growing industry standard message passing library, showing how the model exposes errors hidden by the C reference solution provided by the Multicore Association.

Bayesian practitioners build models of the world without regarding how difficult it will be to answer questions about them. When answering questions, they put off approximating as long as possible, and usually must write programs to compute converging approximations. Writing the programs is distracting, tedious and error-prone, and we wish to relieve them of it by providing languages and compilers. Their style constrains our work: the tools we provide cannot approximate early. Our approach to meeting this constraint is to 1) determine their notation's meaning in a suitable theoretical framework; 2) generalize our interpretation in an uncomputable, exact semantics; 3) approximate the exact semantics and prove convergence; and 4) implement the approximating semantics in Racket (formerly PLT Scheme). In this way, we define languages with at least as much exactness as Bayesian practitioners have in mind, and also put off approximating as long as possible. In this paper, we demonstrate the approach using our preliminary work on discrete (countably infinite) Bayesian models.

This paper explores the semantics of the meta-notation used in the style of operational semantics introduced by Felleisen and Hieb. Specifically, it defines a formal system that gives precise meanings to the notions of contexts, decomposition, and plugging (recomposition) left implicit in most expositions. This semantics is not naturally algorithmic, so the paper also provides an algorithm and proves a correspondence with the declarative definition. The motivation for this investigation is PLT Redex, a domain-specific programming language designed to support Felleisen-Hieb-style semantics. This style of semantics is the de-facto standard in operational semantics and, as such, is widely used. Accordingly, our goal is that Redex programs should, as much as possible, look and behave like those semantics. Since Redex's first public release more than seven years ago, its precise interpretation of contexts has changed several times, as we repeatedly encountered reduction systems that did not behave according to their authors' intent. This paper describes the culimation of that experience. To the best of our knowledge, the semantics given here accommodates even the most complex uses of contexts available.

Continuation-based Web servers provide advantages over traditional Web application development through the increase of expressive power they allow. This leads to fewer errors and more productivity for the programmers that adopt them. Unfortunately, existing implementation techniques force a hard choice between scalability and expressiveness.Our technique allows a smoother path to scalable, continuation-based Web programs. We present a modular program transformation that allows scalable Web applications to use third-party, higher-order libraries with higher-order arguments that cause Web interaction. Consequently, our system provides existing Web applications with more scalability through significantly less memory use than the traditional technique.

We present an analysis that determines when it is possible to multiplex a pair of cryptographic protocols. We present a transformation that improves the coverage of this analysis on common protocol formulations. We discuss the gap between the merely possible and the pragmatic through an optimization that informs a multiplexer. We also address the security ramifications of trusting external parties for this task and evaluate our work on a large repository of cryptographic protocols. We have verified this work using the Coq proof assistant.

Continuation-based Web servers provide distinct advantages over traditional Web application development: expressive power and modularity. This power leads to fewer errors and more interesting applications. Furthermore, these Web servers are more than prototypes; they are used in some real commercial applications. Unfortunately, they pay a heavy price for the additional power in the form of lack of scalability.We fix this key problem with a modular program transformation that produces scalable, continuation-based Web programs based on the REST architecture. Our programs use the same features as non-scalable, continuation-based Web programs, so we do not sacrifice expressive power for performance. In particular, we allow continuation marks in Web programs. Our system uses 10 percent (or less) of the memory required by previous approaches.

As cryptographic protocols execute they accumulate information such as values and keys, and evidence of properties about this information. As execution proceeds, new information becomes relevant while some old information ceases to be of use. Identifying what information is necessary at each point in a protocol run is valuable for both analysis and deployment.We formalize this necessary information as the minimal backup of a protocol. We present an analysis that determines the minimal backup at each point in a protocol run. We show that this minimal backup has many uses: it serves as a foundation for job-migration and other kinds of fault-tolerance, and also assists protocol designers understand the structure of protocols and identify potential flaws.In a cryptographic context it is dangerous to reason informally. We have therefore formalized and verified this work using the Coq proof assistant. Additionally, Coq provides a certified implementation of our analysis. Concretely, our analysis and its implementation consume protocols written in a variant of the Cryptographic Protocol Programming Language, CPPL.

Cryptographic protocols are useful for engineering trust in transactions. There are several languages for describing these protocols, but these tend to capture the communications from the perspective of an individual role. In contrast, traditional protocol descriptions as found in a state of nature tend to employ a whole-protocol description, resulting in an impedance mismatch. In this paper we present two results to address this gap between human descriptions and deployable specifications. The first is an end-point projection technique that consumes an explicit whole-protocol description and generates specifications that capture the behavior of each participant role. In practice, however, many whole-protocol descriptions contain idiomatic forms of implicit specification. We therefore present our second result, a transformation that identifies and eliminates these implicit patterns, thereby preparing protocols for end-point projection. Concretely, our tools consume protocols written in our whole-protocol language, wppl , and generate role descriptions in the cryptographic protocol programming language, cppl . We have formalized and established properties of the transformations using the Coq proof assistant. We have validated our transformations by applying them successfully to most of the protocols in the spore repository.

Cryptographic protocols are useful for trust engineering in Web transactions. The Cryptographic Protocol Programming Language (CPPL) provides a model wherein trust management annotations are attached to protocol actions, and are used to constrain the behavior of a protocol participant to be compatible with its own trust policy. The first implementation of CPPL generated stand-alone, single-session servers, making it unsuitable for deploying protocols on the Web. We describe a new compiler that uses a constraint-based analysis to produce multi-session server programs. The resulting programs run without persistent TCP connections for deployment on traditional Web servers. Most importantly, the compiler preserves existing proofs about the protocols. We present an enhanced version of the CPPL language, discuss the generation and use of constraints, show their use in the compiler, formalize the preservation of properties, present subtleties, and outline implementation details.

INTRODUCTION In this editorial, we report on the development of a smart-home-based cognitive prosthetic that will deliver 24/7 rehabilitation at the James A. Haley Veterans' Hospital Polytrauma Transitional Rehabilitation Program (PTRP) facility in Tampa, Florida. The Tampa Smart Home was designed to address two weaknesses identified by PTRP clinicians in the rehabilitation process for patients with traumatic brain injury (TBI): (1) patient safety and (2) inadequate timing and repetition of prompts used to overcome TBI-related cognitive and memory deficits. Smart homes monitor residents' behaviors and provide assistance for various physical and neurological disabilities [1]. The Tampa Smart Home creates a pervasive supportive environment to assist cognitive rehabilitation in patients with TBI [2-3] by continuously identifying the movements and locations of all patient residents and clinical staff. The location information permits the intelligent software to deliver customized prompts and information to the patient via numerous interactive multimedia displays located on walls throughout the PTRP. The residential setting lends itself well to the enriched interactive rehabilitative environment, in which patients with TBI are "immersed" in their rehabilitation, and leverages the "digital generation" of veterans' active technology engagement to facilitate their own recovery [4]. A powerful feature of the Tampa Smart Home is the precision of the customized therapeutic information that can be provided to the recovering veteran. Individual-level data for every interaction with clinical and medical staff and with the interactive displays are recorded continuously and analyzed using state-of-the-art data mining, which, when fully implemented, will allow staff to visualize subtle but therapeutically significant behavioral changes to better inform treatment plans and potentially prevent untoward medication effects on veterans' memory, as well as gait and balance. This approach is expected to yield important insights into the cognitive recovery process by assisting therapists in targeting problem behaviors for remediation and then linking the behaviors to automata that ensure consistently provided therapy. Consistently delivered automated interventions will shorten recovery time while complementing or reducing therapist monitoring of patient locations and activities within the facility. BACKGROUND AND RELATED WORK Department of Veterans Affairs Polytrauma Centers The signature injuries of soldiers returning from Afghanistan and Iraq are polytrauma and TBI [5-6]. In the majority of Department of Veterans Affairs (VA) clinical cases, polytrauma and TBI are caused by blast injuries from improvised explosive devices, although TBI also results from noncombat events such as motor vehicle accidents. Polytrauma is defined as injuries to two or more body systems from one event. An extreme example would be injuries that simultaneously result in limb amputation, TBI, burns, deafness, and blindness, with long-term physical and cognitive impairments and functional disabilities. TBI, while part of the constellation of injuries encompassing polytrauma, is the most serious and common injury [5]. The variable emotional, cognitive, and behavioral consequences of TBI determine the specific course of rehabilitation [3]. Mild injuries, managed properly, have excellent recovery prospects; moderate to severe injuries require specialized care and intensive early rehabilitation and often require lifelong assistance to manage routine daily activities. The VA has four polytrauma centers that serve as regional centers for medical and rehabilitation care and hubs for research and education located in Minneapolis, Minnesota; Palo Alto, California; Richmond, Virginia; and Tampa, Florida. The comprehensive medical and rehabilitation services provided include acute medical care, outpatient programs, and PTRPs. …

Many probabilistic programming languages allow programs to be run under constraints in order to carry out Bayesian inference. Running programs under constraints could enable other uses such as rare event simulation and probabilistic verification---except that all such probabilistic languages are necessarily limited because they are defined or implemented in terms of an impoverished theory of probability. Measure-theoretic probability provides a more general foundation, but its generality makes finding computational content difficult. We develop a measure-theoretic semantics for a first-order probabilistic language with recursion, which interprets programs as functions that compute preimages. Preimage functions are generally uncomputable, so we derive an abstract semantics. We implement the abstract semantics and use the implementation to carry out Bayesian inference, stochastic ray tracing (a rare event simulation), and probabilistic verification of floating-point error bounds., 26 pages, ESOP 2015 (to appear)