Engineering PapersSearch

SEARCH · Engineering Papers

Results for “Lustre”

Search indexed NASA NTRS and DOE OSTI research on propulsion, heat transfer, battery materials and energy systems. Follow report and document links to the original sources.

Quote a phrase for an exact phrase match. Source license links do not imply unrestricted reuse.

I/O Performance Characterization of Lustre and NASA Applications on Pleiades

In this paper we study the performance of the Lustre file system using five scientific and engineering applications representative of NASA workload on large-scale supercomputing systems such as NASA s Pleiades. In order to facilitate the collection of Lustre performance metrics, we have developed a software tool that exports a wide variety of client and server-side metrics using SGI's Performance Co-Pilot (PCP), and generates a human readable report on key metrics at the end of a batch job. These performance metrics are (a) amount of data read and written, (b) number of files opened and closed, and (c) remote procedure call (RPC) size distribution (4 KB to 1024 KB, in powers of 2) for I/O operations. RPC size distribution measures the efficiency of the Lustre client and can pinpoint problems such as small write sizes, disk fragmentation, etc. These extracted statistics are useful in determining the I/O pattern of the application and can assist in identifying possible improvements for users applications. Information on the number of file operations enables a scientist to optimize the I/O performance of their applications. Amount of I/O data helps users choose the optimal stripe size and stripe count to enhance I/O performance. In this paper, we demonstrate the usefulness of this tool on Pleiades for five production quality NASA scientific and engineering applications. We compare the latency of read and write operations under Lustre to that with NFS by tracing system calls and signals. We also investigate the read and write policies and study the effect of page cache size on I/O operations. We examine the performance impact of Lustre stripe size and stripe count along with performance evaluation of file per process and single shared file accessed by all the processes for NASA workload using parameterized IOR benchmark.

Saini, Subhash

Methodology and Application of HPC I/O Characterization with MPIProf and IOT

Combining the strengths of MPIProf and IOT, an efficient and systematic method is devised for I/O characterization at the per-job, per-rank, per-file and per-call levels of HPC programs running on the NASA Advanced Supercomputing Center. This method is applied to answer four I/O questions in this paper. A total of 13 MPI programs and 15 cases, ranging from 24 to 5968 ranks, are analyzed to establish the I/O landscape from answers to the four questions. Four of the 13 programs use MPI I/O and the behavior of their collective writes depends on the specific implementation of the MPI library used. The SGI MPT library, the prevailing MPI library for our systems, was found to gather small writes from a large number of ranks to perform larger writes by a small subset of collective buffering ranks. The number of collective buffering ranks invoked by MPT depends on the Lustre stripe count and the number of nodes used for the run. A demonstration of varying the stripe count to achieve double-digit speedup of one program's I/O was presented. Another program, which concurrently opens private files by all ranks and could potentially create a heavy load on the Lustre servers, was identified. The ability to systematically characterize I/O for a large number of programs running on a supercomputer, seek I/O optimization opportunity and identify programs that could cause a high load and instability on the filesystems is important for pursuing exascale in a real production environment.

Characterization

In Situ Identification of Mineral Resources with an X-Ray-Optical "Hands-Lens" Instrument

The recognition of material resources on a planetary surface requires exploration strategies not dissimilar to those employed by early field geologists who searched for ore deposits primarily from surface clues. In order to determine the location of mineral ores or other materials, it will be necessary to characterize host terranes at regional or subregional scales. This requires geographically broad surveys in which statistically significant numbers of samples are rapidly scanned from a roving platform. To enable broad-scale, yet power-conservative planetary-surface exploration, we are developing an instrument that combines x-ray diffractometry (XRD), x-ray fluorescence spectrometry (XRF), and optical capabilities; the instrument can be deployed at the end of a rover's robotic arm, without the need for sample capture or preparation. The instrument provides XRD data for identification of mineral species and lithological types; diffractometry of minerals is conducted by ascertaining the characteristic lattice parameters or "d-spacings" of mineral compounds. D-spacings of 1.4 to 25 angstroms can be determined to include the large molecular structures of hydrated minerals such as clays. The XRF data will identify elements ranging from carbon (Atomic Number = 6) to elements as heavy as barium (Atomic Number = 56). While a sample is being x-rayed, the instrument simultaneously acquires an optical image of the sample surface at magnifications from lx to at least 50x (200x being feasible, depending on the sample surface). We believe that imaging the sample is extremely important as corroborative sample-identification data (the need for this capability having been illustrated by the experience of the Pathfinder rover). Very few geologists would rely on instrument data for sample identification without having seen the sample. Visual inspection provides critical recognition data such as texture, crystallinity, granularity, porosity, vesicularity, color, lustre, opacity, and so forth. These data can immediately distinguish sedimentary from igneous rocks, for example, and can thus eliminate geochemical or mineral ambiguities arising, say between arkose and granite. It would be important to know if the clay being analyzed was part of a uniform varve deposit laid down in a quiescent lake, or the matrix of a megabreccia diamictite deposited as a catastrophic impact ejecta blanket. The unique design of the instrument, which combines Debye-Scherrer geometry with elements of standard goniometry, negates the need for sample preparation of any kind, and thus negates the need for power-hungry and mechanically-complex sampling systems that would have to chip, crush, sieve, and mount the sample for x-ray analysis. Instead, the instrument is simply rested on the sample surface of interest (like a hand lens); the device can interrogate rough rock surfaces, coarse granular material, or fine rock flour. A breadboard version of the instrument has been deployed from the robotic arm of the Marsokhod rover in field trials at NASA Ames, where large vesicular boulders were x-rayed to demonstrate the functionality of the instrument design, and the ability of such a device to comply with constraints imposed by a roving platform. Currently under development is a flight prototype concept of this instrument that will weigh 0.3 kg, using about 4500 J of energy per sample analysis. It requires about 5 min. for XRD analysis, and about 30 min. for XRF interrogation. Its small mass and rugged design make it ideal for deployment on small rovers of the type currently envisaged for the exploration of Mars (e.g., Sojourner-scale platforms). The design utilizes a monolithic P-N junction photodiode pixel array for XRD, a Si PIN photodiode/avalanche photodiode system for XRF, and an endoscopic imaging camera system unobtrusively embedded between the detectors and the x-ray source (the endoscope with its board-mounted camera can be adapted for IR light in addition to visible wavelenths. A rugged, miniature (7 cu cm) x-ray source for the instrument has already been breadboarded.

Marshall, J.

ADGS-2100 Adaptive Display and Guidance System Window Manager Analysis

Recent advances in modeling languages have made it feasible to formally specify and analyze the behavior of large system components. Synchronous data flow languages, such as Lustre, SCR, and RSML-e are particularly well suited to this task, and commercial versions of these tools such as SCADE and Simulink are growing in popularity among designers of safety critical systems, largely due to their ability to automatically generate code from the models. At the same time, advances in formal analysis tools have made it practical to formally verify important properties of these models to ensure that design defects are identified and corrected early in the lifecycle. This report describes how these tools have been applied to the ADGS-2100 Adaptive Display and Guidance Window Manager being developed by Rockwell Collins Inc. This work demonstrates how formal methods can be easily and cost-efficiently used to remove defects early in the design cycle.

Whalen, Mike W.

Testing-Based Compiler Validation for Synchronous Languages

In this paper we present a novel lightweight approach to validate compilers for synchronous languages. Instead of verifying a compiler for all input programs or providing a fixed suite of regression tests, we extend the compiler to generate a test-suite with high behavioral coverage and geared towards discovery of faults for every compiled artifact. We have implemented and evaluated our approach using a compiler from Lustre to C.

Compiler Validation

NASA Advanced Supercomputing Facility Expansion

The NASA Advanced Supercomputing (NAS) Division enables advances in high-end computing technologies and in modeling and simulation methods to tackle some of the toughest science and engineering challenges facing NASA today. The name "NAS" has long been associated with leadership and innovation throughout the high-end computing (HEC) community. We play a significant role in shaping HEC standards and paradigms, and provide leadership in the areas of large-scale InfiniBand fabrics, Lustre open-source filesystems, and hyperwall technologies. We provide an integrated high-end computing environment to accelerate NASA missions and make revolutionary advances in science. Pleiades, a petaflop-scale supercomputer, is used by scientists throughout the U.S. to support NASA missions, and is ranked among the most powerful systems in the world. One of our key focus areas is in modeling and simulation to support NASA's real-world engineering applications and make fundamental advances in modeling and simulation methods.

NASA

Expanding a Supercomputer Facility Using Modular Data Center Technology

With the expansion of high-end computing resources needed to support NASA's increasing demands for physics-based simulations, the facility housing Pleiades-the agency's largest supercomputer-recently reached its power and cooling capacity. In response, the NASA Advanced Supercomputing Division at Ames Research Center undertook a prototype project that resulted in a new facility based on modular data center technology. The facility, a ~1000 square-foot module on a concrete pad with room for 16-18 compute racks, was completed in fall 2016 and an SGI computer system, named Electra, was deployed there in early 2017. Cooling is performed via an evaporative system built into the module, and preliminary experience shows a Power Usage Effectiveness (PUE) of ~1.03. Electra achieved over a petaflop on the LINPACK benchmark, sufficient to rank number 96 on the November 2016 TOP500 list. The system consists of 1,152 InfiniBand-connected Intel Xeon Broadwell-based nodes. Its users access their files on a facility wide file system shared by all compute assets via Mellanox MetroX InfiniBand extenders, which connect the Electra fabric to Lustre routers InfiniBand fabric over fiber-optic links about 300 meters long. The prototype has exceeded expectations and is serving as a blueprint for future expansions.*†

Facility

Electra: A Modular-Based Expansion of NASA's Supercomputing Capability

NASA has increasingly relied on high-performance computing (HPC) re- sources for computational modeling, simulation, and data analysis to meet the science and engineering goals of its missions in space exploration, aeronautics, and Earth and space science. The NASA Advanced Supercomputing (NAS) Division at Ames Research Center in Silicon Valley, Calif., hosts NASA’s premier supercomputing resources, integral to achieving and enhancing the success of the agency’s missions. NAS provides a balanced environment, funded under the High-End Computing Capability (HECC) project, comprised of world-class supercomputers, including its flagship distributed-memory cluster, Pleiades; high-speed networking; and massive data storage facilities, along with multi-disciplinary support teams for user support, code porting and optimization, and large-scale data analysis and scientific visualization. However, as scientists have increased the fidelity of their simulations and engineers are conducting larger parameter-space studies, the requirements for supercomputing resources have been growing by leaps and bounds. With the facility housing the HECC systems reaching its power and cooling capacity, NAS undertook a prototype project to investigate an alternative approach for housing supercomputers. Modular supercomputing, or container-based computing, is an innovative concept for expanding NASA’s HPC capabilities. With modular supercomputing, additional containers—similar to portable storage pods—can be connected together as needed to accommodate the agency’s ever-increasing demand for computing resources. In addition, taking advantage of the local weather permits the use of cooling technologies that would additionally save energy and reduce annual water usage. The first stage of NASA’s Modular Supercomputing Facility (MSF) prototype, which resulted in a 1,000 square-foot module on a concrete pad with room for 16 compute racks, was completed in Fall 2016 and an SGI (now HPE) computer system, named Electra, was deployed there in early 2017. Cooling is performed via an evaporative system built into the module, and preliminary experience shows a Power Usage Effectiveness (PUE) measurement of 1.03. Electra achieved over a petaflop on the LINPACK benchmark, sufficient to rank number 96 on the November 2016 TOP500 list [14]. The system consists of 1,152 InfiniBand-connected Intel Xeon Broadwell-based nodes. Its users access their files on a facility-wide file system shared by all HECC compute assets via Mellanox MetroX InfiniBand extenders, which connect the Electra fabric to Lustre routers in the primary facility over fiber-optic links about 900 feet long. The MSF prototype has exceeded expectations and is serving as a blueprint for future expansions. In the remainder of this chapter, we detail how modular data center technology can be used to expand an existing compute resource. We begin by describing NASA’s requirements for supercomputing and how resources were provided prior to the integration of the Electra module-based system.

Biswas, Rupak

Integrating Realizability Checking in FRET

Realizability (alternatively referred to as relative consistency or implementability) - checking whether a specification can be implemented by an open system - has been the subject of extensive study. Realizability can be viewed as a stronger analysis method when compared to consistency checking in that it does not only check whether the system works in some environment, but instead whether the system works in all environments. In this report, we experiment and build on the approach presented by Gacek et al. that supports checking realizability of contracts involving infinite theories using SMT solvers. In particular, we 1) extend the Formal Requirements Elicitation Tool (FRET) to support generation of Lustre contracts that can be checked for realizability with the JKind k-induction and fix point generation engines; 2) study a compositional way for checking realizability based on the notion of connected components; and 3) test our approach and the capabilities of the JKind realizability engines on a large subset of the Lockheed Martin Cyber Physical System Challenge Problems.

Kooi, David

CoCoSim, a Code Generation Framework for Control/command Applications: An Overview of CoCoSim for Multi-Periodic Discrete Simulink Models

We present CoCoSim, a framework to support the design, code generation and analysis of discrete dataflow model expressed in Simulink. In this work, we specifically focus on the analysis and code generation of multi-periodic systems. For that CoCoSim provides two complementary approaches: the first amounts to encode the multiperiodic semantics in a pure-synchronous one – à la Lustre–, enabling the use of model checker for verifying properties. The second provides a faithful code generation into multiple communicating (mono)synchronous components – à la Prelude– that can be then simulated or embedded in the final platform with any real-time scheduler. These approaches have been experimented in various settings.

Bourbouh, Hamza

CoCoSim Tutorial: Contract-based Compositional Verification of Simulink Models

This tutorial presents CoCoSim, a verification framework for MATLAB Simulink and Stateflow models. We demonstrate CoCoSim’s architecture, designed to be compatible with Lustre-based verification tools, as well as easily extensible to other candidate backends. We focus on CoCoSim’s powerful compositional verification scheme, which allows for scalable verification through the usage of abstractions of subsystems, express ed in the form of Assume-Guarantee Contracts. We show CoCoSim’s interconnection with NASA’s Formal Requirements Tool (FRET), that enables a seamless transition between authoring and formally verifying requirements for Simulink/Stateflow models. Finally, we discuss work in progress with regards to test case generation options in CoCoSim, demonstrating the generation of MC/DC tests for Simulink artifacts.

Formal Verification

FRET Tutorial

In this tutorial, we present the FRET tool for writing, understanding, formalizing and analyzing requirements. In practice, requirements are typically written in natural language, which is ambiguous and consequently not amenable to formal analysis. Since formal, mathematical notations are unintuitive, requirements in FRET are entered in a restricted, natural language, called FRETish with precise unambiguous meaning. This tutorial explains how requirements can be captured in FRETish and subsequently formalized in temporal logics and in the synchronous data flow language Lustre. We show, through multiple examples, how FRET assists users in understanding FRETish requirements and clarifying subtle semantic issues through English and diagrammatic explanations as well as interactive simulation. FInally, this tutorial describes how FRET can be used to perform realizability checking for identifying conflicting requirements and the connection of FRET with (1) the CoCoSim automated analysis tool for the verification of Simulink and Stateflow models, and (2) the Copilot runtime monitoring tool for the analysis of C programs.

FRET

Global earth mineral inventory: A data legacy

Minerals contain important clues to understanding the complex geologic history of Earth and other planetary bodies. Therefore, geologists have been collecting mineral samples and compiling data about these samples for centuries. These data have been used to better understand the movement of continental plates, the oxidation of Earth's atmosphere and the water regime of ancient martian landscapes. Datasets found at ‘RRUFF.info/Evolution’ and ‘mindat.org’ have documented a wealth of mineral occurrences around the world. One of the main goals in geoinformatics has been to facilitate discovery by creating and merging datasets from various scientific fields and using statistical methods and visualization tools to inspire and test hypotheses applicable to modelling Earth's past environments. To help achieve this goal, we have compiled physical, chemical and geological properties of minerals and linked them to the above-mentioned mineral occurrence datasets. As a part of the Deep Time Data Infrastructure, funded by the W.M. Keck Foundation, with significant support from the Deep Carbon Observatory (DCO) and the A.P. Sloan Foundation, GEMI (‘Global Earth Mineral Inventory’) was developed from the need of researchers to have all of the required mineral data visible in a single portal, connected by a robust, yet easy to understand schema. Our data legacy integrates these resources into a digestible format for exploration and analysis and has allowed researchers to gain valuable insights from mineralogical data. GEMI can be considered a network, with every node representing some feature of the datasets, for example, a node can represent geological parameters like colour, hardness or lustre. Exploring subnetworks gives the researcher a specific view of the data required for the task at hand. GEMI is accessible through the DCO Data Portal (https://dx.deepcarbon.net/11121/6200-6954-6634-8243-CC). We describe our efforts in compiling GEMI, the Data Policies for usage and sharing, and the evaluation metrics for this data legacy.

data legacy

Bridging the Gap Between Requirements and Simulink Model Analysis

Formal veri fication and simulation are powerful tools for the veri fication of requirements against complex systems. Requirements are developed in early stages of the software lifecycle and are typically expressed in natural language. There is a gap between such requirements and their software implementations. We present a framework that bridges this gap by supporting a tight integration and feedback loop between high-level requirements and their analysis against software artifacts. Our framework implements an analysis portal within the fret requirements elicitation tool, thus forming an end-to-end, open-source environment where requirements are written in an intuitive, structured natural language, and are veri fied automatically against Simulink models.

FRET