Studies of Aspect-Oriented programming (AOP) usually focus on a language in which a specific aspect extension is integrated with a base language. languages specified in this manner have a fixed, non-extensible AOP fun...
详细信息
ISBN:
(纸本)9781595930316
Studies of Aspect-Oriented programming (AOP) usually focus on a language in which a specific aspect extension is integrated with a base language. languages specified in this manner have a fixed, non-extensible AOP functionality. This paper argues the need for AOP to support the integration and use of multiple domain-specific aspect extensions together. We study the more general case of integrating a base language with a set of third-party aspect extensions for that language. We present a general mixin-based semantic framework for implementing dynamic aspect extensions in such a way that multiple, independently developed aspect mechanisms can be subject to third-party composition and work collaboratively. Principles governing the design of a collaborative aspect mechanism are aspectual effect exposure and implementation hiding.
Future mainstream microprocessors will likely integrate specialized accelerators, such as GPUs, onto a single die to achieve better performance and power efficiency. However, it remains a keen challenge to program suc...
详细信息
Future mainstream microprocessors will likely integrate specialized accelerators, such as GPUs, onto a single die to achieve better performance and power efficiency. However, it remains a keen challenge to program such a heterogeneous multi-core platform, since these specialized accelerators feature ISAs and functionality that are significantly different from the general purpose CPU cores. In this paper, we present EXOCHI: (1) Exoskeleton Sequencer (EXO), an architecture to represent heterogeneous accelerators as ISA-based MIMD architecture resources, and a shared virtual memory heterogeneous multithreaded program execution model that tightly couples specialized accelerator cores with general purpose CPU cores, and (2) C for Heterogeneous Integration (CHI), an integrated C/C++ programming environment that supports accelerator-specific inline assembly and domain-specific languages. The CHI compiler extends the OpenMP pragma for heterogeneous multithreading programming, and produces a single fat binary with code sections corresponding to different instruction sets. The runtime can judiciously spread parallel computation across the heterogeneous cores to optimize performance and power. We have prototyped the EXO architecture on a physical heterogeneous platform consisting of an Intel (R) Core (TM) 2 Duo processor and an 8-core 32-thread Intel (R) Graphics Media Accelerator X3000. In addition, we have implemented the CHI integrated programming environment with the Intel (R) C++ Compiler, runtime toolset, and debugger. On the EXO prototype system, we have enhanced a suite of production-quality media kernels for video and image processing to utilize the accelerator through the CHI programming interface, achieving significant speedup (1.41X to 10.97X) over execution on the IA32 CPU alone.
This paper presents the design and implementation of a compiler that translates programs written in a type-safe subset of the C programminglanguage into highly optimized DEC Alpha assembly language programs, and a ce...
ISBN:
(纸本)9780897919876
This paper presents the design and implementation of a compiler that translates programs written in a type-safe subset of the C programminglanguage into highly optimized DEC Alpha assembly language programs, and a certifier that automatically checks the type safety and memory safety of any assembly language program produced by the compiler. The result of the certifier is either a formal proof of type safety or a counterexample pointing to a potential violation of the type system by the target program. The ensemble of the compiler and the certifier is called a certifying *** advantages of certifying compilation over previous approaches can be claimed. The notion of a certifying compiler is significantly easier to employ than a formal compiler verification, in part because it is generally easier to verify the correctness of the result of a computation than to prove the correctness of the computation itself. Also, the approach can be applied even to highly optimizing compilers, as demonstrated by the fact that our compiler generates target code, for a range of realistic C programs, which is competitive with both the cc and gcc compilers with all optimizations enabled. The certifier also drastically improves the effectiveness of compiler testing because, for each test case, it statically signals compilation errors that might otherwise require many executions to detect. Finally, this approach is a practical way to produce the safety proofs for a Proof-Carrying Code system, and thus may be useful in a system for safe mobile code.
An operating system (OS) kernel forms the lowest level of any system software stack. The correctness of the OS kernel is the basis for the correctness of the entire system. Recent efforts have demonstrated the feasibi...
详细信息
An operating system (OS) kernel forms the lowest level of any system software stack. The correctness of the OS kernel is the basis for the correctness of the entire system. Recent efforts have demonstrated the feasibility of building formally verified general-purpose kernels, but it is unclear how to extend their work to verify the functional correctness of device drivers, due to the non-local effects of interrupts. In this paper, we present a novel compositional framework for building certified interruptible OS kernels with device drivers. We provide a general device model that can be instantiated with various hardware devices, and a realistic formal model of interrupts, which can be used to reason about interruptible code. We have realized this framework in the Coq proof assistant. To demonstrate the effectiveness of our new approach, we have successfully extended an existing verified non-interruptible kernel with our framework and turned it into an interruptible kernel with verified device drivers. To the best of our knowledge, this is the first verified interruptible operating system with device drivers.
Data stream processing applications are often expressed as data flow graphs, composed of operators connected via streams. This structured representation provides a simple yet powerful paradigm for building large-scale...
详细信息
We present CLAP, a new technique to reproduce concurrency bugs. CLAP has two key steps. First, it logs thread local execution paths at runtime. Second, offline, it computes memory dependencies that accord with the log...
详细信息
ISBN:
(纸本)9781450320146
We present CLAP, a new technique to reproduce concurrency bugs. CLAP has two key steps. First, it logs thread local execution paths at runtime. Second, offline, it computes memory dependencies that accord with the logged execution and are able to reproduce the observed bug. The second step works by combining constraints from the thread paths and constraints based on a memory model, and computing an execution with a constraint solver. CLAP has four major advantages. First, logging purely local execution of each thread is substantially cheaper than logging memory interactions, which enables CLAP to be efficient compared to previous approaches. Second, our logging does not require any synchronization and hence with no added memory barriers or fences; this minimizes perturbation and missed bugs due to extra synchronizations foreclosing certain racy behaviors. Third, since it uses no synchronization, we extend CLAP to work on a range of relaxed memory models, such as TSO and PSO, in addition to sequential consistency. Fourth, CLAP can compute a much simpler execution than the original one, that reveals the bug with minimal thread context switches. To mitigate the scalability issues, we also present an approach to parallelize constraint solving, which theoretically scales our technique to programs with arbitrary execution length. Experimental results on a variety of multithreaded benchmarks and real world concurrent applications validate these advantages by showing that our technique is effective in reproducing concurrency bugs even under relaxed memory models; furthermore, it is significantly more efficient than a state-of-the-art technique that records shared memory dependencies, reducing execution time overhead by 45% and log size by 88% on average.
In many areas, such as image recognition, natural language processing, search, recommendation, autonomous cars, systems software and infrastructure, and even Software Engineering tools themselves, Software 2.0 (= prog...
详细信息
ISBN:
(纸本)9781450355735
In many areas, such as image recognition, natural language processing, search, recommendation, autonomous cars, systems software and infrastructure, and even Software Engineering tools themselves, Software 2.0 (= programming using learned models) is quickly swallowing Software 1.0 (= programming using handcrafted algorithms). Where the Software 1.0 Engineer formally specifies their problem, carefully designs algorithms, composes systems out of subsystems or decomposes complex systems into smaller components, the Software 2.0 Engineer amasses training data and simply feeds it into an ML algorithm that will synthesize an approximation of the function whose partial extensional definition is that training data. Instead of code as the artifact of interest, in Software 2.0 it is all about the data where compilation of source code is replaced by training models with data. This new style of programming has far-reaching consequences for traditional software engineering practices. Everything we have learned about life cycle models, project planning and estimation, requirements analysis, program design, construction, debugging, testing, maintenance and implementation, ... runs the danger of becoming obsolete. One way to try to prepare for the new realities of software engineering is not to zero in on the differences between Software 1.0 and Software 2.0 but instead focus on their similarities. If you carefully look at what a neural net actually represents, you realize that in essence it is a pure function, from multi-dimensional arrays of floating point numbers to multi-dimensional arrays of floating point numbers (tensors). What is special about these functions is that they are differentiable (yes, exactly as you remember from middle school calculus), which allows them to be trained using back propagation. The programminglanguage community has also discovered that there is a deep connection between back propagation and continuations. Moreover, when you look closely at how So
What does it mean for a programminglanguage to exist? Usually languages are defined by an informal description augmented by a reference compiler whose behavior is regarded as normative. This approach works well so lo...
ISBN:
(纸本)9781595930644
What does it mean for a programminglanguage to exist? Usually languages are defined by an informal description augmented by a reference compiler whose behavior is regarded as normative. This approach works well so long as the one true implementation suffices, but as soon as we wish to have multiple compilers for the same language, we must agree on what the language is independently of its implementations. Most often this is accomplished through social processes such as standardization committees for building *** processes have served us well, and will continue to be important for languagedesign. But they are not sufficient to support the level of rigor required to prove theorems about languages and programs written in them. For that we need a semantics, which provides an objective foundation for such analyses, typically in the form of a type system and an operational semantics. But merely having such a rigorous definition for a language is not enough — it must be validated by a body of meta-theory that establishes its coherence and its consistency with *** how are we to develop and maintain this body of theory? For full-scale languages the task is so onerous as to inhibit innovation and foster stagnation. The way forward is to take advantage of the recent advances in mechanized reasoning. By representing a language definition within a logical framework we may subject it to formal analysis, much as we use types to express and enforce crucial invariants in our programs. I will describe our use of the Twelf implementation of the LF logical framework, and discuss our successes and difficulties in using it as a tool for mechanizing the meta-theory of programminglanguages.
In this paper we present a modular interprocedural pointer analysis algorithm based on access-paths for C programs. We argue that access paths can reduce the overhead of representing context-sensitive transfer functio...
ISBN:
(纸本)9781581131994
In this paper we present a modular interprocedural pointer analysis algorithm based on access-paths for C programs. We argue that access paths can reduce the overhead of representing context-sensitive transfer functions and effectively distinguish non-recursive heap objects. And when the modular analysis paradigm is used together with other techniques to handle type casts and function pointers, we are able to handle significant programs like those in the SPECcint92 and SPECcint95 suites. We have implemented the algorithm and tested it on a Pentium II 450 PC running Linux. The observed resource consumption and performance improvement are very encouraging.
SKILL is a programminglanguage that supports both command entry and procedural customization in OpusTM design FrameworkTM. After briefly considering some related work, we examine the requirements that motivate the pr...
ISBN:
(纸本)9780897913638
SKILL is a programminglanguage that supports both command entry and procedural customization in OpusTM design FrameworkTM. After briefly considering some related work, we examine the requirements that motivate the provision of a programminglanguage available to the user and describe some of the technical characteristics of the languagedesign and implementation. Finally, we describe our experience with the language and outline future work. A number of programming examples are appended.
暂无评论