Abstract 1 Introduction 2 Definitions 3 Consensus number of 𝒏-Writer, 𝒎-Reader Auditable Register ≥𝒎+𝒏 4 Implementing an 𝒏-Writer 𝒎-Reader Auditable Register Using (𝒏+𝒎)-Sliding Registers 5 Auditable LL/SC from 𝟐⁢𝒏-Sliding Register 6 Immediate Deny List from Auditable Registers 7 Conclusions and Future Work References Appendix A Additional Lemmas and Proofs for Section 4 Appendix B Proof Sketch for Section 5 Appendix C Proof Sketch for Section 6

Auditable Shared Objects: From Registers to Synchronization Primitives

Hagit Attiya ORCID Technion – Israel Institute of Technology, Haifa, Israel Antonio Fernández Anta ORCID IMDEA Software Institute & IMDEA Networks Institute, Madrid, Spain Alessia Milani ORCID Aix Marseille Univ, CNRS, LIS, Marseille, France Alexandre Rapetti ORCID Université Paris-Saclay, CEA, List, F-91120, Palaiseau, France Corentin Travers ORCID Aix Marseille Univ, CNRS, LIS, Marseille, France
Abstract

Auditability allows to track operations performed on a shared object, recording who accessed which information. This gives data owners more control on their data. Initially studied in the context of single-writer registers, this work extends the notion of auditability to other shared objects, and studies their properties.

We start by moving from single-writer to multi-writer registers, and provide an implementation of an auditable n-writer m-reader read / write register, with O⁢(n+m) step complexity. This implementation uses (m+n)-sliding registers, which have consensus number m+n. We show that this consensus number is necessary. The implementation extends naturally to support an auditable load-linked / store-conditional (LL/SC) shared object. LL/SC is a primitive that supports efficient implementation of many shared objects. Finally, we relate auditable registers to other access control objects, by implementing an anti-flickering deny list from auditable registers.

Keywords and phrases:
Auditability, Wait-free implementation, Synchronization power, Distributed objects, Shared memory, LL/SC, Deny List
Funding:
Hagit Attiya: Supported by the Israel Science Foundation (22/1425 and 25/1849).
Antonio Fernández Anta: Supported by project PID2022-140560OB-I00 (DRONAC) funded by MICIU/AEI /10.13039/501100011033 and ERDF, EU.
Alessia Milani: Supported in part by ANR project TRUSTINCloudS (ANR-23-PECL-0009).
Corentin Travers: Supported in part by ANR project DUCAT (ANR-20-CE48-0006).
Copyright and License:
[Uncaptioned image] © Hagit Attiya, Antonio Fernández Anta, Alessia Milani, Alexandre Rapetti, and Corentin Travers; licensed under Creative Commons License CC-BY 4.0
2012 ACM Subject Classification:
Theory of computation → Distributed algorithms
Related Version:
Full Version: https://arxiv.org/abs/2508.14506 [5]
Editor:
Dariusz R. Kowalski

1 Introduction

The ability to track operations on shared objects is a fundamental feature in distributed systems. Auditability, in particular, enables data owners to monitor access to their data by recording who accessed which information. This mechanism provides a robust alternative to traditional access control mechanisms, shifting the emphasis from access restriction to post-hoc accountability. Auditability is helpful for preserving data privacy, as it can be used after a data breach, to enforce accountability for data access. This is particularly useful in shared, remotely accessed storage systems, where, for instance, understanding the extent of a data breach can help mitigate its impact.

Auditability has been initially studied in the context of non-atomic replicated storage [8] and single-writer atomic registers [6]. This work explores auditability for other shared objects, considering the following key questions: (1) What types of base objects are necessary and sufficient to implement auditable multi-writer atomic registers? (2) How does auditability impact the design of common synchronization primitives? (3) Can auditable registers be leveraged to construct more complex access control mechanisms?

We begin to answer these questions by presenting a wait-free, linearizable implementation of an auditable n-writer m-reader read/write register (abbreviated as (m,n)-auditable register), with linear (in n+m) step complexity. To achieve these properties, our algorithm uses sliding registers [19]: a k-sliding register keeps an ordered list of the latest k values written to it. If each reader and writer writes at most once in an (m+n)-sliding register, the sliding register can be used to uniquely order the operations. This implies a linearization of the read and write operations on the auditable register. The key challenge is, therefore, how to deal with multiple read and write operations on the auditable register. The backbone of our (m,n)-auditable register implementation is a sequence of (m+n)-sliding registers, each associated with a different value written to the auditable register. The sliding registers are used to agree which write operation will set the next value of the register, and to track which readers have read this value. An additional challenge is to be able to efficiently find the “current” sliding register when reading and writing, to maintain bounded step complexity.

The consensus number of (m+n)-sliding registers is exactly m+n. (I.e., they allow to solve consensus among exactly m+n processes.) Thus, consensus number m+n is sufficient for implementing an (m,n)-auditable register. We prove that it is also necessary, by showing that an (m,n)-auditable register can be used to solve consensus among m+n processes.

Beyond registers, we explore auditability for more expressive synchronization primitives, like load-linked/store-conditional (LL/SC) objects [17]. The LL operation reads a value from a memory location, while the SC operation writes a new value to the same location only if no process has written to it since the LL operation. If another process has changed the value, the SC fails, requiring the operation to be retried. LL/SC enables the efficient construction of a wide range of non-blocking data structures [10]. We leverage the algorithmic ideas of our auditable register to construct an algorithm that implements an LL/SC object for n processes, using 2⁢n-sliding register.

Finally, we relate auditable registers to Deny Lists [11], showcasing how auditability can be leveraged to build security primitives. Allow Lists and Deny Lists, as defined by Frey, Gestin, and Raynal [11], are two access control objects that give designated processes (called managers) the ability to grant and/or revoke access rights for a given set of resources. Their work specifies and investigates the synchronization power of Allow Lists and Deny Lists; the latter in two flavors, with and without an anti-flickering property. (An anti-flickering Deny List ensures that transient revocations do not undermine long-term access control policies.)

We give a relatively simple specification of an immediate Deny List, which is stronger than the anti-flickering Deny List of Frey et al., and show that it can be efficiently implemented from auditable registers. The step complexity of the resulting implementation (polynomially) depends on the number of resources and the number of processes. In contrast, while being wait-free, the step complexity of the anti-flickering Deny List implementation in [11] grows with the number of operations, and is, essentially, unbounded.

Related Work

Auditability was introduced by Cogo and Bessani [8] in the context of replicated registers. They considered a register as an abstraction for distributed storage that provides read and write operations to clients. Cogo and Bessani define auditability in terms of two properties: completeness ensures that all readers’ data access are detected, while accuracy ensures that readers who do not access data are not wrongly incriminated. They present an algorithm to implement an auditable regular (non-atomic) register, using n≥4⁢f+1 atomic read/write shared objects, f of which may be faulty (writers and auditors fail only by crashing; faulty readers may be Byzantine). Their implementation relies on information dispersal schemes, where the input of a high-level write is split into several pieces, each written in a different low-level shared object. Each low-level shared object keeps a trace of each access, and in order to read, a process has to collect sufficiently many pieces of information in many low-level shared objects, which allows to audit the read.

In asynchronous message-passing systems where f processes can be Byzantine, Del Pozzo, Milani, and Rapetti [9] study the possibility of implementing an atomic auditable register. They prove that without communication between servers, auditability requires at least 4⁢f+1 servers. They also show that allowing servers to communicate with each other admits an auditable atomic register with optimal resilience of 3⁢f+1.

The auditability definition of [8] is tightly coupled with their multi-writer, multi-reader register emulation in a replicated storage system using an information-dispersal scheme. An implementation-agnostic auditability definition was later proposed by Attiya et al. [6], based on collectively linearizing read, write, and audit operations. They show that auditing adds power to reading and writing, as it allows to solve consensus, implying that auditing requires strong synchronization primitives. They also give several implementations that use non-universal primitives (like swap and fetch&add), for a single writer and either several readers or several auditors (but not both).

Recent work [4] have extended auditability to ensure that even a curious (but honest) reader cannot effectively read data without being audited; in fact, curious readers cannot even audit other readers. The paper provides implementations of several auditable objects, including registers. However, the constructions depend on universal primitives, including compare&swap, in contrast to our constructions, which only employ sliding registers, whose consensus number is bounded.

Alhajaili and Jhumka [1] study an interesting variant of auditability with malicious processes, with and without a trusted party. Their definition of auditability has to do with the ability of determining if a system runs as specified, and determine the incorrect behavior in case it does not. This involves systematically tracking and recording system activities to facilitate fault detection and diagnosis. The authors propose methodologies for integrating auditability into system design, emphasizing its role in simplifying the debugging process and improving overall system robustness.

Our algorithms (like most prior work) maintain a large amount of auditing information, which grows with the number of operations performed in an execution. Hajisheykhi, Roohitavaf, and Kulkarni [13] investigate how to reduce the space used for saving auditing data (to be used to restore the state after a fault), by leveraging causal dependencies among them. They propose protocols for ensuring accountability in distributed systems when auditable events – deviations from standard protocols – occur. They introduce two self-stabilizing protocols: an unbounded state space protocol that propagates auditable events across all nodes and a more efficient bounded state space protocol that achieves the same awareness without increasing resource demands. Their approach ensures that before a system can recover from an auditable event, all processes are aware of it, preventing unauthorized restorations and reinforcing accountability.

Access control objects regulate access to resources by defining policies for granting or denying permissions. Some of the most common access control mechanisms include Access Control Lists [21], which specify allowed or denied actions for individual users or processes, and Capability-Based Access Control [18], where access is granted through transferable tokens rather than predefined rules. Role-Based Access Control [20] simplifies management by assigning permissions to roles instead of individuals, making it widely used in enterprise environments, while Attribute-Based Access Control [15] dynamically evaluate attributes such as user location, device type, and time of access. AllowLists and DenyLists [11] further control access by explicitly specifying permitted or blocked users or processes, often used in security filters and authentication systems.

An area related to auditability is data provenance (also called lineage) in databases [7, 12], which involves tracking the origin and transformations of data, focusing on its lineage across different processes or systems. Provenance is concerned with the integrity, quality, and reproducibility of data as it moves through various stages, such as aggregation or computation. While both auditability and provenance track interactions with data, auditability is more focused on recording who performed an operation, primarily for access control and security, while provenance aims to provide transparency about the history and transformations of the data for purposes such as verification and accountability in data analysis.

Summary of Our Contributions and Organization of the Paper

  • ■

    We extend auditability from single-writer to multi-writer registers and characterize the necessary and sufficient consensus number needed for their implementation.

  • ■

    We introduce and implement auditable LL/SC objects, demonstrating auditability can be provided beyond read / write operations.

  • ■

    We construct an anti-flickering Deny List object from auditable registers, illustrating the connection between auditability and access control mechanisms.

Section 2 presents our model and formally defines auditable shared objects. Sections 3 and 4 prove the necessary and sufficient conditions for auditable multi-writer registers, respectively. Section 5 describes how to implement auditable LL/SC objects. Section 6 presents the algorithm to implement an anti-flickering Deny List object with auditable registers. Finally, Section 7 concludes with open questions and future directions. Proofs omitted due to space constraints can be found in the full version [5].

2 Definitions

We use a standard model, in which a set of processes p1,…,pn, communicate through a shared memory consisting of base objects. The base objects are accessed with primitive operations. In addition to atomic registers, our implementations use k-sliding registers, whose consensus number is exactly k [19]. Specifically, a k-sliding register [19] stores the sequence of the last k values written to it (or the last x values when only x<k values have been written). A w⁢r⁢i⁢t⁢e with input v appends v at the end of the sequence and removes the first one if the sequence is already of size k. A r⁢e⁢a⁢d operation returns the current sequence. A standard read / write register is a 1-sliding register.

An implementation of a (high-level) object T specifies a program for each process and each operation of the object T; when receiving an invocation of an operation, the process takes steps according to this program. Each step by a process consists of some local computation, followed by a single primitive operation on a base object. The process may change its local state after a step, and it may return a response to the operation of the high-level object.

In order not to confuse operations performed on the implementation of the high-level object T and primitives applied to base objects, the former are denoted with capital letters and the later in normal font.

A configuration C specifies the state of every process and of every base object. An execution α is an alternating sequence of configurations and events, starting with an initial configuration; it can be finite or infinite. An operation completes in an execution α if α includes both the invocation and response of the operation; if α includes the invocation of an operation, but no matching response, then the operation is pending. An operation o⁢p precedes another operation o⁢p′ in α if the response of o⁢p appears before the invocation of o⁢p′.

A history H is a sequence of invocation and response events. The notions of complete, pending and preceding operations extend naturally to histories.

The standard correctness condition for concurrent implementations is linearizability [14]: intuitively, it requires that each operation appears to take place instantaneously at some point between its invocation and its response. Formally:

Definition 1.

Let 𝒜 be an implementation of an object T. An execution α of 𝒜 is linearizable if there is a sequential execution λ⁢(α) (a linearization of the operations on T in α) such that:

  • ■

    λ⁢(α) contains all complete operations in α, and a (possibly empty) subset of the pending operations in α (completed with response events),

  • ■

    If an operation o⁢p precedes an operation o⁢p′ in α, then o⁢p appears before o⁢p′ in λ⁢(α), and

  • ■

    λ⁢(α) respects the sequential specification of the high-level object T.

𝒜 is linearizable if all its executions are linearizable.

An implementation is wait-free if, whenever there is a pending operation by process p, this operation returns in a finite number of steps by p.

An auditable register supports, in addition to the standard read and write operations, also an audit operation that reports which values were read by each process [6]. An audit has no parameters and it returns a set of pairs, (j,v), where j is a process id, and v is a value of the register. A pair (j,v) indicates that process pj has read the value v. The sequential specification of an auditable register enforces, in addition to the usual specification of read and write operations, that a pair appears in the set returned by an audit operation if and only if it corresponds to a preceding read operation.

We implement a load-linked / store-conditional (LL/SC) variable, supporting the following operations: LL⁢(x) returns the value stored in x, and SC⁢(x,𝑛𝑒𝑤) writes the value 𝑛𝑒𝑤 to x, if it was not written since the last LL⁢(x) performed by the process; otherwise, x is not modified. SC returns true if it writes successfully, and false otherwise. An auditable LL/SC variable adds an audit operation, whose sequential specification returns a set of process-value pairs, corresponding to preceding LL operations.

3 Consensus number of 𝒏-Writer, 𝒎-Reader Auditable Register ≥𝒎+𝒏

An (m,n)-auditable register can be written by n processes, read by m processes, and be audited by all processes. An audit operation returns a set of pairs (p,v) where p is a process id, and v is a value. This set holds the values returned by the read operations that precede the audit.

Theorem 2.

For every pair of integers m,n>0, there is an (m+n)-process consensus algorithm using (m,n)-auditable registers.

Proof.

The proof is by induction on ℓ=n+m. The base case, ℓ=2, is proved in [6, Proposition 19].

For the induction step, assume the lemma holds for all pairs of values n′,m′, such that n′+m′=ℓ≥2, and we prove it for ℓ+1>2. Pick m>0,n>0 such that n+m=ℓ+1; note that m,n≤ℓ. To solve consensus among ℓ+1 processes p1,…,pℓ+1, we partition the processes into two sets: R (the readers) of size m, and W (the writers) of size n. Since m>0 and n>0, both sets R and W are non-empty.

Each process pi,1≤i≤ℓ+1 has a standard single-writer multi-reader register Si. By the induction hypothesis, since n≤ℓ, the n writers can agree on one of their proposals with an n-process consensus that uses (1,n−1)-auditable registers. Similarly, the m readers can agree on one of their proposal using (m−1,1)-auditable registers. Each reader and writer process pi writes the value agreed upon in its register Si.

We use now one (m,n)-auditable register, A⁢R, whose initial value is ⊥. Writers and readers access A⁢R to select one of the two consensus values. Each writer ∈W writes ⊤ to A⁢R and each reader ∈R performs a read operation on A⁢R. Writers and readers then audit A⁢R. If the set returned is empty or contains no pair (pr,⊥) where r∈R, then the first operation performed on A⁢R is a write and the writers win. Then, the decision for consensus can be read from at least one of the registers of the writers. Otherwise, the audit operation returns a set containing a pair (pr,⊥) with r∈R. In that case, the first operation performed on A⁢R is a read operation and the readers win. As in the previous case, the decision for consensus can be found by reading the readers’ registers. ◀

4 Implementing an 𝒏-Writer 𝒎-Reader Auditable Register Using (𝒏+𝒎)-Sliding Registers

We present a wait-free and linearizable implementation of an n-writer m-reader auditable register; it can support any number of auditors. The implementation uses (m+n)-sliding registers. Since the consensus number of (m,n)-auditable registers is m+n (Theorem 2), objects with consensus number ≥m+n, like (m+n)-sliding registers, are required. (Objects with consensus number ∞, like compare&swap, can also be used [4], but our goal is to use objects with the minimal consensus number.) Our main result is:

Theorem 3.

There is a wait-free linearizable implementation of an m-reader, n-writer auditable register from (m+n)-sliding registers. The step complexity of each operation is in O⁢(m+n).

4.1 The Algorithm

An implementation of an auditable register has to keep track of the latest value written to the register as well as, for each written value, its set of readers. This can be easily achieved using a single sliding register 𝑆𝐿𝑅, provided that its window is unbounded. Such a register hence stores the complete sequence of values written to it, ordered by the oldest first but has infinite consensus number. To perform a write(v), a writer simply writes v to 𝑆𝐿𝑅. For auditing purpose, a reader pi first writes its identifier i to the sliding register, before reading it. The value returned by this read is then the nearest non-identifier value in the sequence read from 𝑆𝐿𝑅 previous to the identifier i written by pi. The reader set of each value can easily be inferred from the sequence stored in 𝑆𝐿𝑅. For a value v in the sequence, its reader set is the set of processes whose identifiers follows v, and are before the first non-identifier value that succeeds v, if any.

Our implementation (Algorithms 1 and 2) is based on this simple idea, but instead of a single sliding register with an unbounded window, we use an unbounded array S⁢L⁢R⁢[−1,…] of sliding registers, each with a bounded window of size m+n. In order not to confuse identifiers and written values, write operations insert into the sliding registers w-tuples of the form (𝗐,j,v,h), where j the identifier of the writer, v is the input value of the write operation, and h a helping set of readers’ identifiers (whose role will be explained later).

Algorithm 1 Multi-writer auditable register: read and write and audit.
Algorithm 2 Multi-writer auditable register: auxiliary functions getValue and readers.

Each sliding register 𝑆𝐿𝑅⁢[x] contains initially the empty sequence (), except the first 𝑆𝐿𝑅⁢[−1] whose sequence contains the w-tuple (𝗐,j0,v0,∅) where v0 is the initial value of the auditable register and j0 an arbitrary writer’s identifier. At any point in the execution, the current value v of the auditable register is found in the sliding register with highest index x whose sequence contains a w-tuple. Specifically, v is the value contained in the first w-tuple in the sequence stored in SLR⁢[x]. Similarly to the basic implementation sketched above, readers of this value (if any) are the processes whose identifiers appear before any w-tuple in the next sliding register SLR⁢[x+1].

Therefore, reading or writing the auditable register involves finding the valid sliding register (that is, one that does not contain a w-tuple) with lowest index. If this is not done with care, progress of some operation may be lost. For example, the same writer may be always the first to write in each sliding register (i.e., each non empty sequence in any sliding register starts with a w-tuple posted by this writer), thus preventing read operations from completing or other writers from changing the value of the auditable register. We also have to make sure that each writer or reader writes at most once to each sliding register. Otherwise, the auditing may become inaccurate (as readers identifiers may be removed from some sequence), or the current value of the auditable register may be lost.

To solve theses challenges, the implementation combines the following ideas:

First, we observe that a write operation can terminate after writing in a given sliding register 𝑆𝐿𝑅⁢[x], even if its corresponding w-tuple is not the first in the sequence held in 𝑆𝐿𝑅⁢[x], provided that that it is concurrent with the write operation that writes first its w-tuple into S⁢L⁢R⁢[x]. Indeed, in that case, the write operations that are late to post their w-tuple may be linearized immediately before the write whose w-tuple is first. Accordingly, the value, denoted vx, in the first w-tuple in the sequence stored in S⁢L⁢R⁢[x] is said to be visible. The values in the other w-tuple are never returned by any read operation, and are thus invisible.

Second, we use a max register M to store the current smallest index w⁢i⁢d⁢x of the still valid sliding registers. Recall that a max register retains the largest value written to it; wait-free and linearizable max registers can be implemented from atomic read/write registers with linear step complexity [3]. A write thus starts by retrieving this index from M, writes its w-tuple in S⁢L⁢R⁢[w⁢i⁢d⁢x], and finally updates M with the new index w⁢i⁢d⁢x+1. This ensures that, if several write operations post w-tuples in the same sliding register S⁢L⁢R⁢[x], they are concurrent.

In addition, M stores an m-vector r⁢i⁢d⁢x of indexes of sliding registers (which is part of the helping mechanism described next) and, for convenience, the a⁢u⁢d⁢i⁢t⁢s⁢e⁢t of the values written whose set of readers is already completely determined (the set of readers of each visible value vx, for x<w⁢i⁢d⁢x). Triples (w⁢i⁢d⁢x,r⁢i⁢d⁢x,a⁢u⁢d⁢i⁢t⁢s⁢e⁢t) are ordered by their first field. An audit operation therefore reads M, and for M.w⁢i⁢d⁢x=x, gets the definitive readers of values vx′,x′≤x−2 from M.a⁢u⁢d⁢i⁢t⁢s⁢e⁢t, to which it adds the possibly non-definitive set of readers of vx−1 by reading S⁢L⁢R⁢[x].

Finally, a helping mechanism is used to make sure that read operations are wait-free. The set of readers of the visible value vx (that appears in the first w-tuple stored in S⁢L⁢R⁢[x]) are the processes whose identifiers are before any w-tuple in S⁢L⁢R⁢[x+1] or are in the helping set h of the first w-tuple of S⁢L⁢R⁢[x+1]. An additional array H indicates, for each reader, the index of the latest sliding register in which it attempted to write its identifier before any w-tuple. The array r⁢i⁢d⁢x (stored, as seen above, in the max register M), records for each reader the highest index of a sliding register in which it has received help (that is, the identifier of the reader is included in the helping set of the first w-tuple of that sliding register). A writer pj hence determines if a given reader pi needs help by comparing H⁢[i] and M.r⁢i⁢d⁢x⁢[i]. If M.r⁢i⁢d⁢x⁢[i]<H⁢[i], pi has an ongoing read operation, and i is therefore added to the helping set of the w-tuple of the writer. Similarly, reader pi discovers if it has received help by comparing M.r⁢i⁢d⁢x⁢[i] with the index of the latest sliding register in which it writes its identifier.

Hence, besides w-tuples, a given sliding register S⁢L⁢R⁢[x] may also include identifiers i of readers, with the following meaning:

  1. 1.

    If i appears before the first w-tuple in S⁢L⁢R⁢[x], then pi’s read returns vx−1, which is the value stored in the first w-tuple in S⁢L⁢R⁢[x−1].

  2. 2.

    If i appears in the helping set of the first w-tuple in S⁢L⁢R⁢[x], then pi’s read also returns vx−1 as in the previous case.

  3. 3.

    If i appears after the first w-tuple, then it is too late and fails to read vx−1.

The reader processes satisfying Cases (1) and (2) are said to be recorded in S⁢L⁢R⁢[x]. The function readers in Algorithm 2 returns the ids of readers recorded in a sliding register (which is used, in particular, to update the audit set). The processes satisfying Case (2) are called helped in S⁢L⁢R⁢[x].

Regarding Case (3), we prove that after at most two failed attempts, a reader pi receives help, or succeeds in appearing before any w-tuple in a sliding register. The algorithm also ensures that a read operation is helped at most once. Before an attempt to write its id into S⁢L⁢R⁢[x], reader pi knows, by checking if r⁢i⁢d⁢x⁢[i]≥H⁢[i], if it has already received help. If this is the case, it directly returns the corresponding value without updating H⁢[i].

4.2 Proof of Correctness

In this section, we prove Theorem 3, starting with basic properties. We show that each operation returns within O⁢(m+n) of its own steps, and then explain how to construct a sequential execution λ that contains all completed operations in an execution α, and some pending operations. Lemma 13 shows that λ preserves the real-time order between operations in α. By Lemma 14, Lemma 15, and Lemma 16, λ is a sequential execution of a m-reader, n-writer auditable register.

To proceed with the detailed proofs, fix a finite execution α of the algorithm. We start with some basic properties. Lemma 4, whose proof is in the full version, shows that that each sliding register retains the complete history of the 𝗐𝗋𝗂𝗍𝖾s applied to it.

Lemma 4.

Each process applies at most one 𝗐𝗋𝗂𝗍𝖾 to S⁢L⁢R⁢[k], for any k≥0,

The max register M stores a triple (w⁢i⁢d⁢x,r⁢i⁢d⁢x,a⁢u⁢d⁢i⁢t⁢s⁢e⁢t), where r⁢i⁢d⁢x is a m-vector and a⁢u⁢d⁢i⁢s⁢e⁢t a set of (process,value) pairs. Triples are ordered in increasing order of their first element. At any point in the execution, the triple stored in M is thus a triple with the largest first member written to M. We also partially order m-vectors as follows: r⁢i⁢d⁢x≤r⁢i⁢d⁢x′ if and only ∀i∈{1,…,m},r⁢i⁢d⁢x⁢[i]≤r⁢i⁢d⁢x′⁢[i].

Proposition 5.

The successive values of M.w⁢i⁢d⁢x are 0,1,2,….

In the full version, we prove the following lemma by induction on k.

Lemma 6.

Suppose 𝗐𝗋𝗂𝗍𝖾𝖬𝖺𝗑⁢(k,i⁢v,_) and 𝗐𝗋𝗂𝗍𝖾𝖬𝖺𝗑⁢(k′,i⁢v′,_) are applied to M. (1) if k=k′ then i⁢v=i⁢v′ and, (2) if k<k′ then i⁢v≤i⁢v′.

By Proposition 5, the successive values of M.w⁢i⁢d⁢x are 0,1,… By Lemma 6(1), M.r⁢i⁢d⁢x remains the same while M.w⁢i⁢d⁢x does not change. Lemma 6(2) implies that the successive vectors in M.r⁢i⁢d⁢x are ordered and form an increasing sequence.

Let 𝑊𝐼𝐷𝑋 denote the highest index of a sliding register to which a w-tuple has been written. That is, at the end of a finite execution α, 𝑊𝐼𝐷𝑋=k if and only a w-tuple was written in S⁢L⁢R⁢[k], and no w-tuple was written in S⁢L⁢R⁢[k′], for any k′>k. When 𝑊𝐼𝐷𝑋 is changed to k+1 as a result of some process p applying 𝗐𝗋𝗂𝗍𝖾⁢(𝗐,_,_,_) to S⁢L⁢R⁢[k+1], M.w⁢i⁢d⁢x≥k+1. Indeed, before writing a w-tuple to S⁢L⁢R⁢[k+1], p has read k from M.w⁢i⁢d⁢x in line 30. Observe also that when M.w⁢i⁢d⁢x is changed from k to k+1 by some process p, M.w⁢i⁢d⁢x≥k. Indeed, before applying M.𝗐𝗋𝗂𝗍𝖾𝖬𝖺𝗑⁢(k+1,_,_), p reads a sequence from S⁢L⁢R⁢[k] that contains a w-tuple (line 11 or line 22, p is performing a read), or has written a w-tuple to S⁢L⁢R⁢[k] (line 35, p is performing a write). This implies that M.w⁢i⁢d⁢x is always in {𝑊𝐼𝐷𝑋,𝑊𝐼𝐷𝑋−1}, which shows:

Proposition 7.

For every x≥0, if S⁢L⁢R⁢[x] is accessed then S⁢L⁢R⁢[x−1] contains a w-tuple.

Combining these observations with Lemma 6(2), we have:

Lemma 8.

For some k≥0, the finite execution α can be written as either D0⁢ρ0⁢E0⁢μ1⁢D1⁢ρ1⁢E1⁢…⁢μk⁢Dk or D0⁢ρ0⁢E0⁢μ1⁢D1⁢ρ1⁢E1⁢…⁢μk⁢Dk⁢ρk⁢Ek, where:

  • ■

    ρℓ is the first step that writes a w-tuple to S⁢L⁢R⁢[ℓ] (applied by a writer, line 35), μℓ is the step that changes M.w⁢i⁢d⁢x from ℓ−1 to ℓ (applied within a read, line 26 or line 16, or a write, line 38).

  • ■

    in any configuration in Dℓ, M.w⁢i⁢d⁢x=ℓ=𝑊𝐼𝐷𝑋+1, and in any configuration in Eℓ, M.w⁢i⁢d⁢x=ℓ=𝑊𝐼𝐷𝑋

Therefore, the first step that writes a w-tuple to S⁢L⁢R⁢[x] is preceded by steps ρ0,…,ρx−1 that write w-tuples to S⁢L⁢R⁢[0],…,S⁢L⁢R⁢[x−1], and they are never deleted (by Lemma 4).

Let x0 be the value of the local variable l⁢s⁢r when read operation o⁢p by process pi starts.

Proposition 9.

If o⁢p enters the repeat loop (line 12), then x0<x1<x2<… where xk, k>0, is the value read from M.w⁢i⁢d⁢x (line 18) at the beginning of the kth iteration.

If o⁢p does not terminate in the kth iteration of the loop (line 20), after reading (xk,_,_) from M, then xk is written to H⁢[i] (line 21) before an attempt is made to place i ahead of any w-tuple in S⁢L⁢R⁢[xk]. In the full version, we further prove:

Lemma 10.

If xk is written to H⁢[i] then i∉readers(w⁢i⁢n), for any sequence w⁢i⁢n in any sliding register S⁢L⁢R⁢[x],x0<x<xk.

Finally, we prove, in the full version, that o⁢p does not find help in S⁢L⁢R⁢[x], for any x,x0<x<x1.

Lemma 11.

i∉readers(w⁢i⁢n), for any sequence w⁢i⁢n in a sliding register S⁢L⁢R⁢[x], x0<x<x1.

An audit operation reads M once and a single sliding register. A write operation applies a single 𝗐𝗋𝗂𝗍𝖾𝖬𝖺𝗑 and a single 𝗋𝖾𝖺𝖽 to M, reads O⁢(m) registers and writes O⁢(1) registers. Since there is a linearizable implementation of max registers for (m+n) processes using registers with O⁢(m+n) step complexity per operation [3], this implies that the step complexity of a write or a audit operation is in O⁢(m+n).

Lemma 20 (Appendix A) shows that read operations are also wait-free, by proving that the repeat loop has at most 3 iterations. This is because a writer may place a w-tuple in at most one sliding register without detecting a concurrent read operation and helping it.

To prove linearizability, let H be the history of read, write and audit operations in the execution α. For simplicity, we assume that the values written to the register in α are unique. We start by classifying the operations in H. Each classified operation o⁢p is also associated with an integer i⁢d⁢x⁢(o⁢p), which is the index of a sliding register.

For read, we distinguish silent, direct and helped operations. Let o⁢p be a read operation by some process pi. We denote by x0 the value the local variable l⁢s⁢r when o⁢p starts.

  • ■

    r⁢o⁢p is silent if it is not the first read operation by pi and it immediately returns after reading S⁢L⁢R⁢[x0] (line 12). This corresponds to the case in which no new write operation has occurred since the last read by pi. We set i⁢d⁢x⁢(o⁢p)=x0.

If there is no x>x0 for which i∈readers⁢(𝑆𝐿𝑅⁢[x]), o⁢p is unclassified. In that case, note that o⁢p has no response in H. Otherwise, let x1>x0 be the smallest index such that i∈readers(𝑆𝐿𝑅⁢[x1]). We set i⁢d⁢x⁢(o⁢p)=x1 and say that

  • ■

    o⁢p is direct if i precedes any w-tuple in S⁢L⁢R⁢[x1], and helped otherwise, as in that case, i appears in the helping set of the first w-tuple in S⁢L⁢R⁢[x1].

A write(v) operation o⁢p by some process pj applies at most one write to a sliding register (line 35). o⁢p is unclassified if does not write to a sliding register. Otherwise, let x be the index of the sliding register o⁢p writes to. x=i⁢d⁢x⁢(o⁢p) and we say that

  • ■

    o⁢p is visible if (𝗐,j,v,_) is the first w-tuple written to S⁢L⁢R⁢[x1], and hidden otherwise.

For audit, only operations that have a response in H are classified. Let o⁢p be an audit operation that terminates. We define i⁢d⁢x⁢(o⁢p)=x, where x is the value read from M.w⁢i⁢d⁢x in the first step of o⁢p (line 40). o⁢p is non-definitive if there is no w-tuple in the sequence it reads from S⁢L⁢R⁢[x] (in line 41), and definitive otherwise. Indeed, once a w-tuple has been written to S⁢L⁢R⁢[x], the set of readers of vx−1 no longer changes, while read operations may still return vx−1 after o⁢p terminates otherwise (vx−1 the value in the first w-tuple in S⁢L⁢R⁢[x−1].). In Appendix A, we prove:

Lemma 12.

If an operation o⁢p terminates before an operation o⁢p′ starts in H′, then i⁢d⁢x⁢(o⁢p)≤i⁢d⁢x⁢(o⁢p′).

We define H′ that contains every completed operation of H as well as some incomplete operations, to which we add a matching response. We first discard from H every audit and every silent read invocation without a matching response, as well as every invocation of an unclassified read and write operation. We then add at the end a response for each remaining read and write operation that has no response in H. The return value of a read operation o⁢p with i⁢d⁢x⁢(o⁢p)=x is the value v⁢a⁢l in the first w-tuple in (𝗐,_,v⁢a⁢l,_) in S⁢L⁢R⁢[x−1]. Responses are added in arbitrary order.

A linearization λ⁢(α) of α is defined in two steps. We first order operations in H′ according to their associated index, in ascending order (rule R⁢0). We then order operations with the same index. Let B⁢(x) be the set of operations o⁢p∈H′ such that i⁢d⁢x⁢(o⁢p)=x. These operations are ordered according to the following rules.

  1. R1

    We place first silent read, direct read and non-definitive audit operations. They are ordered according to the order in which they apply a read (for silent read and non-definitive audit) or a write (for direct read) to S⁢L⁢R⁢[x] in α.

  2. R2

    We then place helped read in arbitrary order, followed by the definitive audit operations. The definitive audit are ordered according to the order in which they apply a read to S⁢L⁢R⁢[x] in α.

  3. R3

    We next put every hidden write. They are ordered according to the order in which their write to S⁢L⁢R⁢[x] is applied in α.

  4. R4

    The (unique) visible write is placed last.

Let λ be the linearization obtained by applying linearization rules R⁢0-R⁢4 to the operations in H′. In Appendix A, we prove:

Lemma 13.

If an operation o⁢p terminates before an operation o⁢p′ starts in H′, then o⁢p precedes o⁢p′ in λ.

Lemma 14.

If read operation o⁢p in H′ returns v, then v is the value written by the last write that precedes o⁢p in λ, or the initial value v0 if there is no such write.

Finally, we prove (in Appendix A) that a pair (p,v) is in the set returned by an audit operation o⁢p if and only if there is a read by p returning v precedes o⁢p.

Lemma 15.

Let a⁢o⁢p be an audit operation in H′ that returns A. If there is a read operation r⁢o⁢p by process pj returning v and that precedes a⁢o⁢p in λ, (j,v)∈A.

Lemma 16.

Let a⁢o⁢p be an audit operation in H′ whose response contains (j,v). There exists a read operation by pj returning v that precedes a⁢o⁢p in λ.

5 Auditable LL/SC from 𝟐⁢𝒏-Sliding Register

We show how to adapt our auditable register algorithm to implement an auditable LL/SC object for n processes, and an arbitrary number of auditors. An audit operation returns a set of pairs (p,v), representing the values returned by the processes by the ll operations preceding the audit. The implementation uses 2⁢n-sliding registers, showing:

Theorem 17.

There is a wait-free, linearizable implementation of an n-process auditable LL/SC object from 2⁢n-sliding registers and standard registers with O⁢(n) step complexity per operation.

Algorithm 3 is essentially the same as Algorithm 1. ll operations are identified with read operations, and sc with write. At the end of a finite execution α of Algorithm 1, the sequences stored in the sliding registers in the array S⁢L⁢R indicate, for each x, which is the xth value vx held in the auditable register, and which processes write or read this value. Specifically, given the sequence w⁢i⁢nx stored in S⁢L⁢R⁢[x], the first w-tuple (𝗐,j,v,h) in w⁢i⁢nx indicates that vx=v, and its writer is pj. The readers of vx−1 are the processes pi, where i∈h, or precedes (𝗐,j,v,h) in w⁢i⁢nx. Each other w-tuple (𝗐,j′,v′,_) in w⁢i⁢nx corresponds to an invisible write operation, whose input v′ is never read. We may think as these operations as unsuccessful, in the sense that they fail to change the value of the auditable register, being immediately overwritten by another write.

Algorithm 3 n-process LL/SC with auditable LL.

Alternatively, we may think of the sequences in S⁢L⁢R as a trace of an execution β of an LL/SC object implementation by identifying reads with ll and writes with sc. Again, the xth value held by the object in β is vx, the value in the first w-tuple (𝗐,j,v,h) in w⁢i⁢nx. Each process pi, with pi∈h or preceding this tuple has an ll that returns vx−1. The first w-tuple (𝗐,j,v,h) indicates a successful sc⁢(v) by process pj, that changes the object from vx−1 to vx=v. And every following tuple (𝗐,j′,v′,_) marks an unsuccessful sc⁢(v′) by process pj′. Recall that, per its specification, an sc is successful if and only if it is preceded by an ll by the same process, without any successful sc operation between them. In particular, β is a valid sequential execution if (1) in each sequence w⁢i⁢nx, the first w-tuple (𝗐,j,v,h) is after pj’s ll and (2) each sc(v′) operation corresponding to a following (𝗐,j′,v′,_) tuple is after sc(v) in β.

The code of an ll operation is the same as for a read operation in Algorithm 1, while audit and the auxiliary functions getValues and readers are identical. sc operations follow the code of write, with two additions (line 9 and line 18) highlighted in gray.

To maintain property (1), an sc operation o⁢p by process pi should be prevented from writing a w-tuple to a sliding register S⁢L⁢R⁢[x] in which pi ’s last ll is not recorded. In Algorithm 1, the local variable l⁢s⁢r of a process pi is the highest index of a sliding register that keeps track of pi’s last read, and hence here, S⁢L⁢R⁢[l⁢s⁢r] records pi’s last ll. Therefore, before writing to S⁢L⁢R⁢[w⁢i⁢d⁢x] (in line 14), pi checks that l⁢s⁢r=w⁢i⁢d⁢x. If this is not the case, a successful sc has occurred since pi’s last ll, and o⁢p may immediately return false (line 9). The other addition is the return statement at line 18: true is returned if pi’s w-tuple is the first in S⁢L⁢R⁢[w⁢i⁢d⁢x], and false otherwise.

For property (2), the linearization rules are slightly modified. In Algorithm 1, write operations recorded in the same sliding register S⁢L⁢R⁢[x] are linearized in the reverse order of their corresponding w-tuple appearance in the sequence stored in S⁢L⁢R⁢[x]. Here, we do the opposite, linearizing sc operations in the same order their corresponding w-tuple appear in S⁢L⁢R⁢[x]. Only the first w-tuple represents a successful sc, which is aligned with the return statement of line 18.

Finally, as each process may write twice to a sliding register, once in an ll operation, and once in a sc operation, S⁢L⁢R is an array of 2⁢n-sliding registers. The code of audit may easily be adapted to report which process has successfully stored which value instead of or in complement to values returned by ll operations to the processes.

The code of audit is the same in Algorithm 1 and Algorithm 3, and the same code is shared by read and ll operations. For sc, the additional statements (line 9 and line 18) in the code do not affect termination or step-complexity. Therefore, the step complexity of ll, sc, and audit is O⁢(n).

Fix a finite well-formed execution β, in which each process alternates ll and sc operations. Thanks to the similarities in the code, a linearization μ⁢(β) of β can be obtained from a linearization λ⁢(α) of an execution α of the auditable register implementation induced by β. α is constructed as follows. We introduce a new class for sc operations that terminate immediately after reading M.w⁢i⁢d⁢x in line 9. Those operations are said to be silent (similarly to silent read operations). We next extract from β an execution α of Algorithm 1 by removing all steps applied by silent sc, and replacing each invocation of sc and ll by and invocation of write and read, respectively, with the same input. α is a valid execution of Algorithm 1, as besides early termination for sc (line 9), which we dispose of by removing steps of silent sc operations, the code of sc and ll is the same as the code of write and read, respectively, and the code for audit is identical. We explain in Appendix B how a linearization μ⁢(β) can be inferred from the linearization λ⁢(α) of α.

6 Immediate Deny List from Auditable Registers

A Deny List [11] is used to control resources, by having a set of managers maintain a list of which users are unauthorized to access which resources. To access a resource, a user must prove that the corresponding user-resource pair has not been added to the Deny List. The managers have to agree on the set of process-resource pairs in the Deny List. A Deny List has an anti-flickering property that ensures that there are no transient periods: once access is disallowed, it is never allowed again.

More formally, a deny list object over a set of resources S supports three operations, for x∈S: append⁢(x), prove⁢(x) which returns a Boolean value, and read⁢(), which returns a set of process-resource (p,x) pairs. A prove⁢(x) that returns false is invalid; otherwise, it is valid. The intuition is that an append⁢(x) revokes the authorization to access a resource x to all processes. A valid prove⁢(x) by process p indicates that p is authorized to access x. The set of processes that can invoke append is called the managers, and those that can invoke prove are called the provers. These sets of processes are predefined and static. The property termination requires that the operations prove, append, and read return within a finite number of steps.

In the original definition [11], an append can be successful or unsuccessful. Their sequential specification in the anti-flickering flavor of a deny list is as follows:

Append progress:

Only a finite number of append⁢(x) operations are unsuccessful; that is, append⁢(x) is eventually successful.

Prove progress:

After a successful append⁢(x) operation, only a finite number of prove⁢(x) operations can be valid; that is, prove⁢(x) is eventually invalid after a successful append⁢(x).

Prove validity:

A prove⁢(x) operation is invalid only if a successful append⁢(x) operation appears before it.

Prove anti-flickering:

If a prove⁢(x) operation o⁢p is invalid, then all following prove⁢(x) operations are invalid.

Read validity:

The set of object-process pairs returned by a read⁢() operation includes exactly all preceding valid prove⁢(x) operations and the processes that invoked them.

We consider a stronger version, called immediate deny list, where all append⁢(x) are successful, and where all prove⁢(x) operations that follow an append⁢(x) are invalid. The sequential specification for the immediate deny list is therefore as follows:

Strong prove validity:

A prove⁢(x) operation is invalid if and only if an append⁢(x) operation appears before it.

Read validity:

The set of object-process pairs returned by a read⁢() operation includes exactly all preceding valid prove⁢(x) operations and the processes that invoked them.

An Immediate Deny List guarantees all the properties of the Anti-flickering Deny List: Since all append⁢(x) are successful, we trivially guarantee Append progress. Our Strong prove validity includes the Prove validity and Prove progress where the number of prove⁢(x) that can be valid after an append⁢(x) is 0. Prove anti-flickering is trivially implied by our Strong prove validity property.

It is already known that the consensus number of an Anti-flickering Deny List object where n processes can both do append⁢(x) and prove⁢(x), denoted anti-flickering n-deny list, is n [11]. In particular, they show how to solve consensus among n processes using this object with a single resource. Thus, an Anti-flickering n-deny list has at least consensus number n, and therefore, the consensus number of an immediate n-deny list is also at least n.

They also present an algorithm to show that the consensus number of the anti-flickering n-deny list over a set of resources S is at most n. In the following, we show how to implement (Algorithm 4) an immediate-n-deny list object using (1,n−1)-auditable registers, which have consensus number n as proved in Sections 3 and 4. This proves that the immediate n-deny list has consensus number at most n. Our algorithm provides a somewhat simpler proof for their upper bound. We present the algorithm for a single resource. The generalized version can be easily built thanks to the locality property of linearizability, and by implementing the read⁢() on the set of resource 𝒮 using classical techniques to implement a snapshot by applying the read⁢() on each x∈𝒮.

Algorithm 4 implements an immediate n-deny list for a resource x. It uses a vector A⁢Rx⁢[1⁢…⁢n] of binary auditable registers, initially true. A⁢Rx⁢[i] is written by process pi and read by all other processes. When a process pi wants to perform append⁢(x), it writes false in its auditable register A⁢Rx⁢[i] and locally stores the information that it did an append.

To perform prove⁢(x), a process simply checks if it previously did an append⁢(x), and if not, it reads all the auditable registers (but its own) to check if some process wrote into one such register. If none of the previous conditions happen, then it can return t⁢r⁢u⁢e.

The read⁢() repeatedly audits all the registers to collect the processes that have executed a valid prove⁢(x). These are the ones that read t⁢r⁢u⁢e in all registers. To obtain a snapshot, the read⁢() terminates when two consecutive collects returns the same set. Appendix C presents proof sketch of the correctness of the algorithm.

Algorithm 4 Immediate n deny-list object from auditable registers, code for process pi.

7 Conclusions and Future Work

In this work, we extended the concept of auditability from single-writer registers to more general shared objects. We start by providing a rigorous characterization of the synchronization power required to support auditable multi-writer registers. Our results establish a tight bound on the consensus number necessary for achieving auditability, demonstrating the feasibility of implementing auditable storage mechanisms.

Looking ahead, there are several promising directions for future research. First, extending auditability to a broader range of shared objects beyond registers and LL/SC remains an open challenge. Second, investigating the impact of adversarial behavior on auditable implementations could lead to more robust security guarantees. Finally, exploring efficient, scalable implementations of auditable objects in real-world distributed storage systems could bridge the gap between theoretical feasibility and practical deployment. In particular, while sliding registers are not supported in hardware (to the best of our knowledge), they bear resemblance to shift registers. This hardware object [16] holds the last w bits “shifted in” the register and has a functionality similar to a sliding register; the consensus number of shift registers is w [2], Although they cannot directly replace sliding registers in our implementations, our algorithmic insights might be leveraged to develop other algorithms that employ shift registers.

References

  • [1] Sara Alhajaili and Arshad Jhumka. Auditability: An approach to ease debugging of reliable distributed systems. In IEEE 24th Pacific Rim International Symposium on Dependable Computing (PRDC), pages 227–2278, 2019. doi:10.1109/PRDC47002.2019.00053.
  • [2] James Aspnes. The consensus number of a shift register equals its width, 2025. doi:10.48550/arXiv.2505.01691.
  • [3] James Aspnes, Hagit Attiya, and Keren Censor-Hillel. Polylogarithmic concurrent data structures from monotone circuits. Journal of the ACM, 59(1), March 2012. doi:10.1145/2108242.2108244.
  • [4] Hagit Attiya, Antonio Fernández Anta, Alessia Milani, Alexandre Rapetti, and Corentin Travers. Auditing without leaks despite curiosity. In Proceedings of the ACM Symposium on Principles of Distributed Computing (PODC), pages 455–465. ACM, 2025. doi:10.1145/3732772.3733516.
  • [5] Hagit Attiya, Antonio Fernández Anta, Alessia Milani, Alexandre Rapetti, and Corentin Travers. Auditable shared objects: From registers to synchronization primitives, 2025. arXiv:2508.14506.
  • [6] Hagit Attiya, Antonella Del Pozzo, Alessia Milani, Ulysse Pavloff, and Alexandre Rapetti. The synchronization power of auditable registers. In 27th International Conference on Principles of Distributed Systems OPODIS, volume 286 of LIPIcs, pages 4:1–4:23. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2023. doi:10.4230/LIPICS.OPODIS.2023.4.
  • [7] Richard A Becker and John M Chambers. Auditing of data analyses. SIAM Journal on Scientific and Statistical Computing, 9(4):747–760, 1988.
  • [8] Vinicius Vielmo Cogo and Alysson Bessani. Brief announcement: Auditable register emulations. In Seth Gilbert, editor, 35th International Symposium on Distributed Computing, DISC 2021, October 4-8, 2021, Freiburg, Germany (Virtual Conference), volume 209 of LIPIcs, pages 53:1–53:4. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2021. doi:10.4230/LIPICS.DISC.2021.53.
  • [9] Antonella Del Pozzo, Alessia Milani, and Alexandre Rapetti. Byzantine auditable atomic register with optimal resilience. In 41st International Symposium on Reliable Distributed Systems (SRDS), pages 121–132. IEEE Computer Society, 2022. doi:10.1109/SRDS55811.2022.00020.
  • [10] Faith Ellen, Panagiota Fatourou, Eleftherios Kosmas, Alessia Milani, and Corentin Travers. Universal constructions that ensure disjoint-access parallelism and wait-freedom. In ACM Symposium on Principles of Distributed Computing (PODC), pages 115–124, 2012. doi:10.1145/2332432.2332457.
  • [11] Davide Frey, Mathieu Gestin, and Michel Raynal. The synchronization power (consensus number) of access-control objects: the case of allowlist and denylist. In Rotem Oshman, editor, 37th International Symposium on Distributed Computing, DISC 2023, October 10-12, 2023, L’Aquila, Italy, volume 281 of LIPIcs, pages 21:1–21:23. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2023. doi:10.4230/LIPICS.DISC.2023.21.
  • [12] Boris Glavic et al. Data provenance. Foundations and Trends® in Databases, 9(3-4):209–441, 2021. doi:10.1561/1900000068.
  • [13] Reza Hajisheykhi, Mohammad Roohitavaf, and Sandeep S. Kulkarni. Bounded auditable restoration of distributed systems. IEEE Transactions on Computers, 66(2):240–255, 2017. doi:10.1109/TC.2016.2595578.
  • [14] Maurice P Herlihy and Jeannette M Wing. Linearizability: A correctness condition for concurrent objects. ACM Transactions on Programming Languages and Systems (TOPLAS), 12(3):463–492, 1990. doi:10.1145/78969.78972.
  • [15] Vincent C Hu, D Richard Kuhn, David F Ferraiolo, and Jeffrey Voas. Attribute-based access control. Computer, 48(2):85–88, 2015. doi:10.1109/MC.2015.33.
  • [16] Intel. x86 assembly/shift and rotate. URL: https://en.wikibooks.org/wiki/X86_Assembly/Shift_and_Rotate.
  • [17] Eric H Jensen, Gary W Hagensen, and Jeffrey M Broughton. A new approach to exclusive data access in shared memory multiprocessors. Technical report, Technical Report UCRL-97663, Lawrence Livermore National Laboratory, 1987.
  • [18] Henry M Levy. Capability-based computer systems. Digital Press, 2014.
  • [19] Achour Mostéfaoui, Matthieu Perrin, and Michel Raynal. A simple object that spans the whole consensus hierarchy. Parallel Process. Lett., 28(2):1850006:1–1850006:9, 2018. doi:10.1142/S0129626418500068.
  • [20] Ravi S Sandhu. Role-based access control. In Advances in computers, volume 46, pages 237–286. Elsevier, 1998. doi:10.1016/S0065-2458(08)60206-5.
  • [21] Ravi S. Sandhu and Pierangela Samarati. Access control: principle and practice. IEEE communications magazine, 32(9):40–48, 1994. doi:10.1109/35.312842.

Appendix A Additional Lemmas and Proofs for Section 4

We present in this appendix missing proof and additional lemmas for Section 4. Omitted proofs can be found in the full version.

The function readers extracts from a sequence read from some sliding register S⁢L⁢R⁢[x] a set of processes. This set does not change once a w-tuple has been written to S⁢L⁢R⁢[x].

Proposition 18.

If w⁢i⁢n and w⁢i⁢n′ are two sequences read from S⁢L⁢R⁢[x] after S⁢L⁢R⁢[x].𝗐𝗋𝗂𝗍𝖾⁢(𝗐,_,_,_) has been applied, then readers⁢(w⁢i⁢n)=readers⁢(w⁢i⁢n′).

Lemma 19.

M.r⁢i⁢d⁢x⁢[i]≥x if and only if S⁢L⁢R⁢[x] holds a sequence w⁢i⁢n such that i∈readers(w⁢i⁢n).

Lemma 20.

The step complexity of a read operation is in O⁢(m+n).

Lemma 12. [Restated, see original statement.]

If an operation o⁢p terminates before an operation o⁢p′ starts in H′, then i⁢d⁢x⁢(o⁢p)≤i⁢d⁢x⁢(o⁢p′).

Proof.

Let x=i⁢d⁢x⁢(o⁢p) and x′=i⁢d⁢x⁢(o⁢p′), and let pi and pi′ be the processes that perform o⁢p and o⁢p′ respectively.

We first prove that when o⁢p terminates, M.w⁢i⁢d⁢x≥x. As M.w⁢i⁢d⁢x is increasing (Proposition 5), it is enough to show that M.w⁢i⁢d⁢x≥x in a configuration in the execution interval of o⁢p. If o⁢p is a write or an audit, o⁢p writes to S⁢L⁢R⁢[x] (line 35) or reads from S⁢L⁢R⁢[x] (line 41) after reading x from M.w⁢i⁢d⁢x (line 30 or line 40).

If o⁢p is a direct read, pi writes i to S⁢L⁢R⁢[x] (line 22) after having read x from M.w⁢i⁢d⁢x (line 18). If o⁢p is helped, M.r⁢i⁢d⁢x⁢[i]=x when M is read at the beginning of some iteration of the loop (line 18). Therefore M.w⁢i⁢d⁢x>x, as the writeMax that changes M.r⁢i⁢d⁢x⁢[i] to x also set M.w⁢i⁢d⁢x to x+1 (lines 15-16, lines 25-26, or lines 37-38). If o⁢p is silent, it is preceded by direct read o⁢p′′ with the same index x, and hence M.w⁢i⁢d⁢x≥x already when o⁢p′′ terminates.

We next examine several cases according to the type of o⁢p′.

  • ■

    o⁢p′ is a silent read. In o⁢p′, S⁢L⁢R⁢[x′] is read by pi′ and does not contain a w-tuple. Hence, before o⁢p starts, 𝑊𝐼𝐷𝑋=x′−1 (the largest index of a sliding register to which a w-tuple has been written), and therefore, by Lemma 8, M.w⁢i⁢d⁢x≤x′−1, from which we have x≤x′−1, as x≤M.w⁢i⁢d⁢x when o⁢p terminates.

  • ■

    o⁢p′ is a direct or a helped read. Let x0 be the value of the local variable l⁢s⁢r when o⁢p′ starts. o⁢p′ does not terminate before reading some value x1 from M.w⁢i⁢d⁢x (line 18) in the first iteration of the repeat loop. By Lemma 11, for every y, x0<y<x1, the helping set of the first w-tuple in S⁢L⁢R⁢[y] does not contains i′. Therefore, x1≤x′=i⁢d⁢x⁢(o⁢p′) and hence x≤x′ as x≤M.w⁢i⁢d⁢x before o⁢p′ starts.

  • ■

    o⁢p′ is a write or an audit. pi′ reads x′ from M.w⁢i⁢d⁢x (line 30 and line 40, respectively). As x≤M.w⁢i⁢d⁢x when o⁢p terminates, x≤x′.

◀

To show real-time order is preserved, we first prove the following facts about the precedence of operations with the same sequence number.

Lemma 21.

Let o⁢p, o⁢p′ be two operations in H′ with i⁢d⁢x⁢(o⁢p)=i⁢d⁢x⁢(o⁢p′)=x. Let x≥0.

  1. 1.

    If o⁢p is a silent read, a direct read, or a non-definitive audit, and o⁢p′ is a helped read, a definitive audit, or a write operation, then o⁢p′ does not precede o⁢p.

  2. 2.

    If o⁢p is any operation and o⁢p′ is a write, then o⁢p′ does not precede o⁢p.

Lemma 22.

Let o⁢p be a helped read operation in H′ with i⁢d⁢x⁢(o⁢p)=x. The first write of a w-tuple to S⁢L⁢R⁢[x] happens during the execution interval of o⁢p.

Lemma 13. [Restated, see original statement.]

If an operation o⁢p terminates before an operation o⁢p′ starts in H′, then o⁢p precedes o⁢p′ in λ.

Proof.

By Lemma 12, i⁢d⁢x⁢(o⁢p)≤i⁢d⁢x⁢(o⁢p′). If i⁢d⁢x⁢(o⁢p)<i⁢d⁢x⁢(o⁢p′), o⁢p is before o⁢p′ in λ by rule R⁢0. We assume in the following that i⁢d⁢x⁢(o⁢p)=i⁢d⁢x⁢(o⁢p′)=x.

  • ■

    If o⁢p′ is a silent read, a direct read, or non-definitive audit, it follows from Lemma 21(1) that o⁢p also falls into this category. Therefore, o⁢p and o⁢p′ are both ordered in λ using rule R⁢1. They are ordered according to the order in which a step in their execution interval occurs in α. Hence, o⁢p precedes o⁢p′ in α implies that o⁢p precedes o⁢p′ in λ.

  • ■

    If o⁢p′ is a helped read or a definitive audit, it follows from Lemma 21(1) and Lemma 21(2) that o⁢p also falls into this category, or is a silent or direct read, or a non-definitive audit. In the latter case, o⁢p is ordered in λ according to rule R⁢1, and o⁢p′, rule R⁢2, from which we have that o⁢p precedes o⁢p′ in λ.

    In the former case, as o⁢p and o⁢p′ are both helped read, their execution interval intersect (Lemma 22) and thus o⁢p cannot precedes o⁢p′. If o⁢p and o⁢p′ are both definitive audit, they are placed according to the order in which they apply a read to S⁢L⁢R⁢[x] in α. Hence o⁢p is before o⁢p′ in λ. If o⁢p is an helped read and o⁢p′ a definitive audit, o⁢p is placed before o⁢p′ in λ by rule R⁢2. The last case remaining is o⁢p being a definitive audit and o⁢p′, a helped read. As o⁢p is a definitive audit, it sees a w-tuple mark in S⁢L⁢R⁢[x], but the step in which the first such tuple is written to S⁢L⁢R⁢[x] is in the execution interval of o⁢p′ (Lemma 22). Therefore o⁢p cannot terminate before o⁢p′ starts.

  • ■

    If o⁢p′ is a write visible or hidden, Lemma 21(2) implies that o⁢p cannot be a write. Therefore, o⁢p is placed according to rule R⁢1 or R⁢2, and sthus precedes o⁢p′ which is placed after, according to R⁢3 or R⁢4.

◀

Lemma 14. [Restated, see original statement.]

If read operation o⁢p in H′ returns v, then v is the value written by the last write that precedes o⁢p in λ, or the initial value v0 if there is no such write.

Proof.

Let x=i⁢d⁢x⁢(o⁢p), and let pj be the process that performs o⁢p.

We first consider the case x>0. If o⁢p is helped or direct, the value returned by o⁢p is the value v in the first w-tuple (𝗐,i,v,_) stored in S⁢L⁢R⁢[x−1] (lines 45). Note that i and v are well defined, as when pj reads from or writes to S⁢L⁢R⁢[x], a w-tuple has already be written to S⁢L⁢R⁢[s−1] (Proposition 7). Let w⁢o⁢p be the operation pi is performing when it writes (𝗐,i,v,_) to S⁢L⁢R⁢[x−1]. By definition, i⁢d⁢x⁢(o⁢p)=x−1, and w⁢o⁢p is a visible write. Therefore, among the operations with index x−1, w⁢o⁢p is placed last in λ (rule R⁢4), and there is no other write operation between w⁢o⁢p and o⁢p (every write operation with index ≥x is after o⁢p in λ.)

If r⁢o⁢p is silent, it is preceded by a direct read o⁢p′ by the same process with the same index x. By the linearization rule R⁢1, there is no write operation between o⁢p′ and o⁢p in λ. Also, o⁢p and o⁢p′ return the same value. By the same reasoning as above, it follows that o⁢p returns the input value of the last write operation that precedes it in λ.

If x=0, o⁢p returns the initial value v0. Indeed, S⁢L⁢R⁢[−1] is initialized with a sequence that contains a single tuple (𝗐,i0,v0,∅). There is no write that precedes o⁢p in λ, as for every write operation w⁢o⁢p, i⁢d⁢x⁢(w⁢o⁢p)≥0. ◀

Lemma 23.

If i∈readers⁢(S⁢L⁢R⁢[x]) then there exists a read operation o⁢p in H′ by process pi with i⁢d⁢x⁢(o⁢p)=x.

Proof.

Suppose that i precedes any w-tuple in S⁢L⁢R⁢[x]. pi writes i to S⁢L⁢R⁢[x] (line 22) while performing the kth iteration of the repeat loop (lines 17-27) in some read operation o⁢p. Let x0 be the value of l⁢s⁢r when o⁢p starts, and let x1<…<xk be the value read from M.w⁢i⁢d⁢x (line 18) in the first k iterations of the loop. Note that x=xk. As before writing i to S⁢L⁢R⁢[xk=x], H⁢[i] is changed to xk (line 21), it follows from Lemma 10 that for every x′,x0<x′<xk, i∉readers⁢(S⁢L⁢R⁢[x′]). As i∈readers⁢(S⁢L⁢R⁢[xk]), xk=min{x′>x0:i∈readers(SLR[x′])} and therefore by definition x=xk=s⁢n⁢(o⁢p).

Suppose now that i is in the helping set of the first w-tuple (𝗐,j,_,h) written to S⁢L⁢R⁢[x]. Before writing (𝗐,j,_,h) (line 35), pj reads x from M.w⁢i⁢d⁢x , y from M.r⁢i⁢d⁢x⁢[i] (line 30) and xℓ from H⁢[i] (line 31). As i is placed into t⁢o⁢_⁢h⁢e⁢l⁢p, y<xℓ.

H⁢[i] is changed by pi (line 21) in an iteration of the repeat loop while performing some read operation o⁢p. Let x0 be the value of l⁢s⁢r when o⁢p starts, and pi is performing iteration ℓ when it writes xℓ to H⁢[i]. By the code, xℓ is the value read from M.w⁢i⁢d⁢x in that iteration, and by Lemma 10, i∉readers⁢(S⁢L⁢R⁢[x′]), for every x′,x0<x′<xℓ.

To summarize, starting from i∈readers(S⁢L⁢R⁢[x]), we have shown that there exists a read operation o⁢p by pi that starts with l⁢s⁢r=x0, and that for every x′,x0<x′<x(=xℓ), i∉readers(S⁢L⁢R⁢[x′]). By definition, i⁢d⁢x⁢(o⁢p)=x. ◀

Lemma 15. [Restated, see original statement.]

Let a⁢o⁢p be an audit operation in H′ that returns A. If there is a read operation r⁢o⁢p by process pj returning v and that precedes a⁢o⁢p in λ, (j,v)∈A.

Proof.

By linearization rules R⁢0-R⁢2, i⁢d⁢x⁢(r⁢o⁢p)=x≤i⁢d⁢x⁢(a⁢o⁢p). Let pi be the process that performs the audit operation a⁢o⁢p.

If r⁢o⁢p is silent, it is preceded by a direct read operation by the same process, with the same output value v and the same index x. In the following, we thus assume that r⁢o⁢p is direct or helped. In S⁢L⁢R⁢[x], j is written before any w-tuple, or the first w-tuple written to S⁢L⁢R⁢[x] has an helping set h containing i. Note that v is the value of the first w-tuple in S⁢L⁢R⁢[x−1].

Let us assume that x<i⁢d⁢x⁢(a⁢o⁢p)=x′. In a⁢o⁢p, pi reads x′ from M.w⁢i⁢d⁢x and a set a⁢s′ from M.a⁢u⁢d⁢i⁢t⁢s⁢e⁢t (line 40). Before this step, M is changed from x to x+1 (in line 16, line 26 or line 38), after a w⁢i⁢n containing a w-tuple is read from S⁢L⁢R⁢[x]. Hence, j∈readers⁢(w⁢i⁢n), and therefore (j,v) is added to the audit set a⁢s written together with x+1 to M. By the code (line 15, line 25 or line 37 and line 42), we have that a⁢s⊆a⁢s′⊆A.

We now assume that x=i⁢d⁢x⁢(a⁢o⁢p). If a⁢o⁢p is a non-definitive audit, no w-tuple has been written to S⁢L⁢R⁢[x] when pi reads S⁢L⁢R⁢[x]. As r⁢o⁢p precedes a⁢o⁢p in λ, there are both placed in λ following rule R⁢1 and therefore pj writes j to S⁢L⁢R⁢[x] before the sliding register is read in a⁢o⁢p, from which it follows that (j,v)∈A (line 42). Otherwise, a⁢o⁢p is a definitive audit, which means that the value w⁢i⁢n reads from S⁢L⁢R⁢[x] (line 42) contains the first w-tuple (𝗐,_,_,h) written to S⁢L⁢R⁢[x]. As j precedes this tuple or i∈h, j∈readers⁢(w⁢i⁢n) and therefore (j,v)∈A. ◀

Lemma 16. [Restated, see original statement.]

Let a⁢o⁢p be an audit operation in H′ whose response contains (j,v). There exists a read operation by pj returning v that precedes a⁢o⁢p in λ.

Proof.

Let pi be the process that performs a⁢o⁢p, and let A be the set of pairs (process,value) returned by this operation. As (j,v) is in A, there exists x such that i∈readers(S⁢L⁢R⁢[x]) and v is the value in the first w-tuple (𝗐,_,v⁢_) written to S⁢L⁢R⁢[x−1]. Indeed, pair (j,v) is inserted to A by pi after reading S⁢L⁢R⁢[x], if x=i⁢d⁢x⁢(a⁢o⁢p) (line 42), or when M.w⁢i⁢d⁢x is changed to x+1 (lines 15-16, lines 25-26 or lines 37-38) if x<i⁢d⁢x⁢(a⁢o⁢p).

By Lemma 23 shows there is a read operation o⁢p by process pi with i⁢d⁢x⁢(o⁢p)=x. This read returns v, which is the value of the first w-tuple written to S⁢L⁢R⁢[x−1]. It remains to prove that o⁢p precedes a⁢o⁢p in λ. If x<i⁢d⁢x⁢(a⁢o⁢p), o⁢p precedes a⁢o⁢p in λ (rule R⁢0). Otherwise, x=i⁢d⁢x⁢(a⁢o⁢p). If a⁢o⁢p is definitive, it is linearized after r⁢o⁢p by rules R⁢1 and R⁢2. Else, a⁢o⁢p is non-definitive, and j is before any w-tuple in S⁢L⁢R⁢[x]. j is also written to S⁢L⁢R⁢[x] before before S⁢L⁢R⁢[x] is read by pi. o⁢p is hence direct, and linearized before a⁢o⁢p by rule R⁢1. ◀

Appendix B Proof Sketch for Section 5

Recall that β is an execution of the auditable LL/SC implementation (Algorithm 3) and α an execution of the auditable register implementation induced from β. We build a linearization μ⁢(β) of β from the linearization λ⁢(α) of α as follows:

  1. 1.

    write operations with the same index x are reordered, by applying first rule R⁢4 and then rule R⁢3. Hence, the write operation corresponding to the first w-tuple in S⁢L⁢R⁢[x] is placed first, and then the writes corresponding to the other w-tuples follow, in arbitrary order. The resulting sequence λ′⁢(α) is no longer a valid linearization of an auditable register, but still extends the real-time order among operations, as writes with the same index are concurrent (Lemma 21(2)). Observe that in λ′⁢(α), as in λ⁢(α), writes with the same index form a contiguous block, denoted Wx. A read operation no longer returns the input of the last preceding write, but rather the input vx of the first write in the last block Wx that precedes it.

  2. 2.

    We revert to ll/sc operations, by replacing in λ′⁢(α) each read and write operation by the ll or sc operation it originated from. This results in a partial linearization μ′⁢(β) of β, missing silent sc operations. In μ′⁢(β), an ll operation o⁢p returns the input vx of the first sc operation s⁢o⁢p in the last block Wx that precedes it. Every sc operation in Wx writes a w-tuple to S⁢L⁢R⁢[x], s⁢o⁢p being the first to do so. Hence, except s⁢o⁢p, each of them returns false (line 18). Consequently, o⁢p returns the input of the last preceding successful sc.

    If pi has a sc operation in Wx, its matching preceding ll operation o⁢p is recorded in S⁢L⁢R⁢[x] (line 9) and therefore, has index i⁢d⁢x⁢(o⁢p)=x. By rules R⁢1-R⁢2, o⁢p is before Wx, and after any operation o⁢p′ with index i⁢d⁢x⁢(o⁢p′)<x (rule R⁢0). Only the first sc operation s⁢o⁢p in Wx returns true, and indeed, there is no sc between s⁢o⁢p and its last preceding ll. Each other sc operation in Wx is unsuccessful, in agreement with the fact that it preceded by the successful sc s⁢o⁢p, with no ll operation in between.

    ll and audit are ordered in μ′⁢(β) as their corresponding read and audit in λ⁢(α), and each ll returns the same value as its corresponding read. Hence, a pair (p,v) is included in the response of an audit operation o⁢p if and only if there is an ll by p that returns v before o⁢p in μ′⁢(β).

  3. 3.

    Finally, we bring back the silent sc operations that were removed from β to form a full linearization μ⁢(β). Each silent sc operation o⁢p that returns is unsuccessful and therefore can be inserted in μ′⁢(β) without affecting the outcome of other sc or ll operations, as long as there is a successful sc between the matching ll o⁢p′ by the same process and o⁢p.

    Let x be the value read by o⁢p from M.w⁢i⁢d⁢x. We insert o⁢p in μ′⁢(β) within the operations whose index is x and after every operation that terminates before o⁢p starts. As x>x′, o⁢p is placed after the operations with index x′. In particular, o⁢p follows the successful sc operation s⁢o⁢p that writes the first w-tuple to S⁢L⁢R⁢[x], which in turn follows o⁢p′. This can be done while preserving the real-time order, as when x>x′ is read from M.w⁢i⁢d⁢x in o⁢p, a w-tuple has already been written to S⁢R⁢L⁢[x′] (Lemma 8).

Appendix C Proof Sketch for Section 6

To prove the correctness of Algorithm 4, we start by noting that all operations terminate within a finite number of their own steps. This is obvious for append and prove, relying on wait-freedom of the encapsulated auditable register operations. For a read operation, note that the sets it returns are monotonically contained in each other; the maximal set is the one containing all process-object pairs. Furthermore, if two sets are equal, the operation terminates. Thus, the loop can be repeated at most n times.

We next prove that Algorithm 4 implements a linearizable immediate n-deny list. First, for all i∈{1,…,n}, we linearize all the append⁢(x) in the step corresponding to the write to the auditable register. append⁢(x) that have not reached this step are discarded.

A prove⁢(x) operation by pi that returns 𝑓𝑎𝑙𝑠𝑒 and that does not return at line 6 is linearized at the last read primitive pi applies to an auditable register A⁢Rx⁢[j]. A prove⁢(x) that returns at line 6 is linearized at its invocation. A read is linearized at the last audit of the second last loop (i.e., the last audit before c1 is set for the last time). We remove incomplete read.

prove⁢(x) operations that return t⁢r⁢u⁢e are inserted at the beginning before the first append⁢(x), according to their real-time order. In particular, we pick one by one in the order of their last step (i.e., the last read from an auditable register), the ones that happen earlier first), denoted s. We put prove⁢(x) immediately before the first read⁢() whose linearization point follows s or immediately the first append⁢(x) if such read⁢() does not exist.

Strong prove validity: A prove⁢(x) by a process p returns 𝑓𝑎𝑙𝑠𝑒, either if p previously performed an append⁢(x) or if it read 𝑓𝑎𝑙𝑠𝑒 in one auditable register. In both cases, there is an append⁢(x) in the set of operations we linearize and it is linearized before the prove⁢(x) according to our rules. The only if part is immediate since we linearize all prove⁢(x) that return t⁢r⁢u⁢e before the first append⁢(x).

Lemma 24.

The set of object-process pairs returned by a read⁢() operation includes exactly all preceding valid prove⁢(x) operations and the processes that invoked them.

Proof.

A o⁢p=prove⁢(x) that returns t⁢r⁢u⁢e is linearized before the first audit, namely o⁢p′, whose linearization point follows the last read primitive applied by o⁢p to an auditable register. After the step where it is linearized o⁢p′ executes a second loop where it audits all the auditable registers. At that point o⁢p is added in c2. By the definition of the linearization point of o⁢p′, o⁢p is in the set returned by o⁢p′.

On the other hand, suppose that a pair (q,t⁢r⁢u⁢e) is in the set c2 returned by a read⁢() by p. Then, there is a prove⁢(x) by q that read t⁢r⁢u⁢e in all the auditable registers (but A⁢Rx⁢[q]) before p start the execution of the last loop. By a simple inspection of the pseudo code it is easy to see that o⁢p returns t⁢r⁢u⁢e. Our linearization rule completes the proof. ◀

Finally, we show that our linearization respects the real-time order of operations. All operations but the prove⁢(x) that return t⁢r⁢u⁢e are linearized in a point of their execution. A prove⁢(x) operations that returns t⁢r⁢u⁢e is linearized before the first append⁢(x) in the linearization. As it reads t⁢r⁢u⁢e in all low-level auditable registers, there is no append⁢(x) that completes before this prove⁢(x) is invoked, otherwise one of the low-level read would have returned 𝑓𝑎𝑙𝑠𝑒. If prove⁢(x) o⁢p completes before a read⁢() o⁢p′ starts, then the last step of o⁢p precedes the linearization point of o⁢p′. Thus, o⁢p is linearized before o⁢p′. Similarly if o⁢p is invoked after o⁢p′ completes, then the linearization point of o⁢p′ precedes the last step of o⁢p which is then linearized after o⁢p′. This concludes the proof since prove⁢(x) are linearized in the order of their last step.