This paper presents the design and implementation of Event-driven State-machines programming (ESP) - a language for programmable devices. In traditional languages, like C, using event-driven state-machines forces a tr...
详细信息
ISBN:
(纸本)9781581134148
This paper presents the design and implementation of Event-driven State-machines programming (ESP) - a language for programmable devices. In traditional languages, like C, using event-driven state-machines forces a tradeoff that requires giving up ease of development and reliability to achieve high performance ESP is designed to provide all of these three properties simultaneously. ESP provides a comprehensive set of features to support development of compact and modular programs. The ESP compiler compiles the programs into two targets - a C file that can be used to generate efficient firmware For the device;and a specification that can be used by a verifier like SPIN to extensively test the firmware. As a case study, we reimplemented VMMC firmware that;runs on Myrinet network interface cards using ESP. We found that ESP simplifies the task of programming with event-driven state machines. It required an order of magnitude fewer lines of code than the previous implementation. We also found that model-checking verifiers like SPIN can be used to effectively debug the firmware. Finally. our measurements indicate that, the performance overhead of using ESP is relatively small.
Computer designs are shifting from 32-bit architectures to 64-bit architectures, while most of the programs available today are still designed for 32-bit architectures, Java(TM), for example, specifies the frequently ...
详细信息
ISBN:
(纸本)9781581134636
Computer designs are shifting from 32-bit architectures to 64-bit architectures, while most of the programs available today are still designed for 32-bit architectures, Java(TM), for example, specifies the frequently used "int" as a 32-bit data type. If such Java programs are executed on a 64-bit architecture, many 32-bit values must be sign-extended to 64-bit values for integer operations. This causes serious performance overhead. In this paper, we present a fast and effective algorithm for eliminating sign extensions. We implemented this algorithm in the IBM Java Just-in-Time (JIT) compiler for IA-64(TM). Our experimental results show that our algorithm effectively eliminates the majority of sign extensions, They also show that it significantly improves performance, while it increases JIT compilation time by only 0.11%. We implemented our algorithm for programs in Java, but it can be applied to any language requiring sign extensions.
A general class of program analyses are a combination of context-free and regular language reachability. We define regularly annotated set constraints, a constraint formalism that captures this class. Our results exte...
详细信息
ISBN:
(纸本)9781595936332
A general class of program analyses are a combination of context-free and regular language reachability. We define regularly annotated set constraints, a constraint formalism that captures this class. Our results extend the class of reachability problems expressible naturally in a single constraint formalism, including such diverse applications as interprocedural dataflow analysis, precise type-based flow analysis, and pushdown model checking.
In this paper we describe the design of a global machine independent low level optimizer for the Karlsruhe Ada Compiler. We give a short overview on the optimizations and data structures used in the optimizer as well ...
详细信息
There is an increasing interest in extensible languages, (domain-specific) language extensions, and mechanisms for their specification and implementation. One challenge is to develop tools that allow non-expert progra...
详细信息
ISBN:
(纸本)9781605583921
There is an increasing interest in extensible languages, (domain-specific) language extensions, and mechanisms for their specification and implementation. One challenge is to develop tools that allow non-expert programmers to add an eclectic set of language extensions to a host language. We describe mechanisms for composing and analyzing concrete syntax specifications of a host language and extensions to it. These specifications consist of context-free grammars with each terminal symbol mapped to a regular expression, from which a slightly-modified LR parser and context-aware scanner are generated. Traditionally, conflicts are detected when a parser is generated from the composed grammar, but this comes too late since it is the non-expert programmer directing the composition of independently developed extensions with the host language. The primary contribution of this paper is a modular analysis that is performed independently by each extension designer on her extension ( composed alone with the host language). If each extension passes this modular analysis, then the language composed later by the programmer will compile with no conflicts or lexical ambiguities. Thus, extension writers can verify that their extension will safely compose with others and, if not, fix the specification so that it will. This is possible due to the context-aware scanner's lexical disambiguation and a set of reasonable restrictions limiting the constructs that can be introduced by an extension. The restrictions ensure that the parse table states can be partitioned so that each state can be attributed to the host language or a single extension.
This paper presents an algorithm for synthesizing recursive functions that process algebraic datatypes. It is founded on proof-theoretic techniques that exploit both type information and input-output examples to prune...
详细信息
ISBN:
(纸本)9781450334686
This paper presents an algorithm for synthesizing recursive functions that process algebraic datatypes. It is founded on proof-theoretic techniques that exploit both type information and input-output examples to prune the search space. The algorithm uses refinement trees, a data structure that succinctly represents constraints on the shape of generated code. We evaluate the algorithm by using a prototype implementation to synthesize more than 40 benchmarks and several non-trivial larger examples. Our results demonstrate that the approach meets or outperforms the state-of-the-art for this domain, in terms of synthesis time or attainable size of the generated programs.
Asynchronous exceptions, such as timeouts, are important for robust, modular programs, but are extremely difficult to program with - so much so that most programminglanguages either heavily restrict them or ban them ...
详细信息
ISBN:
(纸本)9781581134148
Asynchronous exceptions, such as timeouts, are important for robust, modular programs, but are extremely difficult to program with - so much so that most programminglanguages either heavily restrict them or ban them altogether. We extend our earlier work, in which we added synchronous exceptions to Haskell, to support asynchronous exceptions too. Our design introduces scoped combinators for blocking and unblocking asynchronous interrupts, along with a somewhat surprising semantics for operations that can suspend. Uniquely, we also give a formal semantics for our system.
We have implemented an illustrated compiIer for a simple block structured language. The compiler graphically displays its control and data structures, and so gives its viewers an intuitive understanding of compiler or...
详细信息
The combination of pointers and pointer arithmetic in C makes the task of improving C programs somewhat more difficult than improving programs written in simpler languages like Fortran. While much work has been publis...
详细信息
The combination of pointers and pointer arithmetic in C makes the task of improving C programs somewhat more difficult than improving programs written in simpler languages like Fortran. While much work has been published that focuses on the analysis of pointers, little has appeared that uses the results of such analysis to improve the code compiled for C. This paper examines the problem of register promotion in C and presents experimental results showing that it can have dramatic effects on memory traffic.
Achieving high code coverage is essential in testing, which gives us confidence in code quality. Testing floating-point code usually requires painstaking efforts in handling floating-point constraints, e.g., in symbol...
详细信息
ISBN:
(纸本)9781450349888
Achieving high code coverage is essential in testing, which gives us confidence in code quality. Testing floating-point code usually requires painstaking efforts in handling floating-point constraints, e.g., in symbolic execution. This paper turns the challenge of testing floating-point code into the opportunity of applying unconstrained programming-the mathematical solution for calculating function minimum points over the entire search space. Our core insight is to derive a representing function from the floating-point program, any of whose minimum points is a test input guaranteed to exercise a new branch of the tested program. This guarantee allows us to achieve high coverage of the floating-point program by repeatedly minimizing the representing function. We have realized this approach in a tool called CoverMe and conducted an extensive evaluation of it on Sun's C math library. Our evaluation results show that CoverMe achieves, on average, 90.8% branch coverage in 6.9 seconds, drastically outperforming our compared tools: (1) Random testing, (2) AFL, a highly optimized, robust fuzzer released by Google, and (3) Austin, a state-of-the-art coverage-based testing tool designed to support floating-point code.
暂无评论