A Forward Simulation-Based Hierarchy of Linearizable Concurrent Objects

Chao Wang; Jianwei Liao; Jim Woodcock; Peng Wu; Ruijia Li; Yang Zhou; Yi Lv; Zhiming Liu

REVIEW 5 major objections 4 minor 27 references

An object is linearizable exactly when it forward-simulates into one universal object, and the simulation order makes linearizable objects a bounded lattice or, under liveness constraints, a bounded join-semilattice.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

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

T0 review · deepseek-v4-flash

2026-08-03 10:25 UTC pith:SHO7BNU2

load-bearing objection Interesting structural claims, but the central equivalence theorem is unproved and the machine-verified proof claim is unverifiable as submitted. the 5 major comments →

arxiv 2601.11646 v2 pith:SHO7BNU2 submitted 2026-01-15 cs.DC cs.FL

A Forward Simulation-Based Hierarchy of Linearizable Concurrent Objects

Chao Wang , Ruijia Li , Yang Zhou , Peng Wu , Yi Lv , Jianwei Liao , Jim Woodcock , Zhiming Liu This is my paper

classification cs.DC cs.FL MSC 68Q8568Q60

keywords linearizabilityforward simulationconcurrent objectsuniversal constructionbounded latticejoin-semilatticewait-freedomlock-freedom

verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

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

This paper proves that linearizability, the standard correctness condition for concurrent objects, is not only checkable by forward simulation but is precisely the same thing as forward simulation into a single constructed object called the universal object U_Spec. If the main theorem is right, verifying that any concurrent object is linearizable reduces to producing one forward simulation from that object's operational semantics into U_Spec. The paper then shows the simulation relation organizes all linearizable objects into a bounded lattice when liveness is ignored, and into bounded join-semilattices when wait-freedom, lock-freedom, or obstruction-freedom is required. Two concrete queue implementations are shown to sit in this hierarchy, with the timestamp-based queue simulating the classic lock-free queue, and the classic queue simulating into U_Spec. The central claim, stated in good faith, is that forward simulation is the intrinsic structural order of linearizability, giving a hierarchy rather than a flat correctness predicate.

Core claim

The paper's central discovery is a characterization: for deterministic non-blocking sequential specifications, a concurrent object O is linearizable with respect to Spec for n processes if and only if its operational semantics JO,nK is forward-simulated by JU_Spec,nK, where U_Spec is a wait-free universal object that records every call/return history and attaches a linearization to each node in a consensus-ordered list. From this equivalence and the construction of least-upper-bound objects (a nondeterministic choice between two objects) and greatest-lower-bound objects (running both objects and returning only when both agree), the paper derives its hierarchy: the equivalence classes of line

What carries the argument

The load-bearing object is U_Spec, a wait-free universal construction whose only method apply() takes an invocation (m,a) and returns the corresponding response. Each apply() call creates a node holding the operation's identity, method, argument, the current recorded history, and a chosen linearization of that history, and inserts it into a linked list whose order is decided by consensus, as in the classical universal construction. The critical extra steps are a history recorder that stores every call/return action, and genLin(), which nondeterministically returns a linearization of the recorded history h1; the node stores h1 and this linearization. The lin-field later determines the return

Load-bearing premise

The universal object's genLin() is only defined when every history recorded during a run of U_Spec is linearizable with respect to the specification; the paper relies on this invariant in its key lemma and theorem but does not prove it before Theorem 1 uses it.

What would settle it

A concrete way to test the central theorem: implement U_Spec for a small deterministic non-blocking specification (say a FIFO queue or a register) with two processes, run the most general client, and inspect the history recorder at the moment genLin() is called. If that recorded history is not linearizable with respect to the spec, genLin() is undefined and the construction fails. Alternatively, if one can exhibit a linearizable object O such that no forward simulation from JO,nK into JU_Spec,nK can be defined, Theorem 1 is contradicted.

Watch this falsifier. Get emailed when new claim-graph text bears on it.

If this is right

If Theorem 1 holds, verifying linearizability becomes a single forward-simulation problem toward U_Spec; any sound simulation checker that can handle the constructed object yields a complete verification method.
Because strongly linearizable wait-free (resp., lock-free, obstruction-free) objects all lie in the bottom equivalence class, they simulate each other; there is no finer simulation-based hierarchy among them.
The lattice order gives a way to compare distinct implementations of the same specification: if A simulates B but B does not simulate A, A sits strictly higher, meaning B's behaviors are a subset of A's possible behaviors in a precise sense.
The concrete queue result shows that implementations with very different data layouts (array-swap based versus timestamp pools) can be formally related by forward simulation, which transfers properties that simulations preserve from one to the other.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The equivalence with a single simulation suggests a generic verification toolchain: instead of bespoke linearizability proofs, one could search for a forward simulation against U_Spec; the paper machine-checked three proofs, which hints at but does not fully develop such automation.
The lattice hierarchy offers a natural measure of implementation strength: objects higher in the simulation order are more abstract or universal. A testable extension is to classify incomparable linearizable objects in the middle of the lattice, since the paper proves joins and meets exist but does not enumerate the objects.
The GLB construction's infinite loop on disagreement explains why liveness constraints shatter the lattice into a semilattice. A plausible extension is to replace 'both return the same value' with a weaker agreement condition, such as both returning values from the same equivalence class, and ask whether a lattice reappears for some liveness class.
The authors note that forward simulation preserves hyperproperties; if so, the simulation between the two queues would transfer those properties between the implementations, an implication the paper only hints at in its conclusion.

Editorial analysis

A structured set of objections, weighed in public.

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

Desk Editor's Note

Interesting structural claims, but the central equivalence theorem is unproved and the machine-verified proof claim is unverifiable as submitted.

read the letter

Short version: the paper has a real thesis — linearizable objects, quotiented by mutual forward simulation, form a bounded semilattice with liveness and a bounded lattice without it, with a single universal object U_Spec at the top. If that's right, it gives the verification community a common target. But the load-bearing proof is missing. Theorem 1, the equivalence between linearizability and simulation to U_Spec, has no proof in the text, and the proof needs an invariant — every history U_Spec records must be linearizable — that the text never establishes. genLin() at Line 16 presumes exactly that. Without it, U_Spec isn't well-defined. The lattice theorems are only sketched, and the Isabelle/HOL claim in the abstract has no accompanying theory files, so it can't be checked.

What's genuinely new: the lattice/semilattice framing, the LUB/GLB object constructions, and the proof that the time-stamped queue simulates the Herlihy-Wing queue. That last result is a concrete, nontrivial simulation. The paper also cites the Shimon et al. register work that overlaps with U_Spec, which is honest.

The soft spots are serious. Theorem 1 is the foundation; without its proof, the lattice hierarchy and the verification story don't stand. The introduction also has an apparent contradiction: it says all wait-free linearizable objects simulate each other, which would collapse the semilattice to one class, while Theorem 4 later limits that to strongly linearizable objects. That reads like a missing word, but it needs fixing. The GLB construction has an infinite loop when return values conflict, which is acceptable for the no-liveness lattice, but the paper should be explicit about why that doesn't contaminate the liveness-semilattice claims.

The U_Queue-to-HW-queue case study is a nice sanity check, but since Theorem 1 is unproved, Corollary 1 doesn't follow yet.

Who should read this: concurrency-verification researchers interested in simulation-based methods and the structure of linearizable objects. The question is worth pursuing. I wouldn't use the results as they are. This needs a major revision: full proof of Theorem 1 (or at least a rigorous proof sketch), a proof of the genLin invariant, and the Isabelle/HOL development made available. If those come, it's a solid paper. I'd send it to referees rather than desk-reject — the topic matters and the structural idea deserves scrutiny — but I'd tell the authors proofs are mandatory.

Referee Report

5 major / 4 minor

Summary. The paper proposes a hierarchy of linearizable concurrent objects under forward simulation. It defines a universal construction U_Spec and states (Theorem 1) that a concurrent object O is linearizable w.r.t. a deterministic, non-blocking sequential specification Spec for n processes iff JO,nK is forward-simulated by JU_Spec,nK. From this it derives a bounded join-semilattice for wait-free, lock-free, and obstruction-free linearizable classes, and a bounded lattice for all linearizable classes, using objects A_Spec, D_Spec, LUB(O1,O2), and GLB(O1,O2). Two case studies claim that the time-stamped queue simulates the Herlihy-Wing queue and that the Herlihy-Wing queue is simulated by U_Queue; the abstract further claims machine verification in Isabelle/HOL.

Significance. If established, the results would be significant: they would reduce linearizability checking to one forward-simulation check, reveal an algebraic structure over linearizable objects, and connect concrete non-strongly-linearizable implementations through simulation. The location of strongly linearizable objects in the semilattice is also interesting. The claimed Isabelle/HOL verification is a potential strength, but only if the artifacts are actually available and the proofs are present. As submitted, the paper does not provide enough support for these claims: the central theorem is unproved, several load-bearing lemmas are only sketched or stated, and there is a direct internal contradiction about which objects lie in the A_Spec class.

major comments (5)

[Section 3, Theorem 1] The equivalence 'O is linearizable w.r.t. Spec for n processes iff JO,nK ⪯(c,r) JU_Spec,nK' is stated with no proof. This is the load-bearing result: Lemma 3, Theorem 3, Corollary 1, and the proposed verification methodology all reduce to it. The (⇒) direction requires constructing a forward simulation from an arbitrary linearizable O to U_Spec, and the (⇐) direction requires showing that U_Spec's traces are exactly linearizable histories. Neither construction nor argument is provided. A complete proof must be supplied.
[Section 3, Method 1 and Lemma 1] U_Spec is not shown to be well-defined. At Line 14, h1 := O_his.read(); at Line 16, l := genLin(). genLin() is specified only for histories that have a linearization. During a run, h1 may contain pending calls whose returns have not yet been recorded (returns are stored only at Line 23); no invariant is proved that every such h1 is linearizable w.r.t. Spec. Lemma 1, which would supply that invariant, is only stated. If a reachable h1 were non-linearizable, genLin is undefined, U_Spec is not a well-defined concurrent object, and both directions of Theorem 1 collapse.
[Section 4.1, Lemmas 2 and 4] Lemma 4 asserts JA_Spec,nK ⪯(c,r) JO,nK for every linearizable and wait-free/lock-free/obstruction-free O. This is a strong, nontrivial claim: A_Spec must simulate any such O despite O's implementation-specific behavior. No proof is given. Lemma 2's proof is only a sketch ('First, we prove... Then, we prove...'); the linearizability and liveness preservation of LUB(O1,O2) and the least-upper-bound property require detailed argument. Since Theorems 2 and 3 depend on these, the semilattice and lattice claims are unsupported.
[Section 1 vs. Section 4.3] The introduction states: 'we prove that all the linearizable and wait-free objects simulate each other, and are all located in the W F-class containing JA_Spec,nK' (Section 1, paragraph beginning 'It is known...'). This directly contradicts Theorem 4, which restricts that conclusion to strongly linearizable objects. It would collapse the semilattice to a single class and is inconsistent with the case studies of non-strongly-linearizable queues. This is not a minor wording issue; it changes the main hierarchy claimed. The authors should correct and reconcile this statement.
[Abstract and Section 5] The abstract claims the Herlihy-Wing queue cannot simulate the time-stamped queue and that three proofs are machine-verified by Isabelle/HOL, but no Isabelle theories, proof scripts, or repository location are provided, and Theorems 5–6 are supported only by informal sketches. The simulation relation R and invariant set S_INV in Section 5.2 are not specified. Thus neither the case-study results nor the machine-verification claim can be independently checked.

minor comments (4)

[Section 3, forward simulation definition] The definition of forward simulation is informal: 'reachable from c2 with transitions ls' does not state whether ls is a sequence, how it matches α, or how internal actions are interleaved. This matters because Theorem 1 quantifies over simulations.
[Section 4.2, Lemma 6] The notation '≺(c,r)' is used for the partial order, but elsewhere the paper uses '⪯(c,r)'. Please standardize.
[Throughout] The object U_Spec is sometimes written 'USpec' (e.g., in the abstract and introduction). Please use one consistent notation.
[Section 5.2] The 'history tuple', 'linearization tuple', and the invariant set S_INV are described only informally. If this simulation proof is to be usable, these should be defined precisely, at least in a technical appendix.

Circularity Check

1 steps flagged

Theorem 1's characterization is partly built into U_Spec's genLin oracle; the completeness half is unproved.

specific steps

self definitional [Method 1 (Lines 14-17), Lemma 1, Theorem 1]
"At Line 16, genLin() calculates a linearization of h. ... The following lemma states that U Spec is wait-free and linearizable w.r.t. Spec. ... Theorem 1. Given a deterministic and non-blocking sequential specification Spec and a concurrent object O, O is linearizable w.r.t. Spec for n processes, if and only if J O, nK ⪯(c,r) J USpec, nK."

U_Spec's apply() uses genLin() to 'return a linearization of h' for the recorded history before any return is stored. Thus the reachable histories of U_Spec are linearizable by construction; Lemma 1 is exactly this invariant and is stated without proof. Since ⪯(c,r) makes call/return actions visible, the soundness direction of Theorem 1—if J O,nK ⪯ J U_Spec,nK then O is linearizable—is immediate from trace inclusion plus the built-in oracle. The completeness direction (every linearizable O has such a simulation) is asserted with no construction or proof. Hence the 'equivalent characterization' is not an independent reduction; the witness to linearizability is inserted into the universal object's definition, so the equivalence is partly a restatement of Definition 1.

full rationale

The central load-bearing claim is Theorem 1, and the paper's own definition of U_Spec makes its reachable histories linearizable by construction: genLin() is specified to return a linearization of the recorded history. The soundness half of the equivalence is therefore a trace-inclusion consequence of the built-in oracle, while the completeness half—the part that would make the characterization substantive—is never proved. This is a genuine, if partial, circular burden: the reduction is not to an independently defined simulation condition but to an object whose behaviour is defined using the very linearization witness the theorem is about. The lattice/semilattice theorems (Lemmas 2-6, Theorems 2-4) and the case studies are not themselves fitted parameters or renamed empirical results; they inherit the gap from Theorem 1 but do not add circularity. The self-citation to the authors' prior universal construction [24] is not load-bearing here: the paper says the new U_Spec 'extends' it, but the correctness of the new genLin-based lines is not delegated to [24]. The abstract's claim that the three proofs are machine-verified by Isabelle/HOL is not backed by a shipped development, so it cannot serve as independent evidence for the missing proofs of Lemma 1 or Theorem 1. Those are correctness and evidence gaps, not additional circularity. Overall, the central equivalence is close to a reformulation because of genLin, but the lattice results and case studies have independent mathematical content, so the score is moderate rather than extreme.

Axiom & Free-Parameter Ledger

0 free parameters · 6 axioms · 4 invented entities

The paper has no fitted numerical parameters. Its central constructions are new mathematical objects (U_Spec, LUB, GLB, D_Spec) whose correctness is asserted by theorems rather than demonstrated in the submitted text. The main background assumptions are the deterministic non-blocking specification model, the n-process most-general-client model, the chosen visible-action simulation relation, and two cited theorems about strong linearizability and A_Spec.

axioms (6)

domain assumption The sequential specification Spec is deterministic and non-blocking.
Stated in Section 2.3; used to define U_Spec and to ensure genLin terminates with at most one return per method/argument from each state.
domain assumption The system consists of n processes each running a most general client that can call any method with any argument.
Used throughout to define the operational semantics JO,nK and the linearizability condition for n processes (Section 2.1).
standard math Forward simulation with call/return actions visible and internal actions unobservable is the refinement order under consideration.
Definition in Section 3; lifted to equivalence classes in Section 4. The choice of visible actions directly determines the partial order.
domain assumption Strong linearizability of O w.r.t. Spec is equivalent to JO,nK being simulated by the atomic implementation AT(Spec,n) (Attiya and Enea [16]).
Invoked in the proof of Theorem 4 to locate strongly linearizable objects at the minimum element of the semilattice.
domain assumption Herlihy and Shavit's universal construction A_Spec is wait-free and linearizable w.r.t. Spec.
Used as background in Lemma 5 and Theorem 4; cited to [2].
ad hoc to paper Every history recorded by O_his during any U_Spec run is linearizable, so genLin() always returns a linearization.
This invariant is asserted as part of Lemma 1 but not proved in the text; Theorem 1 depends on genLin being total.

invented entities (4)

U_Spec no independent evidence
purpose: Universal wait-free object with history recorder and genLin oracle; used as the maximum element and for the equivalent characterization of linearizability.
Defined in Section 3; its correctness is the content of Lemma 1 and Theorem 1, not independently evidenced outside the paper.
LUB(O1,O2) no independent evidence
purpose: Nondeterministic choice between two object instances; realizes the least upper bound (join) in the semilattice.
Defined in Section 4.1, Method 2; used to prove Theorem 2.
GLB(O1,O2) no independent evidence
purpose: Interleaving of two objects returning only when both return the same value; realizes the greatest lower bound (meet) in the liveness-free lattice.
Defined in Section 4.2, Method 3; its failure of liveness is used to explain why the meet does not exist in the liveness-constrained semilattice.
D_Spec no independent evidence
purpose: Object whose methods never return; provides the minimum element of the liveness-free lattice.
Defined in Section 4.2; its linearizability is argued from the non-blocking assumption on Spec.

pith-pipeline@v1.3.0-alltime-deepseek · 3800 in / 3896 out tokens · 284109 ms · 2026-08-03T10:25:59.267253+00:00 · methodology

0 comments

read the original abstract

In this paper, we systematically investigate the connection between linearizable objects and forward simulation. We prove that the sets of linearizable objects satisfying wait-freedom (resp., lock-freedom or obstruction-freedom) form a bounded join-semilattice under the forward simulation relation, and that the sets of linearizable objects without liveness constraints form a bounded lattice under the same relation. Thus, forward simulation is not only a proof technique for linearizability but also induces an algebraic hierarchy of linearizable objects. As part of our lattice result, we propose an equivalent characterization of linearizability by reducing checking linearizability w.r.t. sequential specification $Spec$ into checking forward simulation w.r.t. a wait-free universal construction $\mathcal{U}_{Spec}^{WF}$. We also propose an object $\mathcal{U}_{Spec}^s$, which simplifies $\mathcal{U}_{Spec}^{WF}$ and is more suitable for verification. We prove that the Herlihy-Wing queue is simulated by $\mathcal{U}_{Queue}^s$ with $Queue$ the sequential specification of the queue. Thus, our object $\mathcal{U}_{Spec}^s$ can be used in the verification of linearizability. To demonstrate the forward simulation relation between concrete linearizable objects, we prove that the time-stamped queue simulates the Herlihy-Wing queue, while the Herlihy-Wing queue cannot simulate the time-stamped queue. All these three proofs have been machine-verified by Isabelle/HOL.

discussion (0)

Reference graph

Works this paper leans on

27 extracted references · 1 linked inside Pith

[1]

ACM Trans

Herlihy, M., Wing, J.M.: Linearizability: A correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst.12(1990) 463–492

1990
[2]

Morgan Kaufmann (2008)

Herlihy, M., Shavit, N.: The art of multiprocessor programming. Morgan Kaufmann (2008)

2008
[3]

Vafeiadis, V ., Herlihy, M., Hoare, T., Shapiro, M.: Proving correctness of highly-concurrent linearisable objects. In Torrellas, J., Chatterjee, S., eds.: Proceedings of the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPOPP 2006, New York, New York, USA, March 29-31, 2006, ACM (2006) 129–136

2006
[4]

Vale, A.O., Shao, Z., Chen, Y .: A compositional theory of linearizability. J. ACM71(2024) 14:1–14:107

2024
[5]

Filipovic, I., O’Hearn, P.W., Rinetzky, N., Yang, H.: Abstraction for concurrent objects. In Castagna, G., ed.: Programming Languages and Systems, 18th European Symposium on Programming, ESOP 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings. V olume 5502 of Lectur...

2009
[6]

In Majumdar, R., Kuncak, V ., eds.: Computer Aided Verification - 29th Inter- national Conference, CA V 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II

Bouajjani, A., Emmi, M., Enea, C., Mutluergil, S.O.: Proving linearizability using forward simulations. In Majumdar, R., Kuncak, V ., eds.: Computer Aided Verification - 29th Inter- national Conference, CA V 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II. V olume 10427 of Lecture Notes in Computer Science., Springer (2017) 542–563

2017
[7]

In Damm, W., Hermanns, H., eds.: Computer Aided Verification, 19th International Conference, CA V 2007, Berlin, Germany, July 3-7, 2007, Proceedings

Amit, D., Rinetzky, N., Reps, T.W., Sagiv, M., Yahav, E.: Comparison under abstraction for verifying linearizability. In Damm, W., Hermanns, H., eds.: Computer Aided Verification, 19th International Conference, CA V 2007, Berlin, Germany, July 3-7, 2007, Proceedings. V olume 4590 of Lecture Notes in Computer Science., Springer (2007) 477–490

2007
[8]

Vafeiadis, V .: Shape-value abstraction for verifying linearizability. In Jones, N.D., M ¨uller- Olm, M., eds.: Verification, Model Checking, and Abstract Interpretation, 10th International Conference, VMCAI 2009, Savannah, GA, USA, January 18-20, 2009. Proceedings. V olume 5403 of Lecture Notes in Computer Science., Springer (2009) 335–348

2009
[9]

Abdulla, P.A., Haziza, F., Hol ´ık, L., Jonsson, B., Rezine, A.: An integrated specification and verification technique for highly concurrent data structures. Int. J. Softw. Tools Technol. Transf.19(2017) 549–563

2017
[10]

Jayanti, P., Jayanti, S., Yavuz, U.Y ., Hernandez, L.: A universal, sound, and complete forward reasoning technique for machine-verified proofs of linearizability. Proc. ACM Program. Lang.8(2024) 2456–2484

2024
[11]

PhD thesis, University of Cambridge, UK (2008)

Vafeiadis, V .: Modular fine-grained concurrency verification. PhD thesis, University of Cambridge, UK (2008)

2008
[12]

ACM Trans

Liang, H., Feng, X., Fu, M.: Rely-guarantee-based simulation for compositional verification of concurrent program transformations. ACM Trans. Program. Lang. Syst.36(2014) 3:1– 3:55

2014
[13]

In Boehm, H., Flanagan, C., eds.: ACM SIGPLAN Conference on Programming Lan- guage Design and Implementation, PLDI ’13, Seattle, W A, USA, June 16-19, 2013, ACM (2013) 459–470

Liang, H., Feng, X.: Modular verification of linearizability with non-fixed linearization points. In Boehm, H., Flanagan, C., eds.: ACM SIGPLAN Conference on Programming Lan- guage Design and Implementation, PLDI ’13, Seattle, W A, USA, June 16-19, 2013, ACM (2013) 459–470

2013
[14]

ACM Trans

Herlihy, M.: Wait-free synchronization. ACM Trans. Program. Lang. Syst.13(1991) 124– 149

1991
[15]

In D’Argenio, P.R., Melgratti, H.C., eds.: CONCUR 2013 - Concurrency Theory - 24th International Conference, CONCUR 2013, Buenos Aires, Argentina, August 27-30, 2013

Liang, H., Hoffmann, J., Feng, X., Shao, Z.: Characterizing progress properties of concurrent objects via contextual refinements. In D’Argenio, P.R., Melgratti, H.C., eds.: CONCUR 2013 - Concurrency Theory - 24th International Conference, CONCUR 2013, Buenos Aires, Argentina, August 27-30, 2013. Proceedings. V olume 8052 of Lecture Notes in Computer Scien...

2013
[16]

In Suomela, J., ed.: 33rd International Symposium on Distributed Computing, DISC 2019, October 14-18, 2019, Budapest, Hungary

Attiya, H., Enea, C.: Putting strong linearizability in context: Preserving hyperproperties in programs that use concurrent objects. In Suomela, J., ed.: 33rd International Symposium on Distributed Computing, DISC 2019, October 14-18, 2019, Budapest, Hungary. V olume 146 of LIPIcs., Schloss Dagstuhl - Leibniz-Zentrum f¨ur Informatik (2019) 2:1–2:17

2019
[17]

Master’s thesis, York University, Toronto, Canada (2017)

Rady, A.S.: Characterizing Implementations that Preserve Properties of Concurrent Ran- domized Algorithms. Master’s thesis, York University, Toronto, Canada (2017)

2017
[18]

Dodds, M., Haas, A., Kirsch, C.M.: A scalable, correct time-stamped stack. In Rajamani, S.K., Walker, D., eds.: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Sympo- sium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, ACM (2015) 233–246

2015
[19]

Khyzha, A., Dodds, M., Gotsman, A., Parkinson, M.J.: Proving linearizability using partial orders. In Yang, H., ed.: Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings. V olume 1...

2017
[20]

CoRRabs/2408.11015(2024)

Shimon, Y .B., Lahav, O., Shoham, S.: Hyperproperty-preserving register specifications (ex- tended version). CoRRabs/2408.11015(2024)

Pith/arXiv arXiv 2024
[21]

In Alistarh, D., ed.: 38th International Symposium on Distributed Computing, DISC 2024, Madrid, Spain, October 28 - November 1, 2024

Shimon, Y .B., Lahav, O., Shoham, S.: Hyperproperty-preserving register specifications. In Alistarh, D., ed.: 38th International Symposium on Distributed Computing, DISC 2024, Madrid, Spain, October 28 - November 1, 2024. V olume 319 of LIPIcs., Schloss Dagstuhl - Leibniz-Zentrum f¨ur Informatik (2024) 8:1–8:19

2024
[22]

ACM Trans

Schellhorn, G., Derrick, J., Wehrheim, H.: A sound and complete proof technique for lin- earizability of concurrent data structures. ACM Trans. Comput. Log.15(2014) 31:1–31:37

2014
[23]

In Kowalski, D., Panconesi, A., eds.: ACM Symposium on Principles of Distributed Computing, PODC ’12, Funchal, Madeira, Portugal, July 16-18, 2012, ACM (2012) 385–394

Helmi, M., Higham, L., Woelfel, P.: Strongly linearizable implementations: possibilities and impossibilities. In Kowalski, D., Panconesi, A., eds.: ACM Symposium on Principles of Distributed Computing, PODC ’12, Funchal, Madeira, Portugal, July 16-18, 2012, ACM (2012) 385–394

2012
[24]

In Bourke, T., Chen, L., Goharshady, A.K., eds.: Dependable Software Engineering

Wang, C., Wu, P., Petri, G., Jia, Q., He, Y ., Lv, Y ., Liu, Z.: Universal construction for lineariz- able but not strongly linearizable concurrent objects. In Bourke, T., Chen, L., Goharshady, A.K., eds.: Dependable Software Engineering. Theories, Tools, and Applications - 10th In- ternational Symposium, SETTA 2024, Hong Kong, China, November 26-28, 2024...

2024
[25]

In Fortnow, L., Vadhan, S.P., eds.: Proceedings of the 43rd ACM Symposium on Theory of Computing, STOC 2011, San Jose, CA, USA, 6-8 June 2011, ACM (2011) 373–382

Golab, W.M., Higham, L., Woelfel, P.: Linearizable implementations do not suffice for ran- domized distributed computation. In Fortnow, L., Vadhan, S.P., eds.: Proceedings of the 43rd ACM Symposium on Theory of Computing, STOC 2011, San Jose, CA, USA, 6-8 June 2011, ACM (2011) 373–382

2011
[26]

Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur.18(2010) 1157–1210

2010
[27]

In Klin, B., Lasota, S., Muscholl, A., eds.: 33rd International Conference on Concurrency Theory, CONCUR 2022, September 12-16, 2022, Warsaw, Poland

Dongol, B., Schellhorn, G., Wehrheim, H.: Weak progressive forward simulation is necessary and sufficient for strong observational refinement. In Klin, B., Lasota, S., Muscholl, A., eds.: 33rd International Conference on Concurrency Theory, CONCUR 2022, September 12-16, 2022, Warsaw, Poland. V olume 243 of LIPIcs., Schloss Dagstuhl - Leibniz-Zentrum f¨ur ...

2022

[1] [1]

ACM Trans

Herlihy, M., Wing, J.M.: Linearizability: A correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst.12(1990) 463–492

1990

[2] [2]

Morgan Kaufmann (2008)

Herlihy, M., Shavit, N.: The art of multiprocessor programming. Morgan Kaufmann (2008)

2008

[3] [3]

Vafeiadis, V ., Herlihy, M., Hoare, T., Shapiro, M.: Proving correctness of highly-concurrent linearisable objects. In Torrellas, J., Chatterjee, S., eds.: Proceedings of the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPOPP 2006, New York, New York, USA, March 29-31, 2006, ACM (2006) 129–136

2006

[4] [4]

Vale, A.O., Shao, Z., Chen, Y .: A compositional theory of linearizability. J. ACM71(2024) 14:1–14:107

2024

[5] [5]

Filipovic, I., O’Hearn, P.W., Rinetzky, N., Yang, H.: Abstraction for concurrent objects. In Castagna, G., ed.: Programming Languages and Systems, 18th European Symposium on Programming, ESOP 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings. V olume 5502 of Lectur...

2009

[6] [6]

In Majumdar, R., Kuncak, V ., eds.: Computer Aided Verification - 29th Inter- national Conference, CA V 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II

Bouajjani, A., Emmi, M., Enea, C., Mutluergil, S.O.: Proving linearizability using forward simulations. In Majumdar, R., Kuncak, V ., eds.: Computer Aided Verification - 29th Inter- national Conference, CA V 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II. V olume 10427 of Lecture Notes in Computer Science., Springer (2017) 542–563

2017

[7] [7]

In Damm, W., Hermanns, H., eds.: Computer Aided Verification, 19th International Conference, CA V 2007, Berlin, Germany, July 3-7, 2007, Proceedings

Amit, D., Rinetzky, N., Reps, T.W., Sagiv, M., Yahav, E.: Comparison under abstraction for verifying linearizability. In Damm, W., Hermanns, H., eds.: Computer Aided Verification, 19th International Conference, CA V 2007, Berlin, Germany, July 3-7, 2007, Proceedings. V olume 4590 of Lecture Notes in Computer Science., Springer (2007) 477–490

2007

[8] [8]

Vafeiadis, V .: Shape-value abstraction for verifying linearizability. In Jones, N.D., M ¨uller- Olm, M., eds.: Verification, Model Checking, and Abstract Interpretation, 10th International Conference, VMCAI 2009, Savannah, GA, USA, January 18-20, 2009. Proceedings. V olume 5403 of Lecture Notes in Computer Science., Springer (2009) 335–348

2009

[9] [9]

Abdulla, P.A., Haziza, F., Hol ´ık, L., Jonsson, B., Rezine, A.: An integrated specification and verification technique for highly concurrent data structures. Int. J. Softw. Tools Technol. Transf.19(2017) 549–563

2017

[10] [10]

Jayanti, P., Jayanti, S., Yavuz, U.Y ., Hernandez, L.: A universal, sound, and complete forward reasoning technique for machine-verified proofs of linearizability. Proc. ACM Program. Lang.8(2024) 2456–2484

2024

[11] [11]

PhD thesis, University of Cambridge, UK (2008)

Vafeiadis, V .: Modular fine-grained concurrency verification. PhD thesis, University of Cambridge, UK (2008)

2008

[12] [12]

ACM Trans

Liang, H., Feng, X., Fu, M.: Rely-guarantee-based simulation for compositional verification of concurrent program transformations. ACM Trans. Program. Lang. Syst.36(2014) 3:1– 3:55

2014

[13] [13]

In Boehm, H., Flanagan, C., eds.: ACM SIGPLAN Conference on Programming Lan- guage Design and Implementation, PLDI ’13, Seattle, W A, USA, June 16-19, 2013, ACM (2013) 459–470

Liang, H., Feng, X.: Modular verification of linearizability with non-fixed linearization points. In Boehm, H., Flanagan, C., eds.: ACM SIGPLAN Conference on Programming Lan- guage Design and Implementation, PLDI ’13, Seattle, W A, USA, June 16-19, 2013, ACM (2013) 459–470

2013

[14] [14]

ACM Trans

Herlihy, M.: Wait-free synchronization. ACM Trans. Program. Lang. Syst.13(1991) 124– 149

1991

[15] [15]

In D’Argenio, P.R., Melgratti, H.C., eds.: CONCUR 2013 - Concurrency Theory - 24th International Conference, CONCUR 2013, Buenos Aires, Argentina, August 27-30, 2013

Liang, H., Hoffmann, J., Feng, X., Shao, Z.: Characterizing progress properties of concurrent objects via contextual refinements. In D’Argenio, P.R., Melgratti, H.C., eds.: CONCUR 2013 - Concurrency Theory - 24th International Conference, CONCUR 2013, Buenos Aires, Argentina, August 27-30, 2013. Proceedings. V olume 8052 of Lecture Notes in Computer Scien...

2013

[16] [16]

In Suomela, J., ed.: 33rd International Symposium on Distributed Computing, DISC 2019, October 14-18, 2019, Budapest, Hungary

Attiya, H., Enea, C.: Putting strong linearizability in context: Preserving hyperproperties in programs that use concurrent objects. In Suomela, J., ed.: 33rd International Symposium on Distributed Computing, DISC 2019, October 14-18, 2019, Budapest, Hungary. V olume 146 of LIPIcs., Schloss Dagstuhl - Leibniz-Zentrum f¨ur Informatik (2019) 2:1–2:17

2019

[17] [17]

Master’s thesis, York University, Toronto, Canada (2017)

Rady, A.S.: Characterizing Implementations that Preserve Properties of Concurrent Ran- domized Algorithms. Master’s thesis, York University, Toronto, Canada (2017)

2017

[18] [18]

Dodds, M., Haas, A., Kirsch, C.M.: A scalable, correct time-stamped stack. In Rajamani, S.K., Walker, D., eds.: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Sympo- sium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, ACM (2015) 233–246

2015

[19] [19]

Khyzha, A., Dodds, M., Gotsman, A., Parkinson, M.J.: Proving linearizability using partial orders. In Yang, H., ed.: Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings. V olume 1...

2017

[20] [20]

CoRRabs/2408.11015(2024)

Shimon, Y .B., Lahav, O., Shoham, S.: Hyperproperty-preserving register specifications (ex- tended version). CoRRabs/2408.11015(2024)

Pith/arXiv arXiv 2024

[21] [21]

In Alistarh, D., ed.: 38th International Symposium on Distributed Computing, DISC 2024, Madrid, Spain, October 28 - November 1, 2024

Shimon, Y .B., Lahav, O., Shoham, S.: Hyperproperty-preserving register specifications. In Alistarh, D., ed.: 38th International Symposium on Distributed Computing, DISC 2024, Madrid, Spain, October 28 - November 1, 2024. V olume 319 of LIPIcs., Schloss Dagstuhl - Leibniz-Zentrum f¨ur Informatik (2024) 8:1–8:19

2024

[22] [22]

ACM Trans

Schellhorn, G., Derrick, J., Wehrheim, H.: A sound and complete proof technique for lin- earizability of concurrent data structures. ACM Trans. Comput. Log.15(2014) 31:1–31:37

2014

[23] [23]

In Kowalski, D., Panconesi, A., eds.: ACM Symposium on Principles of Distributed Computing, PODC ’12, Funchal, Madeira, Portugal, July 16-18, 2012, ACM (2012) 385–394

Helmi, M., Higham, L., Woelfel, P.: Strongly linearizable implementations: possibilities and impossibilities. In Kowalski, D., Panconesi, A., eds.: ACM Symposium on Principles of Distributed Computing, PODC ’12, Funchal, Madeira, Portugal, July 16-18, 2012, ACM (2012) 385–394

2012

[24] [24]

In Bourke, T., Chen, L., Goharshady, A.K., eds.: Dependable Software Engineering

Wang, C., Wu, P., Petri, G., Jia, Q., He, Y ., Lv, Y ., Liu, Z.: Universal construction for lineariz- able but not strongly linearizable concurrent objects. In Bourke, T., Chen, L., Goharshady, A.K., eds.: Dependable Software Engineering. Theories, Tools, and Applications - 10th In- ternational Symposium, SETTA 2024, Hong Kong, China, November 26-28, 2024...

2024

[25] [25]

In Fortnow, L., Vadhan, S.P., eds.: Proceedings of the 43rd ACM Symposium on Theory of Computing, STOC 2011, San Jose, CA, USA, 6-8 June 2011, ACM (2011) 373–382

Golab, W.M., Higham, L., Woelfel, P.: Linearizable implementations do not suffice for ran- domized distributed computation. In Fortnow, L., Vadhan, S.P., eds.: Proceedings of the 43rd ACM Symposium on Theory of Computing, STOC 2011, San Jose, CA, USA, 6-8 June 2011, ACM (2011) 373–382

2011

[26] [26]

Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur.18(2010) 1157–1210

2010

[27] [27]

In Klin, B., Lasota, S., Muscholl, A., eds.: 33rd International Conference on Concurrency Theory, CONCUR 2022, September 12-16, 2022, Warsaw, Poland

Dongol, B., Schellhorn, G., Wehrheim, H.: Weak progressive forward simulation is necessary and sufficient for strong observational refinement. In Klin, B., Lasota, S., Muscholl, A., eds.: 33rd International Conference on Concurrency Theory, CONCUR 2022, September 12-16, 2022, Warsaw, Poland. V olume 243 of LIPIcs., Schloss Dagstuhl - Leibniz-Zentrum f¨ur ...

2022