EDBT 2026 Demo / reviewers in the wild / expert
Dawson R. Engler
dblp:e/DREngler
· DBLP profile ↗
61ranked-venue papers
18as first author
0since 2021 · last 2020
—ORCID · none
Domains — the database's venue-derived domains; a paper can count in several
Software engineering, systems software and programming languages · 38 · 14 first-authorSystems, architecture and hardware · 12 · 2 first-authorSecurity and privacy · 9 · 1 first-authorComputer networks · 4 · 1 first-authorTheory of computation · 3 · 2 first-authorArtificial intelligence and machine learning · 1Databases, data management, data science and information retrieval · 1 · 1 first-authorGraphics, computer vision, multimedia, augmented reality and games · 1
Expertise — from the expertise taxonomy: the topics of the expert's papers under the CCF categories. A weight counts papers with recency: 1 for a paper about the topic, 0.3 when the topic is its context, halved every five years.
| Software engineering, system software, and programming languages
49 papers |
Program analysis · 66% Operating systems · 10% Software testing · 7% | |
| Network and information security
8 papers |
Systems and software security · 100% | |
| Computer architecture, parallel and distributed computing, and storage systems
10 papers |
Storage systems · 45% Memory systems · 31% Hardware reliability and fault tolerance · 14% |
Topics — the 30 heaviest of 91, each with the papers that count most for it
| Topic | Weight | Papers | Last | Evidence papers |
|---|---|---|---|---|
Program analysis
static analysis |
1.4 | 14 | 2020 | Sys: A Static/Symbolic Tool for Finding Good Bugs in Good (Browser) Code · USENIX Security Symposium 2020 Finding and Preventing Bugs in JavaScript Bindings · IEEE Symposium on Security and Privacy 2017 How to Build Static Checking Systems Using Orders of Magnitude Less Code · ASPLOS 2016 |
Program analysis
symbolic execution |
1.2 | 6 | 2020 | Sys: A Static/Symbolic Tool for Finding Good Bugs in Good (Browser) Code · USENIX Security Symposium 2020 Under-Constrained Symbolic Execution: Correctness Checking for Real Code · USENIX ATC 2016 Under-Constrained Symbolic Execution: Correctness Checking for Real Code · USENIX Security Symposium 2015 |
Program analysis › symbolic execution
under-constrained symbolic execution |
0.5 | 2 | 2016 | Under-Constrained Symbolic Execution: Correctness Checking for Real Code · USENIX ATC 2016 Under-Constrained Symbolic Execution: Correctness Checking for Real Code · USENIX Security Symposium 2015 |
Program analysis › static analysis
bug detection |
0.4 | 5 | 2016 | How to Build Static Checking Systems Using Orders of Magnitude Less Code · ASPLOS 2016 A Factor Graph Model for Software Bug Finding · IJCAI 2007 Using Redundancies to Find Errors · IEEE Trans. Software Eng. 2003 |
Systems and software security
vulnerability discovery |
0.4 | 6 | 2020 | Sys: A Static/Symbolic Tool for Finding Good Bugs in Good (Browser) Code · USENIX Security Symposium 2020 A System's Hackers Crash Course: Techniques that Find Lots of Bugs in Real (Storage) System Code · FAST 2007 Automatically Generating Malicious Disks using Symbolic Execution · S&P 2006 |
Software testing
test generation |
0.3 | 3 | 2013 | Redundant State Detection for Dynamic Symbolic Execution · USENIX ATC 2013 KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs · OSDI 2008 Under-constrained execution: making automatic code destruction easy and scalable · ISSTA 2007 |
Systems and software security
memory safety |
0.3 | 1 | 2017 | Finding and Preventing Bugs in JavaScript Bindings · IEEE Symposium on Security and Privacy 2017 |
Operating systems › resource management › memory management › virtual memory
address translation |
0.2 | 1 | 2014 | symMMU: symbolically executed runtime libraries for symbolic memory access · ASE 2014 |
Program analysis › symbolic execution
dynamic symbolic execution |
0.2 | 1 | 2013 | Redundant State Detection for Dynamic Symbolic Execution · USENIX ATC 2013 |
Program verification
model checking |
0.2 | 4 | 2006 | Using model checking to find serious file system errors · ACM Trans. Comput. Syst. 2006 Using Model Checking to Find Serious File System Errors (Awarded Best Paper!) · OSDI 2004 A simple method for extracting models for protocol code · ISCA 2001 |
Systems and software security › vulnerability discovery
bug finding |
0.1 | 2 | 2007 | A System's Hackers Crash Course: Techniques that Find Lots of Bugs in Real (Storage) System Code · FAST 2007 EXE: automatically generating inputs of death · CCS 2006 |
Software maintenance and evolution › software ecosystems
dependency management |
0.1 | 1 | 2011 | Using automatic persistent memoization to facilitate data analysis scripting · ISSTA 2011 |
Program verification
equivalence checking |
0.1 | 1 | 2011 | Practical, Low-Effort Equivalence Verification of Real Code · CAV 2011 |
Compilers and program optimization
memoization |
0.1 | 1 | 2011 | Using automatic persistent memoization to facilitate data analysis scripting · ISSTA 2011 |
Storage systems › storage reliability
file system reliability |
0.1 | 2 | 2006 | Using model checking to find serious file system errors · ACM Trans. Comput. Syst. 2006 Using Model Checking to Find Serious File System Errors (Awarded Best Paper!) · OSDI 2004 |
Automated reasoning and model checking
model checking |
0.1 | 2 | 2008 | Lessons in the Weird and Unexpected: Some Experiences from Checking Large Real Systems · FM 2008 From Uncertainty to Belief: Inferring the Specification Within · OSDI 2006 |
Systems and software security
exploitation |
0.1 | 1 | 2017 | Finding and Preventing Bugs in JavaScript Bindings · IEEE Symposium on Security and Privacy 2017 |
Operating systems › extensible operating systems
exokernel |
0.1 | 4 | 2002 | Fast and flexible application-level networking on exokernel systems · ACM Trans. Comput. Syst. 2002 Application Performance and Flexibility on Exokernel Systems · SOSP 1997 Exokernel: An Operating System Architecture for Application-Level Resource Management · SOSP 1995 |
Program analysis › code quality analysis
redundancy detection |
0.1 | 2 | 2003 | Using Redundancies to Find Errors · IEEE Trans. Software Eng. 2003 Using redundancies to find errors · SIGSOFT FSE 2002 |
Programming languages and type systems
language specification |
0.1 | 1 | 2016 | How to Build Static Checking Systems Using Orders of Magnitude Less Code · ASPLOS 2016 |
Systems and software security › vulnerability discovery
symbolic execution |
0.1 | 1 | 2006 | EXE: automatically generating inputs of death · CCS 2006 |
Program analysis
specification mining |
0.1 | 1 | 2006 | From Uncertainty to Belief: Inferring the Specification Within · OSDI 2006 |
Hardware reliability and fault tolerance
error detection |
0.1 | 1 | 2006 | EXPLODE: A Lightweight, General System for Finding Serious Storage System Errors · OSDI 2006 |
Storage systems
file systems |
0.1 | 1 | 2006 | Using model checking to find serious file system errors · ACM Trans. Comput. Syst. 2006 |
Memory systems › memory management
memory management unit |
0.1 | 1 | 2014 | symMMU: symbolically executed runtime libraries for symbolic memory access · ASE 2014 |
Network management and operations › network verification
model checking |
0.0 | 1 | 2004 | Model Checking Large Network Protocol Implementations · NSDI 2004 |
Network management and operations
protocol verification |
0.0 | 1 | 2004 | Model Checking Large Network Protocol Implementations · NSDI 2004 |
Program analysis › static analysis › bug detection
false positive reduction |
0.0 | 1 | 2004 | Correlation exploitation in error ranking · SIGSOFT FSE 2004 |
Operating systems › resource management › storage management › file systems
file system bug detection |
0.0 | 1 | 2004 | Using Model Checking to Find Serious File System Errors (Awarded Best Paper!) · OSDI 2004 |
Systems and software security › security verification
security property verification |
0.0 | 1 | 2003 | MECA: an extensible, expressive system and language for statically checking security properties · CCS 2003 |
Methods — techniques the papers use, named apart from their topics
symbolic execution · 1.0static checker · 0.6API design · 0.6model checking · 0.5theorem proving · 0.4constraint solving · 0.4static checking · 0.3fuzzing · 0.1memoization · 0.1equivalence checking · 0.1dependency tracking · 0.1state space reduction · 0.1error detection · 0.1dynamic symbolic execution · 0.1microbenchmarking · 0.1symbolic analysis · 0.0statistical code analysis · 0.0path-sensitive analysis · 0.0
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2020 | Sys: A Static/Symbolic Tool for Finding Good Bugs in Good (Browser) Code
Fraser Brown, Deian Stefan, Dawson R. Engler |
USENIX Security Symposium | 3 |
| 2017 | Finding and Preventing Bugs in JavaScript BindingsabstractJavaScript, like many high-level languages, relies on runtime systemswritten in low-level C and C++. For example, the Node.js runtime systemgives JavaScript code access to the underlying filesystem, networking, and I/O by implementing utility functions in C++. Since C++'s typesystem, memory model, and execution model differ significantly fromJavaScript's, JavaScript code must call these runtime functions viaintermediate binding layer code that translates type, state, and failure between the two languages. Unfortunately, binding code isboth hard to avoid and hard to get right. This paper describes several types of exploitable errors that bindingcode creates, and develops both a suite of easily-to-build static checkersto detect such errors and a backwards-compatible, low-overhead API toprevent them. We show that binding flaws are a serious security problem byusing our checkers to craft 81 proof-of-concept exploits forsecurity flaws in the binding layers of the Node.js and Chrome, runtimesystems that support hundreds of millions of users. As one practical measure of binding bug severity, we were awarded $6,000 in bounties for just two Chrome bug reports. Fraser Brown, Shravan Narayan, Riad S. Wahby, Dawson R. Engler, Ranjit Jhala, Deian Stefan |
IEEE Symposium on Security and Privacy | 4 |
| 2016 | How to Build Static Checking Systems Using Orders of Magnitude Less CodeabstractModern static bug finding tools are complex. They typically consist of hundreds of thousands of lines of code, and most of them are wedded to one language (or even one compiler). This complexity makes the systems hard to understand, hard to debug, and hard to retarget to new languages, thereby dramatically limiting their scope. This paper reduces checking system complexity by addressing a fundamental assumption, the assumption that checkers must depend on a full-blown language specification and compiler front end. Instead, our program checkers are based on drastically incomplete language grammars ("micro-grammars") that describe only portions of a language relevant to a checker. As a result, our implementation is tiny-roughly 2500 lines of code, about two orders of magnitude smaller than a typical system. We hope that this dramatic increase in simplicity will allow people to use more checkers on more systems in more languages. Fraser Brown, Andres Nötzli, Dawson R. Engler |
ASPLOS | 3 |
| 2016 | Under-Constrained Symbolic Execution: Correctness Checking for Real Code
David A. Ramos, Dawson R. Engler |
USENIX ATC | 2 |
| 2015 | Under-Constrained Symbolic Execution: Correctness Checking for Real Code
David A. Ramos, Dawson R. Engler |
USENIX Security Symposium | 2 |
| 2014 | symMMU: symbolically executed runtime libraries for symbolic memory accessabstractSymbolic execution calls for specialized address translation. Unlike a pointer on a traditional machine model, which corresponds to a single address, a symbolic pointer may represent multiple feasible addresses. A symbolic pointer dereference manipulates symbolic state, potentially submitting many theorem prover requests in the process. Hence, design and management of symbolic accesses critically affects symbolic executor performance, complexity, and completeness. Anthony Romano, Dawson R. Engler |
ASE | 2 |
| 2013 | Expression Reduction from Programs in a Symbolic Binary Executor
Anthony Romano, Dawson R. Engler |
SPIN | 2 |
| 2013 | Redundant State Detection for Dynamic Symbolic Execution
Suhabe Bugrara, Dawson R. Engler |
USENIX ATC | 2 |
| 2011 | Practical, Low-Effort Equivalence Verification of Real Code
David A. Ramos, Dawson R. Engler |
CAV | 2 |
| 2011 | Using automatic persistent memoization to facilitate data analysis scriptingabstractProgrammers across a wide range of disciplines (e.g., bioinformatics, neuroscience, econometrics, finance, data mining, information retrieval, machine learning) write scripts to parse, transform, process, and extract insights from data. To speed up iteration times, they split their analyses into stages and write extra code to save the intermediate results of each stage to files so that those results do not have to be re-computed in every subsequent run. As they explore and refine hypotheses, their scripts often create and process lots of intermediate data files. They need to properly manage the myriad of dependencies between their code and data files, or else their analyses will produce incorrect results. Philip J. Guo, Dawson R. Engler |
ISSTA | 2 |
| 2011 | CDE: Using System Call Interposition to Automatically Create Portable Software Packages
Philip J. Guo, Dawson R. Engler |
USENIX ATC | 2 |
| 2009 | Linux Kernel Developer Responses to Static Analysis Bug Reports
Philip J. Guo, Dawson R. Engler |
USENIX ATC | 2 |
| 2008 | Lessons in the Weird and Unexpected: Some Experiences from Checking Large Real Systems
Dawson R. Engler |
FM | 1 |
| 2008 | KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs
Cristian Cadar, Daniel Dunbar, Dawson R. Engler |
OSDI | 3 |
| 2008 | RWset: Attacking Path Explosion in Constraint-Based Test Generation
Peter Boonstoppel, Cristian Cadar, Dawson R. Engler |
TACAS | 3 |
| 2008 | EXE: Automatically Generating Inputs of DeathabstractThis article presents EXE, an effective bug-finding tool that automatically generates inputs that crash real code. Instead of running code on manually or randomly constructed input, EXE runs it on symbolic input initially allowed to be anything. As checked code runs, EXE tracks the constraints on each symbolic (i.e., input-derived) memory location. If a statement uses a symbolic value, EXE does not run it, but instead adds it as an input-constraint; all other statements run as usual. If code conditionally checks a symbolic expression, EXE forks execution, constraining the expression to be true on the true branch and false on the other. Because EXE reasons about all possible values on a path, it has much more power than a traditional runtime tool: (1) it can force execution down any feasible program path and (2) at dangerous operations (e.g., a pointer dereference), it detects if the current path constraints allow any value that causes a bug. When a path terminates or hits a bug, EXE automatically generates a test case by solving the current path constraints to find concrete values using its own co-designed constraint solver, STP. Because EXE’s constraints have no approximations, feeding this concrete input to an uninstrumented version of the checked code will cause it to follow the same path and hit the same bug (assuming deterministic code). EXE works well on real code, finding bugs along with inputs that trigger them in: the BSD and Linux packet filter implementations, the dhcpd DHCP server, the pcre regular expression library, and three Linux file systems. Cristian Cadar, Vijay Ganesh 0001, Peter M. Pawlowski, David L. Dill, Dawson R. Engler |
ACM Trans. Inf. Syst. Secur. | 5 |
| 2007 | A System's Hackers Crash Course: Techniques that Find Lots of Bugs in Real (Storage) System Code
Dawson R. Engler |
FAST | 1 |
| 2007 | A Factor Graph Model for Software Bug Finding
Ted Kremenek, Andrew Y. Ng, Dawson R. Engler |
IJCAI | 3 |
| 2007 | Under-constrained execution: making automatic code destruction easy and scalableabstractArticle Share on Under-constrained execution: making automatic code destruction easy and scalable Authors: Dawson Engler Stanford University Stanford UniversityView Profile , Daniel Dunbar Stanford University Stanford UniversityView Profile Authors Info & Claims ISSTA '07: Proceedings of the 2007 international symposium on Software testing and analysisJuly 2007 Pages 1–4https://doi.org/10.1145/1273463.1273464Online:09 July 2007Publication History 43citation404DownloadsMetricsTotal Citations43Total Downloads404Last 12 Months27Last 6 weeks4 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteGet Access Dawson R. Engler, Daniel Dunbar |
ISSTA | 1 |
| 2006 | EXE: automatically generating inputs of deathabstractThis paper presents EXE, an effective bug-finding tool that automatically generates inputs that crash real code. Instead of running code on manually or randomly constructed input, EXE runs it on symbolic input initially allowed to be "anything." As checked code runs, EXE tracks the constraints on each symbolic (i.e., input-derived) memory location. If a statement uses a symbolic value, EXE does not run it, but instead adds it as an input-constraint; all other statements run as usual. If code conditionally checks a symbolic expression, EXE forks execution, constraining the expression to be true on the true branch and false on the other. Because EXE reasons about all possible values on a path, it has much more power than a traditional runtime tool: (1) it can force execution down any feasible program path and (2) at dangerous operations (e.g., a pointer dereference), it detects if the current path constraints allow any value that causes a bug.When a path terminates or hits a bug, EXE automatically generates a test case by solving the current path constraints to find concrete values using its own co-designed constraint solver, STP. Because EXE's constraints have no approximations, feeding this concrete input to an uninstrumented version of the checked code will cause it to follow the same path and hit the same bug (assuming deterministic code).EXE works well on real code, finding bugs along with inputs that trigger them in: the BSD and Linux packet filter implementations, the udhcpd DHCP server, the pcre regular expression library, and three Linux file systems. Cristian Cadar, Vijay Ganesh 0001, Peter M. Pawlowski, David L. Dill, Dawson R. Engler |
CCS | 5 |
| 2006 | From Uncertainty to Belief: Inferring the Specification Within
Ted Kremenek, Paul Twohey, Godmar Back, Andrew Y. Ng, Dawson R. Engler |
OSDI | 5 |
| 2006 | EXPLODE: A Lightweight, General System for Finding Serious Storage System Errors
Can Sar, Dawson R. Engler |
OSDI | 3 |
| 2006 | Automatically Generating Malicious Disks using Symbolic ExecutionabstractMany current systems allow data produced by potentially malicious sources to be mounted as a file system. File system code must check this data for dangerous values or invariant violations before using it. Because file system code typically runs inside the operating system kernel, even a single unchecked value can crash the machine or lead to an exploit. Unfortunately, validating file system images is complex: they form DAGs with complex dependency relationships across massive amounts of data bound together with intricate, undocumented assumptions. This paper shows how to automatically find bugs in such code using symbolic execution. Rather than running the code on manually-constructed concrete input, we instead run it on symbolic input that is initially allowed to be "anything." As the code runs, it observes (tests) this input and thus constrains its possible values. We generate test cases by solving these constraints for concrete values. The approach works well in practice: we checked the disk mounting code of three widely-used Linux file systems: ext2, ext3, and JFS and found bugs in all of them where malicious data could either cause a kernel panic or form the basis of a buffer overflow attack. Can Sar, Paul Twohey, Cristian Cadar, Dawson R. Engler |
S&P | 5 |
| 2006 | Using model checking to find serious file system errorsabstractThis article shows how to use model checking to find serious errors in file systems. Model checking is a formal verification technique tuned for finding corner-case errors by comprehensively exploring the state spaces defined by a system. File systems have two dynamics that make them attractive for such an approach. First, their errors are some of the most serious, since they can destroy persistent data and lead to unrecoverable corruption. Second, traditional testing needs an impractical, exponential number of test cases to check that the system will recover if it crashes at any point during execution. Model checking employs a variety of state-reducing techniques that allow it to explore such vast state spaces efficiently.We built a system, FiSC, for model checking file systems. We applied it to four widely-used, heavily-tested file systems: ext3, JFS, ReiserFS and XFS. We found serious bugs in all of them, 33 in total. Most have led to patches within a day of diagnosis. For each file system, FiSC found demonstrable events leading to the unrecoverable destruction of metadata and entire directories, including the file system root directory “/”. Paul Twohey, Dawson R. Engler, Madan Musuvathi |
ACM Trans. Comput. Syst. | 3 |
| 2005 | Static Analysis Versus Model Checking for Bug Finding
Dawson R. Engler |
CONCUR | 1 |
| 2004 | Model Checking Large Network Protocol Implementations
Madan Musuvathi, Dawson R. Engler |
NSDI | 2 |
| 2004 | Using Model Checking to Find Serious File System Errors (Awarded Best Paper!)
Paul Twohey, Dawson R. Engler, Madan Musuvathi |
OSDI | 3 |
| 2004 | Correlation exploitation in error rankingabstractStatic program checking tools can find many serious bugs in software, but due to analysis limitations they also frequently emit false error reports. Such false positives can easily render the error checker useless by hiding real errors amidst the false. Effective error report ranking schemes mitigate the problem of false positives by suppressing them during the report inspection process [17, 19, 20]. In this way, ranking techniques provide a complementary method to increasing the precision of the analysis results of a checking tool. A weakness of previous ranking schemes, however, is that they produce static rankings that do not adapt as reports are inspected, ignoring useful correlations amongst reports. This paper addresses this weakness with two main contributions. First, we observe that both bugs and false positives frequently cluster by code locality. We analyze clustering behavior in historical bug data from two large systems and show how clustering can be exploited to greatly improve error report ranking. Second, we present a general probabilistic technique for error ranking that (1) exploits correlation behavior amongst reports and (2) incorporates user feedback into the ranking process. In our results we observe a factor of 2-8 improvement over randomized ranking for error reports emitted by both intra-procedural and inter-procedural analysis tools. Ted Kremenek, Ken Ashcraft, Dawson R. Engler |
SIGSOFT FSE | 4 |
| 2004 | Static Analysis versus Software Model Checking for Bug Finding
Dawson R. Engler, Madan Musuvathi |
VMCAI | 1 |
| 2003 | MECA: an extensible, expressive system and language for statically checking security propertiesabstractThis paper describes a system and annotation language, MECA, for checking security rules. MECA is expressive and designed for checking real systems. It provides a variety of practical constructs to effectively annotate large bodies of code. For example, it allows programmers to write programmatic annotators that automatically annotate large bodies of source code. As another example, it lets programmers use general predicates to determine if an annotation is applied; we have used this ability to easily handle kernel backdoors and other false-positive inducing constructs. Once code is annotated, MECA propagates annotations aggressively, allowing a single manual annotation to derive many additional annotations (e.g., over one hundred in our experiments) freeing programmers from the heavy manual effort required by most past systems.MECA is effective. Our most thorough case study was a user-pointer checker that used 75 annotations to check thousands of declarations in millions of lines of code in the Linux system. It found over forty errors, many of which were serious, while only having eight false positives. Ted Kremenek, Yichen Xie 0001, Dawson R. Engler |
CCS | 4 |
| 2003 | Z-Ranking: Using Statistical Analysis to Counter the Impact of Static Analysis Approximations
Ted Kremenek, Dawson R. Engler |
SAS | 2 |
| 2003 | ARCHER: using symbolic, path-sensitive analysis to detect memory access errorsabstractMemory corruption errors lead to non-deterministic, elusive crashes. This paper describes ARCHER (ARray CHeckER) a static, effective memory access checker. ARCHER uses path-sensitive, interprocedural symbolic analysis to bound the values of both variables and memory sizes. It evaluates known values using a constraint solver at every array access, pointer dereference, or call to a function that expects a size parameter. Accesses that violate constraints are flagged as errors. Those that are exploitable by malicious attackers are marked as security holes.Memory corruption errors lead to non-deterministic, elusive crashes. This paper describes ARCHER (ARray CHeckER) a static, effective memory access checker. ARCHER uses path-sensitive, interprocedural symbolic analysis to bound the values of both variables and memory sizes. It evaluates known values using a constraint solver at every array access, pointer dereference, or call to a function that expects a size parameter. Accesses that violate constraints are flagged as errors. Those that are exploitable by malicious attackers are marked as security holes.We carefully designed ARCHER to work well on large bodies of source code. It requires no annotations to use (though it can use them). Its solver has been built to be powerful in the ways that real code requires, while backing off on the places that were irrelevant. Selective power allows it to gain efficiency while avoiding classes of false positives that arise when a complex analysis interacts badly with statically undecidable program properties. ARCHER uses statistical code analysis to automatically infer the set of functions that it should track --- this inference serves as a robust guard against omissions, especially in large systems which can have hundreds of such functions.In practice ARCHER is effective: it finds many errors; its analysis scales to systems of millions of lines of code and the average false positive rate of our results is below 35%. We have run ARCHER over several large open source software projects --- such as Linux, OpenBSD, Sendmail, and PostgreSQL --- and have found errors in all of them (118 in the case of Linux, including 21 security holes). Yichen Xie 0001, Andy Chou, Dawson R. Engler |
ESEC / SIGSOFT FSE | 3 |
| 2003 | RacerX: effective, static detection of race conditions and deadlocksabstractThis paper describes RacerX, a static tool that uses flow-sensitive, interprocedural analysis to detect both race conditions and deadlocks. It is explicitly designed to find errors in large, complex multithreaded systems. It aggressively infers checking information such as which locks protect which operations, which code contexts are multithreaded, and which shared accesses are dangerous. It tracks a set of code features which it uses to sort errors both from most to least severe. It uses novel techniques to counter the impact of analysis mistakes. The tool is fast, requiring between 2-14 minutes to analyze a 1.8 million line system. We have applied it to Linux, FreeBSD, and a large commercial code base, finding serious errors in all of them. RacerX is a static tool that uses flow-sensitive, interprocedural analysis to detect both race conditions and deadlocks. It uses novel strategies to infer checking information such as which locks protect which operations, which code contexts are multithreaded, and which shared accesses are dangerous. We applied it to FreeBSD, Linux and a large commercial code base and found serious errors in all of them. Dawson R. Engler, Ken Ashcraft |
SOSP | 1 |
| 2003 | Using Redundancies to Find ErrorsabstractProgrammers generally attempt to perform useful work. If they performed an action, it was because they believed it served some purpose. Redundant operations violate this belief. However, in the past, redundant operations have been typically regarded as minor cosmetic problems rather than serious errors. This paper demonstrates that, in fact, many redundancies are as serious as traditional hard errors (such as race conditions or null pointer dereferences). We experimentally test this idea by writing and applying five redundancy checkers to a number of large open source projects, finding many errors. We then show that, even when redundancies are harmless, they strongly correlate with the presence of traditional hard errors. Finally, we show how flagging redundant operations gives a way to detect mistakes and omissions in specifications. For example, a locking specification that binds shared variables to their protecting locks can use redundancies to detect missing bindings by flagging critical sections that include no shared state. Yichen Xie 0001, Dawson R. Engler |
IEEE Trans. Software Eng. | 2 |
| 2002 | CMC: A Pragmatic Approach to Model Checking Real Code
Madan Musuvathi, David Y. W. Park, Andy Chou, Dawson R. Engler, David L. Dill |
OSDI | 4 |
| 2002 | How to write system-specific, static checkers in metalabstractThis paper gives an overview of the metal language, which we have designed to make it easy to construct system-specific, static analyses. We call these analyses extensions because they act as the input to a generic analysis engine that runs the static analysis over a given source base. We also interchangeably refer to them as checkers because they check that a user-specified property holds in the source base and report any violations of that property. Note that checkers may not detect all violations of a specified property. Their goal is to find as many violations as possible with a minimum of false positives Benjamin Chelf, Dawson R. Engler, Seth Hallem |
PASTE | 2 |
| 2002 | A System and Language for Building System-Specific, Static AnalysesabstractThis paper presents a novel approach to bug-finding analysis and an implementation of that approach. Our goal is to find as many serious bugs as possible. To do so, we designed a flexible, easy-to-use extension language for specifying analyses and an efficent algorithm for executing these extensions. The language, metal, allows the users of our system to specify a broad class of analyses in terms that resemble the intuitive description of the rules that they check. The system, xgcc, executes these analyses efficiently using a context-sensitive, interprocedural analysis. Our prior work has shown that the approach described in this paper is effective: it has successfully found thousands of bugs in real systems code. This paper describes the underlying system used to achieve these results. We believe that our system is an effective framework for deploying new bug-finding analyses quickly and easily. Seth Hallem, Benjamin Chelf, Yichen Xie 0001, Dawson R. Engler |
PLDI | 4 |
| 2002 | Cool security trendsabstractTrent Jarger will discuss ongoing work in the verification of authorization hook placement in Linux. The idea is that we can develop tools to check that all security-sensitive kernel operations can be mediated properly. Dawson Engler will discuss ongoing work in static checking for kernal and driver bugs, including security bugs, based on his meta-complier xgcc. The idea is that reguirements can be expressed in a high-level language that the xgcc can check.David Wagner will discuss using formal modeling to guide the identifcation of security bugs. The idea is that a formal model generated fromteh source code can be more easily analyzed to find bugs.Cynthia Irvine will discuss security quality-of-service. The idea is that the cost of security in terms of performance and resource usage can be compared with the security benefits in such a way that decisions about security improvements can be made. Dawson R. Engler, Cynthia E. Irvine, Trent Jaeger, David A. Wagner 0001 |
SACMAT | 1 |
| 2002 | Using redundancies to find errorsabstractThis paper explores the idea that redundant operations, like type errors, commonly flag correctness errors. We experimentally test this idea by writing and applying four redundancy checkers to the Linux operating system, finding many errors. We then use these errors to demonstrate that redundancies, even when harmless, strongly correlate with the presence of traditional hard errors (e.g., null pointer dereferences, unreleased locks). Finally we show that how flagging redundant operations gives a way to make specifications "fail stop" bydetecting dangerous omissions. Yichen Xie 0001, Dawson R. Engler |
SIGSOFT FSE | 2 |
| 2002 | Using Programmer-Written Compiler Extensions to Catch Security HolesabstractThis paper shows how system-specific static analysis can find security errors that violate rules such as "integers from untrusted sources must be sanitized before use" and "do not dereference user-supplied pointers." In our approach, programmers write system-specific extensions that are linked into the compiler and check their code for errors. We demonstrate the approach's effectiveness by using it to find over 100 security errors in Linux and OpenBSD, over 50 of which have led to kernel patches. An unusual feature of our approach is the use of methods to automatically detect when we miss code actions that should be checked. Ken Ashcraft, Dawson R. Engler |
S&P | 2 |
| 2002 | Fast and flexible application-level networking on exokernel systemsabstractApplication-level networking is a promising software organization for improving performance and functionality for important network services. The Xok/ExOS exokernel system includes application-level support for standard network services, while at the same time allowing application writers to specialize networking services. This paper describes how Xok/ExOS's kernel mechanisms and library operating system organization achieve this flexibility, and retrospectively shares our experiences and lessons learned (both positive and negative). It also describes how we used this flexibility to build and specialize three network data services: the Cheetah HTTP server, the webswamp Web benchmarking tool, and an application-level TCP forwarder. Overall measurements show large performance improvements relative to similar services built on conventional interfaces, in each case reaching the maximum possible end-to-end performance for the experimental platform. For example, Cheetah provides factor of 2--4 increases in throughput compared to highly tuned socket-based implementations and factor of 3--8 increases compared to conventional systems. Webswamp can offer loads that are two to eight times heavier. The TCP forwarder provides 50--300% higher throughput while also providing end-to-end TCP semantics that cannot be achieved with POSIX sockets. With more detailed measurements and profiling, these overall performance improvements are also broken down and attributed to the specific specializations described, providing server writers with insights into where to focus their optimization efforts. Gregory R. Ganger, Dawson R. Engler, M. Frans Kaashoek, Héctor M. Briceño, Russell Hunt, Thomas Pinckney |
ACM Trans. Comput. Syst. | 2 |
| 2001 | A simple method for extracting models for protocol codeabstractThe use of model checking for validation requires that models of the underlying system be created. Creating such models is both difficult and error prone and as a result, verification is rarely used despite its advantages. In this paper, we present a method for automatically extracting models from low level software implementations. Our method is based on the use of an extensible compiler system, xg++, to perform the extraction. The extracted model is combined with a model of the hardware, a description of correctness, and an initial state. The whole model is then checked with the Murφ model checker. As a case study, we apply our method to the cache coherence protocols of the Stanford FLASH multiprocessor. Our system has a number of advantages. First, it reduces the cost of creating models, which allows model checking to be used more frequently. Second, it increases the effectiveness of model checking since the automatically extracted models are more accurate and faithful to the underlying implementation. We found a total of 8 errors using our system. Two errors were global resource errors, which would be difficult to find through any other means. We feel the approach is applicable to other low level systems. David Lie, Andy Chou, Dawson R. Engler, David L. Dill |
ISCA | 3 |
| 2001 | An Empirical Study of Operating System ErrorsabstractWe present a study of operating system errors found by automatic, static, compiler analysis applied to the Linux and OpenBSD kernels. Our approach differs from previous studies that consider errors found by manual inspection of logs, testing, and surveys because static analysis is applied uniformly to the entire kernel source, though our approach necessarily considers a less comprehensive variety of errors than previous studies. In addition, automation allows us to track errors over multiple versions of the kernel source to estimate how long errors remain in the system before they are fixed.We found that device drivers have error rates up to three to seven times higher than the rest of the kernel. We found that the largest quartile of functions have error rates two to six times higher than the smallest quartile. We found that the newest quartile of files have error rates up to twice that of the oldest quartile, which provides evidence that code "hardens" over time. Finally, we found that bugs remain in the Linux kernel an average of 1.8 years before being fixed. Andy Chou, Benjamin Chelf, Seth Hallem, Dawson R. Engler |
SOSP | 5 |
| 2001 | Bugs as Deviant Behavior: A General Approach to Inferring Errors in Systems CodeabstractA major obstacle to finding program errors in a real system is knowing what correctness rules the system must obey. These rules are often undocumented or specified in an ad hoc manner. This paper demonstrates techniques that automatically extract such checking information from the source code itself, rather than the programmer, thereby avoiding the need for a priori knowledge of system rules.The cornerstone of our approach is inferring programmer "beliefs" that we then cross-check for contradictions. Beliefs are facts implied by code: a dereference of a pointer, p, implies a belief that p is non-null, a call to "unlock(1)" implies that 1 was locked, etc. For beliefs we know the programmer must hold, such as the pointer dereference above, we immediately flag contradictions as errors. For beliefs that the programmer may hold, we can assume these beliefs hold and use a statistical analysis to rank the resulting errors from most to least likely. For example, a call to "spin_lock" followed once by a call to "spin_unlock" implies that the programmer may have paired these calls by coincidence. If the pairing happens 999 out of 1000 times, though, then it is probably a valid belief and the sole deviation a probable error. The key feature of this approach is that it requires no a priori knowledge of truth: if two beliefs contradict, we know that one is an error without knowing what the correct belief is.Conceptually, our checkers extract beliefs by tailoring rule "templates" to a system --- for example, finding all functions that fit the rule template "a must be paired with b." We have developed six checkers that follow this conceptual framework. They find hundreds of bugs in real systems such as Linux and OpenBSD. From our experience, they give a dramatic reduction in the manual effort needed to check a large system. Compared to our previous work [9], these template checkers find ten to one hundred times more rule instances and derive properties we found impractical to specify manually. Dawson R. Engler, David Yu Chen, Andy Chou |
SOSP | 1 |
| 2001 | Reverse-Engineering Instruction Encodings
Wilson C. Hsieh, Dawson R. Engler, Godmar Back |
USENIX ATC, General Track | 2 |
| 2000 | Using Meta-level Compilation to Check FLASH Protocol CodeabstractBuilding systems such as OS kernels and embedded software is difficult. An important source of this difficulty is the numerous rules they must obey: interrupts cannot be disabled for ~too long," global variables must be protected by locks, user pointers passed to OS code must be checked for safety before use, etc. A single violation can crash the system, yet typically these invariants are unchecked, existing only on paper or in the implementor's mind.This paper is a case study in how system implementors can use a new programming methodology, meta-level compilation (MC), to easily check such invariants. It focuses on using MC to check for errors in the code used to manage cache coherence on the FLASH shared memory multiprocessor. The only real practical method known for verifying such code is testing and simulation. We show that simple, system-specific checkers can dramatically improve this situation by statically pinpointing errors in the program source. These checkers can be written by implementors themselves and, by exploiting the system-specific information this allows, can detect errors unreachable with other methods. The checkers in this paper found 34 bugs in FLASH code despite the care used in building it and the years of testing it has undergone. Many of these errors fall in the worst category of systems bugs: those that show up sporadically only after days of continuous use. The case study is interesting because it shows that the MC approach finds serious errors in well-tested, non-toy systems code. Further, the code to find such bugs is usually 10-100 lines long, written in a few hours, and exactly locates errors that, if discovered during testing, would require several days of investigation by an experienced implementor.The paper presents 8 checkers we wrote, their application to five different protocol implementations, and a discussion of the errors that we found. Andy Chou, Benjamin Chelf, Dawson R. Engler, Mark A. Heinrich |
ASPLOS | 3 |
| 2000 | Checking System Rules Using System-Specific, Programmer-Written Compiler Extensions
Dawson R. Engler, Benjamin Chelf, Andy Chou, Seth Hallem |
OSDI | 1 |
| 1999 | 'C and tcc: A Language and Compiler for Dynamic Code GenerationabstractDynamic code generation allows programmers to use run-time information in order to achieve performance and expressiveness superior to those of static code. The 'C(Tick C) language is a superset of ANSI C that supports efficient and high-level use of dynamic code generation. 'C provides dynamic code generation at the level of C expressions and statements and supports the composition of dynamic code at run time. These features enable programmers to add dynamic code generation to existing C code incrementally and to write important applications (such as “just-in-time” compilers) easily. The article presents many examples of how 'C can be used to solve practical problems. The tcc compiler is an efficient, portable, and freely available implementation of 'C. tcc allows programmers to trade dynamic compilation speed for dynamic code quality: in some aplications, it is most important to generate code quickly, while in others code quality matters more than compilation speed. The overhead of dynamic compilation is on the order of 100 to 600 cycles per generated instruction, depending on the level of dynamic optimizaton. Measurements show that the use of dynamic code generation can improve performance by almost an order of magnitude; two- to four-fold speedups are common. In most cases, the overhead of dynamic compilation is recovered in under 100 uses of the dynamic code; sometimes it can be recovered within one use. Massimiliano Poletto, Wilson C. Hsieh, Dawson R. Engler, M. Frans Kaashoek |
ACM Trans. Program. Lang. Syst. | 3 |
| 1999 | Interface Compilation: Steps Toward Compiling Program Interfaces as LanguagesabstractInterfaces-the collection of procedures and data structures that define a library, a subsystem, a module-are syntactically poor programming languages. They have state (defined both by the interface's data structures and internally), operations on this state (defined by the interface's procedures), and semantics associated with these operations. Given a way to incorporate interface semantics into compilation, interfaces can be compiled in the same manner as traditional languages such as ANSI C or FORTRAN. The article makes two contributions. First, it proposes and explores the metaphor of interface compilation, and provides the beginnings of a programming methodology for exploiting it. Second, it presents MAGIK, a system built to support interface compilation. Using MAGIK, software developers can build optimizers and checkers for their interface languages, and have these extensions incorporated into compilation, with a corresponding gain in efficiency and safety. This organization contrasts with traditional compilation, which relegates programmers to the role of passive consumers, rather than active exploiters of a compiler's transformational abilities. Dawson R. Engler |
IEEE Trans. Software Eng. | 1 |
| 1997 | tcc: A System for Fast, Flexible, and High-level Dynamic Code Generationabstracttcc is a compiler that provides efficient and high-level access to dynamic code generation. It implements the 'C ("Tick-C") programming language, an extension of ANSI C that supports dynamic code generation [15]. 'C gives power and flexibility in specifying dynamically generated code: whereas most other systems use annotations to denote run-time invariants. 'C allows the programmer to specify and compose arbitrary expressions and statements at run time. This degree of control is needed to efficiently implement some of the most important applications of dynamic code generation, such as "just in time" compilers [17] and efficient simulators [10, 48, 46].The paper focuses on the techniques that allow tcc to provide 'C's flexibility and expressiveness without sacrificing run-time code generation efficiency. These techniques include fast register allocation, efficient creation and composition of dynamic code specifications, and link-time analysis to reduce the size of dynamic code generators. tcc also implements two different dynamic code generation strategies, designed to address the tradeoff of dynamic compilation speed versus generated code quality. To characterize the effects of dynamic compilation, we present performance measurements for eleven programs compiled using tcc. On these applications, we measured performance improvements of up to one order of magnitude.To encourage further experimentation and use of dynamic code generation, we are making the tcc compiler available in the public domain. This is, to our knowledge, the first high-level dynamic compilation system to be made available. Massimiliano Poletto, Dawson R. Engler, M. Frans Kaashoek |
PLDI | 2 |
| 1997 | Application Performance and Flexibility on Exokernel SystemsabstractThe exokernel operating system architecture safely gives untrusted software efficient control over hardware and software resources by separating management from protection. This paper describes an exokernel system that allows specialized applications to achieve high performance without sacrificing the performance of unmod-ified UNIX programs. It evaluates the exokernel architecture by measuring end-to-end application performance on Xok, an exo-kernel for Intel x86-based computers, and by comparing Xok’s performance to the performance of two widely-used 4.4BSD UNIX systems (FreeBSD and OpenBSD). The results show that common unmodified UNIX applications can enjoy the benefits of exoker-nels: applications either perform comparably on Xok/ExOS and the BSD UNIXes, or perform significantly better. In addition, the results show that customized applications can benefit substantially from control over their resources (e.g., a factor of eight for a Web server). This paper also describes insights about the exokernel ap-proach gained through building three different exokernel systems, and presents novel approaches to resource multiplexing. 1 M. Frans Kaashoek, Dawson R. Engler, Gregory R. Ganger, Héctor M. Briceño, Russell Hunt, David Mazières, Thomas Pinckney, Robert Grimm 0001, John Jannotti, Kenneth Mackenzie |
SOSP | 2 |
| 1997 | ASHs application-specific handlers for high-performance messagingabstractApplication-specific safe message handlers (ASHs) are designed to provide applications with hardware-level network performance. ASHs are user-written code fragments that safely and efficiently execute in the kernel in response to message arrival. ASHs can direct message transfers (thereby eliminating copies) and send messages (thereby reducing send-response latency). In addition, the ASH system provides support for dynamic integrated layer processing (thereby eliminating duplicate message traversals) and dynamic protocol composition (thereby supporting modularity). ASHs offer this high degree of flexibility while still providing network performance as good as, or (if they exploit application-specific knowledge) even better than, hard-wired in-kernel implementations. A combination of user-level microbenchmarks and end-to-end system measurements using TCP demonstrates the benefits of the ASH system. Deborah A. Wallach, Dawson R. Engler, M. Frans Kaashoek |
IEEE/ACM Trans. Netw. | 2 |
| 1996 | VCODE: a Retargetable, Extensible, Very Fast Dynamic Code Generation SystemabstractDynamic code generation is the creation of executable code at runtime. Such "on-the-fly" code generation is a powerful technique, enabling applications to use runtime information to improve performance by up to an order of magnitude [4, 8,20, 22, 23].Unfortunately, previous general-purpose dynamic code generation systems have been either inefficient or non-portable. We present VCODE, a retargetable, extensible, very fast dynamic code generation system. An important feature of VCODE is that it generates machine code "in-place" without the use of intermediate data structures. Eliminating the need to construct and consume an intermediate representation at runtime makes VCODE both efficient and extensible. VCODE dynamically generates code at an approximate cost of six to ten instructions per generated instruction, making it over an order of magnitude faster than the most efficient general-purpose code generation system in the literature [10].Dynamic code generation is relatively well known within the compiler community. However, due in large part to the lack of a publicly available dynamic code generation system, it has remained a curiosity rather than a widely used technique. A practical contribution of this work is the free, unrestricted distribution of the VCODE system, which currently runs on the MIPS, SPARC, and Alpha architectures. Dawson R. Engler |
PLDI | 1 |
| 1996 | C: A Language for High-Level, Efficient, and Machine-Independent Dynamic Code GenerationabstractDynamic code generation allows specialized code sequences to be created using runtime information. Since this information is by definition not available statically, the use of dynamic code generation can achieve performance inherently beyond that of static code generation. Previous attempts to support dynamic code generation have been low-level, expensive, or machine-dependent. Despite the growing use of dynamic code generation, no mainstream language provides flexible, portable, and efficient support for it.We describe 'C (Tick C), a superset of ANSI C that allows flexible, high-level. efficient, and machine-independent specification of dynamically generated code. 'C provides many of the performance benefits of pure partial evaluation, but in the context of a complex, statically typed, but widely used language. 'C examples illustrate the ease of specifying dynamically generated code and how it can be put to use. Experiments with a prototype compiler show that 'C enables excellent performance improvement (in some cases, more than an order of magnitude). Dawson R. Engler, Wilson C. Hsieh, M. Frans Kaashoek |
POPL | 1 |
| 1996 | DPF: Fast, Flexible Message Demultiplexing Using Dynamic Code GenerationabstractFast and flexible message demultiplexing are well-established goals in the networking community [1, 18, 22]. Currently, however, network architects have had to sacrifice one for the other. We present a new packet-filter system, DPF (Dynamic Packet Filters), that provides both the traditional flexibility of packet filters [18] and the speed of hand-crafted demultiplexing routines [3]. DPF filters run 10-50 times faster than the fastest packet filters reported in the literature [1, 17, 18, 27]. DPF's performance is either equivalent to or, when it can exploit runtime information, superior to hand-coded demultiplexors. DPF achieves high performance by using a carefully-designed declarative packet-filter language that is aggressively optimized using dynamic code generation. The contributions of this work are: (1) a detailed description of the DPF design, (2) discussion of the use of dynamic code generation and quantitative results on its performance impact, (3) quantitative results on how DPF is used in the Aegis kernel to export network devices safely and securely to user space so that UDP and TCP can be implemented efficiently as user-level libraries, and (4) the unrestricted release of DPF into the public domain. Dawson R. Engler, M. Frans Kaashoek |
SIGCOMM | 1 |
| 1996 | ASHs: Application-Specific Handlers for High-Performance MessagingabstractApplication-specific safe message handlers (ASHs) are designed to provide applications with hardware-level network performance. ASHs are user-written code fragments that safely and efficiently execute in the kernel in response to message arrival. ASHs can direct message transfers (thereby eliminating copies) and send messages (thereby reducing send-response latency). In addition, the ASH system provides support for dynamic integrated layer processing (thereby eliminating duplicate message traversals) and dynamic protocol composition (thereby supporting modularity). ASHs provide this high degree of flexibility while still providing network performance as good as, or (if they exploit application-specific knowledge) even better than, hard-wired in-kernel implementations. A combination of user-level microbenchmarks and end-to-end system measurements using TCP demonstrate the benefits of the ASH system. Deborah A. Wallach, Dawson R. Engler, M. Frans Kaashoek |
SIGCOMM | 2 |
| 1995 | AVM: application-level virtual memoryabstractVirtual memory (VM) is a notoriously complicated abstraction to implement, and is hard to change, specialize, or replace. Although a certain degree of flexibility is achieved by user-level pagers, the control they provide is limited: they leave much of the VM system fixed in the kernel, unreachable by the application. As applications become more diverse and the opportunity cost of bad memory policies grows, it is essential for applications to have more control over the VM abstraction. We motivate and describe a VM system that is implemented completely at the application level. To the best of our knowledge this system is the first complete example of application-level virtual memory (AVM). AVM allows applications to easily specialize, modify, or even replace the VM abstractions offered. For example, on architectures with software TLB management, applications can even select their own page-table structures. In addition, AVM simplifies the OS kernel, since the kernel only multiplexes and does not abstract physical memory. A prototype AVM system is implemented for Aegis, an experimental exokernel. Dawson R. Engler, Sandeep K. Gupta 0002, M. Frans Kaashoek |
HotOS | 1 |
| 1995 | Exterminate all operating system abstractionsabstractThe defining tragedy of the operating systems community has been the definition of an operating system as software that both multiplexes and abstracts physical resources. The view that the OS should abstract the hardware is based on the assumption that it is possible bath to define abstractions that are appropriate for all areas and to implement them to perform efficiently in all situations. We believe that the fallacy of this quixotic goal is self-evident, and that the operating system problems of the last two decades (poor performance, poor reliability, poor adaptability, and inflexibility) can be traced back to it. The solution we propose is simple: complete elimination of operating system abstractions by lowering the operating system interface to the hardware level. Dawson R. Engler, M. Frans Kaashoek |
HotOS | 1 |
| 1995 | Exokernel: An Operating System Architecture for Application-Level Resource Managementabstractarticle Exokernel: an operating system architecture for application-level resource management Share on Authors: D. R. Engler M.I.T. Laboratory for Computer Science, Cambridge, MA M.I.T. Laboratory for Computer Science, Cambridge, MAView Profile , M. F. Kaashoek M.I.T. Laboratory for Computer Science, Cambridge, MA M.I.T. Laboratory for Computer Science, Cambridge, MAView Profile , J. O'Toole M.I.T. Laboratory for Computer Science, Cambridge, MA M.I.T. Laboratory for Computer Science, Cambridge, MAView Profile Authors Info & Claims ACM SIGOPS Operating Systems ReviewVolume 29Issue 5Dec. 3, 1995 pp 251–266https://doi.org/10.1145/224057.224076Online:03 December 1995Publication History 700citation13,300DownloadsMetricsTotal Citations700Total Downloads13,300Last 12 Months628Last 6 weeks58 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteGet Access Dawson R. Engler, M. Frans Kaashoek, James W. O'Toole Jr. |
SOSP | 1 |
| 1994 | DCG: An Efficient, Retargetable Dynamic Code Generation SystemabstractDynamic code generation allows aggressive optimization through the use of runtime information. Previous systems typically relied on ad hoc code generators that were not designed for retargetability, and did not shield the client from machine-specific details. We present a system, dcg, that allows clients to specify dynamically generated code in a machine-independent manner. Our one-pass code generator is easily retargeted and extremely efficient (code generation costs approximately 350 instructions per generated instruction). Experiments show that dynamic code generation increases some application speeds by over an order of magnitude. Dawson R. Engler, Todd A. Proebsting |
ASPLOS | 1 |
| 1994 | The Exokernel Approach to Operating System Extensibility (Panel Statement)
Dawson R. Engler, M. Frans Kaashoek, James W. O'Toole Jr. |
OSDI | 1 |