The proceedings contain 19 papers. The topics discussed include: impacts of data interchange formats on energy consumption and performance in smartphones;community sharing platform for mobile devices;performance study...
ISBN:
(纸本)9781450308731
The proceedings contain 19 papers. The topics discussed include: impacts of data interchange formats on energy consumption and performance in smartphones;community sharing platform for mobile devices;performance study of Conillon - a platform for distributed computing;secure deduplication on mobile devices;implementation of business intelligence tools using open source approach;open source data mining tools for audit purposes;audit of e-Commerce process;Plan2See: discovering events through Web 1.0;teaching computer programming with structured programminglanguage and flowcharts;innovate in your program computer class: an approach based on a serious game;training and interface features in technology acceptance;medieval guild as metaphor to a knowledge sharing community;and collaborative framework for browser games development.
Over the past 5-10 years, the rise of software-defined networking (SDN) has inspired a wide range of new systems, libraries, hypervisors and languages for programming, monitoring, and debugging network behavior. Often...
详细信息
Over the past 5-10 years, the rise of software-defined networking (SDN) has inspired a wide range of new systems, libraries, hypervisors and languages for programming, monitoring, and debugging network behavior. Oftentimes, these systems are disjoint-one language for programming and another for verification, and yet another for run-time monitoring and debugging. In this paper, we present a new, unified framework, called Temporal NetKAT, capable of facilitating all of these tasks at once. As its name suggests, Temporal NetKAT is the synthesis of two formal theories: past-time (finite trace) linear temporal logic and (network) Kleene Algebra with Tests. Temporal predicates allow programmers to write down concise properties of a packet's path through the network and to make dynamic packet-forwarding, access control or debugging decisions on that basis. In addition to being useful for programming, the combined equational theory of LTL and NetKAT facilitates proofs of pathbased correctness properties. Using new, general, proof techniques, we show that the equational semantics is sound with respect to the denotational semantics, and, for a class of programs we call network-wide programs, complete. We have also implemented a compiler for temporal NetKAT, evaluated its performance on a range of benchmarks, and studied the effectiveness of several optimizations.
This paper describes PAL—a new computer language. Given the fact that new languages seem to appear in computer literature at the rate of several per month, it seems incumbent on one who creates a new language to just...
ISBN:
(纸本)9781450374866
This paper describes PAL—a new computer language. Given the fact that new languages seem to appear in computer literature at the rate of several per month, it seems incumbent on one who creates a new language to justify having done so. In the present case, there are two important considerations: control and specification. Let us consider each of these in *** virtue of our having designed PAL, it is ours. There is no PAL Users Group or Committee of Vested Interests concerned with retaining upward compatibility with what was done last year (or last month). This doesn't mean we change the specifications of the language every few weeks (our students are, in a real sense, our Committee of Vested Interests), but it does mean we can make decisions on changes solely on technical grounds. More important, though, we can design the language to meet the criteria we think important. For example, the language almost demands interpretive execution. Since no one writes production programs in PAL we are able to put up with inefficiencies in the implementation that would otherwise be intolerable. Thus we have designed our own language so that we will have control over it.
Operators for delimiting control and for capturing composable continuations litter the landscape of theoretical programminglanguage research. Numerous papers explain their advantages, how the operators explain each o...
详细信息
Operators for delimiting control and for capturing composable continuations litter the landscape of theoretical programminglanguage research. Numerous papers explain their advantages, how the operators explain each other (or don't), and other aspects of the operators' existence. Production programminglanguages, however, do not support these operators, partly because their relationship to existing and demonstrably useful constructs-such as exceptions and dynamic binding-remains relatively unexplored. In this paper, we report on our effort of translating the theory of delimited and composable control into a viable implementation for a production system. The report shows how this effort involved a substantial design element, including work with a formal model, as well as significant practical exploration and engineering. The resulting version of PLT Scheme incorporates the expressive combination of delimited and composable control alongside dynamic-wind, dynamic binding, and exception handling. None of the additional operators subvert the intended benefits of existing control operators, so that programmers can freely mix and match control operators.
Software language Engineering (SLE) has emerged as a field in computer science research and software engineering, but it has yet to become entrenched as part of the standard curriculum at universities. Many places hav...
详细信息
Software language Engineering (SLE) has emerged as a field in computer science research and software engineering, but it has yet to become entrenched as part of the standard curriculum at universities. Many places have a compiler construction (CC) course and a programminglanguages (PL) course, but these are not aimed at training students in typical SLE matters such as DSL design and implementation, language workbenches, generalized parsers, and meta-tools. We describe our experiences with developing and teaching software language engineering courses at the Universities of Bergen and Koblenz-Landau. We reflect on lecture topics, assignments, development of course material, and other aspects and variation points in course design.
We propose a technique to efficiently search a large family of abstractions in order to prove a query using a parametric dataflow analysis. Our technique either finds the cheapest such abstraction or shows that none e...
详细信息
ISBN:
(纸本)9781450320146
We propose a technique to efficiently search a large family of abstractions in order to prove a query using a parametric dataflow analysis. Our technique either finds the cheapest such abstraction or shows that none exists. It is based on counterexample-guided abstraction refinement but applies a novel meta-analysis on abstract counterexample traces to efficiently find abstractions that are incapable of proving the query. We formalize the technique in a generic framework and apply it to two analyses: a type-state analysis and a thread-escape analysis. We demonstrate the effectiveness of the technique on a suite of Java benchmark programs.
A design model may be used from functional validation to designimplementation: In this paper a C model that has already been used to validate and estimate functional performance is used to explore data transfer and s...
详细信息
ISBN:
(纸本)0769518079
A design model may be used from functional validation to designimplementation: In this paper a C model that has already been used to validate and estimate functional performance is used to explore data transfer and storage aiming at reducing power consumption. Through this model a systematic methodology for power management (DTSE) is applied to a block turbo-decoding algorithm. Estimations of power dissipation are done using a tool for counting memory accesses in a executable C code. Results show a decrease of 25% in power dissipation.
Software-defined radios (SDR) have the potential to bring major innovation in wireless networking design. However, their impact so far has been limited due to complex programming tools. Most of the existing tools are ...
详细信息
ISBN:
(纸本)9781450336192
Software-defined radios (SDR) have the potential to bring major innovation in wireless networking design. However, their impact so far has been limited due to complex programming tools. Most of the existing tools are either too slow to achieve the full line speeds of contemporary wireless PHYs or are too complex to master. In this demo we present our novel SDR programming environment called Ziria. Ziria consists of a novel programminglanguage and an optimizing compiler. The compiler is able to synthesize very efficient SDR code from high-level PHY descriptions written in Ziria language. To illustrate its potential, we present the design of an LTE-like PHY layer in Ziria. We run it on the Sora SDR platform and demonstrate on a test-bed that it is able to operate in real-time.
High-performance computing applications, such as auto-tuners and domain-specific languages, rely on generative programming techniques to achieve high performance and portability. However, these systems are often imple...
详细信息
ISBN:
(纸本)9781450320146
High-performance computing applications, such as auto-tuners and domain-specific languages, rely on generative programming techniques to achieve high performance and portability. However, these systems are often implemented in multiple disparate languages and perform code generation in a separate process from program execution, making certain optimizations difficult to engineer. We leverage a popular scripting language, Lua, to stage the execution of a novel low-level language, Terra. Users can implement optimizations in the high-level language, and use built-in constructs to generate and execute high-performance Terra code. To simplify meta-programming, Lua and Terra share the same lexical environment, but, to ensure performance, Terra code can execute independently of Lua's runtime. We evaluate our design by reimplementing existing multi-language systems entirely in Terra. Our Terra-based auto-tuner for BLAS routines performs within 20% of ATLAS, and our DSL for stencil computations runs 2.3x faster than hand-written C.
暂无评论