scholarly journals Reasoning about Translation Lookaside Buffers

10.29007/c2f1 ◽  
2018 ◽  
Author(s):  
Hira Syeda ◽  
Gerwin Klein
Keyword(s):  
Operating Systems ◽  
Memory Management ◽  
Formal Model ◽  
Sufficient Conditions ◽  
Management Unit ◽  
Security Mechanism ◽  
Translation Lookaside Buffer ◽  
Address Translation ◽  
Derived Properties ◽  
With Memory

The main security mechanism for enforcing memory isolation in operating systems is provided by page tables. The hardware-implemented Translation Lookaside Buffer (TLB) caches these, and therefore the TLB and its consistency with memory are security crit- ical for OS kernels, including formally verified kernels such as seL4. If performance is paramount, this consistency can be subtle to achieve; yet, all major formally verified ker- nels currently leave the TLB as an assumption.In this paper, we present a formal model of the Memory Management Unit (MMU) for the ARM architecture which includes the TLB, its maintenance operations, and its derived properties. We integrate this specification into the Cambridge ARM model. We derive sufficient conditions for TLB consistency, and we abstract away the functional details of the MMU for simpler reasoning about executions in the presence of cached address translation, including complete and partial walks.

scholarly journals EVector: An Efficient Vector Implementation – Using Virtual Memory for Improving Memory

2006 ◽  
Vol 14 (2) ◽  
pp. 45-59
Author(s):  
Dries Kimpe ◽  
Stefan Vandewalle ◽  
Stefaan Poedts
Keyword(s):  
Operating System ◽  
Programming Languages ◽  
Operating Systems ◽  
Memory Management ◽  
Object Oriented ◽  
Virtual Memory ◽  
Management Unit ◽  
Efficient Vector ◽  
Reference Implementation

Every modern operating system provides some form of virtual memory to its applications. Usually, a hardware memory management unit (MMU) exists to efficiently support this. Although most operating systems allow user programs to indirectly control the MMU, few programs or programming languages actually make use of this facility. This article explores how the MMU can be used to enhance memory handling for resizable arrays. A reference implementation in C++ demonstrates its usability and superiority compared to the standard C++ vector class, and how to combine the scheme with an object-oriented environment. A number of other improvements, based on newly emerged insights in C++ are also presented.

scholarly journals Online Thread and Data Mapping Using a Sharing-Aware Memory Management Unit

2021 ◽  
Vol 5 (4) ◽  
pp. 1-28
Author(s):  
Eduardo H. M. Cruz ◽  
Matthias Diener ◽  
Laércio L. Pilla ◽  
Philippe O. A. Navaux
Keyword(s):  
Energy Efficiency ◽  
Memory Management ◽  
Substantial Reduction ◽  
Management Unit ◽  
Memory Access ◽  
Parallel Applications ◽  
Data Mapping ◽  
Wide Range ◽  
Memory Accesses ◽  
Level Parallelism

Current and future architectures rely on thread-level parallelism to sustain performance growth. These architectures have introduced a complex memory hierarchy, consisting of several cores organized hierarchically with multiple cache levels and NUMA nodes. These memory hierarchies can have an impact on the performance and energy efficiency of parallel applications as the importance of memory access locality is increased. In order to improve locality, the analysis of the memory access behavior of parallel applications is critical for mapping threads and data. Nevertheless, most previous work relies on indirect information about the memory accesses, or does not combine thread and data mapping, resulting in less accurate mappings. In this paper, we propose the Sharing-Aware Memory Management Unit (SAMMU), an extension to the memory management unit that allows it to detect the memory access behavior in hardware. With this information, the operating system can perform online mapping without any previous knowledge about the behavior of the application. In the evaluation with a wide range of parallel applications (NAS Parallel Benchmarks and PARSEC Benchmark Suite), performance was improved by up to 35.7% (10.0% on average) and energy efficiency was improved by up to 11.9% (4.1% on average). These improvements happened due to a substantial reduction of cache misses and interconnection traffic.

Linux Based Mobile Operating Systems

2011 ◽  
pp. 35-50
Author(s):  
Lee Chao
Keyword(s):  
Operating System ◽  
User Interface ◽  
Mobile Learning ◽  
Operating Systems ◽  
Memory Management ◽  
Process Management ◽  
Management Process ◽  
Interface Management ◽  
Device Management ◽  
History Of

In today’s mobile computing, Linux plays a significant role. The Linux kernel has been adopted by a variety of mobile operating systems to handle tasks such as device management, memory management, process management, networking, power management, application interface management, and user interface management. This chapter introduces Linux based mobile operating systems installed on various mobile devices. It first gives a brief introduction of the history of mobile Linux. Then, the chapter introduces the mobile Linux features that can be used to meet the mobile learning requirements. The last part of the chapter presents strategies on selecting a Linux based operating system for a particular mobile learning project.

Sign in / Sign up

Export Citation Format

Share Document