Collective Allocator Abstraction to Control Object Spatial Locality in C++
Authors:
Takato Hideshima,
Shigeyuki Sato,
Tomoharu Ugawa
Abstract:
Disaggregated memory is promising for improving memory utilization in computer clusters in which memory demands significantly vary across computer nodes under utilization. It allows applications with high memory demands to use memory in other computer nodes.
However, disaggregated memory is not easy to use for implementing data structures in C++ because the C++ standard does not provide an adequ…
▽ More
Disaggregated memory is promising for improving memory utilization in computer clusters in which memory demands significantly vary across computer nodes under utilization. It allows applications with high memory demands to use memory in other computer nodes.
However, disaggregated memory is not easy to use for implementing data structures in C++ because the C++ standard does not provide an adequate abstraction to use it efficiently in a high-level, modular manner. Because accessing remote memory involves high latency, disaggregated memory is often used as a far-memory system, which forms a kind of swap memory where part of local memory is used as a cache area, while the remaining memory is not subject to swapping. To pursue performance, programmers have to be aware of this nonuniform memory view and place data appropriately to minimize swapping.
In this work, we model the address space of memory-disaggregated systems as the far-memory model, present the collective allocator abstraction, which enables us to specify object placement aware of memory address subspaces, and apply it to programming aware of the far-memory model.
The far-memory model provides a view of the nonuniform memory space while hiding the details. In the model, the virtual address space is divided into two subspaces; one is subject to swapping and the other is not. The swapping subspace is further divided into even-sized pages, which are units of swapping. The collective allocator abstraction forms an allocator as a collection of sub-allocators, each of which owns a distinct subspace, where every allocation is done via sub-allocators. It enables us to control object placement at allocation time by selecting an appropriate sub-allocator according to different criteria, such as subspace characteristics and object collocation. It greatly facilitates implementing container data structures aware of the far-memory model.
We develop an allocator based on the collective allocator abstraction by extending the C++ standard allocator for container data structures on the far-memory model and experimentally demonstrate that it facilitates implementing containers equipped with object placement strategies aware of spatial locality under the far-memory model in a high-level, modular manner. More specifically, we have successfully implemented B-trees and skip lists with the combined use of two placement strategies. The modifications therein for the original implementations are fairly modest: addition is mostly due to specifying object placement; deletion and modification are at most 1.2 % and 3.2 % of lines of the original code, respectively. We have experimentally confirmed that the modified implementations successfully have data layouts suppressing swapping.
We forecast that the collective allocator abstraction would be a key to high-level integration with different memory hardware technologies because it straightforwardly accommodates new interfaces for subspaces.
△ Less
Submitted 4 March, 2024;
originally announced March 2024.
Reducing State Explosion for Software Model Checking with Relaxed Memory Consistency Models
Authors:
Tatsuya Abe,
Tomoharu Ugawa,
Toshiyuki Maeda,
Kousuke Matsumoto
Abstract:
Software model checking suffers from the so-called state explosion problem, and relaxed memory consistency models even worsen this situation. What is worse, parameterizing model checking by memory consistency models, that is, to make the model checker as flexible as we can supply definitions of memory consistency models as an input, intensifies state explosion. This paper explores specific reasons…
▽ More
Software model checking suffers from the so-called state explosion problem, and relaxed memory consistency models even worsen this situation. What is worse, parameterizing model checking by memory consistency models, that is, to make the model checker as flexible as we can supply definitions of memory consistency models as an input, intensifies state explosion. This paper explores specific reasons for state explosion in model checking with multiple memory consistency models, provides some optimizations intended to mitigate the problem, and applies them to McSPIN, a model checker for memory consistency models that we are developing. The effects of the optimizations and the usefulness of McSPIN are demonstrated experimentally by verifying copying protocols of concurrent copying garbage collection algorithms. To the best of our knowledge, this is the first model checking of the concurrent copying protocols under relaxed memory consistency models.
△ Less
Submitted 21 August, 2016;
originally announced August 2016.
