Demonstration venue · read-only. Every page can be browsed; the buttons that would change it are switched off. Create an account to run TaxoReview on your own data.

Romit Roy Chowdhury

dblp:390/3684 · DBLP profile ↗
← Back
1ranked-venue papers
0as first author
1since 2021 · last 2024
0009-0004-4097-8115ORCID · 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.

Software engineering, system software, and programming languages
1 paper
Concurrent programming · 75% Program verification · 25%

Topics — the 4 heaviest of 4, each with the papers that count most for it

TopicWeightPapersLastEvidence papers
Concurrent programming › atomicity
linearizability
0.812024
Automated Robustness Verification of Concurrent Data Structure Libraries against Relaxed Memory Models · Proc. ACM Program. Lang. 2024
Concurrent programming
memory models
0.812024
Automated Robustness Verification of Concurrent Data Structure Libraries against Relaxed Memory Models · Proc. ACM Program. Lang. 2024
Program verification › neural network verification
robustness verification
0.812024
Automated Robustness Verification of Concurrent Data Structure Libraries against Relaxed Memory Models · Proc. ACM Program. Lang. 2024
Concurrent programming › memory models
weak memory models
0.812024
Automated Robustness Verification of Concurrent Data Structure Libraries against Relaxed Memory Models · Proc. ACM Program. Lang. 2024

Methods — techniques the papers use, named apart from their topics

non-robustness witness search · 0.8inductive verification · 0.8
YearPublicationVenuePosition
2024 Automated Robustness Verification of Concurrent Data Structure Libraries against Relaxed Memory Models
abstract
Clients reason about the behavior of concurrent data structure libraries such as sets, queues, or stacks using specifications that capture well-understood correctness conditions, such as linearizability. The implementation of these libraries, however, focused as they are on performance, may additionally exploit relaxed memory behavior allowed by the language or underlying hardware that weaken the strong ordering and visibility constraints on shared-memory accesses that would otherwise be imposed by a sequentially consistent (SC) memory model. As an alternative to developing new specification and verification mechanisms for reasoning about libraries under relaxed memory model, we instead consider the orthogonal problem of library robustness , a property that holds when all possible behaviors of a library implementation under relaxed memory model are also possible under SC. In this paper, we develop a new automated technique for verifying robustness of library implementations in the context of a C11-style memory model. This task is challenging because a most-general client may invoke an unbounded number of concurrently executing library operations that can manipulate an unbounded number of shared locations. We establish a novel inductive technique for verifying library robustness that leverages prior work on the robustness problem for the C11 memory model based on the search for a non-robustness witness under SC executions. We crucially rely on the fact that this search is carried out over SC executions, and use high-level SC specifications (including linearizability) of the library to verify the absence of a non-robustness witness. Our technique is compositional - we show how we can safely preserve robustness of multiple interacting library implementations and clients using additional SC fences to guarantee robustness of entire executions. Experimental results on a number of complex realistic library implementations demonstrate the feasibility of our approach.
Kartik Nagar, Anmol Sahoo, Romit Roy Chowdhury, Suresh Jagannathan
Proc. ACM Program. Lang.3