bluuebunny/crossref_metadata_2025 huggingface dataset:
A sound (and complete) model of contracts
Authors: Blume Matthias , McAllester David
Published: November 2005

Even in statically typed languages it is useful to have certain invariants checked dynamically. Findler and Felleisen gave an algorithm for dynamically checking expressive higher-order types called contracts. If we postulate soundness (in the sense that whenever a term is accused of violating its contract it really does fail to satisfy it), then their algorithm implies a semantics for contracts. Unfortunately, the implicit nature of the resulting model makes it rather unwieldy.In this paper we demonstrate that a direct approach yields essentially the same semantics without having to refer to contract-checking in its definition. The so-defined model largely coincides with intuition, but it does expose some peculiarities in its interpretation of
predicate contracts
where a notion of
safety
(which we define in the paper) "leaks" into the semantics of Findler and Felleisen's original
unrestricted
predicate contracts.This counter-intuitive aspect of the semantics can be avoided by changing the language, replacing unrestricted predicate contracts with a restricted version. The corresponding loss in expressive power can be recovered by also providing a way of explicitly expressing safety as a contract-either in ad-hoc fashion or, e.g., by including general recursive contracts.
Functional morphology
Authors: Forsberg Markus , Ranta Aarne
Published: November 2005

This paper presents a methodology for implementing natural language morphology in the functional language Haskell. The main idea behind is simple: instead of working with untyped regular expressions, which is the state of the art of morphology in computational linguistics, we use finite functions over hereditarily finite algebraic datatypes. The definitions of these datatypes and functions are the language-dependent part of the morphology. The language-independent part consists of an untyped dictionary format which is used for synthesis of word forms, and a decorated trie, which is used for analysis.Functional Morphology builds on ideas introduced by Huet in his computational linguistics toolkit Zen, which he has used to implement the morphology of Sanskrit. The goal has been to make it easy for linguists, who are not trained as functional programmers, to apply the ideas to new languages. As a proof of the productivity of the method, morphologies for Swedish, Italian, Russian, Spanish, and Latin have already been implemented using the library. The Latin morphology is used as a running example in this article.
Slideshow
Authors: Findler Robert Bruce , Flatt Matthew
Published: November 2005

Among slide-presentation systems, the dominant application offers essentially no abstraction capability. Slideshow, an extension of PLT Scheme, represents our effort over the last several years to build an abstraction-friendly slide system. We show how functional programming is well suited to the task of slide creation, we report on the programming abstractions that we have developed for slides, and we describe our solutions to practical problems in rendering slides. We also describe a prototype extension to DrScheme that supports a mixture of programmatic and WYSIWYG slide creation.
Generics for the masses
Authors: Hinze Ralf
Published: November 2005

A generic function is a function that can be instantiated on many data types to obtain data type specific functionality. Examples of generic functions are the functions that can be derived in Haskell, such as
show
,
read
, and '=='. The recent years have seen a number of proposals that support the definition of generic functions. Some of the proposals define new languages, some define extensions to existing languages. As a common characteristic none of the proposals can be made to work within Haskell 98: they all require something extra, either a more sophisticated type system or an additional language construct. The purpose of this pearl is to show that one can, in fact, program generically within Haskell 98 obviating to some extent the need for fancy type systems or separate tools. Haskell's type classes are at the heart of this approach: they ensure that generic functions can be defined succinctly and, in particular, that they can be used painlessly.
Slicing Z specifications
Authors: Wu Fangjun , Yi Tong
Published: November 2005

Program slicing is a well-known technique that has been broadly applied to a variety of software engineering areas, such as understanding, debugging, testing and others. Although slicing programs written in a high-level language have been widely studied in literatures, very little work is involved in slicing formal specifications. In this paper we put forward a method of specification slicing. First, we analyze dependences in Z and introduce a new kind of dependence, i.e. logic dependence. Second, schema dependence graphs and specification dependence graphs are developed. On the basis of both graphs, a method of slicing specifications is given. Finally, a small but realistic example is illustrated.
A practical adoption of partial redundancy elimination
Authors: Bronnikov Dmitri
Published: November 2005

Partial redundancy elimination is a powerful optimization technique which needs little introduction. The original formulation was introduced in 1979 by Morel and Renvoise. More efficient formulations have since been offered.

We introduce an ever more simple and efficient formulation. We also show how PRE can be used to deal with partially redundant register loads and stores introduced by spilling.
Scalable extensibility via nested inheritance
Authors: Nystrom Nathaniel , Chong Stephen , Myers Andrew C.
Published: November 2005

Inheritance is a useful mechanism for factoring and reusing code. However, it has limitations for building extensible systems. We describe nested inheritance, a mechanism that addresses some of the limitations of ordinary inheritance and other code reuse mechanisms. Using our experience with an extensible compiler framework, we show how nested inheritance can be used to construct highly extensible software frameworks. The essential aspects of nested inheritance are formalized in a simple object-oriented language with an operational semantics and type system. The type system of this language is sound, so no run-time type checking is required to implement it and no run-time type errors can occur. We describe our implementation of nested inheritance as an unobtrusive extension of the Java language, called Jx. Our prototype implementation translates Jx code to ordinary Java code, without duplicating inherited code.
Super and inner
Authors: Goldberg David S. , Findler Robert Bruce , Flatt Matthew
Published: November 2005

In an object-oriented language, a derived class may declare a method with the same signature as a method in the base class. The meaning of the re-declaration depends on the language. Most commonly, the new declaration overrides the base declaration, perhaps completely replacing it, or perhaps using super to invoke the old implementation. Another possibility is that the base class always controls the method implementation, and the new declaration merely augments the method in the case that the base method calls inner. Each possibility has advantages and disadvantages. In this paper, we explain why programmers need both kinds of method redeclaration, and we present a language that integrates them. We also present a formal semantics for the new language, and we describe an implementation for MzScheme.
Measuring the dynamic behaviour of AspectJ programs
Authors: Dufour Bruno , Goard Christopher , Hendren Laurie , de Moor Oege , Sittampalam Ganesh , Verbrugge Clark
Published: November 2005

This paper proposes and implements a rigorous method for studying the dynamic behaviour of AspectJ programs. As part of this methodology several new metrics specific to AspectJ programs are proposed and tools for collecting the relevant metrics are presented. The major tools consist of: (1) a modified version of the AspectJ compiler that tags bytecode instructions with an indication of the cause of their generation, such as a particular feature of AspectJ; and (2) a modified version of the *J dynamic metrics collection tool which is composed of a JVMPI-based trace generator and an analyzer which propagates tags and computes the proposed metrics. This dynamic propagation is essential, and thus this paper contributes not only new metrics, but also non-trivial ways of computing them.

We furthermore present a set of benchmarks that exercise a wide range of AspectJ's features, and the metrics that we measured on these benchmarks. The results provide guidance to AspectJ users on how to avoid efficiency pitfalls, to AspectJ implementors on promising areas for future optimization, and to tool builders on ways to understand the runtime behaviour of AspectJ.
Decentralizing execution of composite web services
Authors: Nanda Mangala Gowri , Chandra Satish , Sarkar Vivek
Published: November 2005

Distributed enterprise applications today are increasingly being built from services available over the web. A unit of functionality in this framework is a web service, a software application that exposes a set of "typed'' connections that can be accessed over the web using standard protocols. These units can then be composed into a composite web service. BPEL (Business Process Execution Language) is a high-level distributed programming language for creating composite web services.

Although a BPEL program invokes services distributed over several servers, the orchestration of these services is typically under centralized control. Because performance and throughput are major concerns in enterprise applications, it is important to remove the inefficiencies introduced by the centralized control. In a distributed, or decentralized orchestration, the BPEL program is partitioned into independent sub-programs that interact with each other without any centralized control. Decentralization can increase parallelism and reduce the amount of network traffic required for an application.

This paper presents a technique to partition a composite web service written as a single BPEL program into an equivalent set of decentralized processes. It gives a new code partitioning algorithm to partition a BPEL program represented as a program dependence graph, with the goal of minimizing communication costs and maximizing the throughput of multiple concurrent instances of the input program. In contrast, much of the past work on dependence-based partitioning and scheduling seeks to minimize the completion time of a single instance of a program running in isolation. The paper also gives a cost model to estimate the throughput of a given code partition.
Transparent proxies for java futures
Authors: Pratikakis Polyvios , Spacco Jaime , Hicks Michael
Published: November 2005

A proxy object is a surrogate or placeholder that controls access to another target object. Proxies can be used to support distributed programming, lazy or parallel evaluation, access control, and other simple forms of behavioral reflection. However, wrapper proxies (like futures or suspensions for yet-to-be-computed results) can require significant code changes to be used in statically-typed languages, while proxies more generally can inadvertently violate assumptions of transparency, resulting in subtle bugs.

To solve these problems, we have designed and implemented a simple framework for proxy programming that employs a static analysis based on qualifier inference, but with additional novelties. Code for using wrapper proxies is automatically introduced via a classfile-to-classfile transformation, and potential violations of transparency are signaled to the programmer. We have formalized our analysis and proven it sound. Our framework has a variety of applications, including support for asynchronous method calls returning futures. Experimental results demonstrate the benefits of our framework: programmers are relieved of managing and/or checking proxy usage, analysis times are reasonably fast, overheads introduced by added dynamic checks are negligible, and performance improvements can be significant. For example, changing two lines in a simple RMI-based peer-to-peer application and then using our framework resulted in a large performance gain.
An efficient parallel heap compaction algorithm
Authors: Abuaiadh Diab , Ossia Yoav , Petrank Erez , Silbershtein Uri
Published: November 2005

We propose a heap compaction algorithm appropriate for modern computing environments. Our algorithm is targeted at SMP platforms. It demonstrates high scalability when running in parallel but is also extremely efficient when running single-threaded on a uniprocessor. Instead of using the standard forwarding pointer mechanism for updating pointers to moved objects, the algorithm saves information for a pack of objects. It then does a small computation to process this information and determine each object's new location. In addition, using a smart parallel moving strategy, the algorithm achieves (almost) perfect compaction in the lower addresses of the heap, whereas previous algorithms achieved parallelism by compacting within several predetermined segments.

Next, we investigate a method that trades compaction quality for a further reduction in time and space overhead. Finally, we propose a modern version of the two-finger compaction algorithm. This algorithm fails, thus, re-validating traditional wisdom asserting that retaining the order of live objects significantly improves the quality of the compaction.

The parallel compaction algorithm was implemented on the IBM production Java Virtual Machine. We provide measurements demonstrating high efficiency and scalability. Subsequently, this algorithm has been incorporated into the IBM production JVM.
Method-level phase behavior in java workloads
Authors: Georges Andy , Buytaert Dries , Eeckhout Lieven , De Bosschere Koen
Published: November 2005

Java workloads are becoming more and more prominent on various computing devices. Understanding the behavior of a Java workload which includes the interaction between the application and the virtual machine (VM), is thus of primary importance during performance analysis and optimization. Moreover, as contemporary software projects are increasing in complexity, automatic performance analysis techniques are indispensable. This paper proposes an off-line method-level phase analysis approach for Java workloads that consists of three steps. In the first step, the execution time is computed for each method invocation. Using an off-line tool, we subsequently analyze the dynamic call graph (that is annotated with the method invocations' execution times) to identify method-level phases. Finally, we measure performance characteristics for each of the selected phases. This is done using hardware performance monitors. As such, our approach allows for linking microprocessor-level information at the individual methods in the Java application's source code. This is extremely interesting information during performance analysis and optimization as programmers can use this information to optimize their code. We evaluate our approach in the Jikes RVM on an IA-32 platform using the SPECjvm98 and SPECjbb2000 benchmarks. This is done according to a number of important criteria: the overhead during profiling, the variability within and between the phases, its applicability in Java workload characterization (measuring performance characteristics of the various VM components) and application bottleneck identification.
Object-oriented units of measurement
Authors: Allen Eric , Chase David , Luchangco Victor , Maessen Jan-Willem , Steele Guy L.
Published: November 2005

Programs that manipulate physical quantities typically represent these quantities as raw numbers corresponding to the quantities' measurements in particular units (e.g., a length represented as a number of meters). This approach eliminates the possibility of catching errors resulting from adding or comparing quantities expressed in different units (as in the Mars Climate Orbiter error [11]), and does not support the safe comparison and addition of quantities of the same dimension. We show how to formulate dimensions and units as classes in a nominally typed object-oriented language through the use of statically typed metaclasses. Our formulation allows both parametric and inheritance poly-morphism with respect to both dimension and unit types. It also allows for integration of encapsulated measurement systems, dynamic conversion factors, declarations of scales (including nonlinear scales) with defined zeros, and nonconstant exponents on dimension types. We also show how to encapsulate most of the "magic machinery" that handles the algebraic nature of dimensions and units in a single meta-class that allows us to treat select static types as generators of a free abelian group.
Pluggable verification modules
Authors: Fong Philip W. L.
Published: November 2005

Through the design and implementation of a JVM that supports Pluggable Verification Modules (PVMs), the idea of an extensible protection mechanism is entertained. Link-time bytecode verification becomes a pluggable service that can be readily replaced, reconfigured and augmented. Application-specific verification services can be safely introduced into the dynamic linking process of the JVM. This feature is enabled by the adoption of a previously proposed modular verification architecture, Proof Linking [23, 24], which decouples bytecode verification from the dynamic linking process, rendering the verifier a replaceable module. The PVM mechanism has been implemented in an open source JVM, the Aegis VM [21]. To evaluate the software engineering and security engineering benefits of this extensible protection mechanism, an augmented type system JAC (Java Access Control) [37] has been successfully implemented as a PVM.
Chianti
Authors: Ren Xiaoxia , Shah Fenil , Tip Frank , Ryder Barbara G. , Chesley Ophelia
Published: November 2005

This paper reports on the design and implementation of Chianti, a change impact analysis tool for Java that is implemented in the context of the Eclipse environment. Chianti analyzes two versions of an application and decomposes their difference into a set of atomic changes. Change impact is then reported in terms of affected (regression or unit) tests whose execution behavior may have been modified by the applied changes. For each affected test, Chianti also determines a set of affecting changes that were responsible for the test's modified behavior. This latter step of isolating the changes that induce the failure of one specific test from those changes that only affect other tests can be used as a debugging technique in situations where a test fails unexpectedly after a long editing session. We evaluated Chianti on a year (2002) of CVS data from M. Ernst's Daikon system, and found that, on average, 52% of Daikon's unit tests are affected. Furthermore, each affected unit test, on average, is affected by only 3.95% of the atomic changes. These findings suggest that our change impact analysis is a promising technique for assisting developers with program understanding and debugging.
D-SPTF
Authors: Lumb Christopher R. , Golding Richard
Published: November 2005

Distributed Shortest-Positioning Time First (D-SPTF) is a request distribution protocol for decentralized systems of storage servers. D-SPTF exploits high-speed interconnects to dynamically select which server, among those with a replica, should service each read request. In doing so, it simultaneously balances load, exploits the aggregate cache capacity, and reduces positioning times for cache misses. For network latencies expected in storage clusters (e.g., 10--200μs), D-SPTF performs as well as would a hypothetical centralized system with the same collection of CPU, cache, and disk resources. Compared to popular decentralized approaches, D-SPTF achieves up to 65% higher throughput and adapts more cleanly to heterogenous server capabilities.
FAB
Authors: Saito Yasushi , Frølund Svend , Veitch Alistair , Merchant Arif , Spence Susan
Published: November 2005

This paper describes the design, implementation, and evaluation of a Federated Array of Bricks (FAB), a distributed disk array that provides the reliability of traditional enterprise arrays with lower cost and better scalability. FAB is built from a collection of
bricks
, small storage appliances containing commodity disks, CPU, NVRAM, and network interface cards. FAB deploys a new majority-voting-based algorithm to replicate or erasure-code logical blocks across bricks and a reconfiguration algorithm to move data in the background when bricks are added or decommissioned. We argue that voting is practical and necessary for reliable, high-throughput storage systems such as FAB. We have implemented a FAB prototype on a 22-node Linux cluster. This prototype sustains 85MB/second of throughput for a database workload, and 270MB/second for a bulk-read workload. In addition, it can outperform traditional master-slave replication through performance decoupling and can handle brick failures and recoveries smoothly without disturbing client requests.
Coherence decoupling
Authors: Huh Jaehyuk , Chang Jichuan , Burger Doug , Sohi Gurindar S.
Published: November 2005

This paper explores a new technique called
coherence decoupling
, which breaks a traditional cache coherence protocol into two protocols: a Speculative Cache Lookup (SCL) protocol and a safe, backing coherence protocol. The SCL protocol produces a speculative load value, typically from an invalid cache line, permitting the processor to compute with incoherent data. In parallel, the coherence protocol obtains the necessary coherence permissions and the correct value. Eventually, the speculative use of the incoherent data can be verified against the coherent data. Thus, coherence decoupling can greatly reduce --- if not eliminate --- the effects of false sharing. Furthermore, coherence decoupling can also reduce latencies incurred by true sharing. SCL protocols reduce those latencies by speculatively writing updates into invalid lines, thereby increasing the accuracy of speculation, without complicating the simple, underlying coherence protocol that guarantees correctness.The performance benefits of coherence decoupling are evaluated using a full-system simulator and a mix of commercial and scientific benchmarks. Our results show that 40% to 90% of all coherence misses can be speculated correctly, and therefore their latencies partially or fully hidden. This capability results in performance improvements ranging from 3% to over 16%, in most cases where the latencies of coherence misses have an effect on performance.
Continual flow pipelines
Authors: Srinivasan Srikanth T. , Rajwar Ravi , Akkary Haitham , Gandhi Amit , Upton Mike
Published: November 2005

Increased integration in the form of multiple processor cores on a single die, relatively constant die sizes, shrinking power envelopes, and emerging applications create a new challenge for processor architects. How to build a processor that provides high single-thread performance and enables multiple of these to be placed on the same die for high throughput while dynamically adapting for future applications? Conventional approaches for high single-thread performance rely on large and complex cores to sustain a large instruction window for memory tolerance, making them unsuitable for multi-core chips. We present
Continual Flow Pipelines
(CFP) as a new non-blocking processor pipeline architecture that achieves the performance of a large instruction window without requiring cycle-critical structures such as the scheduler and register file to be large. We show that to achieve benefits of a large instruction window, inefficiencies in management of both the scheduler and register file must be addressed, and we propose a unified solution. The non-blocking property of CFP keeps key processor structures affecting cycle time and power (scheduler, register file), and die size (second level cache) small. The memory latency-tolerant CFP core allows multiple cores on a single die while outperforming current processor cores for single-thread applications.
Locality phase prediction
Authors: Shen Xipeng , Zhong Yutao , Ding Chen
Published: November 2005

As computer memory hierarchy becomes adaptive, its performance increasingly depends on forecasting the dynamic program locality. This paper presents a method that predicts the locality phases of a program by a combination of locality profiling and run-time prediction. By profiling a training input, it identifies locality phases by sifting through all accesses to all data elements using variable-distance sampling, wavelet filtering, and optimal phase partitioning. It then constructs a phase hierarchy through grammar compression. Finally, it inserts phase markers into the program using binary rewriting. When the instrumented program runs, it uses the first few executions of a phase to predict all its later executions.Compared with existing methods based on program code and execution intervals, locality phase prediction is unique because it uses locality profiles, and it marks phase boundaries in program code. The second half of the paper presents a comprehensive evaluation. It measures the accuracy and the coverage of the new technique and compares it with best known run-time methods. It measures its benefit in adaptive cache resizing and memory remapping. Finally, it compares the automatic analysis with manual phase marking. The results show that locality phase prediction is well suited for identifying large, recurring phases in complex programs.
Performance directed energy management for main memory and disks
Authors: Li Xiaodong , Li Zhenmin , David Francis , Zhou Pin , Zhou Yuanyuan , Adve Sarita , Kumar Sanjeev
Published: November 2005

Much research has been conducted on energy management for memory and disks. Most studies use control algorithms that dynamically transition devices to low power modes after they are idle for a certain threshold period of time. The control algorithms used in the past have two major limitations. First, they require painstaking, application-dependent manual tuning of their thresholds to achieve energy savings without significantly degrading performance. Second, they do not provide performance guarantees. In one case, they slowed down an application by 835.This paper addresses these two limitations for both memory and disks, making memory/disk energy-saving schemes practical enough to use in real systems. Specifically, we make three contributions: (1) We propose a technique that provides a performance guarantee for control algorithms. We show that our method works well for all tested cases, even with previously proposed algorithms that are not performance-aware. (2) We propose a new control algorithm,
Performance-directed Dynamic
(PD), that dynamically adjusts its thresholds periodically, based on available slack and recent workload characteristics. For memory, PD consumes the least energy, when compared to previous hand-tuned algorithms combined with a performance guarantee. However, for disks, PD is too complex and its self-tuning is unable to beat previous hand-tuned algorithms. (3) To improve on PD, we propose a simple, optimization-based, threshold-free control algorithm,
Performance-directed Static
(PS). PS periodically assigns a static configuration by solving an optimization problem that incorporates information about the available slack and recent traffic variability to different chips/disks. We find that PS is the best or close to the best across all performanceguaranteed disk algorithms, including hand-tuned versions.
Environmental acquisition revisited
Authors: Cobbe Richard , Felleisen Matthias
Published: November 2005

In 1996, Gil and Lorenz proposed programming language constructs for specifying environmental acquisition in addition to inheritance acquisition for objects. They noticed that in many programs, objects are arranged in containment hierarchies and need to obtain information from their container objects. Therefore, if languages allowed programmers to specify such relationships directly, type systems and run-time environments could enforce the invariants that make these programming patterns work.In this paper, we present a formal version of environmental acquisition for class-based languages. Specifically, we introduce an extension of the ClassicJava model with constructs for environmental acquisition of fields and methods, a type system for the model, a reduction semantics, and a type soundness proof. We also discuss how to scale the model to a full-scale Java-like programming language.
A simple typed intermediate language for object-oriented languages
Authors: Chen Juan , Tarditi David
Published: November 2005

Traditional class and object encodings are difficult to use in practical type-preserving compilers because of the complexity of the encodings. We propose a simple typed intermediate language for compiling object-oriented languages and prove its soundness. The key ideas are to preserve lightweight notions of classes and objects instead of compiling them away and to separate name-based subclassing from structure-based subtyping. The language can express standard implementation techniques for both dynamic dispatch and runtime type tests. It has decidable type checking even with subtyping between quantified types with different bounds. Because of its simplicity, the language is a more suitable starting point for a practical type-preserving compiler than traditional encoding techniques.
Parametric polymorphism for XML
Authors: Hosoya Haruo , Frisch Alain , Castagna Giuseppe
Published: November 2005

Despite the extensiveness of recent investigations on static typing for XML, parametric polymorphism has rarely been treated. This well-established typing discipline can also be useful in XML processing in particular for programs involving "parametric schemas," i.e., schemas parameterized over other schemas (e.g., SOAP). The difficulty in treating polymorphism for XML lies in how to extend the "semantic" approach used in the mainstream (monomorphic) XML type systems. A naive extension would be "semantic" quantification over all substitutions for type variables. However, this approach reduces to an NEXPTIME-complete problem for which no practical algorithm is known. In this paper, we propose a different method that smoothly extends the semantic approach yet is algorithmically easier. In this, we devise a novel and simple
marking
technique, where we interpret a polymorphic type as a set of values with annotations of which subparts are parameterized. We exploit this interpretation in every ingredient of our polymorphic type system such as subtyping, inference of type arguments, and so on. As a result, we achieve a sensible system that directly represents a usual expected behavior of polymorphic type systems---"values of variable types are never reconstructed"---in a reminiscence of Reynold's parametricity theory. Also, we obtain a set of practical algorithms for typechecking by local modifications to existing ones for a monomorphic system.
Synthesis of interface specifications for Java classes
Authors: Alur Rajeev , Černý Pavol , Madhusudan P. , Nam Wonhong
Published: November 2005

While a typical software component has a clearly specified (static) interface in terms of the methods and the input/output types they support, information about the correct sequencing of method calls the client must invoke is usually undocumented. In this paper, we propose a novel solution for automatically extracting such temporal specifications for Java classes. Given a Java class, and a safety property such as "the exception
E
should not be raised", the corresponding
(dynamic) interface
is the most general way of invoking the methods in the class so that the safety property is not violated. Our synthesis method first constructs a symbolic representation of the finite state-transition system obtained from the class using
predicate abstraction
. Constructing the interface then corresponds to solving a
partial-information two-player game
on this symbolic graph. We present a sound approach to solve this computationally-hard problem approximately using algorithms for learning finite automata and symbolic model checking for branching-time logics. We describe an implementation of the proposed techniques in the tool
JIST
--- Java Interface Synthesis Tool---and demonstrate that the tool can construct interfaces accurately and efficiently for sample Java2SDK library classes.
Dynamic partial-order reduction for model checking software
Authors: Flanagan Cormac , Godefroid Patrice
Published: November 2005

We present a new approach to partial-order reduction for model checking software. This approach is based on initially exploring an arbitrary interleaving of the various concurrent processes/threads, and
dynamically
tracking interactions between these to identify backtracking points where alternative paths in the state space need to be explored. We present examples of multi-threaded programs where our new dynamic partial-order reduction technique significantly reduces the search space, even though traditional partial-order algorithms are helpless.
A probabilistic language based upon sampling functions
Authors: Park Sungwoo , Pfenning Frank , Thrun Sebastian
Published: November 2005

As probabilistic computations play an increasing role in solving various problems, researchers have designed probabilistic languages that treat probability distributions as primitive datatypes. Most probabilistic languages, however, focus only on discrete distributions and have limited expressive power. In this paper, we present a probabilistic language, called λο, which uniformly supports all kinds of probability distributions -- discrete distributions, continuous distributions, and even those belonging to neither group. Its mathematical basis is sampling functions,
i.e.
, mappings from the unit interval (0.0,1.0] to probability domains.We also briefly describe the implementation of λο as an extension of Objective CAML and demonstrate its practicality with three applications in robotics: robot localization, people tracking, and robotic mapping. All experiments have been carried out with real robots.
Transactors
Authors: Field John , Varela Carlos A.
Published: November 2005

We introduce
transactors
, a fault-tolerant programming model for composing loosely-coupled distributed components running in an unreliable environment such as the internet into systems that reliably maintain globally consistent distributed state. The transactor model incorporates certain elements of traditional transaction processing, but allows these elements to be composed in different ways without the need for central coordination, thus facilitating the study of distributed fault-tolerance from a semantic point of view. We formalize our approach via the τ-calculus, an extended lambda-calculus based on the
actor
model, and illustrate its usage through a number of examples. The τ-calculus incorporates constructs which distributed processes can use to create globally-consistent
checkpoints
. We provide an operational semantics for the τ-calculus, and formalize the following safety and liveness properties: first, we show that globally-consistent checkpoints have equivalent execution traces without any node failures or application-level failures, and second, we show that it is possible to reach globally-consistent checkpoints provided that there is some bounded failure-free interval during which checkpointing can occur.
Combinators for bi-directional tree transformations
Authors: Foster J. Nathan , Greenwald Michael B. , Moore Jonathan T. , Pierce Benjamin C. , Schmitt Alan
Published: November 2005

We propose a novel approach to the well-known
view update problem
for the case of tree-structured data: a domain-specific programming language in which all expressions denote bi-directional transformations on trees. In one direction, these transformations---dubbed
lenses
---map a "concrete" tree into a simplified "abstract view"; in the other, they map a modified abstract view, together with the original concrete tree, to a correspondingly modified concrete tree. Our design emphasizes both robustness and ease of use, guaranteeing strong well-behavedness and totality properties for well-typed lenses.We identify a natural space of well-behaved bi-directional transformations over arbitrary structures, study definedness and continuity in this setting, and state a precise connection with the classical theory of "update translation under a constant complement" from databases. We then instantiate this semantic framework in the form of a collection of
lens combinators
that can be assembled to describe transformations on trees. These combinators include familiar constructs from functional programming (composition, mapping, projection, conditionals, recursion) together with some novel primitives for manipulating trees (splitting, pruning, copying, merging, etc.). We illustrate the expressiveness of these combinators by developing a number of bi-directional list-processing transformations as derived forms.
Context logic and tree update
Authors: Calcagno Cristiano , Gardner Philippa , Zarfaty Uri
Published: November 2005

Spatial logics have been used to describe properties of tree-like structures (Ambient Logic) and in a Hoare style to reason about dynamic updates of heap-like structures (Separation Logic). We integrat this work by analyzing dynamic updates to tree-like structures with pointers (such as XML with identifiers and idrefs). Naíve adaptations of the Ambient Logic are not expressive enough to capture such local updates. Instead we must explicitly reason about arbitrary tree contexts in order to capture updates throughout the tree. We introduce Context Logic, study its proof theory and models, and show how it generalizes Separation Logic and its general theory BI. We use it to reason locally about a small imperative programming language for updating trees, using a Hoare logic in the style of O'Hearn, Reynolds and Yang, and show that weakest preconditions are derivable. We demonstrate the robustness of our approach by using Context Logic to capture the locality of term rewrite systems.
Connecting effects and uniqueness with adoption
Authors: Boyland John Tang , Retert William
Published: November 2005

"Adoption" is when on piece of stat is logically embedded in another piece of state. Adoption provides information hiding (the adopter can be used as a proxy for the adoptee) and with linear existentials, provides a way to store unique pointers in shared state. In this paper, we give an operational semantics of adoption in a simple procedural language with pointers to records. We define a "permission" type-system that uses adoption to model both effects and uniqueness. We prove type soundness (well-typed programs don't go wrong) and state separation (separately-typed statements cannot access the same state). Then we show how high-level effects and uniqueness annotations can be expressed in the type-system. The distinction between read and write effects is ignored in the body of this paper.
Region-based shape analysis with tracked locations
Authors: Hackett Brian , Rugina Radu
Published: November 2005

This paper proposes a novel approach to shape analysis: using local reasoning about individual heap locations instead of global reasoning about entire heap abstractions. We present an inter-procedural shape analysis algorithm for languages with destructive updates. The key feature is a novel memory abstraction that differs from traditional abstractions in two ways. First, we build the shape abstraction and analysis on top of a pointer analysis. Second, we decompose the shape abstraction into a set of independent configurations, each of which characterizes one single heap location. Our approach: 1) leads to simpler algorithm specifications, because of local reasoning about the single location; 2) leads to efficient algorithms, because of the smaller granularity of the abstraction; and 3) makes it easier to develop context-sensitive, demand-driven, and incremental shape analyses.We also show that the analysis can be used to enable the static detection of memory errors in programs with explicit deallocation. We have built a prototype tool that detects memory leaks and accesses through dangling pointers in C programs. The experiments indicate that the analysis is sufficiently precise to detect errors with low false positive rates; and is sufficiently lightweight to scale to larger programs. For a set of three popular C programs, the tool has analyzed about 70K lines of code in less than 2 minutes and has produced 97 warnings, 38 of which were actual errors.
Scalable error detection using boolean satisfiability
Authors: Xie Yichen , Aiken Alex
Published: November 2005

We describe a software error-detection tool that exploits recent advances in boolean satisfiability (SAT) solvers. Our analysis is path sensitive, precise down to the bit level, and models pointers and heap data. Our approach is also highly scalable, which we achieve using two techniques. First, for each program function, several optimizations compress the size of the boolean formulas that model the control- and data-flow and the heap locations accessed by a function. Second, summaries in the spirit of type signatures are computed for each function, allowing inter-procedural analysis without a dramatic increase in the size of the boolean constraints to be solved.We demonstrate the effectiveness of our approach by constructing a lock interface inference and checking tool. In an interprocedural analysis of more than 23,000 lock related functions in the latest Linux kernel, the checker generated 300 warnings, of which 179 were unique locking errors, a false positive rate of only 40%.
Notes on notes on postmodern programming
Authors: Noble James , Biddle Robert
Published: November 2005

These notes have the status of letters written to ourselves: we wrote them down because, without doing so, we found ourselves making up new arguments over and over again. So began the abstract of our earlier paper
Notes on Postmodern Programming.
We now revisit the issue of postmodern programming, and attempt to address some of the questions raised by our exposition. To illustrate the nature of postmodernism we do not do this directly, but instead present a series of snapshots, parodies, and imagined conversations that we hope will help. What do you think of the abstract so far? Self-reference and a irreverent approach are part of this topic, so it's important to chill out and let things flow. We claim that computer science and software design grew up amid the unquestioned landscape of modernism, and that too often we cling to the otherwise ungrounded values, even as modernism itself is ever more compromised.
Looking for love (in all the wrong places)
Authors: West David
Published: November 2005

Onward! Seeks future directions. The Feyerabend project seeks to redefine computing. Thoroughly disillusioned with traditional and contemporary practices, a significant number are looking for a software development profession that we can love. If a person has a history of repetitive (only the names change) unsuccessful relationships they are advised to look at themselves in order to discover the roots of the problem that leads to them making the same mistaken choices over and over again. The same advice can be given to our profession -- look inward to discover the true source of our problems. This paper introduces five factors that arise from reflective examination of computing and software development.
Example centric programming
Authors: Edwards Jonathan
Published: November 2005

Programmers tend to understand programs by thinking of concrete examples.
Example Centric Programming
seeks to add IDE support for examples throughout the process of programming. Instead of programmers interpreting examples in their head, the examples are written down and the IDE interprets them automatically. Advanced UI techniques are used to present the results closely integrated with the code. Traditionally distinct programming tools (the editor, Read-Eval-Print-Loop, debugger, and test runner) are unified into a single tool that might be called an
example-enlightened
editor. This is expected to benefit a wide spectrum of programming activities, for both novice and experienced programmers. Some novel methods for testing and development are made possible. In the longer term, example centrism has implications for the design of future programming languages. A prototype has been implemented for Java in Eclipse.
Calculator problem and the design recipe
Authors: Proulx Viera K. , Cashorali Tanya
Published: November 2005

This paper presents an alternative --- and what we believe
a superior
--- approach to designing a solution to the calculator problem due to Alphonce [1]. While Alphonce presents a fictitious one-act play between professors, this paper consists of a narrative explanation of the Java code written by this paper's coauthor, - a student who just completed the freshman year.The purpose of this paper is to illustrate the use of the DESIGN RECIPE pedagogy and the idea of focusing on the design of the structure of data, the classes, and class hierarchies, rather than the design of program actions (the algorithmics) as the core idea for program design. By contrasting the pedagogical approach and the final outcome with the "traditional" objects-first approach, we illustrate the advantages of our curriculum that teaches the students how to think about program design in a truly object-oriented style.
Tired by Forth?
Authors: Frenger Paul
Published: November 2005

You're traveling through another dimension, a dimension not only of sight and sound but of mind; a journey into a wondrous land whose boundaries are that of the imagination. Next stop: the Forth Zone [1].
Extracting grammar from programs
Authors: Črepinšek Matej , Mernik Marjan , Javed Faizan , Bryant Barrett R. , Sprague Alan
Published: November 2005

The paper discusses context-free grammar (CFG) inference using genetic-programming with application to inducing grammars from programs written in simple domain-specific languages. Grammar-specific heuristic operators and non-random construction of the initial population are proposed to achieve this task. Suitability of the approach is shown by small examples where the underlying CFG's are successfully inferred.
Scalable statistical bug isolation
Authors: Liblit Ben , Naik Mayur , Zheng Alice X. , Aiken Alex , Jordan Michael I.
Published: November 2005

We present a statistical debugging algorithm that isolates bugs in programs containing multiple undiagnosed bugs. Earlier statistical algorithms that focus solely on identifying predictors that correlate with program failure perform poorly when there are multiple bugs. Our new technique separates the effects of different bugs and identifies predictors that are associated with individual bugs. These predictors reveal both the circumstances under which bugs occur as well as the frequencies of failure modes, making it easier to prioritize debugging efforts. Our algorithm is validated using several case studies, including examples in which the algorithm identified previously unknown, significant crashing bugs in widely used systems.