Recent advances in quantum hardware and error correction have paved the way for early fault-tolerant (EFT) quantum computing. We propose iSwitch, a hybrid system architecture for trapped-ion quantum computers (TIQC) that exploits ultra-high-fidelity single-qubit gates and efficient logical CNOTs enabled by ion shuttling. iSwitch employs bare qubits for single-qubit operations and QEC-encoded logical qubits for two-qubit gates, avoiding full logical encoding, gate synthesis, and magic state distillation. To enable this selective encoding, we develop a low-noise conversion protocol between bare and logical qubits, a hybrid instruction set tailored to 2D TIQC layouts, and a compiler that minimizes conversion overhead and optimizes scheduling. Evaluations on variational quantum algorithm benchmarks show that iSwitch achieves comparable fidelity to conventional QEC methods, while reducing qubit and operation counts by roughly 33–50%, offering a practical, resource-efficient path toward EFT quantum computing on trapped-ion platforms.

Reasoning about quantum programs remains a fundamental challenge, regardless of the programming model or computational paradigm. Existing verification techniques are insufficient -- even for quantum circuits, a deliberately restricted model that lacks classical control, but still underpins many current quantum algorithms. Many existing formal methods require exponential time and space to represent and manipulate (representations of) assertions and judgments, making them impractical for quantum circuits with many qubits. This paper presents SAQR-QC, a logic for Scalable but Approximate Quantitative Reasoning about Quantum Circuits. SAQR-QC has three characteristics: (i) some deliberate loss of precision is built into it; (ii) it has a mechanism to help the accumulated loss of precision during a sequence of reasoning steps remain small; and (iii) every reasoning step is local -- involving just a small number of qubits -- making reasoning scalable. We demonstrate the effectiveness of SAQR-QC via two case studies: the verification of GHZ circuits involving non-Clifford gates, and the analysis of quantum phase estimation -- a core subroutine in Shor's factoring algorithm.

Toffoli gates are key building blocks in quantum programs, and on most current quantum computers, they must be implemented with smaller gates. Such an implementation requires five 2-qubit gates if we assume that each gate can operate on any two qubits. However, many current quantum computers have only 2-qubit gates that operate on neighboring qubits; we call them neighbor gates. How many neighbor gates are required to implement a Toffoli gate? In this article, we show that six neighbor gates are necessary and sufficient, and we generalize to a characterization of all 3-qubit diagonal gates.

We propose moving from Software Defined Networks (SDN) to Software Managed Networks (SMN) where all information for managing the life cycle of a network (from deployment to operations to upgrades), across all layers (from Layer 1 through 7) is stored in a central repository. Crucially, a SMN also has a generalized control plane that, unlike SDN, controls all aspects of the cloud including traffic management (e.g., capacity planning) and reliability (e.g., incident routing) at both short (minutes) and large (years) time scales. Just as SDN allows better routing, a SMN improves visibility and enables cross-layer optimizations for faster response to failures and better network planning and operations. Implemented naively, SMN for planetary sc6ale networks requires orders of magnitude larger and more heterogeneous data (e.g., alerts, logs) than SDN. We address this using coarsening — mapping complex data to a more compact abstract representation that has approximately the same effect, and is more scalable, maintainable, and learnable. We show examples including Coarse Bandwidth Logs for capacity planning and Coarse Dependency Graphs for incident routing. Coarse Dependency Graphs improve an incident routing metric from 45% to 78% while for a distributed approach like Scouts the same metric was 22%. We end by discussing how to realize SMN, and suggest cross-layer optimizations and coarsenings for other operational and planning problems in networks.

A predictive analysis takes an execution trace as input and discovers concurrency bugs without accessing the program source code. A sound predictive analysis reports no false positives, which sounds like a property that can be defined easily, but which has been defined in many different ways in previous work. In this paper, we unify, simplify, and generalize those soundness defInitions for analyses that discover concurrency bugs that can be represented as a consecutive sequence of events. Our soundness defInition is graph based, separates thread-local properties and whole-execution properties, and works well with weak memory executions. We also present a three-step proof recipe, and we use it to prove six existing analyses sound. This includes the first proof of soundness for a predictive analysis that works with weak memory.

Frameworks for writing, compiling, and optimizing deep learning (DL) models have recently enabled progress in areas like computer vision and natural language processing. Extending these frameworks to accommodate the rapidly diversifying landscape of DL models and hardware platforms presents challenging tradeoffs between expressivity, composability, and portability. We present Relay, a new compiler framework for DL. Relay's functional, statically typed intermediate representation (IR) unifies and generalizes existing DL IRs to express state-of-the-art models. The introduction of Relay's expressive IR requires careful design of domain-specific optimizations, addressed via Relay's extension mechanisms. Using these extension mechanisms, Relay supports a unified compiler that can target a variety of hardware platforms. Our evaluation demonstrates Relay's competitive performance for a broad class of models and devices (CPUs, GPUs, and emerging accelerators). Relay's design demonstrates how a unified IR can provide expressivity, composability, and portability without compromising performance.

We present a compilation scheme for conditional quantumgates. Our scheme compiles amulti-qubit conditional to a linear number of two-qubit conditionals. This can be done straightforwardly with helper qubits, but we show how to do it without using helper qubits and with much fewer gates than in previous work. Specifically, our scheme requires 1/3 as many gates as the previous best scheme without using helper qubits, which is essential for practical use. Our experiments show that several quantum-circuit optimizers have little impact on the compiled code from the previous best scheme, confirming the need for our new scheme. Our experiments with Grover’s algorithm and quantum walk also show that our scheme has a major impact on the reliability of the compiled code.

Resource leaks are a common and elusive source of bugs that can result in crashes and security vulnerabilities. The most effective technique to identify such leaks during development is static analysis. However, empirical studies show that in addition to leak warnings, developers often need help in the form of automated fix suggestions to correctly repair such leaks. The only existing tool that can suggest resource-leak fixes is the general-purpose tool Footpatch. Footpatch, however, performs poorly at this task; it generates fixes for only 6% of the leaks, out of which only 27% are correct.

Researchers have reported that static analysis tools rarely achieve a false-positive rate that would make them attractive to developers. We overcome this problem by a technique that leads to reporting fewer bugs but also much fewer false positives. Our technique prunes the static call graph that sits at the core of many static analyses. Specifically, static call-graph construction proceeds as usual, after which a call-graph pruner removes many false-positive edges but few true edges. The challenge is to strike a balance between being aggressive in removing false-positive edges but not so aggressive that no true edges remain. We achieve this goal by automatically producing a call-graph pruner through an automatic, ahead-of-time learning process. We added such a call-graph pruner to a software tool for null-pointer analysis and found that the false-positive rate decreased from 73% to 23%. This improvement makes the tool more useful to developers.

Long analysis times are a key bottleneck for the widespread adoption of whole-program static analysis tools. Fortunately, however, a user is often only interested in finding errors in the application code, which constitutes a small fraction of the whole program. Current application-focused analysis tools overapproximate the effect of the library and hence reduce the precision of the analysis results. However, empirical studies have shown that users have high expectations on precision and will ignore tool results that don't meet these expectations.

Existing quantum compilers optimize quantum circuits by applying circuit transformations designed by experts. This approach requires significant manual effort to design and implement circuit transformations for different quantum devices, which use different gate sets, and can miss optimizations that are hard to find manually. We propose Quartz, a quantum circuit superoptimizer that automatically generates and verifies circuit transformations for arbitrary quantum gate sets. For a given gate set, Quartz generates candidate circuit transformations by systematically exploring small circuits and verifies the discovered transformations using an automated theorem prover. To optimize a quantum circuit, Quartz uses a cost-based backtracking search that applies the verified transformations to the circuit. Our evaluation on three popular gate sets shows that Quartz can effectively generate and verify transformations for different gate sets. The generated transformations cover manually designed transformations used by existing optimizers and also include new transformations. Quartz is therefore able to optimize a broad range of circuits for diverse gate sets, outperforming or matching the performance of hand-tuned circuit optimizers.

Reducing a failure-inducing input to a smaller one is challenging for input with internal dependencies because most sub-inputs are invalid. Kalhauge and Palsberg made progress on this problem by mapping the task to a reduction problem for dependency graphs that avoids invalid inputs entirely. Their tool J-Reduce efficiently reduces Java bytecode to 24 percent of its original size, which made it the most effective tool until now. However, the output from their tool is often too large to be helpful in a bug report. In this paper, we show that more fine-grained modeling of dependencies leads to much more reduction. Specifically, we use propositional logic for specifying dependencies and we show how this works for Java bytecode. Once we have a propositional formula that specifies all valid sub-inputs, we run an algorithm that finds a small, valid, failure-inducing input. Our algorithm interleaves runs of the buggy program and calls to a procedure that finds a minimal satisfying assignment. Our experiments show that we can reduce Java bytecode to 4.6 percent of its original size, which is 5.3 times better than the 24.3 percent achieved by J-Reduce. The much smaller output is more suitable for bug reports.

In quantum computing, the basic unit of information is a qubit. Simulation of a general quantum program takes exponential time in the number of qubits, which makes simulation infeasible beyond 50 qubits on current supercomputers. So, for the understanding of larger programs, we turn to static techniques. In this paper, we present an abstract interpretation of quantum programs and we use it to automatically verify assertions in polynomial time. Our key insight is to let an abstract state be a tuple of projections. For such domains, we present abstraction and concretization functions that form a Galois connection and we use them to define abstract operations. Our experiments on a laptop have verified assertions about the Bernstein-Vazirani, GHZ, and Grover benchmarks with 300 qubits.

Concurrency bugs are extremely difficult to detect. Recently, several dynamic techniques achieve sound analysis. M2 is even complete for two threads. It is designed to decide whether two events can occur consecutively. However, real-world concurrency bugs can involve more events and threads. Some can occur when the order of two or more events can be exchanged even if they occur not consecutively. We propose a new technique SeqCheck to soundly decide whether a sequence of events can occur in a specified order. The ordered sequence represents a potential concurrency bug. And several known forms of concurrency bugs can be easily encoded into event sequences where each represents a way that the bug can occur. To achieve it, SeqCheck explicitly analyzes branch events and includes a set of efficient algorithms. We show that SeqCheck is sound; and it is also complete on traces of two threads.

Multithreaded programs can have deadlocks, even after deployment, so users may want to run deadlock tools on deployed programs. However, current deadlock predictors such as MagicLock and UnDead have large overheads that make them impractical for end-user deployment and confine their use to development time. Such overhead stems from running an exponential-time algorithm on a large execution trace. In this paper, we present the first low-overhead deadlock predictor, called AirLock, that is fit for both in-house testing and deployed programs. AirLock maintains a small predictive lock reachability graph, searches the graph for cycles, and runs an exponential-time algorithm only for each cycle. This approach lets AirLock find the same deadlocks as MagicLock and UnDead but with much less overhead because the number of cycles is small in practice. Our experiments with real-world benchmarks show that the average time overhead of AirLock is 3.5%, which is three orders of magnitude less than that of MagicLock and UnDead. AirLock's low overhead makes it suitable for use with fuzz testers like AFL and on-the-fly after deployment.

Programmers can use gradual types to migrate programs to have more precise type annotations and thereby improve their readability, efficiency, and safety. Such migration requires an exploration of the migration space and can benefit from tool support, as shown in previous work. Our goal is to provide a foundation for better tool support by settling decidability questions about migration with gradual types. We present three algorithms and a hardness result for deciding key properties and we explain how they can be useful during an exploration. In particular, we show how to decide whether the migration space is finite, whether it has a top element, and whether it is a singleton. We also show that deciding whether it has a maximal element is NP-hard. Our implementation of our algorithms worked as expected on a suite of microbenchmarks.

Delta debugging is a technique for reducing a failure-inducing input to a small input that reveals the cause of the failure. This has been successful for a wide variety of inputs including C programs, XML data, and thread schedules. However, for input that has many internal dependencies, delta debugging scales poorly. Such input includes C#, Java, and Java bytecode and they have presented a major challenge for input reduction until now. In this paper, we show that the core challenge is a reduction problem for dependency graphs, and we present a general strategy for reducing such graphs. We combine this with a novel algorithm for reduction called Binary Reduction in a tool called J-Reduce for Java bytecode. Our experiments show that our tool is 12x faster and achieves more reduction than delta debugging on average. This enabled us to create and submit short bug reports for three Java bytecode decompilers.

Java's memory model was recently updated and expanded with new access modes. The accompanying documentation for these access modes is intended to make strong guarantees about program behavior that the Java compiler must enforce, yet the documentation is frequently unclear. This makes the intended program behavior ambiguous, impedes discussion of key design decisions, and makes it impossible to prove general properties about the semantics of the access modes. In this paper we present the first formalization of Java's access modes. We have constructed an axiomatic model for all of the modes using the Herd modeling tool. This allows us to give precise answers to questions about the behavior of example programs, called litmus tests. We have validated our model using a large suite of litmus tests from existing research which helps to shed light on the relationship with other memory models. We have also modeled the semantics in Coq and proven several general theorems including a DRF guarantee, which says that if a program is properly synchronized then it will exhibit sequentially consistent behavior. Finally, we use our model to prove that the unusual design choice of a partial order among writes to the same location is unobservable in any program.

We present partial evaluation by specialization-safe normalization, a novel partial evaluation technique that is Jones-optimal, that can be self-applied to achieve the Futamura projections and that can be type-checked to ensure it always generates code with the correct type. Jones-optimality is the gold-standard for nontrivial partial evaluation and guarantees that a specializer can remove an entire layer of interpretation. We achieve Jones-optimality by using a novel affine-variable static analysis that directs specialization-safe normalization to always decrease a program’s runtime. We demonstrate the robustness of our approach by showing Jones-optimality in a variety of settings. We have formally proved that our partial evaluator is Jones-optimal for call-by-value reduction, and we have experimentally shown that it is Jones-optimal for call-by-value, normal-order, and memoized normal-order. Each of our experiments tests Jones-optimality with three different self-interpreters. We implemented our partial evaluator in F ω µ i , a recent language for typed self-applicable meta-programming. It is the first Jones-optimal and self-applicable partial evaluator whose type guarantees that it always generates type-correct code.

For a concurrent program, a prediction tool maps the history of a single run to a prediction of bugs in an exponential number of other runs. If all those bugs can occur, then the tool is sound. This is the case for some data race tools like RVPredict, but was, until now, not the case for deadlock tools. We present the first sound tool for predicting deadlocks in Java. Unlike previous work, we use request events and a novel form of executability constraints that enable sound and effective deadlock prediction. We model prediction as a general decision problem, which we show is decidable and can be instantiated to both deadlocks and data races. Our proof of decidability maps the decision problem to an equivalent constraint problem that we solve using an SMT-solver. Our experiments show that our tool finds real deadlocks effectively, including some missed by DeadlockFuzzer, which verifies each deadlock candidate by re-executing the input program. Our experiments also show that our tool can be used to predict more, real data races than RVPredict.

Many popular languages have a self-interpreter, that is, an interpreter for the language written in itself. So far, work on polymorphically-typed self-interpreters has concentrated on self-recognizers that merely recover a program from its representation. A larger and until now unsolved challenge is to implement a polymorphically-typed self-evaluator that evaluates the represented program and produces a representation of the result. We present Fωμi, the first λ-calculus that supports a polymorphically-typed self-evaluator. Our calculus extends Fω with recursive types and intensional type functions and has decidable type checking. Our key innovation is a novel implementation of type equality proofs that enables us to define a versatile representation of programs. Our results establish a new category of languages that can support polymorphically-typed self-evaluators.

According to conventional wisdom, a self-interpreter for a strongly normalizing lambda-calculus is impossible. We call this the normalization barrier. The normalization barrier stems from a theorem in computability theory that says that a total universal function for the total computable functions is impossible. In this paper we break through the normalization barrier and define a self-interpreter for System F_omega, a strongly normalizing lambda-calculus. After a careful analysis of the classical theorem, we show that static type checking in F_omega can exclude the proof's diagonalization gadget, leaving open the possibility for a self-interpreter. Along with the self-interpreter, we program four other operations in F_omega, including a continuation-passing style transformation. Our operations rely on a new approach to program representation that may be useful in theorem provers and compilers.

In a distributed system, access to local data is much faster than access to remote data. As a help to programmers, some languages require every access to be local. A program in those languages can access remote data via first a shift of the place of computation and then a local access. To enforce this discipline, researchers have presented type systems that determine whether every access is local and every place shift is appropriate. However, those type systems fall short of handling a common programming pattern that we call place-oblivious objects. Such objects safely access other objects without knowledge of their place. In response, we present the first type system for place-oblivious objects along with an efficient inference algorithm and a proof that inference is P-complete. Our example language extends the Abadi-Cardelli object calculus with place shift and existential types, and our implementation has inferred types for some microbenchmarks.

Previous work has shown how to insert fences that enforce sequential consistency. However, for many concurrent algorithms, sequential consistency is unnecessarily strong and can lead to high execution overhead. The reason is that, often, correctness relies on the execution order of a few specific pairs of instructions. Algorithm designers can declare those execution orders and thereby enable memory-model-independent reasoning about correctness and also ease implementation of algorithms on multiple platforms. The literature has examples of such reasoning, while tool support for enforcing the orders has been lacking until now. In this paper we present a declarative approach to specify and enforce execution orders. Our fence insertion algorithm first identifies the execution orders that a given memory model enforces automatically, and then inserts fences that enforce the rest. Our benchmarks include three off-the-shelf transactional memory algorithms written in C/C++ for which we specify suitable execution orders. For those benchmarks, our experiments with the x86 and ARMv7 memory models show that our tool inserts fences that are competitive with those inserted by the original authors. Our tool is the first to insert fences into transactional memory algorithms and it solves the long-standing problem of how to easily port such algorithms to a novel memory model.

In 1991, Pfenning and Lee studied whether System F could support a typed self-interpreter. They concluded that typed self-representation for System F "seems to be impossible", but were able to represent System F in Fω. Further, they found that the representation of Fω requires kind polymorphism, which is outside Fω. In 2009, Rendel, Ostermann and Hofer conjectured that the representation of kind-polymorphic terms would require another, higher form of polymorphism. Is this a case of infinite regress? We show that it is not and present a typed self-representation for Girard's System U, the first for a λ-calculus with decidable type checking. System U extends System Fω with kind polymorphic terms and types. We show that kind polymorphic types (i.e. types that depend on kinds) are sufficient to "tie the knot" -- they enable representations of kind polymorphic terms without introducing another form of polymorphism. Our self-representation supports operations that iterate over a term, each of which can be applied to a representation of itself. We present three typed self-applicable operations: a self-interpreter that recovers a term from its representation, a predicate that tests the intensional structure of a term, and a typed continuation-passing-style (CPS) transformation -- the first typed self-applicable CPS transformation. Our techniques could have applications from verifiably type-preserving metaprograms, to growable typed languages, to more efficient self-interpreters.

Detection of data races in Java programs remains a difficult problem. The best static techniques produce many false positives, and also the best dynamic techniques leave room for improvement. We present a new technique called race directed scheduling that for a given race candidate searches for an input and a schedule that lead to the race. The search iterates a combination of concolic execution and schedule improvement, and turns out to find useful inputs and schedules efficiently. We use an existing technique to produce a manageable number of race candidates. Our experiments on 23 Java programs found 72 real races that were missed by the best existing dynamic techniques. Among those 72 races, 31 races were found with schedules that have between 1 million and 108 million events, which suggests that they are rare and hard-to-find races.

We present a new technique to find real deadlocks in concurrent programs that use locks. For 4.5 million lines of Java, our technique found almost twice as many real deadlocks as four previous techniques combined. Among those, 33 deadlocks happened after more than one million computation steps, including 27 new deadlocks. We first use a known technique to find 1275 deadlock candidates and then we determine that 146 of them are real deadlocks. Our technique combines previous work on concolic execution with a new constraint-based approach that iteratively drives an execution towards a deadlock candidate.

Editorial I thank the associate editors who continue to serve TOPLAS, and I also thank Matthew Dwyer who in Summer 2014 reached the end of his term and stepped down as associate editor. Welcome to Kathleen Fisher who is a new associate editor. Jens Palsberg Editor in Chief

For event-driven software on resource-constrained devices, estimates of the maximum stack size can be of paramount importance. For example, a poor estimate led to software failure and closure of a German railway station in 1995. Static analysis may produce a safe estimate but how good is it? In this paper we use testing to evaluate the state-of-the-art static analysis of maximum stack size for event-driven assembly code. First we note that the state-of-the-art testing approach achieves a maximum stack size that is only 67 percent of that achieved by static analysis. Then we present better testing approaches and use them to demonstrate that the static analysis is near optimal for our benchmarks. Our first testing approach achieves a maximum stack size that on average is within 99 percent of that achieved by static analysis, while our second approach achieves 94 percent and is two orders of magnitude faster. Our results show that the state-of-the-art static analysis produces excellent estimates of maximum stack size.

Compilers use software-controlled local memories to provide fast, predictable, and power-efficient access to critical data. We show that the local memory allocation for straight-line, or linearized programs is equivalent to a weighted interval-graph coloring problem. This problem is new when allowing a color interval to “wrap around,” and we call it the submarine-building problem. This graph-theoretical decision problem differs slightly from the classical ship-building problem, and exhibits very interesting and unusual complexity properties. We demonstrate that the submarine-building problem is NP-complete, while it is solvable in linear time for not-so-proper interval graphs, an extension of the the class of proper interval graphs. We propose a clustering heuristic to approximate any interval graph into a not-so-proper interval graph, decoupling spill code generation from local memory assignment. We apply this heuristic to a large number of randomly generated interval graphs reproducing the statistical features of standard local memory allocation benchmarks, comparing with state-of-the-art heuristics.

No abstract available.

We present a core calculus with two of X10's key constructs for parallelism, namely async and finish. Our calculus forms a convenient basis for type systems and static analyses for languages with async-finish parallelism. For example, we present a type system for context-sensitive may-happen-in-parallel analysis, along with experimental results of performing type inference on 13,000 lines of X10 code. Our analysis runs in polynomial time and produces a low number of false positives, which suggests that our analysis is a good basis for other analyses such as race detectors. Our calculus is also a good basis for tractable proofs of correctness. For example, we give a one-page proof of the deadlock-freedom theorem of Saraswat and Jagadeesan, and we prove the correctness of our type system.

TOPLAS will have four issues per year from now on! The goal is to have each of the four issues contain 5--6 articles, instead of the previous schedule of six issues that each typically contained 3--4 articles. Historically, TOPLAS had four issues per volume from 1980 to 1992, and all but three of those issues contained 5 or more articles. I hope that the TOPLAS readers will enjoy the fewer, thicker issues of TOPLAS. I thank the associate editors who continue to serve TOPLAS, and I also thank Wei Li and Aaron Stump who in the Winter of 2012 reached the end of their terms and stepped down as associate editors. Welcome to Michael Hicks who is a new associate editor.

Self-interpreters can be roughly divided into two sorts: self-recognisers that recover the input program from a canonical representation, and self-enactors that execute the input program. Major progress for statically-typed languages was achieved in 2009 by Rendel, Ostermann, and Hofer who presented the first typed self-recogniser that allows representations of different terms to have different types. A key feature of their type system is a type:type rule that renders the kind system of their language inconsistent.

The technique of trace-based just-in-time compilation was introduced by Bala et al. and was further developed by Gal et al. It currently enjoys success in Mozilla Firefox's JavaScript engine. A trace-based JIT compiler leverages run-time profiling to optimize frequently-executed paths while enabling the optimized code to ``bail out'' to the original code when the path has been invalidated. This optimization strategy differs from those of other JIT compilers and opens the question of which trace optimizations are sound. In this paper we present a framework for reasoning about the soundness of trace optimizations, and we show that some traditional optimization techniques are sound when used in a trace compiler while others are unsound. The converse is also true: some trace optimizations are sound when used in a traditional compiler while others are unsound. So, traditional and trace optimizations form incomparable sets. Our setting is an imperative calculus for which tracing is explicitly spelled out in the semantics. We define optimization soundness via a notion of bisimulation, and we show that sound optimizations lead to confluence and determinacy of stores.

Many concurrent programming models enable both transactional memory and message passing. For such models, researchers have built increasingly efficient implementations and defined reasonable correctness criteria, while it remains an open problem to obtain the best of both worlds. We present a programming model that is the first to have opaque transactions, safe asynchronous message passing, and an efficient implementation. Our semantics uses tentative message passing and keeps track of dependencies to enable undo of message passing in case a transaction aborts. We can program communication idioms such as barrier and rendezvous that do not deadlock when used in an atomic block. Our experiments show that our model adds little overhead to pure transactions, and that it is significantly more efficient than Transactional Events. We use a novel definition of safe message passing that may be of independent interest.

No abstract available.

No abstract available.

Consumer electronics today such as cell phones often have one or more low-power FPGAs to assist with energyintensive operations in order to reduce overall energy consumption and increase battery life. However, current techniques for programming FPGAs require people to be specially trained to do so. Ideally, software engineers can more readily take advantage of the benefits FPGAs offer by being able to program them using their existing skills, a common one being object-oriented programming. However, traditional techniques for compiling object-oriented languages are at odds with today's FPGA tools, which support neither pointers nor complex data structures. Open until now is the problem of compiling an object-oriented language to an FPGA in a way that harnesses this potential for huge energy savings. In this paper, we present a new compilation technique that feeds into an existing FPGA tool chain and produces FPGAs with up to almost an order of magnitude in energy savings compared to a low-power microprocessor while still retaining comparable performance and area usage.

We present a core calculus with two of X10's key constructs for parallelism, namely async and finish. Our calculus forms a convenient basis for type systems and static analyses for languages with async-finish parallelism, and for tractable proofs of correctness. For example, we give a short proof of the deadlock-freedom theorem of Saraswat and Jagadeesan. Our main contribution is a type system that solves the open problem of context-sensitive may-happen-in-parallel analysis for languages with async-finish parallelism. We prove the correctness of our type system and we report experimental results of performing type inference on 13,000 lines of X10 code. Our analysis runs in polynomial time, takes a total of 28 seconds on our benchmarks, and produces a low number of false positives, which suggests that our analysis is a good basis for other analyses such as race detectors.

X10 is a modern object-oriented language designed for productivity and performance in concurrent and distributed systems. In this setting, dependent types offer significant opportunities for detecting design errors statically, documenting design decisions, eliminating costly run-time checks (e.g., for array bounds, null values), and improving the quality of generated code.

We show that register allocation can be viewed as solving a collection of puzzles. We model the register file as a puzzle board and the program variables as puzzle pieces; pre-coloring and register aliasing fit in naturally. For architectures such as PowerPC, x86, and StrongARM, we can solve the puzzles in polynomial time, and we have augmented the puzzle solver with a simple heuristic for spilling. For SPEC CPU2000, the compilation time of our implementation is as fast as that of the extended version of linear scan used by LLVM, which is the JIT compiler in the openGL stack of Mac OS 10.5. Our implementation produces x86 code that is of similar quality to the code produced by the slower, state-of-the-art iterated register coalescing of George and Appel with the extensions proposed by Smith, Ramsey, and Holloway in 2004.

Type systems and model checking are two prevalent approaches to program verification. A prominent difference between them is that type systems are typically defined in a syntactic and modular style whereas model checking is usually performed in a semantic and whole-program style. This difference between the two approaches makes them complementary to each other: type systems are good at explaining why a program was accepted while model checkers are good at explaining why a program was rejected. We present a type system that is equivalent to a model checker for verifying temporal safety properties of imperative programs. The model checker is natural and may be instantiated with any finite-state abstraction scheme such as predicate abstraction. The type system, which is also parametric, type checks exactly those programs that are accepted by the model checker. It uses a variant of function types to capture flow sensitivity and intersection and union types to capture context sensitivity. Our result sheds light on the relationship between type systems and model checking, provides a methodology for studying their relative expressiveness, is a step towards sharing results between the two approaches, and motivates synergistic program analyses involving interplay between them.

Research into embedded sensor networks has placed increased focus on the problem of developing reliable and flexible software for microcontroller-class devices. Languages such as nesC [8] and Virgil [14] have brought higher-level programming idioms to this lowest layer of software, thereby adding expressiveness. Both languages are marked by the absence of dynamic memory allocation, which removes the need for a runtime system to manage memory. To provide data structures, nesC offers modules, and Virgil offers the application an opportunity to allocate and initialize objects during compilation. This paper explores techniques for compressing fixed object heaps with the goal of reducing the RAM footprint of a program. We explore table-based compression and introduce a novel form of object layout called vertical object layout. We provide experimental results that measure the impact on RAM size, code size, and execution time for a set of Virgil programs. Our results show that compressed vertical layout has better execution time and code size than table-based compression while achieving more than 20% heap reduction on 6 of 12 benchmark programs.

Embedded systems pose unique challenges to Java application developers and virtual machine designers. Chief among these challenges is the memory footprint of both the virtual machine and the applications that run within it. With the rapidly increasing set of features provided by the Java language, virtual machine designers are often forced to build custom implementations that make various tradeoffs between the footprint of the virtual machine and the subset of the Java language and class libraries that are supported. In this paper, we present the ExoVM, a system in which an application is initialized in a fully featured virtual machine, and then the code, data, and virtual machine features necessary to execute it are packaged into a binary image. Key to this process is feature analysis, a technique for computing the reachable code and data of a Java program and its implementation inside the VM simultaneously. The ExoVM reduces the need to develop customized embedded virtual machines by reusing a single VM infrastructure and automatically eliding the implementation of unused Java features on a per-program basis. We present a constraint-based instantiation of the analysis technique, an implementation in IBM's J9 Java VM, experiments evaluating our technique for the EEMBC benchmark suite, and some discussion of the individual costs of some of Java's features. Our evaluation shows that our system can reduce the non-heap memory allocation of the virtual machine by as much as 75%. We discuss VM and language design decisions that our work shows are important in targeting embedded systems, supporting the long-term goal of a common VM infrastructure spanning from motes to large servers.

No abstract available.

Object-oriented languages provide little support for encapsulating objects. Reference semantics allows objects to escape their defining scope, and the pervasive aliasing that ensues remains a major source of software defects. This paper presents Kacheck/J, a tool for inferring object encapsulation properties of large Java programs. Our goal is to develop practical tools to assist software engineers, thus we focus on simple and scalable techniques. Kacheck/J is able to infer confinement —the property that all instances of a given type are encapsulated in their defining package. This simple property can be used to identify accidental leaks of sensitive objects, as well as for compiler optimizations. We report on the analysis of a large body of code and discuss language support and refactoring for confinement.

Confinement properties impose a structure on object graphs which can be used to enforce encapsulation properties. From a practical point of view, encapsulation is essential for building secure object-oriented systems as security requires that the interface between trusted and untrusted components of a system be clearly delineated and restricted to the smallest possible set of operations and data structures. This paper investigates the notion of package-level confinement and proposes a type system that enforces this notion for a call-by-value object calculus as well as a generic extension thereof. We give a proof of soundness of this type system, and establish links between this work and related research in language-based security.

Simulation can be an important step in the development of software for wireless sensor networks and has been the subject of intense research in the past decade. While most previous efforts in simulating wireless sensor networks have focused on protocol-level issues utilizing models of the software implementation, a significant challenge remains in precisely measuring time-dependent properties such as radio channel utilization. One promising approach, first demonstrated by ATEMU, is to simulate the behavior of sensor network programs at the machine code level with cycle-accuracy, but poor performance has so far limited its scalability. In this paper we present Avrora, a cycle-accurate instruction-level sensor network simulator which scales to networks of up to 10,000 nodes and performs as much as 20 times faster than previous simulators with equivalent accuracy, handling as many as 25 nodes in real-time. We show how an event queue can enable efficient instruction-level simulation of microcontroller programs and allow the hidden parallelism in finegrained sensor network simulations to be extracted, once two core synchronization problems are identified and solved. Avrora's ability to measure detailed time-critical phenomena can shed new light on design Issues for large-scale sensor networks.

Debugging, testing, and profiling microcontroller programs are notoriously difficult. The lack of supporting software such as an operating system, a narrow interface to the hardware chip, and delicately timed sequences of code present significant challenges which can be exacerbated by the presence of additional debugging or profiling code. In this paper we present a solution to the precision instrumentation problem for microcontroller code that is based upon our open, flexible simulator framework, Avrora. Our simulator preserves all timing and behavior of the instrumented program while allowing precision measurement of application-specific quantities.

Denial-of-service attacks are becoming more frequent and sophisticated. Researchers have proposed a variety of defenses, including better system configurations, infrastructures, protocols, firewalls, and monitoring tools. Can we validate a server implementation in a systematic manner? In this paper we focus on a particular attack, SYN flooding, where an attacker sends many TCP-connection requests to a victim's machine. We study the issue of whether a TCP server can keep up with the packets from an attacker, or whether the server exhausts its buffer space. We present a tool for statically validating a TCP server's ability to survive SYN flooding attacks. Our tool automatically transforms a TCP-server implementation into a timed automaton, and it transforms an attacker model, given by the output of a packet generator, into another timed automaton. Together the two timed automata form a system for which the model checker UPPAAL can decide whether a bad state, in which the buffer overruns, can be reached. Our tool has two advantages over simply testing the server implementation with a packet generator. First, our tool is an order of magnitude faster because of aggressive abstraction of the server code. Second, our tool can be applied to a variety of server software without having to install each one in the kernel of an operating system. Thus, a programmer of defensive measures against SYN flooding attacks can get rapid feedback during development.

Understanding how a sensor network system works requires running the system, extracting log files, and manually interpreting system metrics. When interpreting system metrics, we often try to correlate behavior over multiple modalities. For example, if a node is exhibiting strange behaviors, the cause may be due to weak battery, geographically bad placement, collision, interference, sensor failure, algorithmic faults, or a combination of the above. This approach of interpreting metrics is adequate for closed systems such as the ones run in simulations, with limited duration. However, for complex sensor network systems that have already been deployed for weeks or even months in the fields, this approach is difficult, laborious, and error-prone. Thus, a suite of tools to help analyze complex sensor network system is desirable. We have implemented Deployment Analysis System (DAS), a centralized data mining suite designed to better understand sensor networks. It supports visualization and deployment-related queries that allow the user to inspect historical system metrics, environmental data, geographical placements, and system status.

Read-only fields are useful in object calculi, pi calculi, and statically typed intermediate languages because they admit covariant subtyping, unlike updateable fields. For example, Glew's translation of classes and objects to an intermediate calculus relies crucially on covariant subtyping of read-only fields to ensure that subclasses are translated to subtypes.In this article, we present a type inference algorithm for an Abadi--Cardelli object calculus in which fields are marked either as updateable or as read-only. The type inference problem is P-complete, and our algorithm runs in O ( n 3 ) time. The same complexity results hold for the calculus in which the fields are not explicitly annotated as updateable or read-only; perhaps surprisingly, the annotations do not make type inference easier. We show that type inference is equivalent to the problem of solving type constraints, and this forms the core of our algorithm and implementation.

Most compilers ignore the problems of limited code space in embedded systems. Designers of embedded software often have no better alternative than to manually reduce the size of the source code or even the compiled code. Besides being tedious and error prone, such optimization results in obfuscated code that is difficult to maintain and reuse. In this paper, we present a step towards code-size-aware compilation. We phrase register allocation and code generation as an integer linear programming problem where the upper bound on the code size can simply be expressed as an additional constraint. The resulting compiler, when applied to six commercial microcontroller programs, generates code nearly as compact as carefully crafted code.

Real-time, reactive, and embedded systems are increasingly used throughout society (e.g., flight control, railway signaling, vehicle management, medical devices, and many others). For real-time, interrupt-driven software, timely interrupt handling is part of correctness. It is vital for software verification in such systems to check that all specified deadlines for interrupt handling are met. Such verification is a daunting task because of the large number of different possible interrupt arrival scenarios. For example, for a Z86-based microcontroller, there can be up to six interrupt sources and each interrupt can arrive during any clock cycle. Verification of such systems has traditionally relied upon lengthy and tedious testing; even under the best of circumstances, testing is likely to cover only a fraction of the state space in interrupt-driven systems. This paper presents the Zilog architecture resource bounding infrastructure (ZARBI), a tool for deadline analysis of interrupt-driven Z86-based software. The main idea is to use static analysis to significantly decrease the required testing effort by automatically identifying and isolating the segments of code that need the most testing. Our tool combines multiresolution static analysis and testing oracles in such a way that only the oracles need to be verified by testing. Each oracle specifies the worst-case execution time from one program point to another, which is then used by the static analysis to improve precision. For six commercial microcontroller systems, our experiments show that a moderate number of testing oracles are sufficient to do precise deadline analysis.

Processors such as StrongARM and memory such as SDRAM enable efficient execution of multiple loads and stores in a single instruction. This is particularly useful in connection with register allocation where spill code may need to save and restore multiple registers. Until now, there has been no effective strategy for utilizing this to its full potential. In this paper we investigate the use of SDRAM for optimization of spill code. The core of the problem is to arrange the variables in the spill area such that loading to and storing from the SDRAM is optimally efficient. We show that the problem is NP-complete and present a method based on integer linear programming (ILP) to solve the problem. We have implemented our approach as an additional phase in a gcc-based compiler for the StrongARM core of Intel's IXP--1200 network processor. Our optimizer, SLA (stack location allocator), rearranges the scalar variables so that memory accesses can be made cheaper. Our experimental results show that our ILP-based method is efficient and that the code generated for our benchmarks runs 0.8--15.1% faster than the code produced by the original compiler with --O2 optimization. Our SLA phase is guaranteed to not deteriorate the execution-time performance and can be configured such as not to increase the code size.

Confinement properties impose a structure on object graphs which can be used to enforce encapsulation properties essential to certain program optimizations, modular reasoning, and software assurance. This paper formalizes the notion of confined type in the context of Featherweight Java. A static type system that mirrors the informal rules of Grothoff et al [17] is proven sound. The definition of confined types is extended to confined instantiation of generic classes. This allows for confined collection types in Java and for classes that can be confined post hoc. Confinement type rules are given for Generic Featherweight Java, and proven sound.

Real-time, reactive, and embedded systems are widely used throughout society (e.g., flight control, railway signaling, vehicle management, medical devices, and many others). For real-time, interrupt-driven software, timely interrupt handling is part of correctness. It is vital for software verification in such systems to check that all specified deadlines for interrupt handling will be met. Such verification is a daunting task because of the large number of different possible interrupt arrival scenarios. For example, for a Z86-based microcontroller, there can be up to six interrupt sources and each interrupt can arrive during any clock cycle. Verification of such systems has traditionally relied upon lengthy and tedious testing; even under the best of circumstances, testing is likely to cover only a fraction of the state space in interrupt-driven systems.This paper presents a tool for deadline analysis of interrupt-driven Z86-based software. The main idea is to use static analysis to significantly decrease the required testing effort by automatically identifying and isolating the segments of code that need the most testing. Our tool combines multi-resolution static analysis and testing oracles in such a way that only the oracles need to be verified by testing. Each oracle specifies the worst-case execution time from one program point to another, which is then used by the static analysis to improve precision. For six commercial microcontroller systems, our experiments show that a moderate number of testing oracles are sufficient to do precise deadline analysis.

We consider the question of how a Continuation-Passing-Style (CPS) transformation changes the flow analysis of a program. We present an algorithm that takes the least solution to the flow constraints of a program and constructs in linear time the least solution to the flow constraints for the CPS-transformed program. Previous studies of this question used CPS transformations that had the effect of duplicating code, or of introducing flow sensitivity into the analysis. Our algorithm has the property that for a program point in the original program and the corresponding program point in the CPS-transformed program, the flow information is the same. By carefully avoiding both duplicated code and flow-sensitive analysis, we find that the most accurate analysis of the CPS-transformed program is neither better nor worse than the most accurate analysis of the original. Thus a compiler that needed flow information after CPS transformation could use the flow information from the original program to annotate some program points, and it could use our algorithm to find the rest of the flow information quickly, rather than having to analyze the CPS-transformed program.

Record concatenation, multiple inheritance, and multiple-object cloning are closely related and part of various language designs. For example, in Cardelli's untyped Obliq language, a new object can be constructed from several existing objects by cloning followed by concatenation; an error is given in case of field name conflicts. Type systems for record concatenation have been studied by M. Wand (1991), R. Harper and B. Pierce (1991), D. Remy (1992), and others; and type inference for the combination of record concatenation and subtyping has been studied by M. Sulzmann (1997) and by F. Pottier (2000). In this paper we present the first polynomial-time type inference algorithm for record concatenation, subtyping, and recursive types. Our example language is the Abadi-Cardelli object calculus extended with a concatenation operator The type inference algorithm runs in O(n/sup 5/) time where n is the size of the program. Our algorithm enables efficient type checking of Obliq programs without changing the programs at all.

Resource-constrained devices are becoming ubiquitous. Examples include cell phones, Palm Pilots and digital thermostats. It can be difficult to fit the required functionality into such a device without sacrificing the simplicity and clarity of the software. Increasingly complex embedded systems require extensive brute-force testing, making development and maintenance costly. This is particularly true for system components that are written in assembly language. Static checking has the potential of alleviating these problems, but until now there has been little tool support for programming at the assembly level. In this paper, we present the design and implementation of a static checker for interrupt-driven Z86-based software with hard real-time requirements. For six commercial microcontrollers, our checker has produced upper bounds on interrupt latencies and stack sizes, as well as verified fundamental safety and liveness properties. Our approach is based on a known algorithm for the model checking of pushdown systems and produces a control-flow graph annotated with information about time, space, safety and liveness. Each benchmark is approximately 1000 lines of code, and the checking is done in a few seconds on a standard PC. Our tool is one of the first to give an efficient and useful static analysis of assembly code. It enables increased confidence in code correctness, significantly reduced testing requirements and support for maintenance throughout the system life-cycle.

Object-oriented languages provide little support for encapsulating objects. Reference semantics allows objects to escape their defining scope. The pervasive aliasing that ensues remains a major source of software defects. This paper introduces Kacheck/J a tool for inferring object encapulation properties in large Java programs. Our goal is to develop practical tools to assist software engineers, thus we focus on simple and scalable techniques. Kacheck/J is able to infer confinement for Java classes. A class and its sublasses are confined if all of their instances are encapsulated in their defining package. This simple property can be used to identify accidental leaks of sensitive objects. The analysis is scalable and efficient; Kacheck/J is able t infer confinement on a corpus of 46,000 classes (115 MB) in 6 minutes

Type-based analysis is an approach to static analysis of programs that has been studied for more than a decade. A type-based analysis assumes that the program type checks, and the analysis takes advantage of that. This paper examines the state of the art of type-based analysis, and it surveys some of the many software tools that use type-based analysis. Most of the surveyed tools use types as discriminators, while most of the theoretical studies use type and effect systems. We conclude that type-based analysis is a promising approach to achieving both provable correctness and good performance with a reasonable effort.

Many polyvariant program analyses have been studied in the 1990s, including k -CFA, polymorphic splitting, and the cartesian product algorithm. The idea of polyvariance is to analyze functions more than once and thereby obtain better precision for each call site. In this paper we present an equivalence theorem which relates a co-inductively-defined family of polyvariant flow analyses and a standard type system. The proof embodies a way of understanding polyvariant flow information in terms of union and intersection types, and, conversely, a way of understanding union and intersection types in terms of polyvariant flow information. We use the theorem as basis for a new flow-type system in the spirit of the λ CIL -calculus of Wells, Dimock, Muller and Turbak, in which types are annotated with flow information. A flow-type system is useful as an interface between a flow-analysis algorithm and a program optimizer. Derived systematically via our equivalence theorem, our flow-type system should be a good interface to the family of polyvariant analyses that we study.

There are at least four US patents on software watermarking, and an idea for further advancing the state of the art was presented by C. Collberg and C. Thomborsen (1999). The new idea is to embed a watermark in dynamic data structures, thereby protecting against many program-transformation attacks. Until now there have been no reports on practical experience with this technique. We have implemented and experimented with a watermarking system for Java based on the ideas of Collberg and Thomborsen. Our experiments show that watermarking can be done efficiently with moderate increases in code size, execution times and heap-space usage, while making the watermarked code resilient to a variety of program-transformation attacks. For a particular representation of watermarks, the time to retrieve a watermark is on the order of one minute per megabyte of heap space. Our implementation is not designed to resists all possible attacks; to do that, it should be combined with other protection techniques, such as obfuscation and tamperproofing.

Equality and subtyping of recursive types have been studied in the 1990s by: R.M. Amadaio and L. Cardelli (1993); D. Kozen et al. (1993); M. Brandt and F. Henglein (1997) and others. Potential applications include automatic generation of bridge code for multi-language systems and type-based retrieval of software modules from libraries. J. Auerbach et al. (1998) advocate a highly flexible combination of matching rules for which there, until now, are no efficient algorithmic techniques. We present an efficient decision procedure for a notion of type equality that includes unfolding of recursive types, and associativity and commutativity of product types, as advocated by Auerbach et al. For two types of size at most n, our algorithm decides equality in O(n/sup 2/) time. The algorithm iteratively prunes a set of type pairs, and eventually it produces a set of pairs of equal types. In each iteration, the algorithm exploits a so-called coherence property of the set of type pairs produced in the preceding iteration. The algorithm takes O(n) iterations, each of which takes O(n) time, for a total of O(n/sup 2/) time.

Propagation-based call graph construction algorithms have been studied intensively in the 199Os, and differ primarily in the number of sets that are used to approximate run-time values of expressions. In practice, algorithms such as RTA that use a single set for the whole program scale well. The scalability of algorithms such as 0-CFA that use one set per expression remains doubtful.In this paper, we investigate the design space between RTA and 0-CFA. We have implemented various novel algorithms in the context of Jax, an application extractor for Java, and shown that they all scale to a 325,000-line program. A key property of these algorithms is that they do not analyze values on the run-time stack, which makes them efficient and easy to implement. Surprisingly, for detecting unreachable methods, the inexpensive RTA algorithm does almost as well as the seemingly more powerful algorithms. However, for determining call sites with a single target, one of our new algorithms obtains the current best tradeoff between speed and precision.

For object-oriented programming, the Visitor pattern enables the definition of a new operation on an object structure without changing the classes of the objects. The price has been that the set of classes must be fixed in advance, and they must each have a so-called accept method. In this paper we demonstrate how to program visitors without relying on accept methods and without knowing all classes of the objects in advance. The idea, derived from related work on shape polymorphism in functional programming, is to separate (1) accessing subobjects, and (2) acting on them. In the object-oriented setting, reflection techniques support access to sub-objects, as demonstrated in our Java class, Walkabout. It supports all visitors as subclasses, and they can be programmed without any further use of reflection. Thus a program using the Visitor pattern can now be understood as a specialized version of a program using the Walkabout class.

Many polyvariant program analyses have been studied in the 199Os, including k-CFA, poly-k-CFA, and the Cartesian product algorithm. The idea of polyvariance is to analyze functions more than once and thereby obtain better precision for each call site. In this paper we present the first formal relationship between polyvariant analysis and standard notions of type. In the spirit of Nielson and Nielson, we study a parameterized flow analysis which can be instantiated to the analyses of Agesen, Schmidt, and as a simple case also 0-CFA. Extended with safety checks, the flow analysis accepts and rejects programs, much like a type checker. We prove that if a program can be safety-checked by a finitary instantiation of the flow analysis, then it can also be typed in a type system with intersection types, union types, subtyping, and recursive types, but no universal or existential quantifiers. This provides a framework for designing and understanding combinations of flow analyses and type systems.

Equality-based control-flow analysis has been studied by Henglein, Bondorf and Jørgensen, DeFouw, Grove, and Chambers, and others. It is faster than the subset-based-0-CFA, but also more approximate. Heintze asserted in 1995 that a program can be safety checked with an equality-based control-flow analysis if and only if it can be typed with recursive types. In this article we falsify Heintze's assertion, and we present a type system equivalent to equality-based control-flow analysis. The new type system contains both recursive types and an unusual notion of subtyping. We have s ≤ t if s and t unfold to the same regular tree, and we have ⊥≤t≤⊤ where t is a function type. In particular, there is no nontrivial subtyping between function types.

A collection of design patterns was described by E. Gamma et al. (1994). Each pattern ensures that a certain system aspect can vary over time, for example the operations that can be applied to an object or the algorithm of a method. The patterns are described by constructs such as the inheritance and reference relations, attempting to emulate more dynamic relationships. As a result, the design patterns demonstrate how awkward it is to program natural concepts of evolution when using a traditional object oriented language. We present a new relation between classes: the context relation. It directly models dynamic evolution, and it is meaningful at both the design and implementation level. At the design level we extend the Unified Modeling Language (UML) to include the context relation as a new form of arrow between classes. At the implementation level we present a small extension of Java. The context relation introduces a new form of dynamic binding that serves as a replacement to delegation. We demonstrate how the context relation can be used to easily model and program numerous design patterns.

Abstract We present an O(n 3 ) time type inference algorithm for a type system with a largest type Τ , a smallest type ⊥, and the usual ordering between function types. The algorithm infers type annotations of least shape, and it works equally well for recursive types. For the problem of typability, our algorithm is simpler than the one of Kozen, Palsberg, and Schwartzbach for type inference without ⊥. This may be surprising, especially because the system with ⊥ is strictly more powerful.

This paper introduces trust analysis for higher-order languages. Trust analysis encourages the programmer to make explicit the trustworthiness of data, and in return it can guarantee that no mistakes with respect to trust will be made at run-time. We present a confluent λ-calculus with explicit trust operations, and we equip it with a trust-type system which has the subject reduction property. Trust information is presented as annotations of the underlying Curry types, and type inference is computable in O ( n 3 ) time.

A collection of design patterns was described by Gamma, Helm, Johnson, and Vlissides in 1994. Recognizing that designs change, each pattern ensures that a certain system aspect can vary over time such as the operations that can be applied to an object or the algorithm of a method. The patterns are described by constructs such as the inheritance and reference relations, attempting to emulate more dynamic relationships. As a result, the design patterns demonstrate how awkward it is to program natural concepts of behavioral evolution when using a traditional object-oriented language.In this paper we present a new relation between classes: the context relation. It directly supports behavioral evolution, and it is meaningful at the analysis, design, and implementation level. At the design level we picture a context relation as a new form of arrow between classes. At the implementation level we use a small extension of C++. The basic idea is that if class C is context-related to a base class B, then B-objects can get their functionality dynamically altered by C-objects. Our language construct for doing this is a generalization of the method update in Abadi and Cardelli's imperative object calculus. A C-object may be explicitly attached to a B-object, or it may be implicitly attached to a group of B-objects for the duration of a method invocation. We demonstrate how the context relation can be used to easily model and program the Adapter, Bridge, Chain of Responsibility, Decorator, Iterator, Observer, State, Strategy, and Visitor patterns.

Abstract Compiler generation based on Mosses' action semantics has been studied by Brown, Moura, and Watt, and also by the second author. The core of each of their systems is a handwritten action compiler, producing either C or machine code. We have obtained an action compiler in a much simpler way: by partial evaluation of an action interpreter. Even though our compiler produces Scheme code, the code runs as fast as that produced by the previous action compilers.

Partial-evaluation folklore has it that massaging one's source programs can make them specialize better. In Jones, Gomard, and Sestoft's recent textbook, a whole chapter is dedicated to listing such “binding-time improvements”: nonstandard use of continuation-passing style, eta-expansion, and a popular transformation called “The Trick.” We provide a unified view of these binding-time improvements, from a typing perspective. Just as a proper treatment of product values in partial evaluation requires partially static values, a proper treatment of disjoint sums requires moving static contexts across dynamic case expressions. This requirement precisely accounts for the nonstandard use of continuation-passing style encountered in partial evaluation. Eta-expansion thus acts as a uniform binding-time coercion between values and contexts, be they of function type, product type, or disjoint-sum type. For the latter case, it enables “The Trick.” In this article, we extend Gomard and Jones' partial evaluator for the λ-calculus, λ-Mix, with products and disjoint sums; we point out how eta-expansion for (finite) disjoint sums enable The Trick; we generalize our earlier work by identifying the eta-expansion can be obtained in the binding-time analysis simple by adding two coercion rules; and we specify and prove the correctness of our extension to λ-Mix.

A constrained type consists of both a standard type and a constraint set. Such types enable efficient type inference for object-oriented languages with polymorphism and subtyping, as demonstrated by Eifrig, Smith, and Trifonov. Until now, it has been unclear how expressive constrained types are. In this article we study constrained types without universal quantification. We prove that they accept the same programs as the type system of Amadio and Cardelli with subtyping and recursive types. This result gives a precise connection between constrained types and the standard notion of types.

Flow-based safety analysis of higher-order languages has been studied by Shivers, and Palsberg and Schwartzbach. Open until now is the problem of finding a type system that accepts exactly the same programs as safety analysis.

Subtyping in the presence of recursive types for the λ-calculus was studied by Amadio and Cardelli in 1991 (Amadio and Cardelli 1991). In that paper they showed that the problem of deciding whether one recursive type is a subtype of another is decidable in exponential time. In this paper we give an 0(n2) algorithm. Our algorithm is based on a simplification of the definition of the subtype relation, which allows us to reduce the problem to the emptiness problem for a certain finite automaton with quadratically many states. It is known that equality of recursive types and the covariant Bohm order can be decided efficiently by means of finite automata, since they are just language equality and language inclusion, respectively. Our results extend the automata-theoretic approach to handle orderings based on contravariance.

We study a type system with a notion of subtyping that involves a largest type ⊤, a smallest type ⊥, atomic coercions between base types, and the usual ordering of function types. We prove that any λ-term typable in this system is strongly normalizing, which solves an open problem of Thatte. We also prove that the fragment without ⊥ types has strictly fewer terms. This demonstrates that ⊥ adds power to a type system.

Abstract We have designed and implemented a type inference algorithm for the SELF language. The algorithm can guarantee the safety and disambiguity of message sends, and provide useful information for browsers and optimizing compilers. SELF features objects with dynamic inheritance. This construct has until now been considered incompatible with type inference because it allows the inheritance graph to change dynamically. Our algorithm handles this by deriving and solving type constraints that simultaneously define supersets of both the possible values of expressions and of the possible inheritance graphs. The apparent circularity is resolved by computing a global fixed‐point, in polynomial time. The algorithm has been implemented and can successfully handle the SELF benchmark programs, which exist in the ‘standard SELF world’ of more than 40,000 lines of code.

Flow analyses of untyped higher-order functional programs have in the past decade been presented by Ayers, Bondorf, Consel, Jones, Heintze, Sestoft, Shivers, Steckler, Wand, and others. The analyses are usually defined as abstract interpretations and are used for rather different tasks such as type recovery, globalization, and binding-time analysis. The analyses all contain a global closure analysis that computes information about higher-order control-flow. Sestoft proved in 1989 and 1991 that closure analysis is correct with respect to call-by-name and call-by-value semantics, but it remained open if correctness holds for arbitrary beta-reduction. This article answers the question; both closure analysis and others are correct with respect to arbitrary beta-reduction. We also prove a subject-reduction result: closure information is still valid after beta-reduction. The core of our proof technique is to define closure analysis using a constraint system. The constraint system is equivalent to the closure analysis of Bondorf, which in turn is based on Sestoft's.

Flow-based safety analysis of higher-order languages has been studied by Shivers, and Palsberg and Schwartzbach. Open until now is the problem of finding a type system that accepts exactly the same programs as safety analysis. In this article we prove that Amadio and Cardelli's type system with subtyping and recursive types accepts the same programs as a certain safety analysis. The proof involves mappings from types to flow information and back. As a result, we obtain an inference algorithm for the type system, thereby solving an open problem.

Adaptive programs compute with objects, just like object-oriented programs. Each task to be accomplished is specified by a so-called propagation pattern which traverses the receiver object. The object traversal is a recursive descent via the instance variables where information is collected or propagated along the way. A propagation pattern consists of (1) a name for the task, (2) a succinct specification of the parts of the receiver object that should be traversed, and (3) code fragments to be executed when specific object types are encountered. The propagation patterns need to be complemented by a class graph which defines the detailed object structure. The separation of structure and behavior yields a degree of flexibility and understandability not present in traditional object-oriented languages. For example, the class graph can be changed without changing the adaptive program at all. We present an efficient implementation of adaptive programs. Given an adaptive program and a class graph, we generate an efficient object-oriented program, for example, in C++. Moreover, we prove the correctness of the core of this translation. A key assumption in the theorem is that the traversal specifications are consistent with the class graph. We prove the soundness of a proof system for conservatively checking consistency, and we show how to implement it efficiently.

Abadi and Cardelli (1994) have investigated a calculus of objects. The calculus supports a key feature of object-oriented languages: an object can be emulated by another object that has more refined methods. Abadi and Cardelli presented four first-order type systems for the calculus. The simplest one is based on finite types and no subtyping, and the most powerful one has both recursive types and subtyping. Open until now is the question of type inference, and in the presence of subtyping "the absence of minimum typings poses practical problems for type inference". In this paper we give an O(n/sup 3/) algorithm for each of the four type inference problems and we prove that all the problems are P-complete.>

Subtyping in the presence of recursive types for the l-calculus was studied by Amadio and Cardelli in 1991 [1]. In that paper they showed that the problem of deciding whether one recursive type is a sub-type of another is decidable in exponential time.In this paper we give an O(n2) algorithm. Our algorithm is based on a simplification of the definition of the subtype relation, which allows us to reduce the problem to the emptiness problem for a certain finite automaton with quadratically many states.It is known that equality of recursive types and the covariant Bo¨hm order can be decided efficiently by means of finite automata. Our results extend the automata-theoretic approach to handle orderings based on contravariance.

Abstract A binding-time analysis is correct if it always produces consistent binding-time information. Consistency prevents partial evaluators from ‘going wrong’. A sufficient and decidable condition for consistency, called well-annotatedness, was first presented by Gomard and Jones. In this paper we prove that a weaker condition implies consistency. Our condition is decidable, subsumes the one of Gomard and Jones, and was first studied by Schwartzbach and the present author. Our result implies the correctness of the binding-time analysis of Mogensen, and it indicates the correctness of the core of the binding-time analyses of Bondorf and Consel. We also prove that all partial evaluators will on termination have eliminated all ‘eliminable’-marked parts of an input which satisfies our condition. This generalizes a result of Gomard. Our development is for the pure λ-calculus with explicit binding-time annotations.

Partial types for the lambda -calculus were introduced by Thatte (1988) as a means of typing objects that are not typable with simple types, such as heterogeneous lists and persistent data. He showed that type inference for partial types was semidecidable. Decidability remained open until O'Keefe and Wand gave an exponential time algorithm for type inference. The authors give an O(n/sup 3/) algorithm. The algorithm constructs a certain finite automaton that represents a canonical solution to a given set of type constraints. Moreover, the construction works equally well for recursive types.>

We present a new approach to inferring types in untyped object-oriented programs with inheritance, assignments, and late binding.It guarantees that all messages are understood, annotates the program with type information, allows polymorphic methods, and can be used as the basis of an optimizing compiler.Types are finite sets of classes and subtyping is set inclusion.Using a trace graph, our algorithm constructs a set of conditional type constraints and computes the least solution by least fixed-point derivation.

This paper presents a denotational model of inheritance. The model is based on an intuitive motivation of the purpose of inheritance. The correctness of the model is demonstrated by proving it equivalent to an operational semantics of inheritance based upon the method-lookup algorithm of object-oriented languages. Although it was originally developed to explain inheritance in object-oriented languages, the model shows that inheritance is a general mechanism that may be applied to any form of recursive definition.