Privatization-Safe Transactional Memories (Extended Version)

Alexey Gotsman; Artem Khyzha; Hagit Attiya

Privatization-Safe Transactional Memories (Extended Version)

T0 review · 0 major / 3 minor · reviewed 2026-08-14 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Privatization-safe TMs act atomically for data-race-free programs

desk verdict A solid theory paper that proves the Fundamental Property for privatization-safe TMs under a TDRF variant, gives a reusable proof method, and strengthens the Attiya–Hillel lower bound; the central contract is sound, with one fixable overstatement in Theorem 14. read the letter →

arxiv 1908.03179 v1 pith:BCSBKHAK submitted 2019-08-08 cs.DC

Artem Khyzha , Hagit Attiya , Alexey Gotsman This is my paper · ORCID

classification cs.DC

keywords transactionalmemoryprivatizationdata-racefreedomopacityobservationalrefinementstronglyatomicsemanticsinvisiblereadsprogressiveTM

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Transactional memory lets a programmer mark atomic blocks, but most implementations do not isolate those blocks from non-transactional accesses to the same data. This paper tries to establish an exact division of responsibility that still gives the full atomic guarantee: the programmer's program must be transactional data-race free (TDRF) under strongly atomic semantics, and the TM must be privatization-safe opaque, a generalization of opacity to histories that mix transactional and non-transactional accesses. When both hold, the Fundamental Property says every execution of the program on the TM is observationally equivalent to an execution on an atomic TM, so the programmer can reason as if all transactions were serialized atomically. The paper also contributes a proof method that reduces privatization-safe opacity to ordinary opacity, applies it to two common TMs, and proves an inherent cost: a TM cannot be progressive and have invisible reads while giving strong atomic semantics to all TDRF programs.

What carries the argument

The central object is privatization-safe opacity, $H|_{\mathrm{CDRF}} \subseteq H_{\mathrm{atomic}}$: every CDRF history of the TM has a counterpart in the atomic TM obtained by reordering actions while preserving per-thread and client order. CDRF is the history-level lifting of TDRF; a history is CDRF exactly when every atomic history corresponding to it is TDRF, and Lemma 7 shows TDRF programs only produce CDRF histories. The verification machinery is the opacity graph, which is the graph characterization of opacity (the standard condition that a TM history can be linearized to a legal atomic history preserving real-time order); its vertices are transactions and non-transactional accesses, and its edges combine read-, write-, and anti-dependencies with per-thread and client order. Lemmas 15 and 16 use CDRF to replace paths through non-transactional vertices by real-time order and transactional dependencies, so acyclicity of the extended graph reduces to the acyclicity check for ordinary opacity. This lets proofs for a two-phase-locking TM and for FencedTL2 reuse earlier opacity arguments.

What would settle it

Run a TDRF privatization program on a TM and compare the observable non-transactional traces with those of the atomic TM; an observable difference would refute Theorem 10. For the TM-side condition, record histories and check CDRF: a single CDRF history with no atomic-history counterpart preserving per-thread and client order refutes privatization-safe opacity. For the cost theorem, exhibiting a progressive TM with invisible reads that nevertheless gives strongly atomic semantics to all TDRF programs would falsify Theorem 25.

Watch

Extended reading notes

Core claim

On its own terms, the central result is Theorem 10 (Fundamental Property): if a TM $H$ satisfies privatization-safe opacity, written $H|_{\mathrm{CDRF}} \subseteq H_{\mathrm{atomic}}$, and a program $P$ is TDRF under strongly atomic semantics, then the executions of $P$ under $H$ observationally refine those under $H_{\mathrm{atomic}}$. That is, for every trace the program can produce on the weakly atomic TM, there is a trace of the atomic TM with the same per-thread actions and the same non-transactional actions. Privatization-safe opacity is the TM-side contract: every history of $H$ that is concurrent data-race free (CDRF) can be reordered into a non-interleaved atomic history while preserving per-thread and client order, where CDRF means every atomic history corresponding to it is TDRF. The proof runs through an opacity-graph characterization extended with non-transactional accesses, plus path-reduction lemmas that let acyclicity of the full graph be checked by the ordinary opacity criterion. The companion cost theorem states that no TM giving strongly atomic semantics to all TDRF programs can be progressive and have invisible reads.

Load-bearing premise

The load-bearing premise is that non-transactional accesses see a sequentially consistent memory, which is what justifies adding the client order to happens-before and treating non-transactional races as harmless; under weaker memory models such as C++, the client order would have to be weakened and the Fundamental Property is not established.

Editorial extensions

If this is right

A programmer who writes a TDRF program can reason about it under strongly atomic semantics even when the implementation is a weakly atomic privatization-safe TM; any property of non-transactional behavior proved there carries over.
Verification of a TM against the strong contract can reuse ordinary opacity proofs: prove the ordinary opacity invariant, then discharge the CDRF and fence invariants to get privatization-safe opacity.
FencedTL2 is a concrete instance: TL2 becomes privatization-safe when a fence at the end of each transaction forces concurrent transactions to finish before writes are flushed.
The lower bound is unconditional: no TM can simultaneously be progressive (solo transactions always complete), have invisible reads, and guarantee strong atomicity to all TDRF programs, so privatization-safety has an inherent performance cost.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

The CDRF check is per-history, so a runtime tool could in principle instrument a TM to test whether each actual history has a TDRF atomic justification; this would catch privatization violations dynamically even when static TDRF checks pass.
Theorem 25 suggests a design trade-off map: privatization-safe TMs will either block at privatization points, as with fences or locking, or track reader visibility, so hybrid schemes that switch policy based on detected contention are a natural next step.
If the framework is ported to a weak-memory model such as C++, the client order cannot be taken as full sequential order; some programs that are TDRF here would become racy there, meaning the programmer contract would need stronger synchronization rather than a weaker TM condition.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

The headline: this is a genuinely useful theory paper that does what it says. It proves the Fundamental Property for privatization-safe TMs under a variant of TDRF, gives a reusable proof method, and sharpens the Attiya–Hillel impossibility result. The reader's take is about right; I'd add that the central proof is sound as far as I can tell, and the path-reduction lemmas are intricate but credible.

The key move is defining CDRF relative to histories of the atomic TM, which lets them state privatization-safe opacity as H|CDRF ⊆ H_atomic. That is a clean contract: the programmer checks TDRF under strong atomicity; the TM designer proves CDRF histories justify. The reduction via Lemmas 15 and 16 to ordinary opacity is a real methodological contribution, and they genuinely reuse the earlier TL2 opacity proof rather than hand-waving it. The impossibility theorem (Theorem 25) is also stronger than Attiya–Hillel and is argued carefully.

The main soft spot is exactly what the stress-test flags: Theorem 14 is printed as a criterion for all histories of H, but the proof and the case studies only establish the CDRF-restricted version. That is a statement-level bug, easy to fix, and it does not affect Theorem 10 or the impossibility result. I would also note the sequential-consistency assumption for non-transactional accesses is explicit and flagged in Section 9; that is a scope limitation, not an oversight. The reliance on their own prior opacity proof for TL2 is not circular — that is an independent published result.

This paper is for concurrency/PL theory people working on TM semantics, DRF notions, and consistency models. It deserves a serious referee: the main contract is important, the proofs are detailed enough to check, and the overstatement is local. I would send it to review with a request to fix Theorem 14's statement and double-check the FencedTL2 invariant write-up in the appendix.

Referee Report

0 major / 3 minor

Summary. The paper studies transactional memories that support the privatization idiom, where an object can move between transactional and non-transactional access under programmer synchronization. It introduces a variant of transactional data-race freedom (TDRF) and a correctness condition called privatization-safe opacity, and proves the Fundamental Property: if a TM is privatization-safe opaque and a program is TDRF under strongly atomic semantics, then the program's executions on that TM observationally refine its strongly atomic executions. The paper also gives a graph-theoretic method that reduces proofs of privatization-safe opacity to ordinary opacity proofs, instantiates the method on FencedTL2 and on a two-phase-locking TM, and proves an impossibility result showing that no progressive TM with invisible reads can guarantee strongly atomic semantics to all TDRF programs.

Significance. If correct, the framework provides a clean contract between programmers and implementors of privatization-safe TMs, and it makes a previously informal notion of privatization-safety amenable to proof reuse. The main theorem, Theorem 10, is supported by a coherent proof structure: Lemma 7 connects TDRF with the concurrent generalization CDRF, and Lemma 11 gives the observational-refinement step. The definitions are anchored to the atomic TM rather than fitted to the examples, and the technical appendices contain detailed proofs. The impossibility result sharpens the earlier lower bound of Attiya and Hillel by phrasing it in terms of a formal DRF guarantee. I found no load-bearing flaw in the central derivation; the issues I identified are local and fixable.

minor comments (3)

[Section 6, Theorem 14] As printed, Theorem 14 states the privatization-safe opacity criterion for all histories in H, reading “H ⊐ H_atomic holds if ∀H ∈ H. cons(H) ∧ ∃G ∈ Graph(H). acyclic(G)”. This is overbroad: privatization-safe opacity is defined in Definition 6 only on the CDRF restriction, and both Lemmas 15 and 16 and the case studies in Section 7 use CDRF essentially. The theorem should be restated as: H|CDRF ⊐ H_atomic holds if for every H ∈ H|CDRF, cons(H) and there exists G ∈ Graph(H) with acyclic(G). This is an immediate local correction and does not affect Theorem 10, but the current statement as written is not the theorem that the subsequent proofs establish.
[Section B, Figure 5] The text after the program in Figure 5 contains a stray fragment: “we expect the postcondition shown to hold: .”, and the displayed postcondition has an extra equality symbol. Please clean up the formatting so that the expected postcondition is stated unambiguously.
[Section 6, Definition 12 and Lemmas 15-16] The graph-edge notation in Definitions 12 and the lemmas that follow is dense and the arrow glyphs are easy to misread in the extended version. Adding a short legend near Definition 12, explaining that → denotes a graph edge and →* its reflexive-transitive closure, would substantially improve readability without changing content.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the Fundamental Property is derived from semantic definitions and prior independent results; the only self-citation concern is a reused proof technique, not a circular reduction.

full rationale

The paper's central claim is Theorem 10, which states that if a TM H is privatization-safe opaque (H|CDRF is a subset of H_atomic) and a program P is TDRF under strongly atomic semantics, then JP K(H) observationally refines JP K(H_atomic). The proof is a direct derivation from Lemma 7 and Lemma 11. Lemma 11 is explicitly adapted from a prior published result of Attiya, Gotsman, Hans, and Rinetzky [6], and Lemma 7, proved in Appendix C, uses Lemma 28 and Proposition 29 adapted from the same prior work. These are independent semantics results that do not presuppose the theorem being proved. The notions TDRF and CDRF are defined semantically, anchored to the fixed atomic TM H_atomic, and no parameters are fitted to make the conclusion hold; in particular, CDRF is not defined by 'histories that satisfy the desired refinement' but by a universal condition on matching atomic histories. The paper does reuse the authors' earlier opacity proof for TL2 [26] to discharge the ordinary-opacity obligations in the FencedTL2 case study, and Lemma 13 is said to be 'proven analogously to Lemma 6.4 in [26, Section B.2]'. This is a self-citation, but it is a reuse of a previously published proof technique for ordinary opacity, not an assumed instance of the target privatization-safety result; it does not force Theorem 10 or the TDRF contract. The graph characterization itself comes from Guerraoui and Kapalka [21], an external source. A statement-level defect appears in Theorem 14, which is printed as 'H is a subset of H_atomic holds if for all H in H, cons(H) and there exists G in Graph(H) with acyclic(G)', omitting the restriction to H|CDRF. The surrounding development makes the intended criterion clear: Definition 6 defines privatization-safe opacity as H|CDRF is a subset of H_atomic, the reduction lemmas (Lemmas 15 and 16) explicitly require CDRF, and the case-study theorems (Theorems 21 and 39) establish the needed graph condition only for CDRF histories. This is a statement-level bug and a correctness risk in the printed theorem, but it is not a circularity: nothing in the proof assumes the conclusion it is trying to establish. Overall, the derivation chain is self-contained against the stated semantic assumptions, and no prediction or first-principles result reduces by construction to its inputs.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

The paper is a formal theory paper with no fitted constants. Its central claims rest on modeling assumptions about the programming language and TM semantics, and on the graph-theoretic characterization of opacity from the literature.

assumptions (5)

domain assumption The underlying non-transactional memory model is sequentially consistent.
Stated in Section 2 and Section 9; justifies including the client order cl(H) in the happens-before relation, making non-transactional races harmless in the TDRF variant. Weak memory is deferred to future work.
domain assumption A TM is prefix-closed and closed under appending request actions to well-formed histories.
Stated in Section 2; used to construct executions in the impossibility proof of Theorem 25.
domain assumption A TM does not impose restrictions on the placement of non-transactional accesses.
Stated in Section 2; used in the proof of Proposition 26 to splice non-transactional reads and writes into executions.
domain assumption The programming language forbids nested atomic blocks and explicit aborts; non-transactional accesses execute atomically.
Language restrictions stated in Section 2 and Appendix A.1; they simplify the trace semantics.
standard math The opacity graph characterization (RW, WW, WR, PO, CL edges and acyclicity) is a sound and complete characterization of opacity.
Adapted from Guerraoui and Kapalka [21] and the authors' prior work [26]; used in Section 6 and Lemmas 13, 15, 16.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Privatization-Safe Transactional Memories (Extended Version)." pith.science (2026). https://pith.science/paper/BCSBKHAK

@misc{pith2026190803179,
  author       = {Pith},
  title        = {Pith review of: Privatization-Safe Transactional Memories (Extended Version)},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/BCSBKHAK}},
  note         = {Machine review of arXiv:1908.03179}
}

read the original abstract

Transactional memory (TM) facilitates the development of concurrent applications by letting the programmer designate certain code blocks as atomic. Programmers using a TM often would like to access the same data both inside and outside transactions, and would prefer their programs to have a strongly atomic semantics, which allows transactions to be viewed as executing atomically with respect to non-transactional accesses. Since guaranteeing such semantics for arbitrary programs is prohibitively expensive, researchers have suggested guaranteeing it only for certain data-race free (DRF) programs, particularly those that follow the privatization idiom: from some point on, threads agree that a given object can be accessed non-transactionally. In this paper we show that a variant of Transactional DRF (TDRF) by Dalessandro et al. is appropriate for a class of privatization-safe TMs, which allow using privatization idioms. We prove that, if such a TM satisfies a condition we call privatization-safe opacity and a program using the TM is TDRF under strongly atomic semantics, then the program indeed has such semantics. We also present a method for proving privatization-safe opacity that reduces proving this generalization to proving the usual opacity, and apply the method to a TM based on two-phase locking and a privatization-safe version of TL2. Finally, we establish the inherent cost of privatization-safety: we prove that a TM cannot be progressive and have invisible reads if it guarantees strongly atomic semantics for TDRF programs.

Figures

Figures reproduced from arXiv: 1908.03179 by the authors.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

14 extracted references · 14 canonical work pages

[1]

every action in · has a unique identiﬁer: if · = ·1 (a1, _, _) ·2 (a2, _, _) ·3 then a1 ”= a2

work page
[2]

commands in actions executed by a thread t do not access local variables of other threads tÕ ”= t:i f · = _ (_,t ,c ) _ then c œ LPcommt

work page
[3]

for every thread t, the projection · |t of · onto the actions by t cannot contain a request action immediately followed by a primitive action: if · |t = _–1–2_ and –1 is a request then –2 is a response

work page
[4]

request and response actions are properly matched: for every thread t, history(· )|t consists of alternating request and corresponding response actions, starting from a request action

work page
[5]

actions denoting the beginning and end of transactions are properly matched: for every thread t, in the projection of · |t to begintx, committed and aborted actions, begintx alternates with committed or aborted,s t a r t i n gf r o mbegintx

work page
[6]

non-transactional accesses execute atomically: if · = ·1 –· 2, where – is a read or a write request action by thread t, and all the transactions of t in ·1 completed, then ·2 begins with a response to –

work page
[7]

x := 1; if (x = 1) y := 1 else y := 2

non-transactional accesses never abort: if · = _ –1 –2 ·2, where –1 is a non-transactional request action then –2 is not an aborted action. A.2 Formal Deﬁnition of the Programming Language Semantics The semantics of the programming language is the set of traces that computations of programs produce. We ﬁrst describe its high-level structure, and then pres...

work page 2019
[8]

T h e s e tA(P ) includes traces where both branches are explored

lÕ := 1 else lÕ := 2 ”. T h e s e tA(P ) includes traces where both branches are explored. However, due to the semantics of the assume actions added to the traces according to Figure 4, only the trace executing lÕ := 1 will result in a nonempty set of ﬁnal states after the evaluation and, therefore, only this trace will be included into JP K(s). A.3 The A...

work page

Show all 14 references

[9]

Hc is non-interleaved
[10]

Hc is has no commit-pending transactions
[11]

H is a subsequence of Hc; and
[12]

partitioning by consensus

any action in Hc which is not in H is either a committed or an aborted action. For example, we can obtain a completion of history H0 above by inserting (_,t 1, committed) after (_,t 1, trycommit). We deﬁne Hatomic as the set of all non-interleaved histories H, in which every t...

2019
[13]

there exists T ÕÕ such that T< HB1(H) T ÕÕ <HBk≠1(H) n, or
[14]

if” case is covered by Corollary 35, so here we prove the “only if

there exists nÕÕ such that T< HB1(H) nÕÕ <HBk≠1(H) n. In the ﬁrst case, applying the induction hypothesis (k ≠ 1) to T ÕÕ <HBk≠1(H) n immediately concludes the proof. In the second case, by deﬁnition of CL, nÕÕ <CL(H) n holds. Therefore, T< HB2(H) n holds, so we can apply the ...

2019

Pith tools

Reviewed August 14, 2026 · model on record in the stance chip above.

[1] [1]

every action in · has a unique identiﬁer: if · = ·1 (a1, _, _) ·2 (a2, _, _) ·3 then a1 ”= a2

work page

[2] [2]

commands in actions executed by a thread t do not access local variables of other threads tÕ ”= t:i f · = _ (_,t ,c ) _ then c œ LPcommt

work page

[3] [3]

for every thread t, the projection · |t of · onto the actions by t cannot contain a request action immediately followed by a primitive action: if · |t = _–1–2_ and –1 is a request then –2 is a response

work page

[4] [4]

request and response actions are properly matched: for every thread t, history(· )|t consists of alternating request and corresponding response actions, starting from a request action

work page

[5] [5]

actions denoting the beginning and end of transactions are properly matched: for every thread t, in the projection of · |t to begintx, committed and aborted actions, begintx alternates with committed or aborted,s t a r t i n gf r o mbegintx

work page

[6] [6]

non-transactional accesses execute atomically: if · = ·1 –· 2, where – is a read or a write request action by thread t, and all the transactions of t in ·1 completed, then ·2 begins with a response to –

work page

[7] [7]

x := 1; if (x = 1) y := 1 else y := 2

non-transactional accesses never abort: if · = _ –1 –2 ·2, where –1 is a non-transactional request action then –2 is not an aborted action. A.2 Formal Deﬁnition of the Programming Language Semantics The semantics of the programming language is the set of traces that computations of programs produce. We ﬁrst describe its high-level structure, and then pres...

work page 2019

[8] [8]

T h e s e tA(P ) includes traces where both branches are explored

lÕ := 1 else lÕ := 2 ”. T h e s e tA(P ) includes traces where both branches are explored. However, due to the semantics of the assume actions added to the traces according to Figure 4, only the trace executing lÕ := 1 will result in a nonempty set of ﬁnal states after the evaluation and, therefore, only this trace will be included into JP K(s). A.3 The A...

work page