Showing 1–18 of 18 results for author: Beckett, R

Towards Safer Heuristics With XPlain

Authors: Pantea Karimi, Solal Pirelli, Siva Kesava Reddy Kakarla, Ryan Beckett, Santiago Segarra, Beibin Li, Pooria Namyar, Behnaz Arzani

Abstract: Many problems that cloud operators solve are computationally expensive, and operators often use heuristic algorithms (that are faster and scale better than optimal) to solve them more efficiently. Heuristic analyzers enable operators to find when and by how much their heuristics underperform. However, these tools do not provide enough detail for operators to mitigate the heuristic's impact in prac… ▽ More Many problems that cloud operators solve are computationally expensive, and operators often use heuristic algorithms (that are faster and scale better than optimal) to solve them more efficiently. Heuristic analyzers enable operators to find when and by how much their heuristics underperform. However, these tools do not provide enough detail for operators to mitigate the heuristic's impact in practice: they only discover a single input instance that causes the heuristic to underperform (and not the full set), and they do not explain why. We propose XPlain, a tool that extends these analyzers and helps operators understand when and why their heuristics underperform. We present promising initial results that show such an extension is viable. △ Less

Submitted 19 October, 2024; originally announced October 2024.

Roadmap for Animate Matter

Authors: Giorgio Volpe, Nuno A. M. Araújo, Maria Guix, Mark Miodownik, Nicolas Martin, Laura Alvarez, Juliane Simmchen, Roberto Di Leonardo, Nicola Pellicciotta, Quentin Martinet, Jérémie Palacci, Wai Kit Ng, Dhruv Saxena, Riccardo Sapienza, Sara Nadine, João F. Mano, Reza Mahdavi, Caroline Beck Adiels, Joe Forth, Christian Santangelo, Stefano Palagi, Ji Min Seok, Victoria A. Webster-Wood, Shuhong Wang, Lining Yao , et al. (15 additional authors not shown)

Abstract: Humanity has long sought inspiration from nature to innovate materials and devices. As science advances, nature-inspired materials are becoming part of our lives. Animate materials, characterized by their activity, adaptability, and autonomy, emulate properties of living systems. While only biological materials fully embody these principles, artificial versions are advancing rapidly, promising tra… ▽ More Humanity has long sought inspiration from nature to innovate materials and devices. As science advances, nature-inspired materials are becoming part of our lives. Animate materials, characterized by their activity, adaptability, and autonomy, emulate properties of living systems. While only biological materials fully embody these principles, artificial versions are advancing rapidly, promising transformative impacts across various sectors. This roadmap presents authoritative perspectives on animate materials across different disciplines and scales, highlighting their interdisciplinary nature and potential applications in diverse fields including nanotechnology, robotics and the built environment. It underscores the need for concerted efforts to address shared challenges such as complexity management, scalability, evolvability, interdisciplinary collaboration, and ethical and environmental considerations. The framework defined by classifying materials based on their level of animacy can guide this emerging field encouraging cooperation and responsible development. By unravelling the mysteries of living matter and leveraging its principles, we can design materials and systems that will transform our world in a more sustainable manner. △ Less

Submitted 10 September, 2024; v1 submitted 15 July, 2024; originally announced July 2024.

Oracle-based Protocol Testing with Eywa

Authors: Siva Kesava Reddy Kakarla, Ryan Beckett

Abstract: We present oracle-based testing a new technique for automatic black-box testing of network protocol implementations. Oracle-based testing leverages recent advances in LLMs to build rich models of intended protocol behavior from knowledge embedded in RFCs, blogs, forums, and other natural language sources. From these models it systematically derives exhaustive test cases using symbolic program exec… ▽ More We present oracle-based testing a new technique for automatic black-box testing of network protocol implementations. Oracle-based testing leverages recent advances in LLMs to build rich models of intended protocol behavior from knowledge embedded in RFCs, blogs, forums, and other natural language sources. From these models it systematically derives exhaustive test cases using symbolic program execution. We realize oracle-based testing through Eywa, a novel protocol testing framework implemented in Python. To demonstrate Eywa's effectiveness, we show its use through an extensive case study of the DNS protocol. Despite requiring minimal effort, applying Eywa to the DNS resulting in the discovery of 26 unique bugs across ten widely used DNS implementations, including 11 new bugs that were previously undiscovered despite elaborate prior testing with manually crafted models. △ Less

Submitted 11 December, 2023; originally announced December 2023.

Finding Adversarial Inputs for Heuristics using Multi-level Optimization

Authors: Pooria Namyar, Behnaz Arzani, Ryan Beckett, Santiago Segarra, Himanshu Raj, Umesh Krishnaswamy, Ramesh Govindan, Srikanth Kandula

Abstract: Production systems use heuristics because they are faster or scale better than their optimal counterparts. Yet, practitioners are often unaware of the performance gap between a heuristic and the optimum or between two heuristics in realistic scenarios. We present MetaOpt, a system that helps analyze heuristics. Users specify the heuristic and the optimal (or another heuristic) as input, and MetaOp… ▽ More Production systems use heuristics because they are faster or scale better than their optimal counterparts. Yet, practitioners are often unaware of the performance gap between a heuristic and the optimum or between two heuristics in realistic scenarios. We present MetaOpt, a system that helps analyze heuristics. Users specify the heuristic and the optimal (or another heuristic) as input, and MetaOpt automatically encodes these efficiently for a solver to find performance gaps and their corresponding adversarial inputs. Its suite of built-in optimizations helps it scale its analysis to practical problem sizes. To show it is versatile, we used MetaOpt to analyze heuristics from three domains (traffic engineering, vector bin packing, and packet scheduling). We found a production traffic engineering heuristic can require 30% more capacity than the optimal to satisfy realistic demands. Based on the patterns in the adversarial inputs MetaOpt produced, we modified the heuristic to reduce its performance gap by 12.5$\times$. We examined adversarial inputs to a vector bin packing heuristic and proved a new lower bound on its performance. △ Less

Submitted 21 November, 2023; originally announced November 2023.

Kivi: Verification for Cluster Management

Authors: Bingzhe Liu, Gangmuk Lim, Ryan Beckett, P. Brighten Godfrey

Abstract: Modern cloud infrastructure is powered by cluster management systems such as Kubernetes and Docker Swarm. While these systems seek to minimize users' operational burden, the complex, dynamic, and non-deterministic nature of these systems makes them hard to reason about, potentially leading to failures ranging from performance degradation to outages. We present Kivi, the first system for verifying… ▽ More Modern cloud infrastructure is powered by cluster management systems such as Kubernetes and Docker Swarm. While these systems seek to minimize users' operational burden, the complex, dynamic, and non-deterministic nature of these systems makes them hard to reason about, potentially leading to failures ranging from performance degradation to outages. We present Kivi, the first system for verifying controllers and their configurations in cluster management systems. Kivi focuses on the popular system Kubernetes, and models its controllers and events into processes whereby their interleavings are exhaustively checked via model checking. Central to handling autoscaling and large-scale deployments is our design that seeks to find violations in a smaller and reduced topology. We also develop several model optimizations in Kivi to scale to large clusters. We show that Kivi is effective and accurate in finding issues in realistic and complex scenarios and showcase two new issues in Kubernetes controller source code. △ Less

Submitted 5 November, 2023; originally announced November 2023.

Comments: 18 pages

What do LLMs need to Synthesize Correct Router Configurations?

Authors: Rajdeep Mondal, Alan Tang, Ryan Beckett, Todd Millstein, George Varghese

Abstract: We investigate whether Large Language Models (e.g., GPT-4) can synthesize correct router configurations with reduced manual effort. We find GPT-4 works very badly by itself, producing promising draft configurations but with egregious errors in topology, syntax, and semantics. Our strategy, that we call Verified Prompt Programming, is to combine GPT-4 with verifiers, and use localized feedback from… ▽ More We investigate whether Large Language Models (e.g., GPT-4) can synthesize correct router configurations with reduced manual effort. We find GPT-4 works very badly by itself, producing promising draft configurations but with egregious errors in topology, syntax, and semantics. Our strategy, that we call Verified Prompt Programming, is to combine GPT-4 with verifiers, and use localized feedback from the verifier to automatically correct errors. Verification requires a specification and actionable localized feedback to be effective. We show results for two use cases: translating from Cisco to Juniper configurations on a single router, and implementing no-transit policy on multiple routers. While human input is still required, if we define the leverage as the number of automated prompts to the number of human prompts, our experiments show a leverage of 10X for Juniper translation, and 6X for implementing no-transit policy, ending with verified configurations. △ Less

Submitted 10 July, 2023; originally announced July 2023.

Thermochemical Stability of Low-Iron, Manganese-Enriched Olivine in Astrophysical Environments

Authors: Denton S. Ebel, Michael K. Weisberg, John R. Beckett

Abstract: Low-iron, manganese-enriched (LIME) olivine grains are found in cometary samples returned by the Stardust mission to comet 81P/Wild 2. Similar grains are found in primitive meteoritic clasts and unequilibrated meteorite matrix. LIME olivine is thermodynamically stable in a vapor of solar composition at high temperature at total pressures of a millibar to a microbar, but enrichment of solar composi… ▽ More Low-iron, manganese-enriched (LIME) olivine grains are found in cometary samples returned by the Stardust mission to comet 81P/Wild 2. Similar grains are found in primitive meteoritic clasts and unequilibrated meteorite matrix. LIME olivine is thermodynamically stable in a vapor of solar composition at high temperature at total pressures of a millibar to a microbar, but enrichment of solar composition vapor in a dust of chondritic composition causes the FeO/MnO ratio of olivine to increase. The compositions of LIME olivines in primitive materials indicate oxygen fugacities close to that of a very reducing vapor of solar composition. The compositional zoning of LIME olivines in amoeboid olivine aggregates is consistent with equilibration with nebular vapor in the stability field of olivine, without reequilibration at lower temperatures. A similar history is likely for LIME olivines found in comet samples and in interplanetary dust particles. LIME olivine is not likely to persist in nebular conditions in which silicate liquids are stable. △ Less

Submitted 2 July, 2023; originally announced July 2023.

Comments: 15 pages, 5 figures

Journal ref: Meteoritics and Planetary Sciences 47, 585-593 (2012)

Test Coverage for Network Configurations

Authors: Xieyang Xu, Weixin Deng, Ryan Beckett, Ratul Mahajan, David Walker

Abstract: We develop NetCov, the first tool to reveal which network configuration lines are being tested by a suite of network tests. It helps network engineers improve test suites and thus increase network reliability. A key challenge in its development is that many network tests test the data plane instead of testing the configurations (control plane) directly. We must be able to efficiently infer which c… ▽ More We develop NetCov, the first tool to reveal which network configuration lines are being tested by a suite of network tests. It helps network engineers improve test suites and thus increase network reliability. A key challenge in its development is that many network tests test the data plane instead of testing the configurations (control plane) directly. We must be able to efficiently infer which configuration elements contribute to tested data plane elements, even when such contributions are non-local (on remote devices) or non-deterministic. NetCov uses an information flow graph based model that precisely captures various forms of contributions and a scalable method to lazily infer contributions. Using it, we show that an existing test suite for Internet2 (a nation-wide backbone network in the USA) covers only 26% of the configuration lines. The feedback from NetCov makes it easy to define new tests that improve coverage. For Internet2, adding just three such tests covers an additional 17% of the lines. △ Less

Submitted 26 September, 2022; originally announced September 2022.

FP4: Line-rate Greybox Fuzz Testing for P4 Switches

Authors: Nofel Yaseen, Liangcheng Yu, Caleb Stanford, Ryan Beckett, Vincent Liu

Abstract: Compared to fixed-function switches, the flexibility of programmable switches comes at a cost, as programmer mistakes frequently result in subtle bugs in the network data plane. In this paper, we present the design and implementation of FP4, a fuzz-testing framework for P4 switches that achieves high expressiveness, coverage, and scalability. FP4 directly tests running switches by generating sem… ▽ More Compared to fixed-function switches, the flexibility of programmable switches comes at a cost, as programmer mistakes frequently result in subtle bugs in the network data plane. In this paper, we present the design and implementation of FP4, a fuzz-testing framework for P4 switches that achieves high expressiveness, coverage, and scalability. FP4 directly tests running switches by generating semi-random input packets and observing their resulting execution in the data plane. To achieve high coverage and scalability, at runtime, FP4 leverages P4 itself with another "tester" switch that generates and mutates billions of test packets per second entirely in the dataplane. Because testing some program branches requires navigating complex semantic input requirements, FP4 additionally leverages the programmability of P4 by instrumenting the tested program to pass coverage information back to the tester through the packet header. We present case studies showing that FP4 can validate both safety and stateful properties, improves efficiency over existing random packet generation baselines, and reaches 100% coverage in under a minute on a wide range of examples. △ Less

Submitted 26 July, 2022; originally announced July 2022.

ACORN: Network Control Plane Abstraction using Route Nondeterminism

Authors: Divya Raghunathan, Ryan Beckett, Aarti Gupta, David Walker

Abstract: Networks are hard to configure correctly, and misconfigurations occur frequently, leading to outages or security breaches. Formal verification techniques have been applied to guarantee the correctness of network configurations, thereby improving network reliability. This work addresses verification of distributed network control planes, with two distinct contributions to improve the scalability of… ▽ More Networks are hard to configure correctly, and misconfigurations occur frequently, leading to outages or security breaches. Formal verification techniques have been applied to guarantee the correctness of network configurations, thereby improving network reliability. This work addresses verification of distributed network control planes, with two distinct contributions to improve the scalability of formal verification. Our first contribution is a hierarchy of abstractions of varying precision which introduce nondeterminism into the route selection procedure that routers use to select the best available route. We prove the soundness of these abstractions and show their benefits. Our second contribution is a novel SMT encoding which uses symbolic graphs to encode all possible stable routing trees that are compliant with the given network control plane configurations. We have implemented our abstractions and SMT encodings in a prototype tool called ACORN. Our evaluations show that our abstractions can provide significant relative speedups (up to 323x) in performance, and ACORN can scale up to $\approx37,000$ routers (organized in FatTree topologies, with synthesized shortest-path routing and valley-free policies) for verifying reachability. This far exceeds the performance of existing tools for control plane verification. △ Less

Submitted 5 June, 2022; originally announced June 2022.

Comments: 23 pages, 10 figures

Modular Control Plane Verification via Temporal Invariants

Authors: Timothy Alberdingk Thijm, Ryan Beckett, Aarti Gupta, David Walker

Abstract: 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. Wh… ▽ More 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 naively 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. △ Less

Submitted 8 April, 2023; v1 submitted 21 April, 2022; originally announced April 2022.

Comments: 27 pages (22 pages body, ~3 pages references, ~1 page proofs), 14 figures, accepted to PLDI 2023

ACM Class: C.2.2; D.2.4; F.3.1

LIGHTYEAR: Using Modularity to Scale BGP Control Plane Verification

Authors: Alan Tang, Ryan Beckett, Steven Benaloh, Karthick Jayaraman, Tejas Patil, Todd Millstein, George Varghese

Abstract: Current network control plane verification tools cannot scale to large networks, because of the complexity of jointly reasoning about the behaviors of all nodes in the network. In this paper we present a modular approach to control plane verification, whereby end-to-end network properties are verified via a set of purely local checks on individual nodes and edges. The approach targets the verifica… ▽ More Current network control plane verification tools cannot scale to large networks, because of the complexity of jointly reasoning about the behaviors of all nodes in the network. In this paper we present a modular approach to control plane verification, whereby end-to-end network properties are verified via a set of purely local checks on individual nodes and edges. The approach targets the verification of safety properties for BGP configurations and provides guarantees in the face of both arbitrary external route announcements from neighbors and arbitrary node/link failures. We have proven the approach correct and also implemented it in a tool called Lightyear. Experimental results show that Lightyear scales dramatically better than prior control plane verifiers. Further, we have used Lightyear to verify three properties of the wide area network of a major cloud provider, containing hundreds of routers and tens of thousands of edges. To our knowledge no prior tool has been demonstrated to provide such guarantees at that scale. Finally, in addition to the scaling benefits, our modular approach to verification makes it easy to localize the causes of configuration errors and to support incremental re-verification as configurations are updated. △ Less

Submitted 20 September, 2023; v1 submitted 20 April, 2022; originally announced April 2022.

Comments: 12 pages (+ 2 pages references), 3 figures, Accepted at SIGCOMM '23

Journal ref: In Proceedings of the ACM SIGCOMM 2023 Conference (ACM SIGCOMM '23). Association for Computing Machinery, New York, NY, USA, 94-107

Kirigami, the Verifiable Art of Network Cutting

Authors: Tim Alberdingk Thijm, Ryan Beckett, Aarti Gupta, David Walker

Abstract: We introduce a modular verification approach to network control plane verification, where we cut a network into smaller fragments to improve the scalability of SMT solving. Users provide an annotated cut which describes how to generate these fragments from the monolithic network, and we verify each fragment independently, using the annotations to define assumptions and guarantees over fragments ak… ▽ More We introduce a modular verification approach to network control plane verification, where we cut a network into smaller fragments to improve the scalability of SMT solving. Users provide an annotated cut which describes how to generate these fragments from the monolithic network, and we verify each fragment independently, using the annotations to define assumptions and guarantees over fragments akin to assume-guarantee reasoning. We prove this modular network verification procedure is sound and complete with respect to verification over the monolithic network. We implement this procedure as Kirigami, an extension of NV - a network verification language and tool - and evaluate it on industrial topologies with synthesized policies. We observe a 2-8x improvement in end-to-end NV verification time, with SMT solve time improving by up to 6 orders of magnitude. △ Less

Submitted 12 February, 2022; originally announced February 2022.

Comments: 30 pages, 9 figures, submitted to CAV 2022

ACM Class: C.2.2; D.2.4; F.3.1

IoT Skullfort: Exploring the Impact of Internet Connected Cosplay

Authors: Rhys Beckett, Charith Perera

Abstract: In this paper, we explore the potential impact of Internet of Things (IoT) technology may have on the cosplay community. We developed a costume (an IoT Skullfort) and embedded IoT technology to enhance its capabilities and user interactions. Sensing technologies are widely used in many different wearable domains including cosplay scenarios. However, in most of these scenarios, typical interaction… ▽ More In this paper, we explore the potential impact of Internet of Things (IoT) technology may have on the cosplay community. We developed a costume (an IoT Skullfort) and embedded IoT technology to enhance its capabilities and user interactions. Sensing technologies are widely used in many different wearable domains including cosplay scenarios. However, in most of these scenarios, typical interaction pattern is that the costume responds to its environment or the player's behaviour (e.g., colour of lights may get changed when player moves hands). In contrast, our research focuses on exploring scenarios where the audience (third party) get to manipulate the costume behaviour (e.g., the audience get to change the colour of the Skullfort using a mobile application). We believe such an audience (third party) influenced cosplay brings new opportunities for enhanced entertainment. However, it also creates significant challenges. We report the results gathered through a focus group conducted in collaboration with cosplay community experts. △ Less

Submitted 8 July, 2019; v1 submitted 28 May, 2019; originally announced June 2019.

Journal ref: Proceedings of the 2019 ACM International Joint Conference and 2019 International Symposium on Pervasive and Ubiquitous Computing and Wearable Computers

Contra: A Programmable System for Performance-aware Routing

Authors: Kuo-Feng Hsu, Ryan Beckett, Ang Chen, Jennifer Rexford, Praveen Tammana, David Walker

Abstract: We present Contra, a system for performance-aware routing that can adapt to traffic changes at hardware speeds. While existing work has developed point solutions for performance-aware routing on a fixed topology (e.g., a Fattree) with a fixed routing policy (e.g., use least utilized paths), Contra can be configured to operate seamlessly over any network topology and a wide variety of sophisticated… ▽ More We present Contra, a system for performance-aware routing that can adapt to traffic changes at hardware speeds. While existing work has developed point solutions for performance-aware routing on a fixed topology (e.g., a Fattree) with a fixed routing policy (e.g., use least utilized paths), Contra can be configured to operate seamlessly over any network topology and a wide variety of sophisticated routing policies. Users of Contra write network-wide policies that rank network paths given their current performance. A compiler then analyzes such policies in conjunction with the network topology and decomposes them into switch-local P4 programs, which collectively implement a new, specialized distance-vector protocol. This protocol generates compact probes that traverse the network, gathering path metrics to optimize for the user policy dynamically. Switches respond to changing network conditions at hardware speeds by routing flowlets along the best policy-compliant paths. Our experiments show that Contra scales to large networks, and that in terms of flow completion times, it is competitive with hand-crafted systems that have been customized for specific topologies and policies. △ Less

Submitted 3 February, 2019; originally announced February 2019.

Control Plane Compression

Authors: Ryan Beckett, Aarti Gupta, Ratul Mahajan, David Walker

Abstract: We develop an algorithm capable of compressing large networks into a smaller ones with similar control plane behavior: For every stable routing solution in the large, original network, there exists a corresponding solution in the compressed network, and vice versa. Our compression algorithm preserves a wide variety of network properties including reachability, loop freedom, and path length. Conseq… ▽ More We develop an algorithm capable of compressing large networks into a smaller ones with similar control plane behavior: For every stable routing solution in the large, original network, there exists a corresponding solution in the compressed network, and vice versa. Our compression algorithm preserves a wide variety of network properties including reachability, loop freedom, and path length. Consequently, operators may speed up network analysis, based on simulation, emulation, or verification, by analyzing only the compressed network. Our approach is based on a new theory of control plane equivalence. We implement these ideas in a tool called Bonsai and apply it to real and synthetic networks. Bonsai can shrink real networks by over a factor of 5 and speed up analysis by several orders of magnitude. △ Less

Submitted 22 June, 2018; originally announced June 2018.

Comments: Extended version of the paper appearing in ACM SIGCOMM 2018

Kleene Algebra Modulo Theories

Authors: Michael Greenberg, Ryan Beckett, Eric Campbell

Abstract: Kleene algebras with tests (KATs) offer sound, complete, and decidable equational reasoning about regularly structured programs. Interest in KATs has increased greatly since NetKAT demonstrated how well extensions of KATs with domain-specific primitives and extra axioms apply to computer networks. Unfortunately, extending a KAT to a new domain by adding custom primitives, proving its equational th… ▽ More Kleene algebras with tests (KATs) offer sound, complete, and decidable equational reasoning about regularly structured programs. Interest in KATs has increased greatly since NetKAT demonstrated how well extensions of KATs with domain-specific primitives and extra axioms apply to computer networks. Unfortunately, extending a KAT to a new domain by adding custom primitives, proving its equational theory sound and complete, and coming up with an efficient implementation is still an expert's task. Abstruse metatheory is holding back KAT's potential. We offer a fast path to a "minimum viable model" of a KAT, formally or in code through our framework, Kleene algebra modulo theories (KMT). Given primitives and a notion of state, we can automatically derive a corresponding KAT's semantics, prove its equational theory sound and complete with respect to a tracing semantics (programs are denoted as traces of states), and derive a normalization-based decision procedure for equivalence checking. Our framework is based on pushback, a generalization of weakest preconditions that specifies how predicates and actions interact. We offer several case studies, showing tracing variants of theories from the literature (bitvectors, NetKAT) along with novel compositional theories (products, temporal logic, and sets). We derive new results over unbounded state, reasoning about monotonically increasing, unbounded natural numbers. Our OCaml implementation closely matches the theory: users define and compose KATs with the module system. △ Less

Submitted 4 April, 2022; v1 submitted 10 July, 2017; originally announced July 2017.

Comments: PLDI 2022

Dependence of the superconducting transition temperature of single- and polycrystalline MgB2 on hydrostatic pressure

Authors: S. Deemyad, T. Tomita, J. J. Hamlin, B. R. Beckett, J. S. Schilling, D. G. Hinks, J. D. Jorgensen, S. Lee, S. Tajima

Abstract: The dependence of Tc for MgB2 on purely hydrostatic or nearly hydrostatic pressure has been determined to 23 GPa for single-crystalline and to 32 GPa for polycrystalline samples, and found to be in good agreement. Tc decreases from 39 K at ambient pressure to 15 K at 32 GPa with an initial slope dTc/dP = -1.11(2) K/GPa. Evidence is presented that the differing values of dTc/dP reported in the li… ▽ More The dependence of Tc for MgB2 on purely hydrostatic or nearly hydrostatic pressure has been determined to 23 GPa for single-crystalline and to 32 GPa for polycrystalline samples, and found to be in good agreement. Tc decreases from 39 K at ambient pressure to 15 K at 32 GPa with an initial slope dTc/dP = -1.11(2) K/GPa. Evidence is presented that the differing values of dTc/dP reported in the literature result primarily from shear-stress effects in nonhydrostatic pressure media and not differences in the samples. Although comparison of these results with theory supports phonon-mediated superconductivity, a critical test of theory must await volume-dependent calculations based on the solution of the anisotropic Eliashberg equations. △ Less

Submitted 11 September, 2002; originally announced September 2002.

Comments: Invited paper for a special edition of Physica on MgB2

Journal ref: Physica C 385, 105 (2003)