Demo Data from VLDB 2026 / reviewers in the wild / expert
Peixin You
dblp:390/3228
· DBLP profile ↗
1ranked-venue papers
0as first author
1since 2021 · last 2024
0009-0002-8035-5209ORCID · reported
Domains — the database's venue-derived domains; a paper can count in several
Software engineering, systems software and programming languages · 1 · 1 since 2021
Expertise — from the expertise taxonomy: the topics of the expert's papers under the CCF categories. A weight counts papers with recency: 1 for a paper about the topic, 0.3 when the topic is its context, halved every five years.
| Computer architecture, parallel and distributed computing, and storage systems
1 paper |
Distributed systems · 67% Storage systems · 33% | |
| Software engineering, system software, and programming languages
1 paper |
Concurrent programming · 50% Program verification · 50% |
Topics — the 5 heaviest of 5, each with the papers that count most for it
| Topic | Weight | Papers | Last | Evidence papers |
|---|---|---|---|---|
Concurrent programming › atomicity
linearizability |
0.8 | 1 | 2024 | Compositionality and Observational Refinement for Linearizability with Crashes · Proc. ACM Program. Lang. 2024 |
Program verification
program logic |
0.8 | 1 | 2024 | Compositionality and Observational Refinement for Linearizability with Crashes · Proc. ACM Program. Lang. 2024 |
Storage systems
crash safety |
0.8 | 1 | 2024 | Compositionality and Observational Refinement for Linearizability with Crashes · Proc. ACM Program. Lang. 2024 |
Distributed systems › consistency models
durable linearizability |
0.8 | 1 | 2024 | Compositionality and Observational Refinement for Linearizability with Crashes · Proc. ACM Program. Lang. 2024 |
Distributed systems
fault tolerance |
0.8 | 1 | 2024 | Compositionality and Observational Refinement for Linearizability with Crashes · Proc. ACM Program. Lang. 2024 |
Methods — techniques the papers use, named apart from their topics
program logic · 1.5observational refinement · 1.5compositional semantics · 1.5
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2024 | Compositionality and Observational Refinement for Linearizability with CrashesabstractCrash-safety is an important property of real systems, as the main functionality of some systems is resilience to crashes. Toward a compositional verification approach for crash-safety under full-system crashes, one observes that crashes propagate instantaneously to all components across all levels of abstraction, even to unspecified components, hindering compositionality. Furthermore, in the presence of concurrency, a correctness criterion that addresses both crashes and concurrency proves necessary. For this, several adaptations of linearizability have been suggested, each featuring different trade-offs between complexity and expressiveness. The recently proposed compositional linearizability framework shows that to achieve compositionality with linearizability, both a locality and observational refinement property are necessary. Despite that, no linearizability criterion with crashes has been proven to support an observational refinement property. In this paper, we define a compositional model of concurrent computation with full-system crashes. We use this model to develop a compositional theory of linearizability with crashes, which reveals a criterion, crash-aware linearizability , as its inherent notion of linearizability and supports both locality and observational refinement. We then show that strict linearizability and durable linearizability factor through crash-aware linearizability as two different ways of translating between concurrent computation with and without crashes, enabling simple proofs of locality and observational refinement for a generalization of these two criteria. Then, we show how the theory can be connected with a program logic for durable and crash-aware linearizability, which gives the first program logic that verifies a form of linearizability with crashes. We showcase the advantages of compositionality by verifying a library facilitating programming persistent data structures and a fragment of a transactional interface for a file system. Arthur Oliveira Vale, Zhongye Wang, Yixuan Chen 0002, Peixin You, Zhong Shao 0001 |
Proc. ACM Program. Lang. | 4 |