Engineering Papers⌕ Search

SEARCH · Engineering Papers

Results for “compiler verification”

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.

At least 19 records
All sourcesNASA NTRSDOE OSTI
DOE OSTI2022

EXFOR-NSR PDF database: a system for nuclear knowledge preservation and data curation

Current needs of nuclear science and technology include complete, well-documented, and easily verifiable nuclear data. The complete data records require supporting nuclear bibliography, presently stored in dedicated libraries, in addition, to actual data. Additionally, experimental nuclear reaction data (EXFOR) and Nuclear Science References (NSR) databases contain compilations based on primary (journals) and secondary (conference proceedings, theses, preprints, etc.) publications, and data received from authors via private communications. The secondary library materials and private communications often represent a bottleneck for nuclear data verification, compilation, evaluation, and dissemination activities. To address this issue, bibliographic materials were scanned into PDF (Portable Document Format) files and uploaded in a relational database. The traditional scope of nuclear databases that includes meta-data and numbers derived from data in specialized formats was broadened to accommodate the large volumes of original nuclear data publications. The complete PDF publication files were stored in a relational database as Binary Large OBjects (BLOB). This unique collection of nuclear data compilations and supporting publications generate many opportunities for machine learning applications. The Web interfaces for authorized and public access to the EXFOR-NSR nuclear publications database were implemented at the U.S. National Nuclear Data Center, https://www.nndc.bnl.gov/ and IAEA Nuclear Data Section, https://www-nds.iaea.org/ . The current system is complementary to major nuclear libraries and narrowly focused on nuclear data compilation and evaluation procedures. The contents of the PDF database, details of implementation, and Web interface are described. New capabilities for data curation, knowledge preservation, worldwide dissemination, and natural language processing (NLP) applications are given.

73 NUCLEAR PHYSICS AND RADIATION PHYSICS↗
NASA NTRS1975

CARETS: A prototype regional environmental information system. Volume 5: Interpretation, compilation and field verification procedures in the CARETS project

The production of the CARETS map data base involved the development of a series of procedures for interpreting, compiling, and verifying data obtained from remote sensor sources. Level II land use mapping from high-altitude aircraft photography at a scale of 1:100,000 required production of a photomosaic mapping base for each of the 48, 50 x 50 km sheets, and the interpretation and coding of land use polygons on drafting film overlays. CARETS researchers also produced a series of 1970 to 1972 land use change overlays, using the 1970 land use maps and 1972 high-altitude aircraft photography. To enhance the value of the land use sheets, researchers compiled series of overlays showing i cultural features, county boundaries and census tracts, surface geology, and drainage basins. In producing Level I land use maps from Landsat imagery, at a scale I of 1:250,000, interpreters overlaid drafting film directly on Landsat color composite transparencies and interpreted on the film. They found that such interpretation involves pattern and spectral signature recognition. In studies using Landsat imagery, interpreters identified numerous areas of change but also identified extensive areas of "false change," where Landsat spectral signatures but not land use had changed.

Field verification procedures↗
DOE OSTI2022

Giallar: push-button verification for the qiskit Quantum compiler

This paper presents Giallar, a fully-automated verification toolkit for quantum compilers. Giallar requires no manual specifications, invariants, or proofs, and can automatically verify that a compiler pass preserves the semantics of quantum circuits. To deal with unbounded loops in quantum compilers, Giallar abstracts three loop templates, whose loop invariants can be automatically inferred. To efficiently check the equivalence of arbitrary input and output circuits that have complicated matrix semantics representation, Giallar introduces a symbolic representation for quantum circuits and a set of rewrite rules for showing the equivalence of symbolic quantum circuits. With Giallar, we implemented and verified 44 (out of 56) compiler passes in 13 versions of the Qiskit compiler, the open-source quantum compiler standard, during which three bugs were detected in and confirmed by Qiskit. Furthermore, our evaluation shows that most of Qiskit compiler passes can be automatically verified in seconds and verification imposes only a modest overhead to compilation performance.

automated verification↗
DOE OSTI2022

Towards Ultra-high-resolution E3SM Land Modeling on Exascale Computers

Here we present an ultra-high-resolution E3SM land model (uELM) for high-fidelity land simulations targeting new Exascale computers. After considering modeling infrastructure compatibility and ELM software features, we designed a parallel model for the uELM development targeting hybrid architectures of new US Exascale computers. We also described a function unit test framework to expedite the piece-wise code porting (with compiler directives), verification, and global variable management. Furthermore, in this study, we report an early uELM model development using OpenACC within a function unit test framework on a pre-Exascale computer, demonstrate the performance of a uLEM submodel with a 3.0-time speedup, and summarize the code porting experience regarding global variable handling, deepcopy, memory reduction, and parallel loop reconstruction.

97 MATHEMATICS AND COMPUTING↗
NASA NTRS2014

Evolution of Software-Only-Simulation at NASA IV and V

Software-Only-Simulations have been an emerging but quickly developing field of study throughout NASA. The NASA Independent Verification Validation (IVV) Independent Test Capability (ITC) team has been rapidly building a collection of simulators for a wide range of NASA missions. ITC specializes in full end-to-end simulations that enable developers, VV personnel, and operators to test-as-you-fly. In four years, the team has delivered a wide variety of spacecraft simulations that have ranged from low complexity science missions such as the Global Precipitation Management (GPM) satellite and the Deep Space Climate Observatory (DSCOVR), to the extremely complex missions such as the James Webb Space Telescope (JWST) and Space Launch System (SLS).This paper describes the evolution of ITCs technologies and processes that have been utilized to design, implement, and deploy end-to-end simulation environments for various NASA missions. A comparison of mission simulators are discussed with focus on technology and lessons learned in complexity, hardware modeling, and continuous integration. The paper also describes the methods for executing the missions unmodified flight software binaries (not cross-compiled) for verification and validation activities.

Embedded↗
DOE OSTI2022

ECP SOLLVE: Validation and Verification Testsuite Status Update and Compiler Insight for OpenMP

The OpenMP language continues to evolve with every new specification release, as does the need to validate and verify the new features that have been implemented by the different vendors. With the release of OpenMP 5.0 and OpenMP 5.1, new target offload and host-based features have been introduced to the programming model. While OpenMP continues to grow in maturity, there is an observable growth in the number of compiler and hardware vendors that support OpenMP. In this manuscript, the main focus is on evaluating the conformity and OpenMP implementation progress of various compiler vendors such as Cray, IBM, GNU, Clang/LLVM, NVIDIA, and Intel. More specifically, the 4.5, 5.0, and 5.1 versions of the OpenMP specification are analyzed. For our experimental setup, the Crusher and Summit computing systems hosted by Oak Ridge National Lab’s Computing Facilities are utilized. The effort of vendor agnostic analysis of these implementations is especially valuable for application developers who are using new OpenMP features to accelerate their scientific codes. Insights are presented into the current implementation status of various vendors, the progression of specific compiler’s support for OpenMP overtime, the subset of OpenMP 4.5, 5.0, and 5.1 that is supported by all compilers, and examples of how our test suite has influenced discussion regarding the correct interpretation of the OpenMP specification. By evaluating OpenMP conformity of pre-Exascale computing systems, the aim is to detail progress and status of AMD + Cray ecosystem before the system and their OpenMP implementation is used for mission critical applications when the first Exascale Computer Frontier is made available to applications.

Huber, Thomas↗
NASA NTRSDate not supplied

Runtime Verification with Ogma

Ultra-critical systems require high-level assurance, which cannot always be guaranteed in compile time. The use of runtime verification (RV) enable monitoring these systems in runtime, to detect property violations early and limit their potential consequences. However, the introduction of monitors in ultra-critical systems poses a challenge, as failures and delays in the RV subsystem could affect other subsystems and threaten the mission as a whole. In this talk we discuss two systems: NASA's Ogma, a tool to transform high-level specifications into monitoring code, and Copilot, a runtime verification framework for real-time embedded systems. The toolchain can be used to translate structured natural language requirements into C code with static memory requirements, which can be compiled to run on embedded hardware.

Ogma↗
NASA NTRSDate not supplied

Runtime Verification with Ogma

Ultra-critical systems require high-level assurance, which cannot always be guaranteed in compile time. The use of runtime verification (RV) enable monitoring these systems in runtime, to detect property violations early and limit their potential consequences. However, the introduction of monitors in ultra-critical systems poses a challenge, as failures and delays in the RV subsystem could affect other subsystems and threaten the mission as a whole. In this talk we discuss two systems: NASA's Ogma, a tool to transform high-level specifications into monitoring code, and Copilot, a runtime verification framework for real-time embedded systems. The toolchain can be used to translate structured natural language requirements into C code with static memory requirements, which can be compiled to run on embedded hardware.

Ogma↗
NASA NTRS1993

Automated synthesis and verification of configurable DRAM blocks for ASIC's

A highly flexible embedded DRAM compiler is developed which can generate DRAM blocks in the range of 256 bits to 256 Kbits. The compiler is capable of automatically verifying the functionality of the generated DRAM modules. The fully automated verification capability is a key feature that ensures the reliability of the generated blocks. The compiler's architecture, algorithms, verification techniques and the implementation methodology are presented.

Pakkurti, M.↗
DOE OSTI2023

A Verified Optimizer for Quantum Circuits

We present VOQC, the first verified optimizer for quantum circuits, written using the Coq proof assistant. Quantum circuits are expressed as programs in a simple, low-level language called SQIR, a small quantum intermediate representation, which is deeply embedded in Coq. Optimizations and other transformations are expressed as Coq functions, which are proved correct with respect to a semantics of SQIR programs. SQIR programs denote complex-valued matrices, as is standard in quantum computation, but we treat matrices symbolically to reason about programs that use an arbitrary number of quantum bits. SQIR’s careful design and our provided automation make it possible to write and verify a broad range of optimizations in VOQC, including full-circuit transformations from cutting-edge optimizers.

97 MATHEMATICS AND COMPUTING↗
DOE OSTI2025

ROSE Castor

ROSE Castor is a tool enabling automated verification of C++, built off of the ROSE compiler framework and the Why3 framework. Castor defines a verification language for providing specifications of C++ code, letting users perform automated functional formal verification of their C++ code. Castor is designed to target C++17, and supports a subset of the language, including classes, functions, templates, integers and booleans, pointers and references, and single inheritance. Castor currently does not support multiple or virtual inheritance, virtual functions, floating-point, threading, lambda functions, or the C++ STL, though some of these are planned in future updates. Castor ships with an in-house parser for parsing verification conditions.

Lane, PhillipA [Lawrence Livermore National Labora↗
DOE OSTI2023

Correct Compilation of Concurrent C Code

The CompCert compiler represents a landmark effort in program verification as both a piece of verified software and as a compiler for verified C programs. A key shortcoming of CompCert however is that it does not support multithreaded programs. Prior work to add threads to CompCert has either required major rewrites of parts of the proof or only works for well synchronized programs. The problem is that CompCert’s backward simulation derives from a forward simulation via the determinism of the semantics of intermediate representation languages. This makes the proofs in CompCert easier but also makes them incompatible with standard models of multithreading which are non-deterministic. Here we propose an alternate formulation of CompCert’s proof structure that parameterizes the existing single threaded semantics with nondeterministic behavior generated at the multithreading level. While this is an old trick where program equivalence is concerned, performing it in the context of CompCert is quite subtle. Our approach allows for expressive concurrent semantics and does not require major proof rewrites but still results in a global backward simulation for multithreaded programs.

97 MATHEMATICS AND COMPUTING↗
NASA NTRSDate not supplied

Impact, a Tool Suite for Crew Health and Performance System Trade Analyses and Decision Support - Status of Development

Mission planners, systems engineers, and clinicians that support crew health and performance face very difficult choices on upcoming exploration missions. Given that there will be a heavily constrained mass and volume allocation for a medical system on these missions, what medical capability should be manifested to minimize both medical risk and mission risk? Given that not all promising research and technology proposals can be funded, how can proposals be prioritized so that those funded research investments produce the maximum benefit in reducing overall medical risk? The Informing Mission Planning via Analysis of Complex Tradespaces (IMPACT) project seeks to answer these kinds of questions and others to support upcoming exploration missions. IMPACT enables risk-informed and evidence-based trade space analysis for future space vehicles, missions, and systems. This presentation will discuss the long-term HRP and ExMC vision for the larger ecosystem of tools, which include an updated medical database (consisting of an Evidence Library for medical conditions and a medical item database (MedID) for medical resources), dynamic Probabilistic Risk Assessment (PRA) capabilities, System Modeling Language (SysML) models, and contextual data visualizations of output data. IMPACT is the result of a multi-center collaborative effort. The trade space analyses performed by IMPACT can directly inform mission, vehicle, and habitat development by quantifying medical risk, given a design reference mission, crew attributes and a set of medical capabilities. This presentation will update the audience on the development status of the tool suite, its constituent parts and the plans for when it will deploy as an operational product, currently scheduled for the end of FY22. Recent development successes on the IMPACT project include the ability to cluster medical resources into medical capabilities and mutually-dependent bundles, the ability to perform trade analyses on different medical sets, different DRMs, and different crew complements, and the ability to specify mission segments as periods of time assigned to one or more members of the crew during which unique mission events occur (e.g., extravehicular activities, surface operations, gravity well adaptations, etc.). IMPACT is gearing up for its verification and validation phase to compile the data package necessary for a successful Transition to Operations (TtO), per the guidance in NPR 8900.1B .

IMPACT↗
NASA NTRS2020

Copilot 3

Ultra-critical systems require high-level assurance, which cannot always be guaranteed in compile time. The use of runtime verification (RV) enables monitoring these systems in runtime, to detect property violations early and limit their potential consequences. The introduction of monitors in ultra-critical systems poses a challenge, as failures and delays in the RV subsystem could affect other subsystems and threaten the mission as a whole. This paper presents Copilot 3, a runtime verification framework for real-time embedded systems. Copilot monitors are written in a compositional, stream-based language with support for a variety of Temporal Logics (TL), which results in robust, high-level specifications that are easier to understand than their traditional counterparts. The framework translates monitor specifications into C code with static memory requirements, which can be compiled to run on embedded hardware. This paper presents version 3 of the Copilot language, demonstrates its suitability with a number of examples, and discusses its use in larger applications. Additionally, it describes the framework?s architecture, its implementation as a Domain Specific Language (DSL) embedded in Haskell, and the progress of the project over the years.

Ivan Perez↗
DOE OSTI2022

Automatic inspection of program state in an uncooperative environment

Abstract The program state is formed by the values that the program manipulates. These values are stored in the stack, in the heap, or in static memory. The ability to inspect the program state is useful as a debugging or as a verification aid. Yet, there exists no general technique to insert inspection points in type‐unsafe languages such as C or C++. The difficulty comes from the need to traverse the memory graph in a so‐called uncooperative environment. In this article, we propose an automatic technique to deal with this problem. We introduce a static code transformation approach that inserts in a program the instrumentation necessary to report its internal state. Our technique has been implemented in LLVM. It is possible to adjust the granularity of inspection points trading precision for performance. In this article, we demonstrate how to use inspection points to debug compiler optimizations; to augment benchmarks with verification code; and to visualize data structures.

Magalhães, José Wesley de Souza↗
DOE OSTI2022

Analysis of Validating and Verifying OpenACC Compilers 3.0 and Above

OpenACC is a high-level directive-based parallel programming model that can manage the sophistication of heterogeneity in architectures and abstract it from the users. The portability of the model across CPUs and accelerators has gained the model a wide variety of users. This means it is also crucial to analyze the reliability of the compilers’ implementations. To address this challenge, the OpenACC Validation and Verification team has proposed a validation testsuite to verify the OpenACC implementations across various compilers with an infrastructure for a more streamlined execution. This paper will cover the following aspects: (a) the new developments since the last publication on the testsuite, (b) outline the use of the infrastructure, (c) discuss tests that highlight our workflow process, (d) analyze the results from executing the testsuite on various systems, and (e) outline future developments.

Jarmusch, Aaron↗
DOE OSTI2023

Procedure for locating oil and gas wells in the Appalachian Basin

Locating undocumented (or poorly documented) oil and gas wells for environmental assessment is often difficult. Remnant features that confirm the presence of a well (intact casing/wellhead, well bore, etc.) are typically less than a meter in size and often are obscured from direct observation on the ground or from the air (by dense vegetation, for example). To efficiently find such features, it is useful to first systematically compile publicly available digital data at progressively smaller scales prior to embarking on field campaigns. Further, the information presented here describes the procedure developed and used by the U.S. Department of Energy's National Energy Technology Laboratory to locate potential oil and gas well sites for follow-up field verification and characterization. Digital data are first compiled from national and state resources such as well location/production databases, historical topographic maps, historical aerial photographs, and LiDAR data. Although each data set is likely to be incomplete or inaccurate to some extent, combining the data resources using geographic information system technology can generate potential well site targets with a higher degree of confidence, which improves the efficiency of fieldwork activities. This workflow was developed in the Appalachian Basin region, and although certain aspects may be unique, the general process would be applicable to locating undocumented wells in other regions.

54 ENVIRONMENTAL SCIENCES↗
NASA NTRS2017

Automated Analysis of Stateflow Models

Stateflow is a widely used modeling framework for embedded and cyber physical systems where control software interacts with physical processes. In this work, we present a framework a fully automated safety verification technique for Stateflow models. Our approach is two-folded: (i) we faithfully compile Stateflow models into hierarchical state machines, and (ii) we use automated logic-based verification engine to decide the validity of safety properties. The starting point of our approach is a denotational semantics of State flow. We propose a compilation process using continuation-passing style (CPS) denotational semantics. Our compilation technique preserves the structural and modal behavior of the system. The overall approach is implemented as an open source toolbox that can be integrated into the existing Mathworks Simulink Stateflow modeling framework. We present preliminary experimental evaluations that illustrate the effectiveness of our approach in code generation and safety verification of industrial scale Stateflow models.

Stateflow↗