The object-oriented programming (OOP) constructs of Fortran 2003 facilitate an elegant memory management solution of particular value when Fortran drives a second language that does not provide automatic garbage colle...
详细信息
This tutorial explains how to implement a Service-Oriented Architecture (SOA) for reliable systems using Enterprise Service Bus (ESB) technologies. The first half of the tutorial describes terms of Service-Oriented Ar...
详细信息
ISBN:
(纸本)9781450314008
This tutorial explains how to implement a Service-Oriented Architecture (SOA) for reliable systems using Enterprise Service Bus (ESB) technologies. The first half of the tutorial describes terms of Service-Oriented Architectures (SOA) including service, service registry, service provider, service consumer, Simple Object Access Protocol (SOAP), Representational State Transfer (REST), and Web Service Description language (WSDL). Several examples of REST and SOAP web services are provided using the Ada Web Server (AWS). This tutorial also presents principles of SOA including loose coupling, encapsulation, composibility of web services, and statelessness of web services. The tutorial covers the benefits of SOA and organizations that are supporting SOA infrastructure. The second half of the tutorial covers Enterprise Service Bus (ESB) technologies including definitions, capabilities, benefits and drawbacks. The tutorial discusses the difference between SOA and an ESB, as well as some of the commercially available ESB solutions on the market. The Mule ESB is explored in more detail and several examples are given. Several examples of using an ESB in a SOA application are given using AWS as an Ada implementation. An AWS server is built in the examples and connected to the ESB providing REST and SOAP web services. AWS allows the developer to expose services in a high-integrity system using the Ada and SPARK programminglanguages. This tutorial is slightly different than the one given at Ada Europe 2008 in that it will focus more on the application of SOA and ESB technology to reliable, high-integrity systems. All tutorial material will be provided to attendees and the opportunity for hands-on participation in examples will be possible.
Multi-stage programming (MSP) provides a disciplined approach to run-time code generation. In the purely functional setting, it has been shown how MSP can be used to reduce the overhead of abstractions, allowing clean...
详细信息
ISBN:
(纸本)9781450300193
Multi-stage programming (MSP) provides a disciplined approach to run-time code generation. In the purely functional setting, it has been shown how MSP can be used to reduce the overhead of abstractions, allowing clean, maintainable code without paying performance penalties. Unfortunately, MSP is difficult to combine with imperative features, which are prevalent in mainstream languages. The central difficulty is scope extrusion, wherein free variables can inadvertently be moved outside the scopes of their binders. This paper proposes a new approach to combining MSP with imperative features that occupies a "sweet spot" in the design space in terms of how well useful MSP applications can be expressed and how easy it is for programmers to understand. The key insight is that escapes (or "anti-quotes") must be weakly separable from the rest of the code, i.e. the computational effects occurring inside an escape that are visible outside the escape are guaranteed to not contain code. To demonstrate the feasibility of this approach, we formalize a type system based on Lightweight Java which we prove sound, and we also provide an implementation, called Mint, to validate both the expressivity of the type system and the effect of staging on the performance of Java programs.
Traditional data-oriented programminglanguages such as dataflow languages and stream languages provide a natural abstraction for parallel programming. In these languages, a developer focuses on the flow of data throu...
详细信息
ISBN:
(纸本)9781450300193
Traditional data-oriented programminglanguages such as dataflow languages and stream languages provide a natural abstraction for parallel programming. In these languages, a developer focuses on the flow of data through the computation and these systems free the developer from the complexities of low-level, thread-oriented concurrency primitives. This simplification comes at a cost traditional data-oriented approaches restrict the mutation of state and, in practice, the types of data structures a program can effectively use. Bamboo borrows from work in typestate and software transactions to relax the traditional restrictions of data-oriented programming models to support mutation of arbitrary data structures. We have implemented a compiler for Bamboo which generates code for the TILEPro64 many-core processor. We have evaluated this implementation on six benchmarks: Tracking, a feature tracking algorithm from computer vision;KMeans, a K-means clustering algorithm;Monte Carlo, a Monte Carlo simulation;Filter Bank, a multi-channel filter bank;Fractal, a Mandelbrot set computation;and Series, a Fourier series computation. We found that our compiler generated implementations that obtained speedups ranging from 26.2 x to 61.6 x when executed on 62 cores.
A number of programminglanguages use rich type systems to verify security properties of code. Some of these languages are meant for source programming, but programs written in these languages are compiled without exp...
详细信息
ISBN:
(纸本)9781450300193
A number of programminglanguages use rich type systems to verify security properties of code. Some of these languages are meant for source programming, but programs written in these languages are compiled without explicit security proofs, limiting their utility in settings where proofs are necessary, e.g., proof-carrying authorization. Others languages do include explicit proofs, but these are generally lambda calculi not intended for source programming, that must be further compiled to an executable form. A language suitable for source programming backed by a compiler that enables end-to-end verification is missing. In this paper, we present a type-preserving compiler that translates programs written in FINE, a source-level functional language with dependent refinements and affine types, to DCIL, a new extension of the .NET Common Intermediate language. FINE is type checked using an external SMT solver to reduce the proof burden on source programmers. We extract explicit LCF-style proof terms from the solver and carry these proof terms in the compilation to DCIL, thereby removing the solver from the trusted computing base. Explicit proofs enable DCIL to be used in a number of important scenarios, including the verification of mobile code, proof-carrying authorization, and evidence-based auditing. We report on our experience using FINE to build reference monitors for several applications, ranging from a plugin-based email client to a conference management server.
We present a concurrent scripting language embedded in Haskell, emulating the functionality of the Orc orchestration language by providing many-valued (real) non-determinism in the context of concurrent effects. We pr...
详细信息
ISBN:
(纸本)9781450302524
We present a concurrent scripting language embedded in Haskell, emulating the functionality of the Orc orchestration language by providing many-valued (real) non-determinism in the context of concurrent effects. We provide many examples of its use, as well as a brief description of how we use the embedded Ore DSL in practice. We describe the abstraction layers of the implementation, and use the fact that we have a layered approach to demonstrate algebraic properties satisfied by the combinators.
Modern proof assistants such as Coq and Isabelle provide high degrees of expressiveness and assurance because they support formal reasoning in higher-order logic and supply explicit machine-checkable proof objects. Un...
详细信息
ISBN:
(纸本)9781605587943
Modern proof assistants such as Coq and Isabelle provide high degrees of expressiveness and assurance because they support formal reasoning in higher-order logic and supply explicit machine-checkable proof objects. Unfortunately, large scale proof development in these proof assistants is still an extremely difficult and time-consuming task. One major weakness of these proof assistants is the lack of a single language where users can develop complex tactics and decision procedures using a rich programming model and in a typeful manner. This limits the scalability of the proof development process, as users avoid developing domain-specific tactics and decision procedures. In this paper, we present VeriML-a novel languagedesign that couples a type-safe effectful computational language with first-class support for manipulating logical terms such as propositions and proofs. The main idea behind our design is to integrate a rich logical framework-similar to the one supported by Coq-inside a computational language inspired by ML. The languagedesign is such that the added features are orthogonal to the rest of the computational language, and also do not require significant additions to the logic language, so soundness is guaranteed. We have built a prototype implementation of VeriML including both its type-checker and an interpreter. We demonstrate the effectiveness of our design by showing a number of type-safe tactics and decision procedures written in VeriML.
We present a new programming model GUESSTIMATE for developing collaborative distributed systems. The model allows atomic, isolated operations that transform a system from consistent state to consistent state, and prov...
详细信息
ISBN:
(纸本)9781450300193
We present a new programming model GUESSTIMATE for developing collaborative distributed systems. The model allows atomic, isolated operations that transform a system from consistent state to consistent state, and provides a shared transactional store for a collection of such operations executed by various machines in a distributed system. In addition to "committed state" which is identical in all machines in the distributed system, GUESSTIMATE allows each machine to have a replicated local copy of the state (called "guesstimated state") so that operations on shared state can be executed locally without any blocking, while also guaranteeing that eventually all machines agree on the sequences of operations executed. Thus, each operation is executed multiple times, once at the time of issue when it updates the guesstimated state of the issuing machine, once when the operation is committed (atomically) to the committed state of all machines, and several times in between as the guesstimated state converges toward the committed state. While we expect the results of these executions of the operation to be identical most of the time in the class of applications we study, it is possible for an operation to succeed the first time when it is executed on the guesstimated state, and fail when it is committed. GUESSTIMATE provides facilities that allow the programmer to deal with this potential discrepancy. This paper presents our programming model, its operational semantics, its realization as an API in C#, and our experience building collaborative distributed applications with this model.
MapReduce and similar systems significantly ease the task of writing data-parallel code. However, many real-world computations require a pipeline of Map Reduces, and programming and managing such pipelines can be diff...
详细信息
ISBN:
(纸本)9781450300193
MapReduce and similar systems significantly ease the task of writing data-parallel code. However, many real-world computations require a pipeline of Map Reduces, and programming and managing such pipelines can be difficult. We present Flume Java, a Java library that makes it easy to develop, test, and run efficient data-parallel pipelines. At the core of the Flume Java library are a couple of classes that represent immutable parallel collections, each supporting a modest number of operations for processing them in parallel. Parallel collections and their operations present a simple, high-level, uniform abstraction over different data representations and execution strategies. To enable parallel operations to run efficiently, Flume Java defers their evaluation, instead internally constructing an execution plan dataflow graph. When the final results of the parallel operations are eventually needed, Flume Java first optimizes the execution plan, and then executes the optimized operations on appropriate underlying primitives (e.g., Map Reduces). The combination of high-level abstractions for parallel data and computation, deferred evaluation and optimization, and efficient parallel primitives yields an easy-to-use system that approaches the efficiency of hand-optimized pipelines. Flume Java is in active use by hundreds of pipeline developers within Google.
暂无评论