This paper provides a mathematical model of data center performance based on the recently introduced Quantitative Theory of Bottleneck Structures (QTBS). Using the model, we prove that if the traffic pattern is \textit{interference-free}, there exists a unique optimal design that both minimizes maximum flow completion time and yields maximal system-wide throughput. We show that interference-free patterns correspond to the important set of patterns that display data locality properties and use these theoretical insights to study three widely used interconnects---fat-trees, folded-Clos and dragonfly topologies. We derive equations that describe the optimal design for each interconnect as a function of the traffic pattern. Our model predicts, for example, that a 3-level folded-Clos interconnect with radix 24 that routes 10\% of the traffic through the spine links can reduce the number of switches and cabling at the core layer by 25\% without any performance penalty. We present experiments using production TCP/IP code to empirically validate the results and provide tables for network designers to identify optimal designs as a function of the size of the interconnect and traffic pattern.

Solvers for the Boolean satisfiability problem (SAT) are an enabling technology for a diverse set of applications, including formal verification of both hardware and software, mathematics, and planning. However, solver performance, measured in terms of speed and maximum problem size, is a limiting factor to the application of SAT to real-world problems. We are developing a parallel SAT solver, Alef, to take advantage of HPC hardware.The Alef parallel SAT solver utilizes algorithms and heuristics that improve its performance over existing approaches. We are developing the solver to run well on commercially available HPC hardware. Our analysis shows that our algorithms combined with the low message latency of supercomputers are likely to produce a significant performance improvement over existing solvers in terms of speed and maximum problem size. Our poster will describe the algorithms we are using, illustrate our approach to problem partitioning, and present our performance analysis to date.

Model checking based on validating temporal logic formulas has proven practical and effective for numerous software engineering applications. As systems based on this approach have become more mainstream, a need has arisen to deal effectively with large batches of formulas over a common model. Presently, most systems validate formulas one at a time, with little or no interaction between validation of separate formulas. This is the case despite the fact that, for a wide range of applications, a certain level of redundancy between domain-related formulas can be anticipated.This paper presents an optimizing compiler for batches of temporal logic formulas. A component of the Carnauba model checking system, this compiler addresses the need to handle batches of temporal logic formulas by leveraging the framework common to optimizing programming language compilers. Just as traditional optimizing compilers attempt to exploit redundancy and other solvable properties in a program to reduce the demand on a runtime system, this compiler exploits similar properties in groups of formulas to reduce the demand on a model checking engine. Optimizations are performed via a set of distinct, interchangeable optimization passes operating on a common intermediate representation. The intermediate representation captures the full modal mu-calculus, and the optimization techniques are applicable to any temporal logic subsumed by that logic. The compiler offers a unified framework for expressing some well understood single-formula optimizations as well as numerous inter-formula optimizations that capitalize on redundancy, logical implication, and, optionally, model-specific knowledge. It is capable of working either in place of, or as a preprocessor for, other optimization algorithms. The result is a system that, when applied to a potentially heterogeneous collection of formulas over a common problem domain, is able to measurably reduce the time and space requirements of the subsequent model checking engine.

A context-sensitive analysis is an analysis in which program elements are assigned sets of properties that depend upon the context in which they occur. For analyses on imperative languages, this often refers to considering the behavior of statements in a called procedure with respect to the call-stack that generated the procedure invocation. Algorithms for performing or approximating these types of analyses make up the core of interprocedural program analysis and are pervasive; having applications in program comprehension, optimization, and verification. However, for many of these applications what is of interest is the solution to the dual problem: given a vertex and a desirable set of properties, what is the set of potential stack-contexts leading to that vertex that results in the desirable property set? Many techniques, such as procedure cloning, have been developed to approximately partition the set of stack-contexts leading to a vertex according to such a condition. This paper introduces a broad generalization of this problem referred to as a constraint query on the analysis. This generalization allows sophisticated constraints to be placed on both the desirable property set as well as the set of interesting stack-contexts. From these constraints, a novel technique based on manipulating regular languages is introduced that efficiently produces a concise representation of the exact set of stack-contexts solving this dual problem subject to the constraints. This technique is applied to a pair of emerging software engineering challenges - resolving program comprehension queries over aggregate collections of properties and statically modifying code to enforce a safety policy decidable by the analysis. Practical examples of both applications are presented along with empirical results.