Shouting at Memory: Where Did My Write Go?

Echolocation, as observed in nature, involves emitting a signal and interpreting its returning echoes to infer the spatial arrangement of the environment. Our methodology mirrors this approach in the context of memory systems. By performing a store operation, we create a disruption in the memory hierarchy – analogous to emitting a signal. Subsequently, retrieving this data produces measurable latencies, or “echoes”, that reveal the location and behaviour of the memory hierarchy components involved.

This analogy underscores the power of latency measurement as a diagnostic tool, revealing patterns of memory residency and transitions across architectural layers. The emitted “signal” in our case is the store operation, and the echoes are derived from the variability in memory access times observed during data retrieval.

At the core of our approach is the precise measurement of memory access times. Once the initial store operation is performed, we measure the time required to fetch the data (Figure 2). These timing measurements serve as unique fingerprints of the specific memory layer where the data resides, offering a non-invasive mechanism to explore the memory hierarchy. For example:

• $\mathrm{■}$

  Extremely low latencies indicate L1 cache residency.

• $\mathrm{■}$

  Intermediate latencies may correspond to L2 or L3 caches.

• $\mathrm{■}$

  Longer latencies often point to the Write Pending Queue (WPQ) or main memory (RAM).

• $\mathrm{■}$

  In extended setups, latencies may also reveal accesses to emerging technologies like CXL-enabled memory.

The interaction between the learner and the oracle follows a systematic cycle, illustrated in Figure 3. To explore this process, consider a program $P$ with two consecutive writes: $x\leftarrow 1$ followed by $y\leftarrow 1$. Following a crash and recovery, the values of $x$ and $y$ may vary, and the state $x=0$ and $y=1$ could appear, even though this state is never observable during normal execution. This inconsistency presents an opportunity for the model learner to refine its hypothesis about write persistency.

To reason about the persistency of writes in this example, we use a toy model built around the concept of a persist buffer. This buffer serves as an abstraction that captures the intermediate state of writes that are not yet persisted but are still available within the volatile memory hierarchy. The model incorporates the following elements:

• $\mathrm{■}$

  Writes: $w\in W$, where $W$ is the set of all writes executed by the program.

• $\mathrm{■}$

  Program Order: The relation ${⪯}_{\mathrm{𝑝𝑜}}$ captures the sequential order of writes in $P$, where $w_i{⪯}_{\mathrm{𝑝𝑜}}{w}_j$ means $w_i$ appears before $w_j$ in the program.

• $\mathrm{■}$

  Persist Buffer: $ℬ=(w_1,w_2,\mathrm{\dots },w_n)$, the ordered sequence of writes currently in the persist buffer, where $w_i\in W$ and $w_i{\prec }_{\mathrm{𝑝𝑏}}{w}_j$ if write $w_i$ occurs before $w_j$ in the order within the buffer.

• $\mathrm{■}$

  Persistence States: A write $w$ can be in one of two states:

  Alternatively, we may use $w^{\neg 𝒫}$ to denote $w^{ℬ}$.

• $\mathrm{■}$

  Buffer Transitions: A transition ${ℬ}^{(i)}\stackrel{𝑤}{\hookrightarrow }{ℬ}^{(i+1)}$ represents a change in the contents of the persist buffer $ℬ$ when write $w\in W$ occurs, resulting in a new buffer state ${ℬ}^{(i+1)}$. The exact transformation is defined by specific persistence rules.

• $\mathrm{■}$

  Crash and Echo Recovery: ${𝖷}_{\mathrm{𝑒𝑐ℎ𝑜}}$ represents a “soft crash” simulated using our non-invasive echolocation technique. Instead of a physical crash, this step involves probing the system using timed memory loads to infer the likely location (and thus persistence state) of relevant variables. It approximates the outcome of a crash-recovery cycle without disrupting the system. The specific mechanism for interpreting these probes is detailed in Section 6.

Initially, the model assumes that all writes are persisted immediately upon execution. This is captured by the following invariance rule for the persist buffer:

$\forall w\in W,{ℬ}^{(i)}\stackrel{𝑤}{\hookrightarrow }{ℬ}^{(i)}$

1. 1.

   Initial Hypothesis: The learner begins with the simplest hypothesis, assuming immediate persistence. This predicts $x=1$ and $y=1$ post-crash. The hypothesis is submitted as an Equivalence Query (EQ) to the oracle, which tests it against the actual System Under Learning (SUL).

2. 2.

   Targeted Test Case Generation: To refine its understanding, the learner generates a test case (a Membership Query, MQ) to probe the system’s crash recovery behaviour. The test involves executing a sequence of operations followed by the echolocation probe:

   $${\text{TQ}}_i:(x\leftarrow 1;y\leftarrow 1;{𝖷}_{\mathrm{𝑒𝑐ℎ𝑜}})$$

   The effectiveness of echolocation hinges on using carefully constructed, simple test cases like ${\text{TQ}}_i$. For validating persistency semantics, we employ litmus tests which are kept intentionally small, typically involving only a few memory accesses and persistence-related instructions (flushes, fences). The echolocation probe (${𝖷}_{\mathrm{𝑒𝑐ℎ𝑜}}$) is strategically placed after the sequence of operations whose outcome needs assessment, representing the timed load measurements for relevant variables (here, $x$ and $y$). Complexity in these test cases must be minimised to avoid introducing extraneous micro-architectural effects that could obscure the primary latency signal related to data location. Echolocation is therefore suited for targeted microbenchmarks designed to probe specific persistency interactions, not for direct timing analysis within complex application code.

   The test case ${\text{TQ}}_i$ is submitted as an MQ to observe the actual system behaviour as interpreted through the echolocation probe.

3. 3.

   Oracle Feedback: The oracle executes the MQ on the SUL. Using the ${𝖷}_{\mathrm{𝑒𝑐ℎ𝑜}}$ probe mechanism (detailed in Section 6), it determines the persistence state of the variables. Suppose the oracle concludes from the probes that $x$ was non-persistent at the time of the simulated crash, while $y$ was persistent. This translates to an observed ’recovered’ state of $x=0,y=1$, which contradicts the learner’s initial hypothesis. This counterexample (the test trace ${\text{TQ}}_i$ and its observed outcome) is returned to the learner.

4. 4.

   Discrepancy Analysis and Model Refinement: The learner revises its hypothesis to account for asynchronous persistence, acknowledging that writes pass through the persist buffer before being persisted, with reordering possible. The updated rule is expressed as follows:

   $\forall w\in W,{ℬ}^{(i)}\stackrel{𝑤}{\hookrightarrow }{ℬ}^{(i+1)}\text{where}{ℬ}^{(i+1)}={ℬ}^{(i)}\cup \{w\}\text{and}\forall w^{\prime }\in {ℬ}^{(i)},w^{\prime }{\prec }_{\mathrm{𝑝𝑏}}w$

   This rule accounts for the transient nature of writes in the persist buffer, allowing them to remain temporarily before being committed to persistent storage, with the persistence order potentially non-deterministic.
   
   To accommodate controlled operations that enforce the immediate persistence of specific writes, the model is further refined with a dedicated rule for explicit flushes:

   $\forall w\in W\text{ where }w\text{ modifies }x\text{ and }w{⪯}_{\mathrm{𝑝𝑜}}\text{CLFLUSH}x,\text{CLFLUSH}x⟹w^{𝒫}$

5. 5.

   Iterative Hypothesis Testing: The learner continues generating test cases (MQs or as part of EQs) to challenge the updated model. For instance:

   $${\text{TQ}}_{i+1}:(x\leftarrow 1;\text{CLFLUSH}x;y\leftarrow 1;{𝖷}_{\mathrm{𝑒𝑐ℎ𝑜}})$$

   This test case examines whether the system flushes $x$ to persistent memory before the write to $y$ occurs. If the ${𝖷}_{\mathrm{𝑒𝑐ℎ𝑜}}$ probe (following $y\leftarrow 1$) leads the oracle to conclude that $x$ is persistent but $y$ is not, the inferred recovered state would be $x=1,y=0$.

Algorithm 3 outlines the iterative learning process at a high level, highlighting the roles of Membership Queries (MQs), Equivalence Queries (EQs), and the echolocation probe (${𝖷}_{\mathrm{𝑒𝑐ℎ𝑜}}$). The algorithm addresses several practical considerations in model learning. It establishes explicit termination conditions through $\mathrm{𝑚𝑎𝑥𝐼𝑡𝑒𝑟𝑎𝑡𝑖𝑜𝑛𝑠}$ and $\mathrm{𝑐𝑜𝑛𝑣𝑒𝑟𝑔𝑒𝑛𝑐𝑒𝑇ℎ𝑟𝑒𝑠ℎ𝑜𝑙𝑑}$ parameters. This ensures the learning process eventually terminates, even when a perfect model cannot be achieved due to system complexity or non-determinism. The $\mathrm{𝑒𝑟𝑟𝑜𝑟𝑅𝑎𝑡𝑒}$ tracking provides a quantitative measure of model quality, calculated as the proportion of test cases where the model’s predictions differ from observed outcomes. Central to our approach is the $\mathrm{𝑜𝑏𝑠𝑒𝑟𝑣𝑎𝑡𝑖𝑜𝑛𝑇𝑎𝑏𝑙𝑒}$ $T$, which serves as a structured knowledge repository mapping test sequences to their observed outcomes. This table plays a crucial role in both generating test sequences for equivalence queries and constructing refined hypothesis models. The learning process has two distinct phases:

1. 1.

   Equivalence Query Phase: The algorithm generates test sequences based on the current hypothesis and observation history. Each test is augmented with the echolocation probe and executed on the System Under Learning. Discrepancies between predicted and observed outcomes are collected as counterexamples. If no counterexamples are found, the current hypothesis is accepted as equivalent to the target model.

2. 2.

   Hypothesis Refinement Phase: When counterexamples are found, the algorithm selects the most informative one to guide the generation of targeted membership queries. These queries explore specific aspects of the system’s behaviour revealed by the counterexample. Results from these queries update the observation table, which is then used to construct a new hypothesis model.

The $\mathrm{𝐻𝑦𝑝𝑜𝑡ℎ𝑒𝑠𝑖𝑠𝑀𝑜𝑑𝑒𝑙}$ $H$ maintains rich state, tracking the abstract persist buffer content and the status of writes ($w^{𝒫}$ or $w^{ℬ}$). The $\mathrm{𝑜𝑏𝑠𝑒𝑟𝑣𝑒𝑑}\mathrm{\_}\mathrm{𝑜𝑢𝑡𝑐𝑜𝑚𝑒}$ and $\mathrm{𝑝𝑟𝑒𝑑𝑖𝑐𝑡𝑒𝑑}\mathrm{\_}\mathrm{𝑜𝑢𝑡𝑐𝑜𝑚𝑒}$ represent the inferred set of persisted variable states (e.g., $x=0,y=1$) after a test sequence. The refinement process involves updating $H$’s internal representation of buffering and persistence rules based on the observed outcomes stored in the observation table. This algorithm strikes a balance between theoretical soundness and practical applicability, accommodating the inherent challenges in learning models of complex persistency semantics in real-world systems.

Event Structures [44] provide a principled foundation for modelling persistency for several key reasons:

The alphabet $𝒜$ of memory operations is structured hierarchically:

1. 1.

   Basic Memory Operations:

   • $\mathrm{■}$

     Initialisation Operation $\mathbb{𝟘}$, representing the initialisation of all locations in persistent memory appeared in the program, typically setting them to 0.

   • $\mathrm{■}$

     Read Operations $R=\{{\text{R}}_x^v\mid x\in X,v\in V\}$, where ${\text{R}}_x^v$ denotes reading the value $v$ from $x$.

   • $\mathrm{■}$

     Write Operations $W=\{{\text{W}}_x^v\mid x\in X,v\in V\}\cup \{\mathbb{𝟘}\}$, where ${\text{W}}_x^v$ denotes writing $v$ to $x$, and $\mathbb{𝟘}=\{{\text{W}}_x^0\mid x\in X\}$ represents the initialisation of all locations to zero. All writes are durable, meaning their effects may be observed after system recovery.

   • $\mathrm{■}$

     Read-Modify-Write Operations $\mathrm{𝑅𝑀𝑊}=\{{\text{RMW}}_x^f\mid x\in X,f\in F\}$ denotes atomic updates to $x$ using the function $f$. These operations atomically read the value of $x$, modify it using $f$, and write the result back to $x$, ensuring no interference from other threads during execution. Common atomic operations in Intel architectures include:

     • –

       lock xadd: Atomic fetch-and-add. Adds a value to $x$ and returns its previous value.

     • –

       lock cmpxchg: Atomic compare-and-swap. Compares $x$ with a specified operand and updates $x$ if they match.

     • –

       lock or/and: Atomic bitwise OR/AND. Performs a bitwise OR/AND operation on $x$.

     • –

       lock add: Atomic addition. Adds a value to $x$ and stores the result atomically.

2. 2.

   Synchronisation Operations:

   • $\mathrm{■}$

     Memory Fence $({\mathrm{𝐹𝐸}}_{\mathrm{𝑚𝑒𝑚}})$ ensures all preceding memory operations (loads and stores) complete before any subsequent ones. In Intel architectures, this is enforced via the MFENCE instruction.

   • $\mathrm{■}$

     Store Fence $({\mathrm{𝐹𝐸}}_{\mathrm{𝑠𝑡𝑜𝑟𝑒}})$ guarantees that all previous store operations complete before any subsequent stores. This is implemented in Intel architectures via the SFENCE instruction.

3. 3.

   Persistency Operations:

   • $\mathrm{■}$

     Regular Flush $\mathrm{𝐹𝐿}=\{\text{flush}x\mid x\in X\}$ writes back the cache line containing $x$ to memory, ensuring that all pending writes to that cache line are asynchronously persisted. In Intel architectures, this is implemented via the CLFLUSH instruction.

   • $\mathrm{■}$

     Optimised Flush ${\mathrm{𝐹𝐿}}_{\mathrm{𝑜𝑝𝑡}}=\{\text{flushopt}x\mid x\in X\}$ also flushes the cache line containing $x$. However, it imposes different ordering constraints: a $\text{flushopt}x$ operation is ordered only with respect to earlier writes to the same cache line; in contrast, a $\text{flush}x$ operation is ordered with respect to all writes, regardless of their cache line. In Intel architectures, this functionality is provided by the CLFLUSHOPT instruction.

   • $\mathrm{■}$

     Write Back $\mathrm{𝑊𝐵}=\{\text{wb}x\mid x\in X\}$ behaves like $\text{flushopt}x$ but provides better performance; both persist the cache line of $x$, but $\text{flushopt}x$ invalidates it, whereas $\text{wb}x$ may retain it for reuse. Implemented in Intel architectures via the ‘CLWB‘ instruction.

We define $W^{𝒫}\subseteq W$ as the subset of writes that have reached persistent memory. The initialisation is always persistent: $\mathbb{𝟘}\in W^{𝒫}$.
The complete event alphabet is therefore:

Refining the previously defined resulting-from relation over the event alphabet, we have:

meaning:

• $\mathrm{■}$

  $\mathbb{𝟘}$ justifies reading zero from any location $x$;

• $\mathrm{■}$

  a write of $v$ to $x$ justifies reading $v$ from $x$.

A refinement of the program order is the adjacent program order relation, ${⪯}_{\mathrm{𝑎𝑑𝑗}}\subseteq {⪯}_{\mathrm{𝑝𝑜}}$, which captures the adjacency of events within the same thread. Formally, it is defined as:

In other words, two events $a$ and $b$ are adjacent in the program order if there is no event $c$ such that $a{⪯}_{\mathrm{𝑝𝑜}}c{⪯}_{\mathrm{𝑝𝑜}}b$ except for $a$ and $b$ themselves.

Events that are neither ordered by happens-before nor in conflict are considered concurrent. To formally capture the independence of events across different threads, we define the concurrency relation, denoted $\parallel$, as follows:

The following example illustrates the application of event structures in this context.

We encode the semantics of persistent event structures using the Alloy modelling language [20], a declarative framework that expresses systems as relational structures. This encoding facilitates the analysis of program behaviour under diverse memory access patterns. The model is structured into a set of entities, each representing a distinct aspect of memory semantics. Figure 6 illustrates the hierarchical relationships between these entities and their interconnections within the event structure. The corresponding Alloy code defining these entities is provided in Listing 1.

In Alloy, memory events are defined as signatures, introducing new types in the model. The Event signature serves as the supertype, with specialised event types extending it via the extends keyword. Events are structured through relations that link their attributes to other entities (e.g., $\text{Read}\stackrel{𝑟𝑓}{\to }\text{Write}$) or within the same entity (e.g., $\text{Event}\stackrel{ℎ𝑏}{\to }\text{Event}$). These relationships are further constrained using facts – axiomatic formulae that Alloy assumes to be always true, shaping the space of possible examples and counterexamples generated by the Alloy analyser. For instance, to enforce that the relation adjacent program order (adj_po) applies only within the same thread, the following fact is defined:

To illustrate how our Alloy model is executed to generate concrete instances, consider the following predicate, volatile. It expresses conditions under which a write w could be considered volatile when event e occurs. The Alloy analyser systematically explores the model to find instances satisfying this predicate, revealing concrete memory event orderings that meet these constraints.

By executing Alloy’s run command with this predicate, we generate concrete executions that reveal scenarios where a write remains volatile. The analyser constructs instances that adhere to the specified constraints. One such instance, discussed in Figure 5, satisfies the volatile predicate and can be obtained by executing the following command, which explores possible executions within a bounded model of 7 events, 2 threads, and 3 memory locations:

Our preliminary implementation, used to generate the latency data shown in Figure 7 and Table 1, employs a microbenchmark written in C (available at DOI 10.5281/zenodo.15045528). The core measurement technique involves timing individual memory load operations using the TSC. Specifically, we utilise the rdtscp ³³3Read Time-Stamp Counter and Processor ID is an assembly instruction available on x86 processors that retrieves the current value of the CPU’s time-stamp counter (TSC) along with the processor ID. This instruction offers a high-resolution timing mechanism often used for performance monitoring and benchmarking, and is partially serializing. instruction, accessed via inline assembly, to obtain cycle counts immediately before and after the target memory load operation (e.g., sum += array[i] in our benchmark code).

To prevent the compiler from optimising away the timed memory load, the target memory array (array) and the variable accumulating the result (sum) are declared volatile. Memory for the array is allocated using posix_memalign to ensure 64-byte alignment, minimising potential variations due to unaligned accesses.

The elapsed cycle count (end cycles - start cycles) for each load is then converted into nanoseconds. This conversion uses the CPU’s clock frequency, which is determined dynamically at the start of the benchmark by parsing the ’cpu MHz’ field from /proc/cpuinfo on the Linux test system. We acknowledge this frequency detection method is specific to the Linux environment.

In the specific experiment designed to populate the latency distribution (Figure 7), each timed load access to an array element array[i] was preceded by a write to that element and an explicit clflush instruction (also invoked via inline assembly) targeting its cache line. This was done to ensure that the subsequent timed load would likely fetch data from deeper levels of the memory hierarchy (e.g., L3, WPQ, DRAM) rather than potentially hitting in L1/L2 caches, allowing us to observe the full spectrum of access latencies. The benchmark performs numerous such timed accesses across a large memory region and repeats the entire measurement process multiple times. Individual nanosecond latency measurements are recorded (written to a CSV file in our implementation) to allow for detailed statistical analysis and visualization.

Our tests, carried out on an Intel® Xeon® E-2286G CPU (4.00 GHz, 14 cores) running Linux kernel version 4.18.0 on Red Hat Enterprise Linux 8, demonstrated that we could differentiate memory access latencies across various hierarchical levels based on these measurements. In Figure 7, we present a distribution plot based on approximately 25 million memory fetch operations. The observed latencies ranged from as low as 15 ns for the fastest L1 cache to up to 10,000 ns for the slowest swapped memory on disk. The vertical axis represents the order in which these memory accesses occurred, serving only to visualise the distribution of memory accesses across the entire dataset.

The fetch latencies are clearly segmented into six distinct zones, as highlighted by the shaded regions in the plot and detailed with range values in Table 1. These zones correspond to the hierarchical memory locations of the test system: L1 cache, L2 cache, L3 cache, Write Pending Queue (WPQ), DRAM, and swapped memory. This clear segmentation suggests the potential of our approach in profiling memory access patterns and indicates the reliability of timestamp-based latency measurements for inferring data location.

When measuring memory fetch latencies, the elapsed time includes not only the pure data fetch duration but also several overheads. These include the time required to issue the memory access command, the execution time of the memory access instruction itself, and the small but consistent cost of retrieving timestamps using the rdtscp instruction. Additionally, micro-architectural factors, such as cache coherence traffic, prefetcher activity, pipeline effects, resource contention, or cache invalidation caused by instructions like clflush, can contribute noise to the measured time. While these overheads and noise sources are present in the absolute measurements, they often remain relatively consistent or manifest as outliers across different fetches under controlled conditions.

For our purpose, which is to differentiate memory access locations within the hierarchy (e.g., cache, write pending queue, DRAM), the absolute latencies are less significant than the relative differences and distinct clusters observed between fetch times originating from different levels (Figure 7). These large differences tend to cancel out fixed overheads, allowing us to reliably identify the memory hierarchy level from which the data is being fetched based on its characteristic latency range. This approach ensures that variations in fetch latencies used for inference are primarily attributable to the memory location itself rather than extraneous factors, although careful statistical analysis and threshold selection (see Section 8) are needed to handle ambiguity.

The core idea of using echolocation for validation is to map the measured memory load latencies, discussed in the previous subsection, to an inferred persistence state for a given write. This allows us to approximate the outcome of a crash-recovery cycle non-invasively.

With this mapping (Definition 2) established, we can validate correctness conditions required after a potential crash. For example, consider the litmus test from Figure 4 and its instrumented version in Figure 8. The expected post-crash condition is:

Validation of this condition relies on determining the state of ready_to_cook after the program sequence. Our approach uses the ${𝖷}_{\mathrm{𝑒𝑐ℎ𝑜}}$ probe (executed after the write ready_to_cook == true in Figure 8) to measure $L(\text{ready\_to\_cook})$. The Oracle then applies Definition 2:

and the condition (Equation 2) must hold for the validation to pass. Figure 8 illustrates how this check, driven by the echolocation-derived status, is conceptually embedded in the validation logic.

This implementation demonstrating the echolocation probe and its application concept represents a foundational step. As discussed in Section 10, future work involves implementing the full model learning framework and extending validation to more complex scenarios and diverse hardware.

Echolocation is used to approximate memory access patterns occurring during recovery by analysing write echo times. As demonstrated in Figure 7, the access time zones are generally well-segmented for different memory regions. However, very few access times fall ambiguously between these zones, making it difficult to assign them definitively to a specific storage hierarchy. Such ambiguities may lead to misinterpretations of persistency behaviours.

While the proposed validation approach uses model learning to penetrate the actual system and explore edge cases, some rare or complex execution paths, particularly those that are non-deterministic or timing-dependent, may remain untested, leading to incomplete coverage and potentially missing subtle persistency behaviours.

The model learning process, as discussed in Section 4.1, begins with a simplistic initial hypothesis. While this serves as a foundation for systematic refinement, it may inadvertently introduce constraints or assumptions that bias subsequent learning steps. Such biases could narrow the exploration of the state space, leading to an incomplete or inaccurate understanding of the system’s persistency semantics.