Search for: All records

Networking researchers and engineers spend much of their time trying to understand the performance of contention points---network components where multiple incoming packet streams share the same outgoing link(s). Recently, researchers have developed new logical models for analyzing such contention points, but unfortunately, such models are expensive: They do not scale well as buffer capacities increase beyond 10s of packets, making it difficult or impossible to reason about real-world systems faithfully. In this paper, we develop a suite of effective, new abstractions for reasoning about buffers and their performance characteristics. We also show how to architect a performance analysis framework for contention points in a modular way so it can take advantage of a range of abstractions that trade performance off against precision. We evaluate our abstractions against a collection of benchmarks and demonstrate their scaling benefits. 

C−H terminated nanometer scale diamonds (d = 1 to 15 nm) are synthesized from 1-fluoroadamantane at high pressure (6−8 GPa) and high temperature (500−1500 °C) in a multianvil press. High resolution transmission electron microscopy, X-ray diffraction, Raman, diffuse reflectance Fourier transform infrared, and X-ray absorption spectroscopies demonstrate the excellent crystallinity and atomically flat C−H terminated surfaces of nanodiamonds with (111) and (110) facets. The importance of hydrogen to the synthesis of nanodiamond and its faceting is discussed. Following vacancy generation, annealing and oxidation of the nanodiamonds, optically detected magnetic resonance and electron spin resonance coherence times (T2 = 0.9 and 2.1 μs) of nitrogen vacancy (NV) centers are measured. The obtained T2 values are equivalent to the shallow NV centers (depth <10 nm) in bulk diamond crystals and larger nanocrystals prepared by mechanical milling. 

Satisfiability Modulo Theories (SMT)-based analysis allows exhaustive reasoning over complex distributed control plane routing behaviors, enabling verification of converged routing states under arbitrary conditions. To improve scalability of SMT solving, we introduce a modular verification approach to network control plane verification, where we cut a network into smaller fragments. Users specify an annotated cut which describes how to generate these fragments from the monolithic network, and we verify each fragment independently, using these annotations to define assumptions and guarantees over fragments akin to assume-guarantee reasoning. We prove that any converged states of the fragments are converged states of the monolithic network, and there exists an annotated cut that can generate fragments corresponding to any converged state of the monolithic network. We implement this procedure as Kirigami, an extension of the network verification language and tool NV, and evaluate it on industrial topologies with synthesized policies. We observe a 10x improvement in end-to-end NV verification time, with SMT solve time improving by up to 6 orders of magnitude. 

Relational network verification is a new approach for validating network changes. In contrast to traditional network verification, which analyzes specifications for a single network snapshot, it analyzes specifications that capture similarities and differences between two network snapshots (e.g., pre- and post-change snapshots). Relational specifications are compact and precise because they focus on the flows and paths that change between snapshots and then simply mandate that all other network behaviors "stay the same", without enumerating them. To achieve similar guarantees, single-snapshot specifications would need to enumerate all flow and path behaviors that are not expected to change in order to enable checking that nothing has accidentally changed. Such specifications are proportional to network size, which makes them impractical to generate for many real-world networks. We demonstrate the value of relational reasoning by developing Rela, a high-level relational specification language and verification tool for network changes. Rela compiles input specifications and network snapshot representations to finite state automata, and it then verifies compliance by checking automaton equivalence. Our experiments using data from a global backbone with over 103 routers find that Rela specifications need fewer than 10 terms for 93% of the complex, high-risk changes. Rela validates 80% of the changes within 20 minutes. 

Two new compounds, Zn2FeSbO6 and Zn2MnSbO6, have been synthesized under high-pressure and high-temperature conditions. The synthesis, single-crystal and powder X-ray diffraction, X-ray absorption near-edge spectroscopy (XANES), optical second harmonic generation (SHG), and magnetic and heat capacity measurements were carried out for both compounds and are described. The lattice parameters are a = 5.17754(6) Å and c = 13.80045(16) Å for Zn2FeSbO6 and a = 5.1889(10) Å and c = 14.0418(3) Å for Zn2MnSbO6. Single-crystal X-ray diffraction analyses indicate that Zn2FeSbO6 consists of a cocrystal of superimposed Ni3TeO6 (NTO) and ordered ilmenite (OIL) components with a ratio of approximately 2:1 and Zn2MnSbO6 contains two nearly identical, but noncrystallographically related, OIL components in a ratio of approximately 6:1. 

We develop FLM, a high-level language that enables network operators to write programs that recognize and react to specific packet sequences. To be able to examine every packet, our compilation procedure can transform FLM programs into P4 code that can run on programmable switch ASICs. It first splits FLM programs into a state management component and a classical regular expression, then generates an efficient implementation of the regular expression using SMT-based program synthesis. Our experiments find that FLM can express 15 sequence monitoring tasks drawn from prior literature. Our compiler can convert all of these programs to run on switch hardware in way that fit within available pipeline stages and consume less than 15% additional header fields and instruction words when run alongside switch programs. 

Monolithic control plane verification cannot scale to hyperscale network architectures with tens of thousands of nodes, heterogeneous network policies and thousands of network changes a day. Instead, modular verification offers improved scalability, reasoning over diverse behaviors, and robustness following policy updates. We introduce Timepiece, a new modular control plane verification system. While one class of verifiers, starting with Minesweeper, were based on analysis of stable paths, we show that such models, when deployed naïvely for modular verification, are unsound. To rectify the situation, we adopt a routing model based around a logical notion of time and develop a sound, expressive, and scalable verification engine. Our system requires that a user specifies interfaces between module components. We develop methods for defining these interfaces using predicates inspired by temporal logic, and show how to use those interfaces to verify a range of network-wide properties such as reachability or access control. Verifying a prefix-filtering policy using a non-modular verification engine times out on an 80-node fattree network after 2 hours. However, Timepiece verifies a 2,000-node fattree in 2.37 minutes on a 96-core virtual machine. Modular verification of individual routers is embarrassingly parallel and completes in seconds, which allows verification to scale beyond non-modular engines, while still allowing the full power of SMT-based symbolic reasoning.