The proceedings contain 8 papers. The topics discussed include: towards concurrent type theory;exact type parameterization and this type support;types for relaxed memory models;towards a formal semantics for a structu...
ISBN:
(纸本)9781450311205
The proceedings contain 8 papers. The topics discussed include: towards concurrent type theory;exact type parameterization and this type support;types for relaxed memory models;towards a formal semantics for a structurally dynamic noncausal modelling language;semantics for graphical user interfaces;giving Haskell a promotion;static lock capabilities for deadlock freedom;type systems for dummies;and row-based effect types for database integration.
Parallel programs are known to be difficult to analyze. A key reason is that they typically have an enormous number of execution inter-leavings, or schedules. Static analysis over all schedules requires over-approxima...
详细信息
ISBN:
(纸本)9781450312059
Parallel programs are known to be difficult to analyze. A key reason is that they typically have an enormous number of execution inter-leavings, or schedules. Static analysis over all schedules requires over-approximations, resulting in poor precision;dynamic analysis rarely covers more than a tiny fraction of all schedules. We propose an approach called schedule specialization to analyze a parallel program over only a small set of schedules for precision, and then enforce these schedules at runtime for soundness of the static analysis results. We build a schedule specialization framework for C/C++ multithreaded programs that use Pthreads. Our framework avoids the need to modify every analysis to be schedule-aware by specializing a program into a simpler program based on a schedule, so that the resultant program can be analyzed with stock analyses for improved precision. Moreover, our framework provides a precise schedule-aware def-use analysis on memory locations, enabling us to build three highly precise analyses: an alias analyzer, a data-race detector, and a path slicer. Evaluation on 17 programs, including 2 real-world programs and 15 popular benchmarks, shows that analyses using our framework reduced may-aliases by 61.9%, false race reports by 69%, and path slices by 48.7%;and detected 7 unknown bugs in well-checked programs.
This paper describes a very high-level language for clear description of distributed algorithms and optimizations necessary for generating efficient implementations. The language supports high-level control flows wher...
详细信息
ISBN:
(纸本)9781450315616
This paper describes a very high-level language for clear description of distributed algorithms and optimizations necessary for generating efficient implementations. The language supports high-level control flows where complex synchronization conditions can be expressed using high-level queries, especially logic quantifications, over message history sequences. Unfortunately, the programs would be extremely inefficient, including consuming unbounded memory, if executed straightforwardly. We present new optimizations that automatically transform complex synchronization conditions into incremental updates of necessary auxiliary values as messages are sent and received. The core of the optimizations is the first general method for efficient implementation of logic quantifications. We have developed an operational semantics of the language, implemented a prototype of the compiler and the optimizations, and successfully used the language and implementation on a variety of important distributed algorithms.
SIMD (single-instruction multiple-data) instruction set extensions are quite common today in both high performance and embedded microprocessors, and enable the exploitation of a specific type of data parallelism calle...
详细信息
ISBN:
(纸本)9781450312059
SIMD (single-instruction multiple-data) instruction set extensions are quite common today in both high performance and embedded microprocessors, and enable the exploitation of a specific type of data parallelism called SLP (Superword Level Parallelism). While prior research shows that significant performance savings are possible when SLP is exploited, placing SIMD instructions in an application code manually can be very difficult and error prone. In this paper, we propose a novel automated compiler framework for improving superword level parallelism exploitation. The key part of our framework consists of two stages: superword statement generation and data layout optimization. The first stage is our main contribution and has two phases, statement grouping and statement scheduling, of which the primary goals are to increase SIMD parallelism and, more importantly, capture more superword reuses among the superword statements through global data access and reuse pattern analysis. Further, as a complementary optimization, our data layout optimization organizes data in memory space such that the price of memory operations for SLP is minimized. The results from our compiler implementation and tests on two systems indicate performance improvements as high as 15.2% over a state-of-the-art SLP optimization algorithm.
Software-defined networks (SDNs) are a new kind of network architecture in which a controller machine manages a distributed collection of switches by instructing them to install or uninstall packet-forwarding rules an...
详细信息
ISBN:
(纸本)9781450310833
Software-defined networks (SDNs) are a new kind of network architecture in which a controller machine manages a distributed collection of switches by instructing them to install or uninstall packet-forwarding rules and report traffic statistics. The recently formed Open Networking Consortium, whose members include Google, Facebook, Microsoft, Verizon, and others, hopes to use this architecture to transform the way that enterprise and data center networks are implemented. In this paper, we define a high-level, declarative language, called Net Core, for expressing packet-forwarding policies on SDNs. Net-Core is expressive, compositional, and has a formal semantics. To ensure that a majority of packets are processed efficiently on switches instead of on the controller we present new compilation algorithms for Net Core and couple them with a new run-time system that issues rule installation commands and traffic-statistics queries to switches. Together, the compiler and run-time system generate efficient rules whenever possible and outperform the simple, manual techniques commonly used to program SDNs today. In addition, the algorithms we develop are generic, assuming only that the packet-matching capabilities available on switches satisfy some basic algebraic laws. Overall, this paper delivers a new design for a high-level network programminglanguage;an improved set of compiler algorithms;a new run-time system for SDN architectures;the first formal semantics and proofs of correctness in this domain;and an implementation and evaluation that demonstrates the performance benefits over traditional manual techniques.
Modern object-oriented languages such as X 1 0 require a rich framework for types capable of expressing both value-dependency and genericity, and supporting pluggable, domain-specific extensions. In earlier work, we p...
详细信息
ISBN:
(纸本)9781450315616
Modern object-oriented languages such as X 1 0 require a rich framework for types capable of expressing both value-dependency and genericity, and supporting pluggable, domain-specific extensions. In earlier work, we presented a framework for constrained types in object-oriented languages, parametrized by an underlying constraint system. Types are viewed as formulas C {c} where C is the name of a class or an interface and c is a constraint on the immutable instance state (the properties) of C. Constraint systems are a very expressive framework for partial information. Many (value-) dependent type systems for object-oriented languages can be viewed as constrained types. This paper extends the constrained types approach to handle type-dependency ("genericity"). The key idea is to introduce constrained kinds: in the same way that constraints on values can be used to define constrained types, constraints on types can define constrained kinds. We develop a core programminglanguage with constrained kinds. Generic types are supported by introducing type variables-literally, variables with "type" Type-and permitting programs to impose subtyping and equality constraints on such variables. We formalize the type-checking rules and establish soundness. While the language now intertwines constraints on types and values, its type system remains parametric in the choice of the value constraint system (language and solver). We demonstrate that constrained kinds are expressive and practical and sketch possible extensions with a discussion of the design and implementation of X10.
Scripting languages are widely used to quickly accomplish a variety of tasks because of the high productivity they enable. Among other reasons, this increased productivity results from a combination of extensive libra...
详细信息
ISBN:
(纸本)9781450315616
Scripting languages are widely used to quickly accomplish a variety of tasks because of the high productivity they enable. Among other reasons, this increased productivity results from a combination of extensive libraries, fast development cycle, dynamic typing, and polymorphism. The dynamic features of scripting languages are traditionally associated with interpreters, which is the approach used to implement most scripting languages. Although easy to implement, interpreters are generally slow, which makes scripting languages prohibitive for implementing large, CPU-intensive applications. This efficiency problem is particularly important for PHP given that it is the most commonly used language for server-side web development. This paper presents the design, implementation, and an evaluation of the HipHop compiler for PHP. HipHop goes against the standard practice and implements a very dynamic language through static compilation. After describing the most challenging PHP features to support through static compilation, this paper presents HipHop's design and techniques that support almost all PHP features. We then present a thorough evaluation of HipHop running both standard benchmarks and the Facebook web site. Overall, our experiments demonstrate that HipHop is about 5.5x faster than standard, interpreted PHP engines. As a result, HipHop has reduced the number of servers needed to run Facebook and other web sites by a factor between 4 and 6, thus drastically cutting operating costs.
The increasing importance of graph-data based applications is fueling the need for highly efficient and parallel implementations of graph analysis software. In this paper we describe Green-Marl, a domain-specific lang...
详细信息
ISBN:
(纸本)9781450307598
The increasing importance of graph-data based applications is fueling the need for highly efficient and parallel implementations of graph analysis software. In this paper we describe Green-Marl, a domain-specific language (DSL) whose high level language constructs allow developers to describe their graph analysis algorithms intuitively, but expose the data-level parallelism inherent in the algorithms. We also present our Green-Marl compiler which translates high-level algorithmic description written in Green-Marl into an efficient C++ implementation by exploiting this exposed data-level parallelism. Furthermore, our Green-Marl compiler applies a set of optimizations that take advantage of the high-level semantic knowledge encoded in the Green-Marl DSL. We demonstrate that graph analysis algorithms can be written very intuitively with Green-Marl through some examples, and our experimental results show that the compiler-generated implementation out of such descriptions performs as well as or better than highly-tuned handcoded implementations.
The proceedings contain 57 papers. The topics discussed include: the storyteller version control system: tackling version control, code comments, and team learning;the ALIA4J approach to efficient language implementat...
ISBN:
(纸本)9781450315630
The proceedings contain 57 papers. The topics discussed include: the storyteller version control system: tackling version control, code comments, and team learning;the ALIA4J approach to efficient languageimplementation;Citisense: mobile air quality sensing for individuals and communities;analyzing ultra-large-scale code corpus with Boa;OpenRefactory/C: an infrastructure for developing program transformations for C programs;SCuV: a novel software clustering and visualization tool;generic adaptable test cases for software product line testing;using software quality standards to assure the quality of the mobile software product;developing a new computer music programminglanguage in the 'research through design' context;automated behavioral testing of refactoring engines;software tools research: a matter of scale and scope - or commoditization?;and programminglanguage abstractions for self-reconfigurable robots.
Self-adapting systems are becoming widespread in emerging fields such as autonomic, mobile and ubiquitous computing. Context-oriented programming (COP) is a promising language-level solution for the implementation of ...
详细信息
暂无评论