A simple but key aspect of parallel jobs is the all-or-nothing property: unless all tasks of a job are provided equal improvement, there is no speedup in the completion of the job. The all-or-nothing property is critical for the promise of efficient and fault-tolerant parallel computations on large clusters. Meeting this promise in clusters of these scales is challenging and a key departure from prior work on distributed systems. This talk will look at the execution of a job from first principles and propose techniques spanning the software stack of data analytics systems such that its tasks achieve homogeneous performance while overcoming the various heterogeneities. To that end, we will propose techniques for (i) caching and cache replacement for parallel jobs, which outperforms even Belady's MIN (that uses an oracle), (ii) data locality, and (iii) straggler mitigation. Our analyses and evaluation are performed using workloads from Facebook and Bing production datacenters Along the way, we will also describe how we broke the myth of disk-locality's importance in datacenter computing.

关键词：集群技术；并行工作；数据密集型

查看摘要 索取原文[125页]

In this paper, we investigate the relation between interface theories (specifically, relational interfaces) and assume-guarantee (A/G) contracts, revealing some of the subtleties involved. We show that the natural transformation of interfaces to A/G contracts represented by linear temporal logic (LTL) formulas preserves refinement, but does not generally preserve serial composition, and we present an assumption-projection operator to remedy the latter issue. We also discuss the properties of our transformation with respect to conjunction. Finally, we provide illustrative examples that shed light on the effectiveness of both frameworks for requirement formalization, early detection of integration errors, and principled use of abstraction-refinement.

关键词：接口理论；关系接口；Assume-Guarantee；假设保证

查看摘要 索取原文[8页]

We address the problem of synthesizing optimal energy pricing strategies, while quantitatively constraining the risk due to uncertainty for the network operator and guaranteeing quality-of-service for the users. We use Ellipsoidal Markov Decision Processes (EMDP) to model the decision-making scenario. These models are trained with measured data and allow to quantitatively capture the uncertainty in the prediction of energy generation. We then cast the constrained optimization problem as the strategy synthesis problem for EMDPs, with the goal to maximize the total expected reward constrained to properties expressed using the Probabilistic Computation Tree Logic (PCTL), and propose a novel sound and complete synthesis algorithm. An experimental comparison shows the effectiveness of our method with respect to previous approaches presented in the literature.

关键词：可再生能源；概率统计系统；策略合成；风险有限

查看摘要 索取原文[27页]

The proliferation of large High-Performance Computing clusters executing computation-intensive jobs on large data sets has made cluster power proportionality very important. Despite publicly available traces showing that many clusters have a low average utilization, existing power-proportionality techniques have seen low adoption, a major reason being that these techniques require modifications to the existing cluster software and network stack, and do not address the reliability concerns that may arise during the course of server power-cycling.We present Hypnos, a defensive power proportionality system which is unobtrusive, extensible and gracefully handles possible server software and hardware failures which may occur during server power-cycling. We deployed Hypnos on a 57-server production cluster. From a 21-day run, we obtained a 36% energy saving in spite of multiple server and network failures.

关键词：HPCC；功率比；功率循环

查看摘要 索取原文[14页]

This dissertation proposes an architecture for cluster computing systems that can tackle emerging data processing workloads while coping with larger and larger scales. Whereas early cluster computing systems, like MapReduce, handled batch processing, our architecture also enables streaming and interactive queries, while keeping the scalability and fault tolerance of previous systems. And whereas most deployed systems only support simple one-pass computations (e.g. aggregation or SQL queries), ours also extends to the multi-pass algorithms required for more complex analytics (e.g. iterative algorithms for machine learning). Finally, unlike the specialized systems proposed for some of these workloads, our architecture allows these computations to be combined, enabling rich new applications that intermix, for example, streaming and batch processing, or SQL and complex analytics.

关键词：集群技术；数据处理；集群计算系统

查看摘要 索取原文[127页]

Specification is the first and arguably the most important step for formal verification and correct-by-construction synthesis. It is extremely difficult to manually create a complete suite of good-quality formal specifications. Many real-world experiences indicate that poor or the lack of sufficient specifications can easily lead to misses of critical bugs, and in turn design re-spins and time-to-market slips. This dissertation presents research that seeks to mitigate the manual and error-prone process of creating formal specifications through automation. The overarching theme is specification mining - the process of inferring likely specifications by observing a design's behaviors. We explore novel formalisms and algorithms to mine specifications from different sources, and demonstrate that the mined specifications are useful if not essential for a wide variety of applications such as verification, diagnosis and LTL synthesis. Further, we describe efforts on broadening the scope of specification mining with creative use of human inputs, including the design of a crowdsourced game and judicious use of natural language processing techniques.

关键词：规范；编程；数字电路；线性时序逻辑；自动机

查看摘要 索取原文[156页]

We consider a three-step three-player complete information Colonel Blotto game in this paper, in which the first two players fight against a common adversary. Each player is endowed with certain amount of resources at the beginning of the game, and the number of battlefields on which a player and the adversary fights is specified. The first two players are allowed to form a coalition if it improves their payoffs. In the first stage, the first two players may add battlefields and incur costs. In the second stage, the first two players may transfer resources among each other. The adversary observes this transfer, and decides on the allocation of its resources to the two battles with the players. At the third step, the adversary and the other two players fight on the updated number of battlefields and receive payoffs. We characterize the subgame-perfect Nash equilibrium (SPNE) of the game in various parameter regions. In particular, we show that there are certain parameter regions in which if the players act according to the SPNE strategies, then (i) one of the first two players add battlefields and transfer resources to the other player (a coalition is formed), (ii) there is no addition of battlefields and no transfer of resources (no coalition is formed). We discuss the implications of the results on resource allocation for securing cyber physical systems.

关键词：信息物理安全；Blotto博弈；纳什均衡；网络物理系统

查看摘要 索取原文[25页]

Reactive systems are increasingly developed using high-level modeling tools. Such modeling tools may facilitate formal reasoning about concurrent programs, but provide little help when timing-related problems arise and deadlines are missed when running a real system. In these cases, the modeler has typically no information about timing properties and costly parts of the model; there is little or no guidance on how to improve the timing characteristics of the model. In this paper, we propose a design methodology where interactive timing analysis is an integral part of the modeling process. This methodology concerns how to aggregate timing values in a user-friendly manner and how to define timing analysis requests. We also introduce and formalize a new timing analysis interface that is designed for communicating timing information between a high-level modeling tool and a lower-level timing analysis tool.

关键词：系统设计；反应式；时序分析

查看摘要 索取原文[16页]

We analyze the s-step biconjugate gradient algorithm in finite precision arithmetic and derive a bound for the residual norm in terms of a minimum polynomial of a perturbed matrix multiplied by an amplification factor. Our bound enables comparison of s-step and classical biconjugate gradient in terms of amplification factors. Our results show that for s-step biconjugate gradient, the amplification factor depends heavily on the quality of s-step polynomial bases generated in each outer loop.

关键词：有限精度；双共轭梯度方法；s-step双共轭梯度；Krylov方法

查看摘要 索取原文[17页]

We consider the hypothesis testing problem of detecting a shift between the means of two multivariate normal distributions in the high-dimensional setting, allowing for the data dimension p to exceed the sample size n. Specifically, we propose a new test statistic for the two-sample test of means that integrates a random projection with the classical Hotelling T-squared statistic. Working under a high-dimensional framework with (p,n) tending to infinity, we first derive an asymptotic power function for our test, and then provide sufficient conditions for it to achieve greater power than other state-of-the-art tests. Using ROC curves generated from synthetic data, we demonstrate superior performance against competing tests in the parameter regimes anticipated by our theoretical results.

关键词：随机投影；双样本检验；高维度

查看摘要 索取原文[28页]