Julia L. Lawall

Institut national de recherche en informatique et en automatique

Author Statistics

Papers

Citation

H-Index

i-10 index

Research Trends

Author Order

Document Type

Co-Authors

Gilles Muller

Institut national de recherche en informatique et en automatique

Gilles Muller

San Jose State University

René Rydhof Hansen

Aalborg University

Olivier Danvy

National University of Singapore

Nicolas Palix

Université Grenoble Alpes

Charles Consel

Université de Bordeaux

Yoann Padioleau

Meta (United States)

Laurent Réveillère

Laboratoire Bordelais de Recherche en Informatique

Anne-Françoise Le Meur

Laboratoire d'Informatique Fondamentale de Lille

Harry G. Mairson

Brandeis University

Cooperative Institutions

Institut national de recherche en informatique et en automatique

Centre National de la Recherche Scientifique

University of Copenhagen

Laboratoire Bordelais de Recherche en Informatique

Institut de Recherche en Informatique et Systèmes Aléatoires

École Nationale Supérieure des Mines de Paris

Université de Bordeaux

Institut Polytechnique de Bordeaux

Tsinghua University

Université de Rennes

Author Statistics

Papers

Citation

H-Index

i-10 index

Research Field

SmPL: A Domain-Specific Language for Specifying Collateral Evolutions in Linux Device Drivers

Electronic Notes in Theoretical Computer Science (2006)

Yoann Padioleau Julia L. Lawall Gilles Muller

Collateral evolutions are a pervasive problem in large-scale software development. Such evolutions occur when an evolution that affects the interface of a generic library entails modifications, i.e., collateral evolutions, in all library clients. Performing these collateral evolutions requires identifying the affected files and modifying all of the code fragments in these files that in some way depend on the changed interface. We have studied the collateral evolution problem in the context of Linux device drivers. Currently, collateral evolutions in Linux are mostly done manually using a text editor, possibly with the help of tools such as grep. The large number of Linux drivers, however, implies that this approach is time-consuming and unreliable, leading to subtle errors when modifications are not done consistently. In this paper, we propose a transformation language, SmPL, to specify collateral evolutions. Because Linux programmers are accustomed to exchanging, reading, and manipulating program modifications in terms of patches, we build our language around the idea and syntax of a patch, extending patches to semantic patches.

Domain-specific language

Code (set theory)

Interface (matter)

10.1016/j.entcs.2006.07.022

Cite

Citations (23)

On global dynamics of optimal graph reduction

Julia L. Lawall Harry G. Mairson

Optimal graph reduction technology for the λ-calculus, as developed by Lamping, with modifications by Asperti, Gonthier, Abadl, and Lévy, has a well-understood local dynamics based on a standard menagerie of reduction rules, as well as a global context semantics based on Girard's geometry of interaction. However, the global dynamics of graph reduction has not been subject to careful investigation. In particular, graphs lose their structural resemblance to λ-terms after only a few graph reduction steps, and little is known about graph reduction strategies that maintain efficiency or structure. While the context semantics provides global information about the computation, its use as part of a reduction strategy seems computationally infeasible. We propose a tractable graph reduction strategy that preserves computationally relevant global structure, and allows us to efficiently bound the computational resources needed to implement optimal reduction.A simple canonical representation for graphs is introduced that we call fan-normal form. This normal form allows us to reduce graphs based on efficient identification of β-redexes, rather than being guided by lower-level search for interacting nodes. In addition and perhaps more important, the fan-normal form facilitates a complexity analysis of graph reductions, showing that the number of fan interactions is essentially bounded by a polynomial in the number of unique Lévy labels generated during a labelled reduction. This global analysis of the finitary dynamics of optimal reduction is the first demonstration that a reasonable implementation-independent cost model for the λ-calculus is in fact realized by Lamping's abstract algorithm. It remains to be seen whether similar claims can be made about so-called bookkeeping for fan interactions.

Graph reduction

Finitary

10.1145/258948.258966

Cite

Citations (11)

On global dynamics of optimal graph reduction

ACM SIGPLAN Notices (1997)

Julia L. Lawall Harry G. Mairson

Optimal graph reduction technology for the λ-calculus, as developed by Lamping, with modifications by Asperti, Gonthier, Abadl, and Lévy, has a well-understood local dynamics based on a standard menagerie of reduction rules, as well as a global context semantics based on Girard's geometry of interaction. However, the global dynamics of graph reduction has not been subject to careful investigation. In particular, graphs lose their structural resemblance to λ-terms after only a few graph reduction steps, and little is known about graph reduction strategies that maintain efficiency or structure. While the context semantics provides global information about the computation, its use as part of a reduction strategy seems computationally infeasible. We propose a tractable graph reduction strategy that preserves computationally relevant global structure, and allows us to efficiently bound the computational resources needed to implement optimal reduction.A simple canonical representation for graphs is introduced that we call fan-normal form . This normal form allows us to reduce graphs based on efficient identification of β-redexes, rather than being guided by lower-level search for interacting nodes. In addition and perhaps more important, the fan-normal form facilitates a complexity analysis of graph reductions, showing that the number of fan interactions is essentially bounded by a polynomial in the number of unique Lévy labels generated during a labelled reduction. This global analysis of the finitary dynamics of optimal reduction is the first demonstration that a reasonable implementation-independent cost model for the λ-calculus is in fact realized by Lamping's abstract algorithm. It remains to be seen whether similar claims can be made about so-called bookkeeping for fan interactions.

Graph reduction

Finitary

10.1145/258949.258966

Cite

Citations (1)

Continuation-based partial evaluation

Julia L. Lawall Olivier Danvy

Binding-time improvements aim at making partial evaluation (a.k.a. program specialization) yield a better result. They have been achieved so far mostly by hand-transforming the source program. We observe that as they are better understood, these hand-transformations are progressively integrated into partial evaluators, thereby alleviating the need for source-level binding-time improvements.

Continuation

Partial evaluation

10.1145/182409.182483

Cite

Citations (90)

A foundation for flow-based program matching

Julien Brunel Damien Doligez René Rydhof Hansen Julia L. Lawall Gilles Muller

Reasoning about program control-flow paths is an important functionality of a number of recent program matching languages and associated searching and transformation tools. Temporal logic provides a well-defined means of expressing properties of control-flow paths in programs, and indeed an extension of the temporal logic CTL has been applied to the problem of specifying and verifying the transformations commonly performed by optimizing compilers. Nevertheless, in developing the Coccinelle program transformation tool for performing Linux collateral evolutions in systems code, we have found that existing variants of CTL do not adequately support rules that transform subterms other than the ones matching an entire formula. Being able to transform any of the subterms of a matched term seems essential in the domain targeted by Coccinelle.

Control flow

Program transformation

CTL*

Code (set theory)

Data-flow analysis

Domain-specific language

10.1145/1480881.1480897

Cite

Citations (18)

Partial evaluation of pattern matching in strings, revisited

Nordic journal of computing (2001)

Bernd Grobauer Julia L. Lawall

Specialization of a string matcher is a canonical example of partial evaluation. A naive implementation of a string matcher repeatedly matches a pattern against every substring of the data string; this operation should intuitively benefit from specializing the matcher with respect to the pattern. In practice, however, producing an efficient implementation by performing this specialization using standard partial-evaluation techniques requires non-trivial binding-time improvements. Starting with a naive matcher, we thus present a derivation of such a binding-time improved string matcher. We show that specialization with respect to a pattern yields a matcher with code size linear in the length of the pattern and a running time independent of the length of the pattern and linear in the length of the data string. We then consider several variants of matchers that specialize well, amongst them the first such matcher presented in the literature, and we demonstrate how variants can be derived from each other systematically.

Substring

Partial evaluation

Code (set theory)

10.5555/766502.766505

Cite

Citations (18)

Fuzzing Error Handling Code in Device Drivers Based on Software Fault Injection

Zu-Ming Jiang Jia-Ju Bai Julia L. Lawall Shi‐Min Hu

Device drivers remain a main source of runtime failures in operating systems. To detect bugs in device drivers, fuzzing has been commonly used in practice. However, a main limitation of existing fuzzing approaches is that they cannot effectively test error handling code. Indeed, these fuzzing approaches require effective inputs to cover target code, but much error handling code in drivers is triggered by occasional errors (such as insufficient memory and hardware malfunctions) that are not related to inputs. In this paper, based on software fault injection, we propose a new fuzzing approach named FIZZER, to test error handling code in device drivers. At compile time, FIZZER uses static analysis to recommend possible error sites that can trigger error handling code. During driver execution, by analyzing runtime information, it automatically fuzzes error-site sequences for fault injection to improve code coverage. We evaluate FIZZER on 18 device drivers in Linux 4.19, and in total find 22 real bugs. The code coverage is increased by over 15% compared to normal execution without fuzzing.

Fuzz testing

Code coverage

Fault injection

Software bug

Code (set theory)

10.1109/issre.2019.00022

Cite

Citations (13)

Automatic program specialization for Java

ACM Transactions on Programming Languages and Systems (2003)

Ulrik Pagh Schultz Julia L. Lawall Charles Consel

The object-oriented style of programming facilitates program adaptation and enhances program genericness, but at the expense of efficiency. We demonstrate experimentally that state-of-the-art Java compilers fail to compensate for the use of object-oriented abstractions in the implementation of generic programs, and that program specialization can eliminate a significant portion of these overheads. We present an automatic program specializer for Java, illustrate its use through detailed case studies, and demonstrate experimentally that it can significantly reduce program execution time. Although automatic program specialization could be seen as being subsumed by existing optimizing compiler technology, we show that specialization and compiler optimization are in fact complementary.

Programming style

Dynamic compilation

Just-in-time compilation

10.1145/778559.778561

Cite

Citations (112)

Optimality and inefficiency

Julia L. Lawall Harry G. Mairson

We investigate the computational efficiency of the sharing graphs of Lamping [Lam90], Gonthier, Abadi, and Lévy [GAL92], and Asperti [Asp94], designed to effect so-called optimal evaluation, with the goal of reconciling optimality, efficiency, and the clarification of reasonable cost models for the λ-calculus. Do these graphs suggest reasonable cost models for the λ-calculus? If they are optimal, are they efficient?We present a brief survey of these optimal evaluators, identifying their common characteristics, as well as their shared failures. We give a lower bound on the efficiency of sharing graphs by identifying a class of λ-terms that are normalizable in Θ(n) time, and require Θ(n) "fan interactions," but require Ω(2n) bookkeeping steps. For [GAL92], we analyze this anomaly in terms of the dynamic maintenance of deBruijn indices for intermediate terms. We give another lower bound showing that sharing graphs can do Ω(2n) work (via fan interactions) on graphs that have no β-redexes. Finally, we criticize a proposed cost model for λ-calculus given by Frandsen and Sturtivant [FS91], showing by example that the model does not take account of the size of intermediate forms. Our example is a term requiring Θ(2n) steps while having proposed cost Θ(n). We propose some cost models that both reflect this parameter, and simultaneously reconcile key concepts from optimal reduction.

10.1145/232627.232639

Cite

Citations (33)

Higher-Order and Symbolic Computation (2001)

Olivier Danvy Julia L. Lawall

10.1023/a:1012905312544

Cite

Citations (0)