An official website of the United States government
Memory models play an important role in verified compilation of imperative programming languages. A representative one is the block-based memory model of CompCert---the state-of-the-art verified C compiler. Despite its success, the abstraction over memory space provided by CompCert's memory model is still primitive and inflexible. In essence, it uses a fixed representation for identifying memory blocks in a global memory space and uses a globally shared state for distinguishing between used and unused blocks. Therefore, any reasoning about memory must work uniformly for the global memory; it is impossible to individually reason about different sub-regions of memory (i.e., the stack and global definitions). This not only incurs unnecessary complexity in compiler verification, but also poses significant difficulty for supporting verified compilation of open or concurrent programs which need to work with contextual memory, as manifested in many previous extensions of CompCert. To remove the above limitations, we propose an enhancement to the block-based memory model based on nominal techniques; we call it the nominal memory model. By adopting the key concepts of nominal techniques such as atomic names and supports to model the memory space, we are able to 1) generalize the representation of memory blocks to any types satisfying the properties of atomic names and 2) remove the global constraints for managing memory blocks, enabling flexible memory structures for open and concurrent programs. To demonstrate the effectiveness of the nominal memory model, we develop a series of extensions of CompCert based on it. These extensions show that the nominal memory model 1) supports a general framework for verified compilation of C programs, 2) enables intuitive reasoning of compiler transformations on partial memory; and 3) enables modular reasoning about programs working with contextual memory. We also demonstrate that these extensions require limited changes to the original CompCert, making the verification techniques based on the nominal memory model easy to adopt.
more »
« less
This content will become publicly available on January 1, 2026
Sensor State Protection in Λ-type Atomic Ensemble Quantum Memories
We simulate Λ-type quantum memory in atomic ensembles with the addition of a high-lying sensor state in the continuous dynamical decoupling regime. We find order-of-magnitudes memory lifetime enhancement and explore the dressing-field parameter space.
more »
« less
- Award ID(s):
- 2207822
- PAR ID:
- 10634226
- Publisher / Repository:
- Optica Publishing Group
- Date Published:
- ISBN:
- 978-1-957171-48-7
- Page Range / eLocation ID:
- QTu2B.3
- Format(s):
- Medium: X
- Location:
- San Francisco
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
Far-memory techniques that enable applications to use remote memory are increasingly appealing in modern data centers, supporting applications’ large memory footprint and improving machines’ resource utilization. Unfortunately, most far-memory techniques focus on OS-level optimizations and are agnostic to managed runtimes and garbage collections (GC) underneath applications written in high-level languages. With different object-access patterns from applications, GC can severely interfere with existing far-memory techniques, breaking remote memory prefetching algorithms and causing severe local-memory misses. We developed MemLiner, a runtime technique that improves the performance of far-memory systems by aligning memory accesses from application and GC threads so that they follow similar memory access paths, thereby (1) reducing the local-memory working set and (2) improving remote-memory prefetching through simplified memory access patterns. We implemented MemLiner in two widely used GCs in OpenJDK: G1 and Shenandoah. Our evaluation with a range of widely deployed cloud systems shows that MemLiner improves applications’ end-to-end performance by up to3.3×and reduces applications’ tail latency by up to220.0×.more » « less
-
Summary Traditional relational database systems handle data by dividing their memory into sections such as a buffer cache and working memory, assigning a memory budget to each section to efficiently manage a limited amount of overall memory. They also assign memory budgets to memory‐intensive operators such as sorts and joins and control the allocation of memory to these operators; each memory‐intensive operator attempts to maximize its memory usage to reduce disk I/O cost. Implementing such memory‐intensive operators requires a careful design and application of appropriate algorithms that properly utilize memory. Today's Big Data management systems need the ability to handle large amounts of data similarly, as it is unrealistic to assume that truly big data will fit into memory. In this article, we share our memory management experiences in Apache AsterixDB, an open‐source Big Data management software platform that scales out horizontally on shared‐nothing commodity computing clusters. We describe the implementation of AsterixDB's memory‐intensive operators and their designs related to memory management. We also discuss memory management at the global (cluster) level. We conducted an experimental study using several synthetic and real datasets to explore the impact of this work. We believe that future Big Data management system builders can benefit from these experiences.more » « less
-
Big Data has an insatiable appetite for larger and better-performing memory. While current memory technologies continue to advance, the performance gaps in current memory and storage technology have motivated the exploration of emerging memory technologies capable of providing new functionalities. Ferroelectric memory is one such promising candidate which has recently experienced a revival after the discovery of ferroelectricity in hafnium dioxide (HfO2) – the dielectric of choice in advanced CMOS manufacturing. While the commercial viability of ferroelectric memory technology has made significant progress over the past decade, several challenges related to variation and reliability still stand as a barrier to large-scale commercial implementation. Here, we review some of the outstanding challenges of ferroelectric memory technology along with the recent materials and device innovations that are being considered to overcome them. Moreover, we aim to highlight these challenges as materials and device co-design problems that must be addressed through collaborative efforts that straddle the two disciplines. We identify and provide our perspective on some of the key challenges and opportunities for ferroelectric-based microelectronic technology. Ferroelectrics non-volatile memory, in-memory computationmore » « less
-
Abstract Visual attention both guides and is guided by learning and memory systems. In this article, we use a multiple‐memory systems framework to examine the interplay between attention and memory that begins in early postnatal life. We review how attention and memory interact to support infant development with respect to perceptual learning about objects and features, item‐in‐context spatial memory, and reinforcement and reward learning. We argue that the multiple‐memory systems approach offers a useful organizational structure for research on interactions between attention and memory.more » « less
